Theorem rexcom4 3265

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

Syntax hints:   ↔ wb 206   ∧ wa 395  ∃wex 1779   ∈ wcel 2109  ∃wrex 3054

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 2158

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

This theorem is referenced by:  rexcomOLD  3268  rexcom4a  3269  2ex2rexrot  3275  reuind  3727  uni0b  4900  iuncom4  4967  dfiun2g  4997  dfiun2gOLD  4998  iunn0  5034  iunxiun  5064  iinexg  5306  inuni  5308  iunopab  5522  iunopabOLD  5523  xpiundi  5712  xpiundir  5713  cnvuni  5853  dmiun  5880  dmopab2rex  5884  elsnres  5995  rniun  6123  xpdifid  6144  imaco  6227  coiun  6232  abrexco  7221  imaiun  7222  fliftf  7293  imaeqsexvOLD  7341  imaeqexov  7630  fiun  7924  f1iun  7925  oprabrexex2  7960  releldm2  8025  oarec  8529  omeu  8552  eroveu  8788  brttrcl2  9674  dfac5lem2  10084  genpass  10969  supaddc  12157  supadd  12158  supmul1  12159  supmullem2  12161  supmul  12162  pceu  16824  4sqlem12  16934  mreiincl  17564  psgneu  19443  ntreq0  22971  unisngl  23421  metrest  24419  metuel2  24460  nosupno  27622  nosupfv  27625  noinfno  27637  noinffv  27640  elold  27788  lrrecfr  27857  sleadd1  27903  addsuniflem  27915  addsasslem1  27917  addsasslem2  27918  mulsuniflem  28059  addsdilem1  28061  addsdilem2  28062  mulsasslem1  28073  mulsasslem2  28074  renegscl  28356  readdscl  28357  remulscl  28360  istrkg2ld  28394  fpwrelmapffslem  32662  omssubaddlem  34297  omssubadd  34298  bnj906  34927  satfdm  35363  dmopab3rexdif  35399  rexxfr3dALT  35633  bj-elsngl  36963  bj-restn0  37085  ismblfin  37662  itg2addnclem3  37674  sdclem1  37744  eldmqs1cossres  38658  prter2  38881  lshpsmreu  39109  islpln5  39536  islvol5  39580  cdlemftr3  40566  mapdpglem3  41676  hdmapglem7a  41928  diophrex  42770  imaiun1  43647  coiun1  43648  grumnudlem  44281  upbdrech  45310  usgrgrtrirex  47953