Theorem ex_perm ≪ | index | src | ≫

\ex置换

theorem ex_perm {x y: set} (A: wff x y): $ \ex x \ex y A \iff \ex y \ex x A $;
StepHypRefExpression
1 iff_intro_neg 
(\fo x \neg \neg \fo y \neg A \iff \fo y \neg \neg \fo x \neg A) \imp (\neg \fo x \neg \neg \fo y \neg A \iff \neg \fo y \neg \neg \fo x \neg A)
2 iff_tran 
(\fo x \neg \neg \fo y \neg A \iff \fo y \fo x \neg A) \imp
  (\fo y \fo x \neg A \iff \fo y \neg \neg \fo x \neg A) \imp
  (\fo x \neg \neg \fo y \neg A \iff \fo y \neg \neg \fo x \neg A)
3 iff_tran 
(\fo x \neg \neg \fo y \neg A \iff \fo x \fo y \neg A) \imp
  (\fo x \fo y \neg A \iff \fo y \fo x \neg A) \imp
  (\fo x \neg \neg \fo y \neg A \iff \fo y \fo x \neg A)
4 iff_symm 
(\fo y \neg A \iff \neg \neg \fo y \neg A) \imp (\neg \neg \fo y \neg A \iff \fo y \neg A)
5 negneg_alloc 
\fo y \neg A \iff \neg \neg \fo y \neg A
6 4, 5 ax_mp 
\neg \neg \fo y \neg A \iff \fo y \neg A
7 6 iff_intro_fo 
\fo x \neg \neg \fo y \neg A \iff \fo x \fo y \neg A
8 3, 7 ax_mp 
(\fo x \fo y \neg A \iff \fo y \fo x \neg A) \imp (\fo x \neg \neg \fo y \neg A \iff \fo y \fo x \neg A)
9 fo_perm 
\fo x \fo y \neg A \iff \fo y \fo x \neg A
10 8, 9 ax_mp 
\fo x \neg \neg \fo y \neg A \iff \fo y \fo x \neg A
11 2, 10 ax_mp 
(\fo y \fo x \neg A \iff \fo y \neg \neg \fo x \neg A) \imp (\fo x \neg \neg \fo y \neg A \iff \fo y \neg \neg \fo x \neg A)
12 negneg_alloc 
\fo x \neg A \iff \neg \neg \fo x \neg A
13 12 iff_intro_fo 
\fo y \fo x \neg A \iff \fo y \neg \neg \fo x \neg A
14 11, 13 ax_mp 
\fo x \neg \neg \fo y \neg A \iff \fo y \neg \neg \fo x \neg A
15 1, 14 ax_mp 
\neg \fo x \neg \neg \fo y \neg A \iff \neg \fo y \neg \neg \fo x \neg A
16 15 conv ex 
\ex x \ex y A \iff \ex y \ex x A

Axiom use

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