Theorem excom 2169

Description: Theorem 19.11 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.) Remove dependencies on ax-5 1911, ax-6 1970, ax-7 2015, ax-10 2145, 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 2163	. . 3 ⊢ (∀𝑥∀𝑦 ¬ 𝜑 ↔ ∀𝑦∀𝑥 ¬ 𝜑)
2	1	notbii 322	. 2 ⊢ (¬ ∀𝑥∀𝑦 ¬ 𝜑 ↔ ¬ ∀𝑦∀𝑥 ¬ 𝜑)
3		2exnaln 1829	. 2 ⊢ (∃𝑥∃𝑦𝜑 ↔ ¬ ∀𝑥∀𝑦 ¬ 𝜑)
4		2exnaln 1829	. 2 ⊢ (∃𝑦∃𝑥𝜑 ↔ ¬ ∀𝑦∀𝑥 ¬ 𝜑)
5	2, 3, 4	3bitr4i 305	1 ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑦∃𝑥𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 208  ∀wal 1535  ∃wex 1780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-11 2161

This theorem depends on definitions:  df-bi 209  df-ex 1781

This theorem is referenced by:  excomim  2170  excom13  2171  exrot3  2172  ee4anv  2372  2sb8ev  2375  sbel2x  2498  2sb8e  2576  2euexv  2716  2euex  2726  2eu4  2739  rexcom4  3249  rexcomOLD  3356  rexcomf  3358  cgsex4g  3539  gencbvex  3549  euind  3715  sbccomlem  3853  opelopabsbALT  5416  elvvv  5627  dmuni  5783  dm0rn0  5795  dmcosseq  5844  rnco  6105  coass  6118  oprabidw  7187  oprabid  7188  dfoprab2  7212  uniuni  7484  opabex3d  7666  opabex3rd  7667  opabex3  7668  frxp  7820  domen  8522  xpassen  8611  scott0  9315  dfac5lem1  9549  dfac5lem4  9552  cflem  9668  ltexprlem1  10458  ltexprlem4  10461  fsumcom2  15129  fprodcom2  15338  gsumval3eu  19024  dprd2d2  19166  cnvoprabOLD  30456  eldm3  32997  dfdm5  33016  dfrn5  33017  elfuns  33376  dfiota3  33384  brimg  33398  funpartlem  33403  bj-19.12  34090  bj-nnflemee  34092  bj-restuni  34391  sbccom2lem  35417  diblsmopel  38322  dicelval3  38331  dihjatcclem4  38572  pm11.6  40744  ax6e2ndeq  40913  e2ebind  40917  ax6e2ndeqVD  41263  e2ebindVD  41266  e2ebindALT  41283  ax6e2ndeqALT  41285  ich2ex  43649  ichexmpl1  43651  elsprel  43657  eliunxp2  44402