Theorem rexcom4 3294

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

Syntax hints:   ↔ wb 206   ∧ wa 395  ∃wex 1777   ∈ wcel 2108  ∃wrex 3076

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-11 2158

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-rex 3077

This theorem is referenced by:  rexcomOLD  3297  rexcom4a  3298  2ex2rexrot  3304  reuind  3775  uni0b  4957  iuncom4  5023  dfiun2g  5053  dfiun2gOLD  5054  iunn0  5090  iunxiun  5120  iinexg  5366  inuni  5368  iunopab  5578  iunopabOLD  5579  xpiundi  5770  xpiundir  5771  cnvuni  5911  dmiun  5938  dmopab2rex  5942  elsnres  6050  rniun  6179  xpdifid  6199  imaco  6282  coiun  6287  abrexco  7281  imaiun  7282  fliftf  7351  imaeqsexvOLD  7399  imaeqexov  7688  fiun  7983  f1iun  7984  oprabrexex2  8019  releldm2  8084  oarec  8618  omeu  8641  eroveu  8870  brttrcl2  9783  dfac5lem2  10193  genpass  11078  supaddc  12262  supadd  12263  supmul1  12264  supmullem2  12266  supmul  12267  pceu  16893  4sqlem12  17003  mreiincl  17654  psgneu  19548  ntreq0  23106  unisngl  23556  metrest  24558  metuel2  24599  nosupno  27766  nosupfv  27769  noinfno  27781  noinffv  27784  elold  27926  lrrecfr  27994  sleadd1  28040  addsuniflem  28052  addsasslem1  28054  addsasslem2  28055  mulsuniflem  28193  addsdilem1  28195  addsdilem2  28196  mulsasslem1  28207  mulsasslem2  28208  renegscl  28448  readdscl  28449  remulscl  28452  istrkg2ld  28486  fpwrelmapffslem  32746  omssubaddlem  34264  omssubadd  34265  bnj906  34906  satfdm  35337  dmopab3rexdif  35373  rexxfr3dALT  35607  bj-elsngl  36934  bj-restn0  37056  ismblfin  37621  itg2addnclem3  37633  sdclem1  37703  eldmqs1cossres  38615  prter2  38837  lshpsmreu  39065  islpln5  39492  islvol5  39536  cdlemftr3  40522  mapdpglem3  41632  hdmapglem7a  41884  diophrex  42731  imaiun1  43613  coiun1  43614  grumnudlem  44254  upbdrech  45220  usgrgrtrirex  47799