Theorem excom 2163

Description: Theorem 19.11 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.) Remove dependencies on ax-5 1910, ax-6 1967, ax-7 2008, ax-10 2142, ax-12 2178. (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 2160	. . 3 ⊢ (∀𝑥∀𝑦 ¬ 𝜑 ↔ ∀𝑦∀𝑥 ¬ 𝜑)
2	1	notbii 320	. 2 ⊢ (¬ ∀𝑥∀𝑦 ¬ 𝜑 ↔ ¬ ∀𝑦∀𝑥 ¬ 𝜑)
3		2exnaln 1829	. 2 ⊢ (∃𝑥∃𝑦𝜑 ↔ ¬ ∀𝑥∀𝑦 ¬ 𝜑)
4		2exnaln 1829	. 2 ⊢ (∃𝑦∃𝑥𝜑 ↔ ¬ ∀𝑦∀𝑥 ¬ 𝜑)
5	2, 3, 4	3bitr4i 303	1 ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑦∃𝑥𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 206  ∀wal 1538  ∃wex 1779

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-11 2158

This theorem depends on definitions:  df-bi 207  df-ex 1780

This theorem is referenced by:  excomim  2164  excom13  2165  exrot3  2166  eeor  2332  ee4anv  2349  ee4anvOLD  2350  2sb8ef  2354  sbel2x  2472  2sb8e  2528  2euexv  2624  2euex  2634  2eu4  2648  rexcom4  3262  rexcomf  3275  gencbvex  3504  euind  3692  sbccomlemOLD  3830  elvvv  5707  dmuni  5868  dm0rn0  5878  dmcosseqOLD  5930  cnvopab  6098  rnco  6213  coass  6226  oprabidw  7400  oprabid  7401  dfoprab2  7427  uniuni  7718  opabex3d  7923  opabex3rd  7924  opabex3  7925  frxp  8082  domen  8910  xpassen  9012  scott0  9815  dfac5lem1  10052  dfac5lem4OLD  10057  cflemOLD  10175  ltexprlem1  10965  ltexprlem4  10968  fsumcom2  15716  fprodcom2  15926  gsumval3eu  19810  dprd2d2  19952  eldm3  35721  dfdm5  35733  dfrn5  35734  elfuns  35876  dfiota3  35884  brimg  35898  funpartlem  35903  bj-19.12  36722  bj-nnflemee  36724  bj-restuni  37058  sbccom2lem  38091  dmqsblocks  38818  diblsmopel  41138  dicelval3  41147  dihjatcclem4  41388  19.9dev  42175  nnoeomeqom  43274  pm11.6  44354  ax6e2ndeq  44522  e2ebind  44526  ax6e2ndeqVD  44871  e2ebindVD  44874  e2ebindALT  44891  ax6e2ndeqALT  44893  ich2ex  47442  ichexmpl1  47443  elsprel  47449  eliunxp2  48295