Theorem excom 2168

Description: Theorem 19.11 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.) Remove dependencies on ax-5 1912, ax-6 1969, ax-7 2010, ax-10 2147, ax-12 2185. (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 2165	. . 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 206  ∀wal 1540  ∃wex 1781

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-11 2163

This theorem depends on definitions:  df-bi 207  df-ex 1782

This theorem is referenced by:  excomim  2169  excom13  2170  exrot3  2171  eeor  2339  ee4anv  2356  ee4anvOLD  2357  2sb8ef  2361  sbel2x  2479  2sb8e  2535  2euexv  2632  2euex  2642  2eu4  2656  rexcom4  3265  rexcomf  3277  gencbvex  3501  euind  3684  sbccomlemOLD  3822  elvvv  5708  dmuni  5871  dm0rn0OLD  5882  dmcosseqOLDOLD  5937  cnvopab  6102  rncoOLD  6219  coass  6232  oprabidw  7399  oprabid  7400  dfoprab2  7426  uniuni  7717  opabex3d  7919  opabex3rd  7920  opabex3  7921  frxp  8078  domen  8910  xpassen  9011  scott0  9810  dfac5lem1  10045  dfac5lem4OLD  10050  cflemOLD  10168  ltexprlem1  10959  ltexprlem4  10962  fsumcom2  15709  fprodcom2  15919  gsumval3eu  19845  dprd2d2  19987  eldm3  35974  dfdm5  35986  dfrn5  35987  elfuns  36126  dfiota3  36134  brimg  36148  funpartlem  36155  bj-19.12  36963  bj-nnflemee  37022  bj-restuni  37347  sbccom2lem  38372  dmqsblocks  39215  diblsmopel  41544  dicelval3  41553  dihjatcclem4  41794  nfe2  42582  19.9dev  42584  nnoeomeqom  43666  pm11.6  44745  ax6e2ndeq  44912  e2ebind  44916  ax6e2ndeqVD  45261  e2ebindVD  45264  e2ebindALT  45281  ax6e2ndeqALT  45283  ich2ex  47825  ichexmpl1  47826  elsprel  47832  eliunxp2  48691