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 2182. (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  2336  ee4anv  2353  ee4anvOLD  2354  2sb8ef  2358  sbel2x  2476  2sb8e  2532  2euexv  2628  2euex  2638  2eu4  2652  rexcom4  3260  rexcomf  3272  gencbvex  3496  euind  3679  sbccomlemOLD  3817  elvvv  5697  dmuni  5860  dm0rn0OLD  5871  dmcosseqOLDOLD  5926  cnvopab  6091  rncoOLD  6208  coass  6221  oprabidw  7386  oprabid  7387  dfoprab2  7413  uniuni  7704  opabex3d  7906  opabex3rd  7907  opabex3  7908  frxp  8065  domen  8894  xpassen  8995  scott0  9790  dfac5lem1  10025  dfac5lem4OLD  10030  cflemOLD  10148  ltexprlem1  10938  ltexprlem4  10941  fsumcom2  15688  fprodcom2  15898  gsumval3eu  19824  dprd2d2  19966  eldm3  35877  dfdm5  35889  dfrn5  35890  elfuns  36029  dfiota3  36037  brimg  36051  funpartlem  36058  bj-19.12  36878  bj-nnflemee  36880  bj-restuni  37214  sbccom2lem  38237  dmqsblocks  39024  diblsmopel  41343  dicelval3  41352  dihjatcclem4  41593  nfe2  42382  19.9dev  42385  nnoeomeqom  43469  pm11.6  44549  ax6e2ndeq  44716  e2ebind  44720  ax6e2ndeqVD  45065  e2ebindVD  45068  e2ebindALT  45085  ax6e2ndeqALT  45087  ich2ex  47630  ichexmpl1  47631  elsprel  47637  eliunxp2  48496