Theorem excom 2203

Description: Theorem 19.11 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.) Remove dependencies on ax-5 1937, ax-6 1994, ax-7 2035, ax-10 2182, ax-12 2219. (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 2200	. . 3 ⊢ (∀𝑥∀𝑦 ¬ 𝜑 ↔ ∀𝑦∀𝑥 ¬ 𝜑)
2	1	notbii 323	. 2 ⊢ (¬ ∀𝑥∀𝑦 ¬ 𝜑 ↔ ¬ ∀𝑦∀𝑥 ¬ 𝜑)
3		2exnaln 1856	. 2 ⊢ (∃𝑥∃𝑦𝜑 ↔ ¬ ∀𝑥∀𝑦 ¬ 𝜑)
4		2exnaln 1856	. 2 ⊢ (∃𝑦∃𝑥𝜑 ↔ ¬ ∀𝑦∀𝑥 ¬ 𝜑)
5	2, 3, 4	3bitr4i 306	1 ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑦∃𝑥𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 209  ∀wal 1565  ∃wex 1806

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

This theorem depends on definitions:  df-bi 210  df-ex 1807

This theorem is referenced by:  excomim  2204  excom13  2205  exrot3  2206  eeor  2372  ee4anv  2389  ee4anvOLD  2390  2sb8ef  2394  sbel2x  2512  2sb8e  2568  2euexv  2665  2euex  2675  2eu4  2688  rexcom4  3298  rexcomf  3310  gencbvex  3519  euind  3696  sbccomlemOLD  3832  elvvv  5735  dmuni  5902  dm0rn0OLD  5913  cnvopab  6135  rncoOLD  6251  coass  6264  oprabidw  7439  oprabid  7440  dfoprab2  7466  uniuni  7757  opabex3d  7958  opabex3rd  7959  opabex3  7960  frxp  8118  domen  8954  xpassen  9055  scott0  9856  dfac5lem1  10103  cflemOLD  10225  ltexprlem1  11017  ltexprlem4  11020  fsumcom2  15821  fprodcom2  16034  gsumval3eu  19970  dprd2d2  20112  eldm3  36148  dfdm5  36160  dfrn5  36161  elfuns  36300  dfiota3  36308  brimg  36322  funpartlem  36329  bj-19.12  37233  bj-nnflemee  37297  bj-restuni  37622  sbccom2lem  38658  dmqsblocks  39501  diblsmopel  41830  dicelval3  41839  dihjatcclem4  42080  nfe2  42867  19.9dev  42869  nnoeomeqom  43924  pm11.6  44987  ax6e2ndeq  45153  e2ebind  45157  ax6e2ndeqVD  45502  e2ebindVD  45505  e2ebindALT  45522  ax6e2ndeqALT  45524  ich2ex  48099  ichexmpl1  48100  elsprel  48106  eliunxp2  48992