Theorem excom 2168

Description: Theorem 19.11 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.) Remove dependencies on ax-5 1918, ax-6 1976, ax-7 2018, ax-10 2143, 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 2162	. . 3 ⊢ (∀𝑥∀𝑦 ¬ 𝜑 ↔ ∀𝑦∀𝑥 ¬ 𝜑)
2	1	notbii 323	. 2 ⊢ (¬ ∀𝑥∀𝑦 ¬ 𝜑 ↔ ¬ ∀𝑦∀𝑥 ¬ 𝜑)
3		2exnaln 1836	. 2 ⊢ (∃𝑥∃𝑦𝜑 ↔ ¬ ∀𝑥∀𝑦 ¬ 𝜑)
4		2exnaln 1836	. 2 ⊢ (∃𝑦∃𝑥𝜑 ↔ ¬ ∀𝑦∀𝑥 ¬ 𝜑)
5	2, 3, 4	3bitr4i 306	1 ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑦∃𝑥𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 209  ∀wal 1541  ∃wex 1787

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-11 2160

This theorem depends on definitions:  df-bi 210  df-ex 1788

This theorem is referenced by:  excomim  2169  excom13  2170  exrot3  2171  ee4anv  2353  2sb8ev  2356  sbel2x  2473  2sb8e  2534  2euexv  2632  2euex  2642  2eu4  2655  rexcom4  3162  rexcomf  3260  cgsex4gOLD  3443  gencbvex  3454  euind  3626  sbccomlem  3769  elvvv  5609  dmuni  5768  dm0rn0  5779  dmcosseq  5827  rnco  6096  coass  6109  oprabidw  7222  oprabid  7223  dfoprab2  7247  uniuni  7525  opabex3d  7716  opabex3rd  7717  opabex3  7718  frxp  7871  domen  8619  xpassen  8717  scott0  9467  dfac5lem1  9702  dfac5lem4  9705  cflem  9825  ltexprlem1  10615  ltexprlem4  10618  fsumcom2  15301  fprodcom2  15509  gsumval3eu  19243  dprd2d2  19385  cnvoprabOLD  30729  eldm3  33398  dfdm5  33417  dfrn5  33418  elfuns  33903  dfiota3  33911  brimg  33925  funpartlem  33930  bj-19.12  34629  bj-nnflemee  34631  bj-restuni  34952  sbccom2lem  35968  diblsmopel  38871  dicelval3  38880  dihjatcclem4  39121  19.9dev  39842  pm11.6  41624  ax6e2ndeq  41793  e2ebind  41797  ax6e2ndeqVD  42143  e2ebindVD  42146  e2ebindALT  42163  ax6e2ndeqALT  42165  ich2ex  44536  ichexmpl1  44537  elsprel  44543  eliunxp2  45285