Theorem reeanv 3295

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 1960	. 2 ⊢ (∃𝑥∃𝑦((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ (𝑦 ∈ 𝐵 ∧ 𝜓)) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ ∃𝑦(𝑦 ∈ 𝐵 ∧ 𝜓)))
2	1	reeanlem 3293	1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐵 𝜓))

Syntax hints:   ↔ wb 205   ∧ wa 396   ∈ wcel 2107  ∃wrex 3066

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-ral 3070  df-rex 3071

This theorem is referenced by:  3reeanv  3296  2ralorOLD  3298  2reu4lem  4457  disjxiun  5072  fliftfun  7192  frrlem9  8119  tfrlem5  8220  uniinqs  8595  eroveu  8610  erovlem  8611  xpf1o  8935  unxpdomlem3  9038  unfiOLD  9090  finsschain  9135  dffi3  9199  ttrcltr  9483  rankxplim3  9648  xpnum  9718  kmlem9  9923  sornom  10042  fpwwe2lem11  10406  cnegex  11165  zaddcl  12369  rexanre  15067  o1lo1  15255  o1co  15304  rlimcn3  15308  o1of2  15331  lo1add  15345  lo1mul  15346  summo  15438  ntrivcvgmul  15623  prodmolem2  15654  prodmo  15655  dvds2lem  15987  odd2np1  16059  opoe  16081  omoe  16082  opeo  16083  omeo  16084  bezoutlem4  16259  gcddiv  16268  divgcdcoprmex  16380  pcqmul  16563  pcadd  16599  mul4sq  16664  4sqlem12  16666  prmgaplem7  16767  cyccom  18831  gaorber  18923  psgneu  19123  lsmsubm  19267  pj1eu  19311  efgredlem  19362  efgrelexlemb  19365  qusabl  19475  cygablOLD  19501  dprdsubg  19636  dvdsrtr  19903  unitgrp  19918  lss1d  20234  lsmspsn  20355  lspsolvlem  20413  lbsextlem2  20430  znfld  20777  cygznlem3  20786  psgnghm  20794  tgcl  22128  restbas  22318  ordtbas2  22351  uncmp  22563  txuni2  22725  txbas  22727  ptbasin  22737  txcnp  22780  txlly  22796  txnlly  22797  tx1stc  22810  tx2ndc  22811  fbasrn  23044  rnelfmlem  23112  fmfnfmlem3  23116  txflf  23166  qustgplem  23281  trust  23390  utoptop  23395  fmucndlem  23452  blin2  23591  metustto  23718  tgqioo  23972  minveclem3b  24601  pmltpc  24623  evthicc2  24633  ovolunlem2  24671  dyaddisj  24769  rolle  25163  dvcvx  25193  itgsubst  25222  plyadd  25387  plymul  25388  coeeu  25395  aalioulem6  25506  dchrptlem2  26422  lgsdchr  26512  mul2sq  26576  2sqlem5  26579  pntibnd  26750  pntlemp  26767  cgraswap  27190  cgracom  27192  cgratr  27193  flatcgra  27194  dfcgra2  27200  acopyeu  27204  ax5seg  27315  axpasch  27318  axeuclid  27340  axcontlem4  27344  axcontlem9  27349  uhgr2edg  27584  2pthon3v  28317  pjhthmo  29673  superpos  30725  chirredi  30765  cdjreui  30803  cdj3i  30812  xrofsup  31099  archiabllem2c  31458  ccfldextdgrr  31751  ordtconnlem1  31883  dya2iocnrect  32257  txpconn  33203  cvmlift2lem10  33283  cvmlift3lem7  33296  msubco  33502  mclsppslem  33554  poseq  33811  soseq  33812  nosupprefixmo  33912  noinfprefixmo  33913  altopelaltxp  34287  funtransport  34342  btwnconn1lem13  34410  btwnconn1lem14  34411  segletr  34425  segleantisym  34426  funray  34451  funline  34453  tailfb  34575  mblfinlem3  35825  ismblfin  35827  itg2addnc  35840  ftc1anclem6  35864  heibor1lem  35976  crngohomfo  36173  ispridlc  36237  prter1  36900  hl2at  37426  cdlemn11pre  39231  dihord2pre  39246  dihord4  39279  dihmeetlem20N  39347  mapdpglem32  39726  diophin  40601  diophun  40602  iunrelexpuztr  41334  mullimc  43164  mullimcf  43171  addlimc  43196  fourierdlem42  43697  fourierdlem80  43734  sge0resplit  43951  hoiqssbllem3  44169