Theorem rexcom4 3212

Description: Commutation of restricted and unrestricted existential quantifiers. (Contributed by NM, 12-Apr-2004.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) Reduce axiom dependencies. (Revised by BJ, 13-Jun-2019.)

Assertion

Ref	Expression
rexcom4	⊢ (∃𝑥 ∈ 𝐴 ∃𝑦𝜑 ↔ ∃𝑦∃𝑥 ∈ 𝐴 𝜑)

Distinct variable groups:   𝑥,𝑦   𝑦,𝐴

Allowed substitution hints:   𝜑(𝑥,𝑦)   𝐴(𝑥)

Proof of Theorem rexcom4

Step	Hyp	Ref	Expression
1		df-rex 3112	. 2 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ ∃𝑦𝜑))
2		19.42v 1954	. . . . 5 ⊢ (∃𝑦(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑥 ∈ 𝐴 ∧ ∃𝑦𝜑))
3	2	bicomi 227	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ∧ ∃𝑦𝜑) ↔ ∃𝑦(𝑥 ∈ 𝐴 ∧ 𝜑))
4	3	exbii 1849	. . 3 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ ∃𝑦𝜑) ↔ ∃𝑥∃𝑦(𝑥 ∈ 𝐴 ∧ 𝜑))
5		excom 2166	. . . 4 ⊢ (∃𝑥∃𝑦(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑦∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
6		df-rex 3112	. . . . . 6 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
7	6	bicomi 227	. . . . 5 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑥 ∈ 𝐴 𝜑)
8	7	exbii 1849	. . . 4 ⊢ (∃𝑦∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑦∃𝑥 ∈ 𝐴 𝜑)
9	5, 8	bitri 278	. . 3 ⊢ (∃𝑥∃𝑦(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑦∃𝑥 ∈ 𝐴 𝜑)
10	4, 9	bitri 278	. 2 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ ∃𝑦𝜑) ↔ ∃𝑦∃𝑥 ∈ 𝐴 𝜑)
11	1, 10	bitri 278	1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦𝜑 ↔ ∃𝑦∃𝑥 ∈ 𝐴 𝜑)

Syntax hints:   ↔ wb 209   ∧ wa 399  ∃wex 1781   ∈ wcel 2111  ∃wrex 3107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-11 2158

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-rex 3112

This theorem is referenced by:  2ex2rexrot  3213  rexcom4a  3214  rexcom  3308  reuind  3692  uni0b  4826  iuncom4  4889  dfiun2g  4917  dfiun2gOLD  4918  iunn0  4952  iunxiun  4982  iinexg  5208  inuni  5210  iunopab  5411  xpiundi  5586  xpiundir  5587  cnvuni  5721  dmiun  5746  dmopab2rex  5750  elsnres  5858  rniun  5973  xpdifid  5992  imaco  6071  coiun  6076  abrexco  6981  imaiun  6982  fliftf  7047  fiun  7626  f1iun  7627  oprabrexex2  7661  releldm2  7724  oarec  8171  omeu  8194  eroveu  8375  dfac5lem2  9535  genpass  10420  supaddc  11595  supadd  11596  supmul1  11597  supmullem2  11599  supmul  11600  pceu  16173  4sqlem12  16282  mreiincl  16859  psgneu  18626  ntreq0  21682  unisngl  22132  metrest  23131  metuel2  23172  istrkg2ld  26254  fpwrelmapffslem  30494  omssubaddlem  31667  omssubadd  31668  bnj906  32312  satfdm  32729  dmopab3rexdif  32765  nosupno  33316  nosupfv  33319  bj-elsngl  34404  bj-restn0  34505  ismblfin  35098  itg2addnclem3  35110  sdclem1  35181  eldmqs1cossres  36053  prter2  36177  lshpsmreu  36405  islpln5  36831  islvol5  36875  cdlemftr3  37861  mapdpglem3  38971  hdmapglem7a  39223  diophrex  39716  imaiun1  40352  coiun1  40353  grumnudlem  40993  upbdrech  41937