Theorem rexcom4 3283

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		exdistr 1956	. 2 ⊢ (∃𝑥∃𝑦(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ ∃𝑦𝜑))
2		df-rex 3069	. . . 4 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
3	2	exbii 1848	. . 3 ⊢ (∃𝑦∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
4		excom 2160	. . 3 ⊢ (∃𝑦∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑥∃𝑦(𝑥 ∈ 𝐴 ∧ 𝜑))
5	3, 4	bitri 274	. 2 ⊢ (∃𝑦∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥∃𝑦(𝑥 ∈ 𝐴 ∧ 𝜑))
6		df-rex 3069	. 2 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ ∃𝑦𝜑))
7	1, 5, 6	3bitr4ri 303	1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦𝜑 ↔ ∃𝑦∃𝑥 ∈ 𝐴 𝜑)

Syntax hints:   ↔ wb 205   ∧ wa 394  ∃wex 1779   ∈ wcel 2104  ∃wrex 3068

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-11 2152

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-rex 3069

This theorem is referenced by:  rexcomOLD  3286  rexcom4a  3287  2ex2rexrot  3293  reuind  3748  uni0b  4936  iuncom4  5004  dfiun2g  5032  dfiun2gOLD  5033  iunn0  5069  iunxiun  5099  iinexg  5340  inuni  5342  iunopab  5558  iunopabOLD  5559  xpiundi  5745  xpiundir  5746  cnvuni  5885  dmiun  5912  dmopab2rex  5916  elsnres  6020  rniun  6146  xpdifid  6166  imaco  6249  coiun  6254  abrexco  7245  imaiun  7246  fliftf  7314  imaeqsexv  7362  imaeqexov  7647  fiun  7931  f1iun  7932  oprabrexex2  7967  releldm2  8031  oarec  8564  omeu  8587  eroveu  8808  brttrcl2  9711  dfac5lem2  10121  genpass  11006  supaddc  12185  supadd  12186  supmul1  12187  supmullem2  12189  supmul  12190  pceu  16783  4sqlem12  16893  mreiincl  17544  psgneu  19415  ntreq0  22801  unisngl  23251  metrest  24253  metuel2  24294  nosupno  27442  nosupfv  27445  noinfno  27457  noinffv  27460  elold  27601  lrrecfr  27665  sleadd1  27711  addsuniflem  27723  addsasslem1  27725  addsasslem2  27726  mulsuniflem  27843  addsdilem1  27845  addsdilem2  27846  mulsasslem1  27857  mulsasslem2  27858  istrkg2ld  27978  fpwrelmapffslem  32224  omssubaddlem  33596  omssubadd  33597  bnj906  34239  satfdm  34658  dmopab3rexdif  34694  bj-elsngl  36152  bj-restn0  36274  ismblfin  36832  itg2addnclem3  36844  sdclem1  36914  eldmqs1cossres  37832  prter2  38054  lshpsmreu  38282  islpln5  38709  islvol5  38753  cdlemftr3  39739  mapdpglem3  40849  hdmapglem7a  41101  diophrex  41815  imaiun1  42704  coiun1  42705  grumnudlem  43346  upbdrech  44313