Theorem excom 2163

Description: Theorem 19.11 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.) Remove dependencies on ax-5 1910, ax-6 1967, ax-7 2008, ax-10 2142, ax-12 2178. (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 2160	. . 3 ⊢ (∀𝑥∀𝑦 ¬ 𝜑 ↔ ∀𝑦∀𝑥 ¬ 𝜑)
2	1	notbii 320	. 2 ⊢ (¬ ∀𝑥∀𝑦 ¬ 𝜑 ↔ ¬ ∀𝑦∀𝑥 ¬ 𝜑)
3		2exnaln 1829	. 2 ⊢ (∃𝑥∃𝑦𝜑 ↔ ¬ ∀𝑥∀𝑦 ¬ 𝜑)
4		2exnaln 1829	. 2 ⊢ (∃𝑦∃𝑥𝜑 ↔ ¬ ∀𝑦∀𝑥 ¬ 𝜑)
5	2, 3, 4	3bitr4i 303	1 ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑦∃𝑥𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 206  ∀wal 1538  ∃wex 1779

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-11 2158

This theorem depends on definitions:  df-bi 207  df-ex 1780

This theorem is referenced by:  excomim  2164  excom13  2165  exrot3  2166  eeor  2332  ee4anv  2349  ee4anvOLD  2350  2sb8ef  2355  sbel2x  2473  2sb8e  2529  2euexv  2625  2euex  2635  2eu4  2649  rexcom4  3265  rexcomf  3279  gencbvex  3510  euind  3698  sbccomlemOLD  3836  elvvv  5717  dmuni  5881  dm0rn0  5891  dmcosseqOLD  5944  cnvopab  6113  rnco  6228  coass  6241  oprabidw  7421  oprabid  7422  dfoprab2  7450  uniuni  7741  opabex3d  7947  opabex3rd  7948  opabex3  7949  frxp  8108  domen  8936  xpassen  9040  scott0  9846  dfac5lem1  10083  dfac5lem4OLD  10088  cflemOLD  10206  ltexprlem1  10996  ltexprlem4  10999  fsumcom2  15747  fprodcom2  15957  gsumval3eu  19841  dprd2d2  19983  eldm3  35755  dfdm5  35767  dfrn5  35768  elfuns  35910  dfiota3  35918  brimg  35932  funpartlem  35937  bj-19.12  36756  bj-nnflemee  36758  bj-restuni  37092  sbccom2lem  38125  dmqsblocks  38852  diblsmopel  41172  dicelval3  41181  dihjatcclem4  41422  19.9dev  42209  nnoeomeqom  43308  pm11.6  44388  ax6e2ndeq  44556  e2ebind  44560  ax6e2ndeqVD  44905  e2ebindVD  44908  e2ebindALT  44925  ax6e2ndeqALT  44927  ich2ex  47473  ichexmpl1  47474  elsprel  47480  eliunxp2  48326