Theorem ex_eqv_negfoneg ≪ | index | src | ≫

\ex等价\neg\fo\neg

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

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

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)