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  2770  gencbvex  2901  euind  3023  sbccomlem  3116  elpw11c  4147  elpw121c  4148  elpw131c  4149  elpw141c  4150  elpw151c  4151  elpw161c  4152  elpw171c  4153  elpw181c  4154  elpw191c  4155  elpw1101c  4156  elpw1111c  4157  eluni1g  4172  opkelcokg  4261  opkelimagekg  4271  dfimak2  4298  insklem  4304  ndisjrelk  4323  dfpw2  4327  dfaddc2  4381  dfnnc2  4395  elsuc  4413  nnsucelrlem1  4424  ltfinex  4464  ssfin  4470  eqpwrelk  4478  eqpw1relk  4479  ncfinraiselem2  4480  ncfinlowerlem1  4482  eqtfinrelk  4486  evenfinex  4503  oddfinex  4504  evenodddisjlem1  4515  nnadjoinlem1  4519  nnpweqlem1  4522  srelk  4524  sfintfinlem1  4531  tfinnnlem1  4533  spfinex  4537  vfinspsslem1  4550  dfop2lem1  4573  el1st  4729  setconslem1  4731  setconslem2  4732  setconslem3  4733  setconslem7  4737  df1st2  4738  dfswap2  4741  brswap2  4860  dmuni  4914  dm0rn0  4921  elimapw11c  4948  dmcoss  4971  dmcosseq  4973  rnuni  5038  rnco  5087  coass  5097  df2nd2  5111  cnvswap  5510  cnvsi  5518  dmsi  5519  oprabid  5550  dfoprab2  5558  brsnsi1  5775  brimage  5793  addcfnex  5824  pw1fnf1o  5855  ceexlem1  6173  ce0nnul  6177  el2c  6191  taddc  6229  tcfnex  6244  csucex  6259  nmembers1lem1  6268  nchoicelem11  6299  nchoicelem16  6304  fnfreclem3  6319