Theorem rexcom4 3272

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

Syntax hints:   ↔ wb 206   ∧ wa 395  ∃wex 1778   ∈ wcel 2107  ∃wrex 3059

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-11 2156

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-rex 3060

This theorem is referenced by:  rexcomOLD  3275  rexcom4a  3276  2ex2rexrot  3282  reuind  3741  uni0b  4913  iuncom4  4980  dfiun2g  5010  dfiun2gOLD  5011  iunn0  5047  iunxiun  5077  iinexg  5328  inuni  5330  iunopab  5544  iunopabOLD  5545  xpiundi  5736  xpiundir  5737  cnvuni  5877  dmiun  5904  dmopab2rex  5908  elsnres  6019  rniun  6147  xpdifid  6168  imaco  6251  coiun  6256  abrexco  7246  imaiun  7247  fliftf  7317  imaeqsexvOLD  7365  imaeqexov  7653  fiun  7949  f1iun  7950  oprabrexex2  7985  releldm2  8050  oarec  8582  omeu  8605  eroveu  8834  brttrcl2  9736  dfac5lem2  10146  genpass  11031  supaddc  12217  supadd  12218  supmul1  12219  supmullem2  12221  supmul  12222  pceu  16866  4sqlem12  16976  mreiincl  17610  psgneu  19492  ntreq0  23031  unisngl  23481  metrest  24481  metuel2  24522  nosupno  27684  nosupfv  27687  noinfno  27699  noinffv  27702  elold  27844  lrrecfr  27912  sleadd1  27958  addsuniflem  27970  addsasslem1  27972  addsasslem2  27973  mulsuniflem  28111  addsdilem1  28113  addsdilem2  28114  mulsasslem1  28125  mulsasslem2  28126  renegscl  28366  readdscl  28367  remulscl  28370  istrkg2ld  28404  fpwrelmapffslem  32678  omssubaddlem  34260  omssubadd  34261  bnj906  34903  satfdm  35333  dmopab3rexdif  35369  rexxfr3dALT  35603  bj-elsngl  36928  bj-restn0  37050  ismblfin  37627  itg2addnclem3  37639  sdclem1  37709  eldmqs1cossres  38619  prter2  38841  lshpsmreu  39069  islpln5  39496  islvol5  39540  cdlemftr3  40526  mapdpglem3  41636  hdmapglem7a  41888  diophrex  42749  imaiun1  43626  coiun1  43627  grumnudlem  44261  upbdrech  45274  usgrgrtrirex  47875