Theorem reeanv 3224

Description: Rearrange restricted existential quantifiers. (Contributed by NM, 9-May-1999.)

Assertion

Ref	Expression
reeanv	⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐵 𝜓))

Distinct variable groups:   𝜑,𝑦   𝜓,𝑥   𝑥,𝑦   𝑦,𝐴   𝑥,𝐵

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)   𝐴(𝑥)   𝐵(𝑦)

Proof of Theorem reeanv

Step	Hyp	Ref	Expression
1		exdistrv 1957	. 2 ⊢ (∃𝑥∃𝑦((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ (𝑦 ∈ 𝐵 ∧ 𝜓)) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ ∃𝑦(𝑦 ∈ 𝐵 ∧ 𝜓)))
2	1	reeanlem 3223	1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐵 𝜓))

Syntax hints:   ↔ wb 205   ∧ wa 394   ∈ wcel 2104  ∃wrex 3068

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 1911

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-ral 3060  df-rex 3069

This theorem is referenced by:  3reeanv  3225  2ralorOLD  3227  2reu4lem  4524  disjxiun  5144  fliftfun  7311  poseq  8146  soseq  8147  frrlem9  8281  tfrlem5  8382  uniinqs  8793  eroveu  8808  erovlem  8809  xpf1o  9141  unxpdomlem3  9254  unfiOLD  9315  finsschain  9361  dffi3  9428  ttrcltr  9713  rankxplim3  9878  xpnum  9948  kmlem9  10155  sornom  10274  fpwwe2lem11  10638  cnegex  11399  zaddcl  12606  rexanre  15297  o1lo1  15485  o1co  15534  rlimcn3  15538  o1of2  15561  lo1add  15575  lo1mul  15576  summo  15667  ntrivcvgmul  15852  prodmolem2  15883  prodmo  15884  dvds2lem  16216  odd2np1  16288  opoe  16310  omoe  16311  opeo  16312  omeo  16313  bezoutlem4  16488  gcddiv  16497  divgcdcoprmex  16607  pcqmul  16790  pcadd  16826  mul4sq  16891  4sqlem12  16893  prmgaplem7  16994  cyccom  19118  gaorber  19213  psgneu  19415  lsmsubm  19562  pj1eu  19605  efgredlem  19656  efgrelexlemb  19659  qusabl  19774  dprdsubg  19935  dvdsrtr  20259  unitgrp  20274  lss1d  20718  lsmspsn  20839  lspsolvlem  20900  lbsextlem2  20917  znfld  21335  cygznlem3  21344  psgnghm  21352  tgcl  22692  restbas  22882  ordtbas2  22915  uncmp  23127  txuni2  23289  txbas  23291  ptbasin  23301  txcnp  23344  txlly  23360  txnlly  23361  tx1stc  23374  tx2ndc  23375  fbasrn  23608  rnelfmlem  23676  fmfnfmlem3  23680  txflf  23730  qustgplem  23845  trust  23954  utoptop  23959  fmucndlem  24016  blin2  24155  metustto  24282  tgqioo  24536  minveclem3b  25176  pmltpc  25199  evthicc2  25209  ovolunlem2  25247  dyaddisj  25345  rolle  25742  dvcvx  25772  itgsubst  25801  plyadd  25966  plymul  25967  coeeu  25974  aalioulem6  26086  dchrptlem2  27004  lgsdchr  27094  mul2sq  27158  2sqlem5  27161  pntibnd  27332  pntlemp  27349  nosupprefixmo  27439  noinfprefixmo  27440  addsproplem2  27692  negsproplem2  27742  mulsuniflem  27843  precsexlem10  27901  cgraswap  28338  cgracom  28340  cgratr  28341  flatcgra  28342  dfcgra2  28348  acopyeu  28352  ax5seg  28463  axpasch  28466  axeuclid  28488  axcontlem4  28492  axcontlem9  28497  uhgr2edg  28732  2pthon3v  29464  pjhthmo  30822  superpos  31874  chirredi  31914  cdjreui  31952  cdj3i  31961  xrofsup  32247  archiabllem2c  32611  ccfldextdgrr  33035  ordtconnlem1  33202  dya2iocnrect  33578  txpconn  34521  cvmlift2lem10  34601  cvmlift3lem7  34614  msubco  34820  mclsppslem  34872  altopelaltxp  35252  funtransport  35307  btwnconn1lem13  35375  btwnconn1lem14  35376  segletr  35390  segleantisym  35391  funray  35416  funline  35418  tailfb  35565  mblfinlem3  36830  ismblfin  36832  itg2addnc  36845  ftc1anclem6  36869  heibor1lem  36980  crngohomfo  37177  ispridlc  37241  prter1  38052  hl2at  38579  cdlemn11pre  40384  dihord2pre  40399  dihord4  40432  dihmeetlem20N  40500  mapdpglem32  40879  diophin  41812  diophun  41813  iunrelexpuztr  42772  mullimc  44630  mullimcf  44637  addlimc  44662  fourierdlem42  45163  fourierdlem80  45200  sge0resplit  45420  hoiqssbllem3  45638