Theorem foneg_eqv_negex ≪ | index | src | ≫

\fo\neg等价\neg\ex

theorem foneg_eqv_negex {x: set} (A: wff x): $ \fo x \neg A \iff \neg \ex x A $;

Step	Hyp	Ref	Expression
1		negneg_alloc	\fo x \neg A \iff \neg \neg \fo x \neg A
2	1	conv ex	\fo x \neg A \iff \neg \ex x A

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)