Theorem excom 2029

Description: Theorem 19.11 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.) Remove dependencies on ax-5 1827, ax-6 1875, ax-7 1922, ax-10 2006, ax-12 2034. (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 2024	. . 3 ⊢ (∀𝑥∀𝑦 ¬ 𝜑 ↔ ∀𝑦∀𝑥 ¬ 𝜑)
2	1	notbii 309	. 2 ⊢ (¬ ∀𝑥∀𝑦 ¬ 𝜑 ↔ ¬ ∀𝑦∀𝑥 ¬ 𝜑)
3		2exnaln 1746	. 2 ⊢ (∃𝑥∃𝑦𝜑 ↔ ¬ ∀𝑥∀𝑦 ¬ 𝜑)
4		2exnaln 1746	. 2 ⊢ (∃𝑦∃𝑥𝜑 ↔ ¬ ∀𝑦∀𝑥 ¬ 𝜑)
5	2, 3, 4	3bitr4i 291	1 ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑦∃𝑥𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 195  ∀wal 1473  ∃wex 1695

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-11 2021

This theorem depends on definitions:  df-bi 196  df-ex 1696

This theorem is referenced by:  excomim  2030  excom13  2031  exrot3  2032  ee4anv  2172  sbel2x  2447  2sb8e  2455  2euex  2532  2eu4  2544  rexcomf  3078  gencbvex  3223  euind  3360  sbccomlem  3475  opelopabsbALT  4909  elvvv  5101  dmuni  5256  dm0rn0  5263  dmcosseq  5308  elres  5355  rnco  5558  coass  5571  oprabid  6576  dfoprab2  6599  uniuni  6865  opabex3d  7037  opabex3  7038  frxp  7174  domen  7854  xpassen  7939  scott0  8632  dfac5lem1  8829  dfac5lem4  8832  cflem  8951  ltexprlem1  9737  ltexprlem4  9740  fsumcom2  14347  fsumcom2OLD  14348  fprodcom2  14553  fprodcom2OLD  14554  gsumval3eu  18128  dprd2d2  18266  usgraedg4  25916  cnvoprab  28886  eldm3  30905  dfdm5  30921  dfrn5  30922  elfuns  31192  dfiota3  31200  brimg  31214  funpartlem  31219  bj-rexcom4  32063  bj-restuni  32231  sbccom2lem  33099  diblsmopel  35478  dicelval3  35487  dihjatcclem4  35728  pm11.6  37614  ax6e2ndeq  37796  e2ebind  37800  ax6e2ndeqVD  38167  e2ebindVD  38170  e2ebindALT  38187  ax6e2ndeqALT  38189  eliunxp2  41905