Theorem excom 2163

Description: Theorem 19.11 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.) Remove dependencies on ax-5 1909, ax-6 1967, ax-7 2007, ax-10 2141, ax-12 2178. (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 2160	. . 3 ⊢ (∀𝑥∀𝑦 ¬ 𝜑 ↔ ∀𝑦∀𝑥 ¬ 𝜑)
2	1	notbii 320	. 2 ⊢ (¬ ∀𝑥∀𝑦 ¬ 𝜑 ↔ ¬ ∀𝑦∀𝑥 ¬ 𝜑)
3		2exnaln 1827	. 2 ⊢ (∃𝑥∃𝑦𝜑 ↔ ¬ ∀𝑥∀𝑦 ¬ 𝜑)
4		2exnaln 1827	. 2 ⊢ (∃𝑦∃𝑥𝜑 ↔ ¬ ∀𝑦∀𝑥 ¬ 𝜑)
5	2, 3, 4	3bitr4i 303	1 ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑦∃𝑥𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 206  ∀wal 1535  ∃wex 1777

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-11 2158

This theorem depends on definitions:  df-bi 207  df-ex 1778

This theorem is referenced by:  excomim  2164  excom13  2165  exrot3  2166  eeor  2339  ee4anv  2357  2sb8ef  2362  sbel2x  2482  2sb8e  2538  2euexv  2634  2euex  2644  2eu4  2658  rexcom4  3294  rexcomf  3309  gencbvex  3553  euind  3746  sbccomlemOLD  3892  elvvv  5775  dmuni  5939  dm0rn0  5949  dmcosseqOLD  6000  cnvopab  6169  rnco  6283  coass  6296  oprabidw  7479  oprabid  7480  dfoprab2  7508  uniuni  7797  opabex3d  8006  opabex3rd  8007  opabex3  8008  frxp  8167  domen  9021  xpassen  9132  scott0  9955  dfac5lem1  10192  dfac5lem4OLD  10197  cflemOLD  10315  ltexprlem1  11105  ltexprlem4  11108  fsumcom2  15822  fprodcom2  16032  gsumval3eu  19946  dprd2d2  20088  cnvoprabOLD  32734  eldm3  35723  dfdm5  35736  dfrn5  35737  elfuns  35879  dfiota3  35887  brimg  35901  funpartlem  35906  bj-19.12  36727  bj-nnflemee  36729  bj-restuni  37063  sbccom2lem  38084  diblsmopel  41128  dicelval3  41137  dihjatcclem4  41378  19.9dev  42207  nnoeomeqom  43274  pm11.6  44361  ax6e2ndeq  44530  e2ebind  44534  ax6e2ndeqVD  44880  e2ebindVD  44883  e2ebindALT  44900  ax6e2ndeqALT  44902  ich2ex  47342  ichexmpl1  47343  elsprel  47349  eliunxp2  48058