Theorem rexcom4 3269

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 1954	. 2 ⊢ (∃𝑥∃𝑦(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ ∃𝑦𝜑))
2		df-rex 3061	. . . 4 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
3	2	exbii 1848	. . 3 ⊢ (∃𝑦∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
4		excom 2162	. . 3 ⊢ (∃𝑦∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑥∃𝑦(𝑥 ∈ 𝐴 ∧ 𝜑))
5	3, 4	bitri 275	. 2 ⊢ (∃𝑦∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥∃𝑦(𝑥 ∈ 𝐴 ∧ 𝜑))
6		df-rex 3061	. 2 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ ∃𝑦𝜑))
7	1, 5, 6	3bitr4ri 304	1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦𝜑 ↔ ∃𝑦∃𝑥 ∈ 𝐴 𝜑)

Syntax hints:   ↔ wb 206   ∧ wa 395  ∃wex 1779   ∈ wcel 2108  ∃wrex 3060

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 1910  ax-11 2157

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-rex 3061

This theorem is referenced by:  rexcomOLD  3272  rexcom4a  3273  2ex2rexrot  3279  reuind  3736  uni0b  4909  iuncom4  4976  dfiun2g  5006  dfiun2gOLD  5007  iunn0  5043  iunxiun  5073  iinexg  5318  inuni  5320  iunopab  5534  iunopabOLD  5535  xpiundi  5725  xpiundir  5726  cnvuni  5866  dmiun  5893  dmopab2rex  5897  elsnres  6008  rniun  6136  xpdifid  6157  imaco  6240  coiun  6245  abrexco  7236  imaiun  7237  fliftf  7308  imaeqsexvOLD  7356  imaeqexov  7645  fiun  7941  f1iun  7942  oprabrexex2  7977  releldm2  8042  oarec  8574  omeu  8597  eroveu  8826  brttrcl2  9728  dfac5lem2  10138  genpass  11023  supaddc  12209  supadd  12210  supmul1  12211  supmullem2  12213  supmul  12214  pceu  16866  4sqlem12  16976  mreiincl  17608  psgneu  19487  ntreq0  23015  unisngl  23465  metrest  24463  metuel2  24504  nosupno  27667  nosupfv  27670  noinfno  27682  noinffv  27685  elold  27833  lrrecfr  27902  sleadd1  27948  addsuniflem  27960  addsasslem1  27962  addsasslem2  27963  mulsuniflem  28104  addsdilem1  28106  addsdilem2  28107  mulsasslem1  28118  mulsasslem2  28119  renegscl  28401  readdscl  28402  remulscl  28405  istrkg2ld  28439  fpwrelmapffslem  32709  omssubaddlem  34331  omssubadd  34332  bnj906  34961  satfdm  35391  dmopab3rexdif  35427  rexxfr3dALT  35661  bj-elsngl  36986  bj-restn0  37108  ismblfin  37685  itg2addnclem3  37697  sdclem1  37767  eldmqs1cossres  38677  prter2  38899  lshpsmreu  39127  islpln5  39554  islvol5  39598  cdlemftr3  40584  mapdpglem3  41694  hdmapglem7a  41946  diophrex  42798  imaiun1  43675  coiun1  43676  grumnudlem  44309  upbdrech  45334  usgrgrtrirex  47962