Theorem excom 2162

Description: Theorem 19.11 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.) Remove dependencies on ax-5 1913, ax-6 1971, ax-7 2011, ax-10 2137, ax-12 2171. (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 2156	. . 3 ⊢ (∀𝑥∀𝑦 ¬ 𝜑 ↔ ∀𝑦∀𝑥 ¬ 𝜑)
2	1	notbii 320	. 2 ⊢ (¬ ∀𝑥∀𝑦 ¬ 𝜑 ↔ ¬ ∀𝑦∀𝑥 ¬ 𝜑)
3		2exnaln 1831	. 2 ⊢ (∃𝑥∃𝑦𝜑 ↔ ¬ ∀𝑥∀𝑦 ¬ 𝜑)
4		2exnaln 1831	. 2 ⊢ (∃𝑦∃𝑥𝜑 ↔ ¬ ∀𝑦∀𝑥 ¬ 𝜑)
5	2, 3, 4	3bitr4i 303	1 ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑦∃𝑥𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 205  ∀wal 1537  ∃wex 1782

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-11 2154

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

This theorem is referenced by:  excomim  2163  excom13  2164  exrot3  2165  eeor  2330  ee4anv  2349  2sb8ef  2354  sbel2x  2474  2sb8e  2535  2euexv  2633  2euex  2643  2eu4  2656  rexcom4  3233  rexcomf  3284  cgsex4gOLD  3477  gencbvex  3488  euind  3659  sbccomlem  3803  elvvv  5662  dmuni  5823  dm0rn0  5834  dmcosseq  5882  rnco  6156  coass  6169  oprabidw  7306  oprabid  7307  dfoprab2  7333  uniuni  7612  opabex3d  7808  opabex3rd  7809  opabex3  7810  frxp  7967  domen  8751  xpassen  8853  scott0  9644  dfac5lem1  9879  dfac5lem4  9882  cflem  10002  ltexprlem1  10792  ltexprlem4  10795  fsumcom2  15486  fprodcom2  15694  gsumval3eu  19505  dprd2d2  19647  cnvoprabOLD  31055  eldm3  33728  dfdm5  33747  dfrn5  33748  elfuns  34217  dfiota3  34225  brimg  34239  funpartlem  34244  bj-19.12  34943  bj-nnflemee  34945  bj-restuni  35268  sbccom2lem  36282  diblsmopel  39185  dicelval3  39194  dihjatcclem4  39435  19.9dev  40178  pm11.6  42010  ax6e2ndeq  42179  e2ebind  42183  ax6e2ndeqVD  42529  e2ebindVD  42532  e2ebindALT  42549  ax6e2ndeqALT  42551  ich2ex  44920  ichexmpl1  44921  elsprel  44927  eliunxp2  45669