Theorem excom 2162

Description: Theorem 19.11 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.) Remove dependencies on ax-5 1913, ax-6 1971, ax-7 2011, ax-10 2137, ax-12 2171. (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 2156	. . 3 ⊢ (∀𝑥∀𝑦 ¬ 𝜑 ↔ ∀𝑦∀𝑥 ¬ 𝜑)
2	1	notbii 319	. 2 ⊢ (¬ ∀𝑥∀𝑦 ¬ 𝜑 ↔ ¬ ∀𝑦∀𝑥 ¬ 𝜑)
3		2exnaln 1831	. 2 ⊢ (∃𝑥∃𝑦𝜑 ↔ ¬ ∀𝑥∀𝑦 ¬ 𝜑)
4		2exnaln 1831	. 2 ⊢ (∃𝑦∃𝑥𝜑 ↔ ¬ ∀𝑦∀𝑥 ¬ 𝜑)
5	2, 3, 4	3bitr4i 302	1 ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑦∃𝑥𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 205  ∀wal 1539  ∃wex 1781

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-11 2154

This theorem depends on definitions:  df-bi 206  df-ex 1782

This theorem is referenced by:  excomim  2163  excom13  2164  exrot3  2165  eeor  2329  ee4anv  2347  2sb8ef  2352  sbel2x  2473  2sb8e  2529  2euexv  2627  2euex  2637  2eu4  2650  rexcom4  3285  rexcomf  3300  cgsex4gOLDOLD  3522  gencbvex  3535  euind  3719  sbccomlem  3863  elvvv  5749  dmuni  5912  dm0rn0  5922  dmcosseq  5970  rnco  6248  coass  6261  oprabidw  7436  oprabid  7437  dfoprab2  7463  uniuni  7745  opabex3d  7948  opabex3rd  7949  opabex3  7950  frxp  8108  domen  8953  xpassen  9062  scott0  9877  dfac5lem1  10114  dfac5lem4  10117  cflem  10237  ltexprlem1  11027  ltexprlem4  11030  fsumcom2  15716  fprodcom2  15924  gsumval3eu  19766  dprd2d2  19908  cnvoprabOLD  31932  eldm3  34719  dfdm5  34732  dfrn5  34733  elfuns  34875  dfiota3  34883  brimg  34897  funpartlem  34902  bj-19.12  35627  bj-nnflemee  35629  bj-restuni  35966  sbccom2lem  36980  diblsmopel  40030  dicelval3  40039  dihjatcclem4  40280  19.9dev  41024  nnoeomeqom  42047  pm11.6  43136  ax6e2ndeq  43305  e2ebind  43309  ax6e2ndeqVD  43655  e2ebindVD  43658  e2ebindALT  43675  ax6e2ndeqALT  43677  ich2ex  46122  ichexmpl1  46123  elsprel  46129  eliunxp2  46962