Theorem exneg_eqv_negfo ≪ | index | src | ≫

\ex\neg等价\neg\fo

theorem exneg_eqv_negfo {x: set} (A: wff x): $ \ex x \neg A \iff \neg \fo x A $;
StepHypRefExpression
1 iff_intro_neg 
(\fo x \neg \neg A \iff \fo x A) \imp (\neg \fo x \neg \neg A \iff \neg \fo x A)
2 iff_symm 
(A \iff \neg \neg A) \imp (\neg \neg A \iff A)
3 negneg_alloc 
A \iff \neg \neg A
4 2, 3 ax_mp 
\neg \neg A \iff A
5 4 iff_intro_fo 
\fo x \neg \neg A \iff \fo x A
6 1, 5 ax_mp 
\neg \fo x \neg \neg A \iff \neg \fo x A
7 6 conv ex 
\ex x \neg A \iff \neg \fo x A

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3, ax_gen, ax_4)