Theorem excom 2042

Description: Theorem 19.11 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.) Remove dependencies on ax-5 1839, ax-6 1888, ax-7 1935, ax-10 2019, ax-12 2047. (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 2037	. . 3 ⊢ (∀𝑥∀𝑦 ¬ 𝜑 ↔ ∀𝑦∀𝑥 ¬ 𝜑)
2	1	notbii 310	. 2 ⊢ (¬ ∀𝑥∀𝑦 ¬ 𝜑 ↔ ¬ ∀𝑦∀𝑥 ¬ 𝜑)
3		2exnaln 1756	. 2 ⊢ (∃𝑥∃𝑦𝜑 ↔ ¬ ∀𝑥∀𝑦 ¬ 𝜑)
4		2exnaln 1756	. 2 ⊢ (∃𝑦∃𝑥𝜑 ↔ ¬ ∀𝑦∀𝑥 ¬ 𝜑)
5	2, 3, 4	3bitr4i 292	1 ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑦∃𝑥𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 196  ∀wal 1481  ∃wex 1704

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-11 2034

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

This theorem is referenced by:  excomim  2043  excom13  2044  exrot3  2045  ee4anv  2184  sbel2x  2459  2sb8e  2467  2euex  2544  2eu4  2556  rexcomf  3097  gencbvex  3250  euind  3393  sbccomlem  3508  opelopabsbALT  4984  elvvv  5178  dmuni  5334  dm0rn0  5342  dmcosseq  5387  elres  5435  rnco  5641  coass  5654  oprabid  6677  dfoprab2  6701  uniuni  6971  opabex3d  7145  opabex3  7146  frxp  7287  domen  7968  xpassen  8054  scott0  8749  dfac5lem1  8946  dfac5lem4  8949  cflem  9068  ltexprlem1  9858  ltexprlem4  9861  fsumcom2  14505  fsumcom2OLD  14506  fprodcom2  14714  fprodcom2OLD  14715  gsumval3eu  18305  dprd2d2  18443  cnvoprab  29498  eldm3  31651  dfdm5  31676  dfrn5  31677  elfuns  32022  dfiota3  32030  brimg  32044  funpartlem  32049  bj-rexcom4  32869  bj-restuni  33050  sbccom2lem  33929  diblsmopel  36460  dicelval3  36469  dihjatcclem4  36710  pm11.6  38592  ax6e2ndeq  38775  e2ebind  38779  ax6e2ndeqVD  39145  e2ebindVD  39148  e2ebindALT  39165  ax6e2ndeqALT  39167  elsprel  41725  eliunxp2  42112