Theorem excom 2200

Description: Theorem 19.11 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.) Remove dependencies on ax-5 1943, ax-6 2000, ax-7 2041, ax-10 2179, ax-12 2216. (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 2197	. . 3 ⊢ (∀𝑥∀𝑦 ¬ 𝜑 ↔ ∀𝑦∀𝑥 ¬ 𝜑)
2	1	notbii 323	. 2 ⊢ (¬ ∀𝑥∀𝑦 ¬ 𝜑 ↔ ¬ ∀𝑦∀𝑥 ¬ 𝜑)
3		2exnaln 1862	. 2 ⊢ (∃𝑥∃𝑦𝜑 ↔ ¬ ∀𝑥∀𝑦 ¬ 𝜑)
4		2exnaln 1862	. 2 ⊢ (∃𝑦∃𝑥𝜑 ↔ ¬ ∀𝑦∀𝑥 ¬ 𝜑)
5	2, 3, 4	3bitr4i 306	1 ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑦∃𝑥𝜑)

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209  ∀wal 1568  ∃wex 1812

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-11 2195

This proof depends on definitions:  df-bi 210  df-ex 1813

This theorem is used by:  excomim  2201  excom13  2202  exrot3  2203  eeor  2368  ee4anv  2385  ee4anvOLD  2386  2sb8ef  2390  sbel2x  2508  2sb8e  2564  2euexv  2661  2euex  2671  2eu4  2684  rexcom4  3294  rexcomf  3306  gencbvex  3513  euind  3689  elvvv  5739  dmuni  5906  dm0rn0OLD  5917  cnvopab  6139  rncoOLD  6256  coass  6269  oprabidw  7447  oprabid  7448  dfoprab2  7474  uniuni  7763  opabex3d  7964  opabex3rd  7965  opabex3  7966  frxp  8124  domen  8960  xpassen  9062  scott0b  9869  scott0OLD  9870  dfac5lem1  10119  ltexprlem1  11032  ltexprlem4  11035  fsumcom2  15843  fprodcom2  16056  gsumval3eu  19997  dprd2d2  20139  eldm3  36266  dfdm5  36278  dfrn5  36279  elfuns  36418  dfiota3  36426  brimg  36440  funpartlem  36447  bj-19.12  37381  bj-nnflemee  37445  bj-restuni  37772  sbccom2lem  38806  dmqsblocks  39649  diblsmopel  41978  dicelval3  41987  dihjatcclem4  42228  nfe2  43017  19.9dev  43019  nnoeomeqom  44072  pm11.6  45135  ax6e2ndeq  45301  e2ebind  45305  ax6e2ndeqVD  45650  e2ebindVD  45653  e2ebindALT  45670  ax6e2ndeqALT  45672  ich2ex  48250  ichexmpl1  48251  elsprel  48257  eliunxp2  49147