Theorem excom 2198

Description: Theorem 19.11 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.) Remove dependencies on ax-5 1942, ax-6 1999, ax-7 2040, ax-10 2177, ax-12 2212. (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 2195	. . 3 ⊢ (∀𝑥∀𝑦 ¬ 𝜑 ↔ ∀𝑦∀𝑥 ¬ 𝜑)
2	1	notbii 323	. 2 ⊢ (¬ ∀𝑥∀𝑦 ¬ 𝜑 ↔ ¬ ∀𝑦∀𝑥 ¬ 𝜑)
3		2exnaln 1861	. 2 ⊢ (∃𝑥∃𝑦𝜑 ↔ ¬ ∀𝑥∀𝑦 ¬ 𝜑)
4		2exnaln 1861	. 2 ⊢ (∃𝑦∃𝑥𝜑 ↔ ¬ ∀𝑦∀𝑥 ¬ 𝜑)
5	2, 3, 4	3bitr4i 306	1 ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑦∃𝑥𝜑)

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-11 2193

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

This theorem is used by:  excomim  2199  excom13  2200  exrot3  2201  eeor  2363  ee4anv  2380  ee4anvOLD  2381  2sb8ef  2385  sbel2x  2503  2sb8e  2559  2euexv  2656  2euex  2666  2eu4  2679  rexcom4  3289  rexcomf  3301  gencbvex  3506  euind  3681  elvvv  5726  dmuni  5895  dm0rn0OLD  5906  cnvopab  6130  rncoOLD  6254  coass  6267  oprabidw  7452  oprabid  7453  dfoprab2  7479  uniuni  7777  opabex3d  7978  opabex3rd  7979  opabex3  7980  frxp  8141  domen  8992  xpassen  9094  scott0b  9941  scott0OLD  9942  dfac5lem1  10206  ltexprlem1  11125  ltexprlem4  11128  fsumcom2  15946  fprodcom2  16157  gsumval3eu  20124  dprd2d2  20266  eldm3  36619  dfdm5  36630  dfrn5  36631  elfuns  36770  dfiota3  36778  brimg  36792  funpartlem  36799  bj-19.12  37718  bj-nnflemee  37782  bj-restuni  38111  sbccom2lem  39150  dmqsblocks  39993  diblsmopel  42322  dicelval3  42331  dihjatcclem4  42572  nfe2  43361  19.9dev  43363  nnoeomeqom  44408  pm11.6  45470  ax6e2ndeq  45636  e2ebind  45640  ax6e2ndeqVD  45985  e2ebindVD  45988  e2ebindALT  46005  ax6e2ndeqALT  46007  ich2ex  48644  ichexmpl1  48645  elsprel  48651  eliunxp2  49540