Theorem rexcom4 3251

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 3146	. 2 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ ∃𝑦𝜑))
2		19.42v 1954	. . . . 5 ⊢ (∃𝑦(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑥 ∈ 𝐴 ∧ ∃𝑦𝜑))
3	2	bicomi 226	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ∧ ∃𝑦𝜑) ↔ ∃𝑦(𝑥 ∈ 𝐴 ∧ 𝜑))
4	3	exbii 1848	. . 3 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ ∃𝑦𝜑) ↔ ∃𝑥∃𝑦(𝑥 ∈ 𝐴 ∧ 𝜑))
5		excom 2169	. . . 4 ⊢ (∃𝑥∃𝑦(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑦∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
6		df-rex 3146	. . . . . 6 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
7	6	bicomi 226	. . . . 5 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑥 ∈ 𝐴 𝜑)
8	7	exbii 1848	. . . 4 ⊢ (∃𝑦∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑦∃𝑥 ∈ 𝐴 𝜑)
9	5, 8	bitri 277	. . 3 ⊢ (∃𝑥∃𝑦(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑦∃𝑥 ∈ 𝐴 𝜑)
10	4, 9	bitri 277	. 2 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ ∃𝑦𝜑) ↔ ∃𝑦∃𝑥 ∈ 𝐴 𝜑)
11	1, 10	bitri 277	1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦𝜑 ↔ ∃𝑦∃𝑥 ∈ 𝐴 𝜑)

Syntax hints:   ↔ wb 208   ∧ wa 398  ∃wex 1780   ∈ wcel 2114  ∃wrex 3141

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-5 1911  ax-11 2161

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-rex 3146

This theorem is referenced by:  2ex2rexrot  3252  rexcom4a  3253  rexcom  3357  reuind  3746  uni0b  4866  iuncom4  4929  dfiun2g  4957  dfiun2gOLD  4958  iunn0  4991  iunxiun  5021  iinexg  5246  inuni  5248  iunopab  5448  xpiundi  5624  xpiundir  5625  cnvuni  5759  dmiun  5784  dmopab2rex  5788  elsnres  5894  rniun  6008  xpdifid  6027  imaco  6106  coiun  6111  abrexco  7005  imaiun  7006  fliftf  7070  fiun  7646  f1iun  7647  oprabrexex2  7681  releldm2  7744  oarec  8190  omeu  8213  eroveu  8394  dfac5lem2  9552  genpass  10433  supaddc  11610  supadd  11611  supmul1  11612  supmullem2  11614  supmul  11615  pceu  16185  4sqlem12  16294  mreiincl  16869  psgneu  18636  ntreq0  21687  unisngl  22137  metrest  23136  metuel2  23177  istrkg2ld  26248  fpwrelmapffslem  30470  omssubaddlem  31559  omssubadd  31560  bnj906  32204  satfdm  32618  dmopab3rexdif  32654  nosupno  33205  nosupfv  33208  bj-elsngl  34282  bj-restn0  34383  ismblfin  34935  itg2addnclem3  34947  sdclem1  35020  eldmqs1cossres  35895  prter2  36019  lshpsmreu  36247  islpln5  36673  islvol5  36717  cdlemftr3  37703  mapdpglem3  38813  hdmapglem7a  39065  diophrex  39379  imaiun1  40003  coiun1  40004  grumnudlem  40628  upbdrech  41579