Theorem rexcom4 3289

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 1986	. 2 ⊢ (∃𝑥∃𝑦(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ ∃𝑦𝜑))
2		df-rex 3087	. . . 4 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
3	2	exbii 1880	. . 3 ⊢ (∃𝑦∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
4		excom 2198	. . 3 ⊢ (∃𝑦∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑥∃𝑦(𝑥 ∈ 𝐴 ∧ 𝜑))
5	3, 4	bitri 278	. 2 ⊢ (∃𝑦∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥∃𝑦(𝑥 ∈ 𝐴 ∧ 𝜑))
6		df-rex 3087	. 2 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ ∃𝑦𝜑))
7	1, 5, 6	3bitr4ri 307	1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦𝜑 ↔ ∃𝑦∃𝑥 ∈ 𝐴 𝜑)

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401  ∃wex 1811   ∈ wcel 2144  ∃wrex 3086

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-11 2193

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-rex 3087

This theorem is used by:  rexcom4a  3292  2ex2rexrot  3297  reuind  3710  uni0b  4893  iuncom4  4959  dfiun2g  4987  iunn0  5024  iunxiun  5056  iinexg  5308  inuni  5310  iunopab  5533  xpiundi  5721  xpiundir  5722  cnvuni  5867  dmiun  5894  dmopab2rex  5898  elsnres  6009  rniun  6138  xpdifid  6158  xpdifcnvepel  6159  imaco  6252  coiun  6258  abrexco  7248  imaiun  7249  fliftf  7323  imaeqexov  7659  fiun  7955  f1iun  7956  oprabrexex2  7990  releldm2  8054  oarec  8571  omeu  8594  eroveu  8834  brttrcl2  9716  dfac5lem2  10204  genpass  11095  supaddc  12285  supadd  12286  supmul1  12287  supmullem2  12289  supmul  12290  pceu  17025  4sqlem12  17135  mreiincl  17767  psgneu  19721  ntreq0  23396  unisngl  23847  metrest  24844  metuel2  24885  nosupno  28061  nosupfv  28064  noinfno  28076  noinffv  28079  elold  28246  lrrecfr  28330  leadds1  28376  addsuniflem  28388  addsasslem1  28390  addsasslem2  28391  mulsuniflem  28536  addsdilem1  28538  addsdilem2  28539  mulsasslem1  28550  mulsasslem2  28551  elreno2  28882  renegscl  28885  readdscl  28886  remulscl  28889  istrkg2ld  28923  fpwrelmapffslem  33367  omssubaddlem  34974  omssubadd  34975  bnj906  35603  satfdm  36203  dmopab3rexdif  36239  rexxfr3dALT  36473  bj-elsngl  37956  bj-restn0  38086  ismblfin  38655  itg2addnclem3  38667  sdclem1  38753  eldmqs1cossres  39752  prter2  40014  lshpsmreu  40242  islpln5  40668  islvol5  40712  cdlemftr3  41698  mapdpglem3  42808  hdmapglem7a  43060  diophrex  43862  imaiun1  44727  coiun1  44728  grumnudlem  45345  upbdrech  46397  usgrgrtrirex  49124