Theorem excom 2151

Description: Theorem 19.11 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.) Remove dependencies on ax-5 1905, ax-6 1963, ax-7 2003, ax-10 2129, ax-12 2166. (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 2148	. . 3 ⊢ (∀𝑥∀𝑦 ¬ 𝜑 ↔ ∀𝑦∀𝑥 ¬ 𝜑)
2	1	notbii 319	. 2 ⊢ (¬ ∀𝑥∀𝑦 ¬ 𝜑 ↔ ¬ ∀𝑦∀𝑥 ¬ 𝜑)
3		2exnaln 1823	. 2 ⊢ (∃𝑥∃𝑦𝜑 ↔ ¬ ∀𝑥∀𝑦 ¬ 𝜑)
4		2exnaln 1823	. 2 ⊢ (∃𝑦∃𝑥𝜑 ↔ ¬ ∀𝑦∀𝑥 ¬ 𝜑)
5	2, 3, 4	3bitr4i 302	1 ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑦∃𝑥𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 205  ∀wal 1531  ∃wex 1773

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-11 2146

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

This theorem is referenced by:  excomim  2152  excom13  2153  exrot3  2154  eeor  2323  ee4anv  2341  2sb8ef  2346  sbel2x  2467  2sb8e  2523  2euexv  2619  2euex  2629  2eu4  2643  rexcom4  3275  rexcomf  3290  cgsex4gOLDOLD  3511  gencbvex  3525  euind  3716  sbccomlem  3860  elvvv  5753  dmuni  5917  dm0rn0  5927  dmcosseq  5976  cnvopab  6144  rnco  6258  coass  6271  oprabidw  7450  oprabid  7451  dfoprab2  7478  uniuni  7765  opabex3d  7970  opabex3rd  7971  opabex3  7972  frxp  8131  domen  8982  xpassen  9091  scott0  9911  dfac5lem1  10148  dfac5lem4  10151  cflem  10271  ltexprlem1  11061  ltexprlem4  11064  fsumcom2  15756  fprodcom2  15964  gsumval3eu  19871  dprd2d2  20013  cnvoprabOLD  32584  eldm3  35483  dfdm5  35496  dfrn5  35497  elfuns  35639  dfiota3  35647  brimg  35661  funpartlem  35666  bj-19.12  36366  bj-nnflemee  36368  bj-restuni  36704  sbccom2lem  37725  diblsmopel  40771  dicelval3  40780  dihjatcclem4  41021  19.9dev  41832  nnoeomeqom  42880  pm11.6  43968  ax6e2ndeq  44137  e2ebind  44141  ax6e2ndeqVD  44487  e2ebindVD  44490  e2ebindALT  44507  ax6e2ndeqALT  44509  ich2ex  46942  ichexmpl1  46943  elsprel  46949  eliunxp2  47580