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  3264  rexcomf  3277  gencbvex  3507  euind  3695  sbccomlemOLD  3833  elvvv  5714  dmuni  5878  dm0rn0  5888  dmcosseqOLD  5941  cnvopab  6110  rnco  6225  coass  6238  oprabidw  7418  oprabid  7419  dfoprab2  7447  uniuni  7738  opabex3d  7944  opabex3rd  7945  opabex3  7946  frxp  8105  domen  8933  xpassen  9035  scott0  9839  dfac5lem1  10076  dfac5lem4OLD  10081  cflemOLD  10199  ltexprlem1  10989  ltexprlem4  10992  fsumcom2  15740  fprodcom2  15950  gsumval3eu  19834  dprd2d2  19976  eldm3  35748  dfdm5  35760  dfrn5  35761  elfuns  35903  dfiota3  35911  brimg  35925  funpartlem  35930  bj-19.12  36749  bj-nnflemee  36751  bj-restuni  37085  sbccom2lem  38118  dmqsblocks  38845  diblsmopel  41165  dicelval3  41174  dihjatcclem4  41415  19.9dev  42202  nnoeomeqom  43301  pm11.6  44381  ax6e2ndeq  44549  e2ebind  44553  ax6e2ndeqVD  44898  e2ebindVD  44901  e2ebindALT  44918  ax6e2ndeqALT  44920  ich2ex  47469  ichexmpl1  47470  elsprel  47476  eliunxp2  48322