Theorem fo_eqv_negexneg ≪ | index | src | ≫

\fo等价\neg\ex\neg

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

Axiom use

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