Theorem excom 2163

Description: Theorem 19.11 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.) Remove dependencies on ax-5 1914, ax-6 1972, ax-7 2012, ax-10 2138, ax-12 2172. (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 2157	. . 3 ⊢ (∀𝑥∀𝑦 ¬ 𝜑 ↔ ∀𝑦∀𝑥 ¬ 𝜑)
2	1	notbii 320	. 2 ⊢ (¬ ∀𝑥∀𝑦 ¬ 𝜑 ↔ ¬ ∀𝑦∀𝑥 ¬ 𝜑)
3		2exnaln 1832	. 2 ⊢ (∃𝑥∃𝑦𝜑 ↔ ¬ ∀𝑥∀𝑦 ¬ 𝜑)
4		2exnaln 1832	. 2 ⊢ (∃𝑦∃𝑥𝜑 ↔ ¬ ∀𝑦∀𝑥 ¬ 𝜑)
5	2, 3, 4	3bitr4i 303	1 ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑦∃𝑥𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 205  ∀wal 1540  ∃wex 1782

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-11 2155

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

This theorem is referenced by:  excomim  2164  excom13  2165  exrot3  2166  eeor  2330  ee4anv  2348  2sb8ef  2353  sbel2x  2474  2sb8e  2530  2euexv  2628  2euex  2638  2eu4  2651  rexcom4  3286  rexcomf  3301  cgsex4gOLDOLD  3523  gencbvex  3536  euind  3721  sbccomlem  3865  elvvv  5752  dmuni  5915  dm0rn0  5925  dmcosseq  5973  rnco  6252  coass  6265  oprabidw  7440  oprabid  7441  dfoprab2  7467  uniuni  7749  opabex3d  7952  opabex3rd  7953  opabex3  7954  frxp  8112  domen  8957  xpassen  9066  scott0  9881  dfac5lem1  10118  dfac5lem4  10121  cflem  10241  ltexprlem1  11031  ltexprlem4  11034  fsumcom2  15720  fprodcom2  15928  gsumval3eu  19772  dprd2d2  19914  cnvoprabOLD  31945  eldm3  34731  dfdm5  34744  dfrn5  34745  elfuns  34887  dfiota3  34895  brimg  34909  funpartlem  34914  bj-19.12  35639  bj-nnflemee  35641  bj-restuni  35978  sbccom2lem  36992  diblsmopel  40042  dicelval3  40051  dihjatcclem4  40292  19.9dev  41029  nnoeomeqom  42062  pm11.6  43151  ax6e2ndeq  43320  e2ebind  43324  ax6e2ndeqVD  43670  e2ebindVD  43673  e2ebindALT  43690  ax6e2ndeqALT  43692  ich2ex  46136  ichexmpl1  46137  elsprel  46143  eliunxp2  47009