Theorem rexcom4 3256

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

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

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 3054

This theorem is referenced by:  rexcom4a  3259  2ex2rexrot  3265  reuind  3715  uni0b  4887  iuncom4  4953  dfiun2g  4983  iunn0  5019  iunxiun  5049  iinexg  5290  inuni  5292  iunopab  5506  xpiundi  5694  xpiundir  5695  cnvuni  5833  dmiun  5860  dmopab2rex  5864  elsnres  5976  rniun  6100  xpdifid  6121  imaco  6204  coiun  6209  abrexco  7184  imaiun  7185  fliftf  7256  imaeqsexvOLD  7304  imaeqexov  7591  fiun  7885  f1iun  7886  oprabrexex2  7920  releldm2  7985  oarec  8487  omeu  8510  eroveu  8746  brttrcl2  9629  dfac5lem2  10037  genpass  10922  supaddc  12110  supadd  12111  supmul1  12112  supmullem2  12114  supmul  12115  pceu  16776  4sqlem12  16886  mreiincl  17516  psgneu  19403  ntreq0  22980  unisngl  23430  metrest  24428  metuel2  24469  nosupno  27631  nosupfv  27634  noinfno  27646  noinffv  27649  elold  27801  lrrecfr  27873  sleadd1  27919  addsuniflem  27931  addsasslem1  27933  addsasslem2  27934  mulsuniflem  28075  addsdilem1  28077  addsdilem2  28078  mulsasslem1  28089  mulsasslem2  28090  renegscl  28385  readdscl  28386  remulscl  28389  istrkg2ld  28423  fpwrelmapffslem  32688  omssubaddlem  34266  omssubadd  34267  bnj906  34896  satfdm  35341  dmopab3rexdif  35377  rexxfr3dALT  35611  bj-elsngl  36941  bj-restn0  37063  ismblfin  37640  itg2addnclem3  37652  sdclem1  37722  eldmqs1cossres  38636  prter2  38859  lshpsmreu  39087  islpln5  39514  islvol5  39558  cdlemftr3  40544  mapdpglem3  41654  hdmapglem7a  41906  diophrex  42748  imaiun1  43624  coiun1  43625  grumnudlem  44258  upbdrech  45287  usgrgrtrirex  47933