Theorem negfo_intro_fo ≪ | index | src | ≫

\fo对\neg\fo引入

theorem negfo_intro_fo {x: set} (A: wff x):
  $ \neg \fo x A \imp \fo x \neg \fo x A $;

Step	Hyp	Ref	Expression
1		ax_10	\neg \fo x A \imp \fo x \neg \fo x A

Axiom use

Logic (ax_10)