Theorem excom 1741

Description: Theorem 19.11 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.) (Revised by Wolf Lammen to remove dependency on ax-11 1746 ax-6 1729 ax-9 1654 ax-8 1675 and ax-17 1616, 8-Jan-2018.)

Assertion

Ref	Expression
excom	⊢ (∃x∃yφ ↔ ∃y∃xφ)

Proof of Theorem excom

Step	Hyp	Ref	Expression
1		alcom 1737	. . . 4 ⊢ (∀x∀y ¬ φ ↔ ∀y∀x ¬ φ)
2	1	notbii 287	. . 3 ⊢ (¬ ∀x∀y ¬ φ ↔ ¬ ∀y∀x ¬ φ)
3		exnal 1574	. . 3 ⊢ (∃x ¬ ∀y ¬ φ ↔ ¬ ∀x∀y ¬ φ)
4		exnal 1574	. . 3 ⊢ (∃y ¬ ∀x ¬ φ ↔ ¬ ∀y∀x ¬ φ)
5	2, 3, 4	3bitr4i 268	. 2 ⊢ (∃x ¬ ∀y ¬ φ ↔ ∃y ¬ ∀x ¬ φ)
6		df-ex 1542	. . 3 ⊢ (∃yφ ↔ ¬ ∀y ¬ φ)
7	6	exbii 1582	. 2 ⊢ (∃x∃yφ ↔ ∃x ¬ ∀y ¬ φ)
8		df-ex 1542	. . 3 ⊢ (∃xφ ↔ ¬ ∀x ¬ φ)
9	8	exbii 1582	. 2 ⊢ (∃y∃xφ ↔ ∃y ¬ ∀x ¬ φ)
10	5, 7, 9	3bitr4i 268	1 ⊢ (∃x∃yφ ↔ ∃y∃xφ)

Syntax hints:  ¬ wn 3   ↔ wb 176  ∀wal 1540  ∃wex 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-7 1734

This theorem depends on definitions:  df-bi 177  df-ex 1542

This theorem is referenced by:  excomim  1742  excom13  1743  exrot3  1744  ee4anv  1915  2exsb  2132  2euex  2276  2eu1  2284  2eu4  2287  rexcomf  2771  gencbvex  2902  euind  3024  sbccomlem  3117  elpw11c  4148  elpw121c  4149  elpw131c  4150  elpw141c  4151  elpw151c  4152  elpw161c  4153  elpw171c  4154  elpw181c  4155  elpw191c  4156  elpw1101c  4157  elpw1111c  4158  eluni1g  4173  opkelcokg  4262  opkelimagekg  4272  dfimak2  4299  insklem  4305  ndisjrelk  4324  dfpw2  4328  dfaddc2  4382  dfnnc2  4396  elsuc  4414  nnsucelrlem1  4425  ltfinex  4465  ssfin  4471  eqpwrelk  4479  eqpw1relk  4480  ncfinraiselem2  4481  ncfinlowerlem1  4483  eqtfinrelk  4487  evenfinex  4504  oddfinex  4505  evenodddisjlem1  4516  nnadjoinlem1  4520  nnpweqlem1  4523  srelk  4525  sfintfinlem1  4532  tfinnnlem1  4534  spfinex  4538  vfinspsslem1  4551  dfop2lem1  4574  el1st  4730  setconslem1  4732  setconslem2  4733  setconslem3  4734  setconslem7  4738  df1st2  4739  dfswap2  4742  brswap2  4861  dmuni  4915  dm0rn0  4922  elimapw11c  4949  dmcoss  4972  dmcosseq  4974  rnuni  5039  rnco  5088  coass  5098  df2nd2  5112  cnvswap  5511  cnvsi  5519  dmsi  5520  oprabid  5551  dfoprab2  5559  brsnsi1  5776  brimage  5794  addcfnex  5825  pw1fnf1o  5856  ceexlem1  6174  ce0nnul  6178  el2c  6192  taddc  6230  tcfnex  6245  csucex  6260  nmembers1lem1  6269  nchoicelem11  6300  nchoicelem16  6305  fnfreclem3  6320