Theorem excom 2164

Description: Theorem 19.11 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.) Remove dependencies on ax-5 1914, ax-6 1972, ax-7 2012, ax-10 2139, ax-12 2173. (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 2158	. . 3 ⊢ (∀𝑥∀𝑦 ¬ 𝜑 ↔ ∀𝑦∀𝑥 ¬ 𝜑)
2	1	notbii 319	. 2 ⊢ (¬ ∀𝑥∀𝑦 ¬ 𝜑 ↔ ¬ ∀𝑦∀𝑥 ¬ 𝜑)
3		2exnaln 1832	. 2 ⊢ (∃𝑥∃𝑦𝜑 ↔ ¬ ∀𝑥∀𝑦 ¬ 𝜑)
4		2exnaln 1832	. 2 ⊢ (∃𝑦∃𝑥𝜑 ↔ ¬ ∀𝑦∀𝑥 ¬ 𝜑)
5	2, 3, 4	3bitr4i 302	1 ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑦∃𝑥𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 205  ∀wal 1537  ∃wex 1783

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-11 2156

This theorem depends on definitions:  df-bi 206  df-ex 1784

This theorem is referenced by:  excomim  2165  excom13  2166  exrot3  2167  ee4anv  2351  2sb8ev  2354  sbel2x  2474  2sb8e  2535  2euexv  2633  2euex  2643  2eu4  2656  rexcom4  3179  rexcomf  3283  cgsex4gOLD  3467  gencbvex  3478  euind  3654  sbccomlem  3799  elvvv  5653  dmuni  5812  dm0rn0  5823  dmcosseq  5871  rnco  6145  coass  6158  oprabidw  7286  oprabid  7287  dfoprab2  7311  uniuni  7590  opabex3d  7781  opabex3rd  7782  opabex3  7783  frxp  7938  domen  8706  xpassen  8806  scott0  9575  dfac5lem1  9810  dfac5lem4  9813  cflem  9933  ltexprlem1  10723  ltexprlem4  10726  fsumcom2  15414  fprodcom2  15622  gsumval3eu  19420  dprd2d2  19562  cnvoprabOLD  30957  eldm3  33634  dfdm5  33653  dfrn5  33654  elfuns  34144  dfiota3  34152  brimg  34166  funpartlem  34171  bj-19.12  34870  bj-nnflemee  34872  bj-restuni  35195  sbccom2lem  36209  diblsmopel  39112  dicelval3  39121  dihjatcclem4  39362  19.9dev  40106  pm11.6  41899  ax6e2ndeq  42068  e2ebind  42072  ax6e2ndeqVD  42418  e2ebindVD  42421  e2ebindALT  42438  ax6e2ndeqALT  42440  ich2ex  44808  ichexmpl1  44809  elsprel  44815  eliunxp2  45557