Theorem excom 2206

Description: Theorem 19.11 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.) Remove dependencies on ax-5 2005, ax-6 2069, ax-7 2105, ax-10 2183, ax-12 2211. (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 2201	. . 3 ⊢ (∀𝑥∀𝑦 ¬ 𝜑 ↔ ∀𝑦∀𝑥 ¬ 𝜑)
2	1	notbii 311	. 2 ⊢ (¬ ∀𝑥∀𝑦 ¬ 𝜑 ↔ ¬ ∀𝑦∀𝑥 ¬ 𝜑)
3		2exnaln 1923	. 2 ⊢ (∃𝑥∃𝑦𝜑 ↔ ¬ ∀𝑥∀𝑦 ¬ 𝜑)
4		2exnaln 1923	. 2 ⊢ (∃𝑦∃𝑥𝜑 ↔ ¬ ∀𝑦∀𝑥 ¬ 𝜑)
5	2, 3, 4	3bitr4i 294	1 ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑦∃𝑥𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 197  ∀wal 1650  ∃wex 1874

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-11 2198

This theorem depends on definitions:  df-bi 198  df-ex 1875

This theorem is referenced by:  excomim  2207  excom13  2208  exrot3  2209  ee4anv  2348  sbel2x  2551  2sb8e  2559  2euex  2666  2eu4  2678  rexcomf  3244  gencbvex  3403  euind  3552  sbccomlem  3667  opelopabsbALT  5145  elvvv  5346  dmuni  5502  dm0rn0  5510  dmcosseq  5556  elresOLD  5611  rnco  5827  coass  5840  oprabid  6873  dfoprab2  6899  uniuni  7169  opabex3d  7343  opabex3  7344  frxp  7489  domen  8173  xpassen  8261  scott0  8964  dfac5lem1  9197  dfac5lem4  9200  cflem  9321  ltexprlem1  10111  ltexprlem4  10114  fsumcom2  14792  fprodcom2  14999  gsumval3eu  18571  dprd2d2  18710  cnvoprabOLD  29882  eldm3  32028  dfdm5  32051  dfrn5  32052  elfuns  32398  dfiota3  32406  brimg  32420  funpartlem  32425  bj-rexcom4  33226  bj-restuni  33410  sbccom2lem  34282  diblsmopel  37059  dicelval3  37068  dihjatcclem4  37309  pm11.6  39198  ax6e2ndeq  39369  e2ebind  39373  ax6e2ndeqVD  39729  e2ebindVD  39732  e2ebindALT  39749  ax6e2ndeqALT  39751  elsprel  42326  eliunxp2  42713