Theorem excom 2167

Description: Theorem 19.11 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.) Remove dependencies on ax-5 1911, ax-6 1968, ax-7 2009, ax-10 2146, ax-12 2184. (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 2164	. . 3 ⊢ (∀𝑥∀𝑦 ¬ 𝜑 ↔ ∀𝑦∀𝑥 ¬ 𝜑)
2	1	notbii 320	. 2 ⊢ (¬ ∀𝑥∀𝑦 ¬ 𝜑 ↔ ¬ ∀𝑦∀𝑥 ¬ 𝜑)
3		2exnaln 1830	. 2 ⊢ (∃𝑥∃𝑦𝜑 ↔ ¬ ∀𝑥∀𝑦 ¬ 𝜑)
4		2exnaln 1830	. 2 ⊢ (∃𝑦∃𝑥𝜑 ↔ ¬ ∀𝑦∀𝑥 ¬ 𝜑)
5	2, 3, 4	3bitr4i 303	1 ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑦∃𝑥𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 206  ∀wal 1539  ∃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 2162

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

This theorem is referenced by:  excomim  2168  excom13  2169  exrot3  2170  eeor  2338  ee4anv  2355  ee4anvOLD  2356  2sb8ef  2360  sbel2x  2478  2sb8e  2534  2euexv  2631  2euex  2641  2eu4  2655  rexcom4  3263  rexcomf  3275  gencbvex  3499  euind  3682  sbccomlemOLD  3820  elvvv  5700  dmuni  5863  dm0rn0OLD  5874  dmcosseqOLDOLD  5929  cnvopab  6094  rncoOLD  6211  coass  6224  oprabidw  7389  oprabid  7390  dfoprab2  7416  uniuni  7707  opabex3d  7909  opabex3rd  7910  opabex3  7911  frxp  8068  domen  8898  xpassen  8999  scott0  9798  dfac5lem1  10033  dfac5lem4OLD  10038  cflemOLD  10156  ltexprlem1  10947  ltexprlem4  10950  fsumcom2  15697  fprodcom2  15907  gsumval3eu  19833  dprd2d2  19975  eldm3  35955  dfdm5  35967  dfrn5  35968  elfuns  36107  dfiota3  36115  brimg  36129  funpartlem  36136  bj-19.12  36962  bj-nnflemee  36964  bj-restuni  37302  sbccom2lem  38325  dmqsblocks  39112  diblsmopel  41431  dicelval3  41440  dihjatcclem4  41681  nfe2  42469  19.9dev  42471  nnoeomeqom  43554  pm11.6  44633  ax6e2ndeq  44800  e2ebind  44804  ax6e2ndeqVD  45149  e2ebindVD  45152  e2ebindALT  45169  ax6e2ndeqALT  45171  ich2ex  47714  ichexmpl1  47715  elsprel  47721  eliunxp2  48580