Theorem excom 2202

Description: Theorem 19.11 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.) Remove dependencies on ax-5 1945, ax-6 2002, ax-7 2043, ax-10 2180, 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 2199	. . 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 2197

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

This theorem is used by:  excomim  2203  excom13  2204  exrot3  2205  eeor  2367  ee4anv  2384  2sb8ef  2388  sbel2x  2506  2sb8e  2562  2euexv  2659  2euex  2669  2eu4  2682  rexcom4  3293  rexcomf  3305  gencbvex  3510  euind  3685  elvvv  5735  dmuni  5908  dm0rn0OLD  5919  cnvopab  6149  rncoOLD  6273  coassOLD  6291  oprabidw  7482  oprabid  7483  dfoprab2  7509  uniuni  7808  opabex3d  8011  opabex3rd  8012  opabex3  8013  frxp  8175  domen  9026  xpassen  9128  scott0b  9974  scott0OLD  9975  dfac5lem1  10241  ltexprlem1  11160  ltexprlem4  11163  fsumcom2  15984  fprodcom2  16195  gsumval3eu  20169  dprd2d2  20311  mirimanofffr  36670  eldm3  36741  dfdm5  36752  dfrn5  36753  elfuns  36892  dfiota3  36900  brimg  36914  funpartlem  36921  bj-19.12  37840  bj-nnflemee  37904  bj-restuni  38288  sbccom2lem  39322  dmqsblocks  40165  diblsmopel  42494  dicelval3  42503  dihjatcclem4  42744  nfe2  43534  19.9dev  43536  nnoeomeqom  44575  pm11.6  45637  ax6e2ndeq  45802  e2ebind  45806  ax6e2ndeqVD  46151  e2ebindVD  46154  e2ebindALT  46171  ax6e2ndeqALT  46173  ich2ex  48823  ichexmpl1  48824  elsprel  48830  eliunxp2  49777