Theorem excom 2082

Description: Theorem 19.11 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.) Remove dependencies on ax-5 1879, ax-6 1945, ax-7 1981, ax-10 2059, ax-12 2087. (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 2077	. . 3 ⊢ (∀𝑥∀𝑦 ¬ 𝜑 ↔ ∀𝑦∀𝑥 ¬ 𝜑)
2	1	notbii 309	. 2 ⊢ (¬ ∀𝑥∀𝑦 ¬ 𝜑 ↔ ¬ ∀𝑦∀𝑥 ¬ 𝜑)
3		2exnaln 1796	. 2 ⊢ (∃𝑥∃𝑦𝜑 ↔ ¬ ∀𝑥∀𝑦 ¬ 𝜑)
4		2exnaln 1796	. 2 ⊢ (∃𝑦∃𝑥𝜑 ↔ ¬ ∀𝑦∀𝑥 ¬ 𝜑)
5	2, 3, 4	3bitr4i 292	1 ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑦∃𝑥𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 196  ∀wal 1521  ∃wex 1744

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-11 2074

This theorem depends on definitions:  df-bi 197  df-ex 1745

This theorem is referenced by:  excomim  2083  excom13  2084  exrot3  2085  ee4anv  2220  sbel2x  2487  2sb8e  2495  2euex  2573  2eu4  2585  rexcomf  3126  gencbvex  3281  euind  3426  sbccomlem  3541  opelopabsbALT  5013  elvvv  5212  dmuni  5366  dm0rn0  5374  dmcosseq  5419  elres  5470  rnco  5679  coass  5692  oprabid  6717  dfoprab2  6743  uniuni  7013  opabex3d  7187  opabex3  7188  frxp  7332  domen  8010  xpassen  8095  scott0  8787  dfac5lem1  8984  dfac5lem4  8987  cflem  9106  ltexprlem1  9896  ltexprlem4  9899  fsumcom2  14549  fsumcom2OLD  14550  fprodcom2  14758  fprodcom2OLD  14759  gsumval3eu  18351  dprd2d2  18489  cnvoprabOLD  29626  eldm3  31777  dfdm5  31800  dfrn5  31801  elfuns  32147  dfiota3  32155  brimg  32169  funpartlem  32174  bj-rexcom4  32994  bj-restuni  33175  sbccom2lem  34059  diblsmopel  36777  dicelval3  36786  dihjatcclem4  37027  pm11.6  38909  ax6e2ndeq  39092  e2ebind  39096  ax6e2ndeqVD  39459  e2ebindVD  39462  e2ebindALT  39479  ax6e2ndeqALT  39481  elsprel  42050  eliunxp2  42437