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

Syntax hints:   ↔ wb 206   ∧ wa 395  ∃wex 1781   ∈ wcel 2114  ∃wrex 3062

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 1912  ax-11 2163

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-rex 3063

This theorem is referenced by:  rexcom4a  3268  2ex2rexrot  3273  reuind  3700  uni0b  4877  iuncom4  4943  dfiun2g  4973  iunn0  5010  iunxiun  5040  iinexg  5283  inuni  5285  iunopab  5505  xpiundi  5693  xpiundir  5694  cnvuni  5833  dmiun  5860  dmopab2rex  5864  elsnres  5978  rniun  6103  xpdifid  6124  imaco  6207  coiun  6213  abrexco  7190  imaiun  7191  fliftf  7261  imaeqsexvOLD  7309  imaeqexov  7596  fiun  7887  f1iun  7888  oprabrexex2  7922  releldm2  7987  oarec  8488  omeu  8511  eroveu  8750  brttrcl2  9624  dfac5lem2  10035  genpass  10921  supaddc  12112  supadd  12113  supmul1  12114  supmullem2  12116  supmul  12117  pceu  16806  4sqlem12  16916  mreiincl  17547  psgneu  19470  ntreq0  23051  unisngl  23501  metrest  24498  metuel2  24539  nosupno  27686  nosupfv  27689  noinfno  27701  noinffv  27704  elold  27870  lrrecfr  27954  leadds1  28000  addsuniflem  28012  addsasslem1  28014  addsasslem2  28015  mulsuniflem  28160  addsdilem1  28162  addsdilem2  28163  mulsasslem1  28174  mulsasslem2  28175  elreno2  28506  renegscl  28509  readdscl  28510  remulscl  28513  istrkg2ld  28547  fpwrelmapffslem  32825  omssubaddlem  34464  omssubadd  34465  bnj906  35093  satfdm  35572  dmopab3rexdif  35608  rexxfr3dALT  35842  bj-elsngl  37288  bj-restn0  37415  ismblfin  37993  itg2addnclem3  38005  sdclem1  38075  eldmqs1cossres  39076  prter2  39338  lshpsmreu  39566  islpln5  39992  islvol5  40036  cdlemftr3  41022  mapdpglem3  42132  hdmapglem7a  42384  diophrex  43218  imaiun1  44093  coiun1  44094  grumnudlem  44727  upbdrech  45753  usgrgrtrirex  48423