Theorem excom 2169

Description: Theorem 19.11 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.) Remove dependencies on ax-5 1911, ax-6 1970, ax-7 2015, ax-10 2145, ax-12 2177. (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 2163	. . 3 ⊢ (∀𝑥∀𝑦 ¬ 𝜑 ↔ ∀𝑦∀𝑥 ¬ 𝜑)
2	1	notbii 322	. 2 ⊢ (¬ ∀𝑥∀𝑦 ¬ 𝜑 ↔ ¬ ∀𝑦∀𝑥 ¬ 𝜑)
3		2exnaln 1829	. 2 ⊢ (∃𝑥∃𝑦𝜑 ↔ ¬ ∀𝑥∀𝑦 ¬ 𝜑)
4		2exnaln 1829	. 2 ⊢ (∃𝑦∃𝑥𝜑 ↔ ¬ ∀𝑦∀𝑥 ¬ 𝜑)
5	2, 3, 4	3bitr4i 305	1 ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑦∃𝑥𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 208  ∀wal 1535  ∃wex 1780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-11 2161

This theorem depends on definitions:  df-bi 209  df-ex 1781

This theorem is referenced by:  excomim  2170  excom13  2171  exrot3  2172  ee4anv  2372  2sb8ev  2375  sbel2x  2498  2sb8e  2576  2euexv  2716  2euex  2726  2eu4  2739  rexcom4  3251  rexcomOLD  3358  rexcomf  3360  cgsex4g  3541  gencbvex  3551  euind  3717  sbccomlem  3855  opelopabsbALT  5418  elvvv  5629  dmuni  5785  dm0rn0  5797  dmcosseq  5846  rnco  6107  coass  6120  oprabidw  7189  oprabid  7190  dfoprab2  7214  uniuni  7486  opabex3d  7668  opabex3rd  7669  opabex3  7670  frxp  7822  domen  8524  xpassen  8613  scott0  9317  dfac5lem1  9551  dfac5lem4  9554  cflem  9670  ltexprlem1  10460  ltexprlem4  10463  fsumcom2  15131  fprodcom2  15340  gsumval3eu  19026  dprd2d2  19168  cnvoprabOLD  30458  eldm3  32999  dfdm5  33018  dfrn5  33019  elfuns  33378  dfiota3  33386  brimg  33400  funpartlem  33405  bj-19.12  34092  bj-nnflemee  34094  bj-restuni  34390  sbccom2lem  35404  diblsmopel  38309  dicelval3  38318  dihjatcclem4  38559  pm11.6  40731  ax6e2ndeq  40900  e2ebind  40904  ax6e2ndeqVD  41250  e2ebindVD  41253  e2ebindALT  41270  ax6e2ndeqALT  41272  ich2ex  43636  ichexmpl1  43638  elsprel  43644  eliunxp2  44389