Theorem excom 2162

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 2007, ax-10 2141, 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 2159	. . 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 2157

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

This theorem is referenced by:  excomim  2163  excom13  2164  exrot3  2165  eeor  2334  ee4anv  2352  ee4anvOLD  2353  2sb8ef  2358  sbel2x  2478  2sb8e  2534  2euexv  2630  2euex  2640  2eu4  2654  rexcom4  3269  rexcomf  3283  gencbvex  3520  euind  3707  sbccomlemOLD  3845  elvvv  5730  dmuni  5894  dm0rn0  5904  dmcosseqOLD  5957  cnvopab  6126  rnco  6241  coass  6254  oprabidw  7436  oprabid  7437  dfoprab2  7465  uniuni  7756  opabex3d  7964  opabex3rd  7965  opabex3  7966  frxp  8125  domen  8976  xpassen  9080  scott0  9900  dfac5lem1  10137  dfac5lem4OLD  10142  cflemOLD  10260  ltexprlem1  11050  ltexprlem4  11053  fsumcom2  15790  fprodcom2  16000  gsumval3eu  19885  dprd2d2  20027  eldm3  35778  dfdm5  35790  dfrn5  35791  elfuns  35933  dfiota3  35941  brimg  35955  funpartlem  35960  bj-19.12  36779  bj-nnflemee  36781  bj-restuni  37115  sbccom2lem  38148  diblsmopel  41190  dicelval3  41199  dihjatcclem4  41440  19.9dev  42265  nnoeomeqom  43336  pm11.6  44416  ax6e2ndeq  44584  e2ebind  44588  ax6e2ndeqVD  44933  e2ebindVD  44936  e2ebindALT  44953  ax6e2ndeqALT  44955  ich2ex  47482  ichexmpl1  47483  elsprel  47489  eliunxp2  48309