Theorem excom 2133

Description: Theorem 19.11 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.) Remove dependencies on ax-5 1888, ax-6 1947, ax-7 1992, ax-10 2112, ax-12 2141. (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 2128	. . 3 ⊢ (∀𝑥∀𝑦 ¬ 𝜑 ↔ ∀𝑦∀𝑥 ¬ 𝜑)
2	1	notbii 321	. 2 ⊢ (¬ ∀𝑥∀𝑦 ¬ 𝜑 ↔ ¬ ∀𝑦∀𝑥 ¬ 𝜑)
3		2exnaln 1810	. 2 ⊢ (∃𝑥∃𝑦𝜑 ↔ ¬ ∀𝑥∀𝑦 ¬ 𝜑)
4		2exnaln 1810	. 2 ⊢ (∃𝑦∃𝑥𝜑 ↔ ¬ ∀𝑦∀𝑥 ¬ 𝜑)
5	2, 3, 4	3bitr4i 304	1 ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑦∃𝑥𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 207  ∀wal 1520  ∃wex 1761

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

This theorem depends on definitions:  df-bi 208  df-ex 1762

This theorem is referenced by:  excomim  2134  excom13  2135  exrot3  2136  ee4anv  2328  2sb8ev  2331  2sb8evOLD  2332  sbel2x  2456  2sb8e  2530  2euexv  2686  2euex  2696  2eu4  2711  rexcom4  3213  rexcomOLD  3317  rexcomf  3319  cgsex4g  3482  gencbvex  3492  euind  3649  sbccomlem  3781  opelopabsbALT  5306  elvvv  5513  dmuni  5669  dm0rn0  5679  dmcosseq  5725  rnco  5980  coass  5993  oprabid  7047  dfoprab2  7071  uniuni  7341  opabex3d  7522  opabex3rd  7523  opabex3  7524  frxp  7673  domen  8370  xpassen  8458  scott0  9161  dfac5lem1  9395  dfac5lem4  9398  cflem  9514  ltexprlem1  10304  ltexprlem4  10307  fsumcom2  14962  fprodcom2  15171  gsumval3eu  18745  dprd2d2  18883  cnvoprabOLD  30144  eldm3  32606  dfdm5  32625  dfrn5  32626  elfuns  32986  dfiota3  32994  brimg  33008  funpartlem  33013  bj-19.12  33884  bj-nnflemee  33886  bj-restuni  34006  sbccom2lem  34953  diblsmopel  37857  dicelval3  37866  dihjatcclem4  38107  pm11.6  40281  ax6e2ndeq  40451  e2ebind  40455  ax6e2ndeqVD  40801  e2ebindVD  40804  e2ebindALT  40821  ax6e2ndeqALT  40823  ich2ex  43131  ichexmpl1  43133  elsprel  43139  eliunxp2  43880