Theorem excom 2165

Description: Theorem 19.11 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.) Remove dependencies on ax-5 1916, ax-6 1974, ax-7 2014, ax-10 2140, ax-12 2174. (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 319	. 2 ⊢ (¬ ∀𝑥∀𝑦 ¬ 𝜑 ↔ ¬ ∀𝑦∀𝑥 ¬ 𝜑)
3		2exnaln 1834	. 2 ⊢ (∃𝑥∃𝑦𝜑 ↔ ¬ ∀𝑥∀𝑦 ¬ 𝜑)
4		2exnaln 1834	. 2 ⊢ (∃𝑦∃𝑥𝜑 ↔ ¬ ∀𝑦∀𝑥 ¬ 𝜑)
5	2, 3, 4	3bitr4i 302	1 ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑦∃𝑥𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 205  ∀wal 1539  ∃wex 1785

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-11 2157

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

This theorem is referenced by:  excomim  2166  excom13  2167  exrot3  2168  eeor  2333  ee4anv  2352  2sb8ev  2355  sbel2x  2475  2sb8e  2536  2euexv  2634  2euex  2644  2eu4  2657  rexcom4  3181  rexcomf  3285  cgsex4gOLD  3475  gencbvex  3486  euind  3662  sbccomlem  3807  elvvv  5661  dmuni  5820  dm0rn0  5831  dmcosseq  5879  rnco  6153  coass  6166  oprabidw  7299  oprabid  7300  dfoprab2  7324  uniuni  7603  opabex3d  7794  opabex3rd  7795  opabex3  7796  frxp  7951  domen  8722  xpassen  8822  scott0  9628  dfac5lem1  9863  dfac5lem4  9866  cflem  9986  ltexprlem1  10776  ltexprlem4  10779  fsumcom2  15467  fprodcom2  15675  gsumval3eu  19486  dprd2d2  19628  cnvoprabOLD  31034  eldm3  33707  dfdm5  33726  dfrn5  33727  elfuns  34196  dfiota3  34204  brimg  34218  funpartlem  34223  bj-19.12  34922  bj-nnflemee  34924  bj-restuni  35247  sbccom2lem  36261  diblsmopel  39164  dicelval3  39173  dihjatcclem4  39414  19.9dev  40158  pm11.6  41963  ax6e2ndeq  42132  e2ebind  42136  ax6e2ndeqVD  42482  e2ebindVD  42485  e2ebindALT  42502  ax6e2ndeqALT  42504  ich2ex  44872  ichexmpl1  44873  elsprel  44879  eliunxp2  45621