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  36177  dmopab3rexdif  36213  rexxfr3dALT  36447  bj-elsngl  37924  bj-restn0  38054  ismblfin  38623  itg2addnclem3  38635  sdclem1  38721  eldmqs1cossres  39720  prter2  39982  lshpsmreu  40210  islpln5  40636  islvol5  40680  cdlemftr3  41666  mapdpglem3  42776  hdmapglem7a  43028  diophrex  43830  imaiun1  44695  coiun1  44696  grumnudlem  45313  upbdrech  46365  usgrgrtrirex  49092