Theorem excom 2165

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 2144, ax-12 2180. (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 2162	. . 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 2160

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

This theorem is referenced by:  excomim  2166  excom13  2167  exrot3  2168  eeor  2334  ee4anv  2351  ee4anvOLD  2352  2sb8ef  2356  sbel2x  2474  2sb8e  2530  2euexv  2626  2euex  2636  2eu4  2650  rexcom4  3259  rexcomf  3271  gencbvex  3495  euind  3678  sbccomlemOLD  3816  elvvv  5687  dmuni  5849  dm0rn0OLD  5860  dmcosseqOLDOLD  5914  cnvopab  6079  rncoOLD  6195  coass  6208  oprabidw  7372  oprabid  7373  dfoprab2  7399  uniuni  7690  opabex3d  7892  opabex3rd  7893  opabex3  7894  frxp  8051  domen  8879  xpassen  8979  scott0  9774  dfac5lem1  10009  dfac5lem4OLD  10014  cflemOLD  10132  ltexprlem1  10922  ltexprlem4  10925  fsumcom2  15676  fprodcom2  15886  gsumval3eu  19811  dprd2d2  19953  eldm3  35797  dfdm5  35809  dfrn5  35810  elfuns  35949  dfiota3  35957  brimg  35971  funpartlem  35976  bj-19.12  36795  bj-nnflemee  36797  bj-restuni  37131  sbccom2lem  38164  dmqsblocks  38891  diblsmopel  41210  dicelval3  41219  dihjatcclem4  41460  19.9dev  42247  nnoeomeqom  43345  pm11.6  44425  ax6e2ndeq  44592  e2ebind  44596  ax6e2ndeqVD  44941  e2ebindVD  44944  e2ebindALT  44961  ax6e2ndeqALT  44963  ich2ex  47499  ichexmpl1  47500  elsprel  47506  eliunxp2  48365