Theorem excom 2195

Description: Theorem 19.11 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.) Remove dependencies on ax-5 1929, ax-6 1986, ax-7 2027, ax-10 2174, ax-12 2211. (Revised by Wolf Lammen, 8-Jan-2018.) (Proof shortened by Wolf Lammen, 22-Aug-2020.)

Assertion

Ref	Expression
excom	⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑦∃𝑥𝜑)

Proof of Theorem excom

Step	Hyp	Ref	Expression
1		alcom 2192	. . 3 ⊢ (∀𝑥∀𝑦 ¬ 𝜑 ↔ ∀𝑦∀𝑥 ¬ 𝜑)
2	1	notbii 322	. 2 ⊢ (¬ ∀𝑥∀𝑦 ¬ 𝜑 ↔ ¬ ∀𝑦∀𝑥 ¬ 𝜑)
3		2exnaln 1848	. 2 ⊢ (∃𝑥∃𝑦𝜑 ↔ ¬ ∀𝑥∀𝑦 ¬ 𝜑)
4		2exnaln 1848	. 2 ⊢ (∃𝑦∃𝑥𝜑 ↔ ¬ ∀𝑦∀𝑥 ¬ 𝜑)
5	2, 3, 4	3bitr4i 305	1 ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑦∃𝑥𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 208  ∀wal 1557  ∃wex 1798

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-11 2190

This theorem depends on definitions:  df-bi 209  df-ex 1799

This theorem is referenced by:  excomim  2196  excom13  2197  exrot3  2198  eeor  2364  ee4anv  2381  ee4anvOLD  2382  2sb8ef  2386  sbel2x  2504  2sb8e  2560  2euexv  2657  2euex  2667  2eu4  2680  rexcom4  3288  rexcomf  3300  gencbvex  3509  euind  3685  sbccomlemOLD  3821  elvvv  5719  dmuni  5886  dm0rn0OLD  5897  dmcosseqOLDOLD  5952  cnvopab  6120  rncoOLD  6235  coass  6248  oprabidw  7422  oprabid  7423  dfoprab2  7449  uniuni  7740  opabex3d  7941  opabex3rd  7942  opabex3  7943  frxp  8100  domen  8936  xpassen  9037  scott0  9838  dfac5lem1  10073  dfac5lem4OLD  10078  cflemOLD  10196  ltexprlem1  10988  ltexprlem4  10991  fsumcom2  15792  fprodcom2  16005  gsumval3eu  19935  dprd2d2  20077  eldm3  36072  dfdm5  36084  dfrn5  36085  elfuns  36224  dfiota3  36232  brimg  36246  funpartlem  36253  bj-19.12  37159  bj-nnflemee  37223  bj-restuni  37548  sbccom2lem  38584  dmqsblocks  39427  diblsmopel  41756  dicelval3  41765  dihjatcclem4  42006  nfe2  42793  19.9dev  42795  nnoeomeqom  43850  pm11.6  44929  ax6e2ndeq  45096  e2ebind  45100  ax6e2ndeqVD  45445  e2ebindVD  45448  e2ebindALT  45465  ax6e2ndeqALT  45467  ich2ex  48035  ichexmpl1  48036  elsprel  48042  eliunxp2  48917