Theorem reeanv 3205

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2113  ∃wrex 3057

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-ral 3049  df-rex 3058

This theorem is referenced by:  3reeanv  3206  2reu4lem  4471  disjxiun  5090  fliftfun  7252  poseq  8094  soseq  8095  frrlem9  8230  tfrlem5  8305  uniinqs  8727  eroveu  8742  erovlem  8743  xpf1o  9059  unxpdomlem3  9149  finsschain  9250  dffi3  9322  ttrcltr  9613  rankxplim3  9781  xpnum  9851  kmlem9  10057  sornom  10175  fpwwe2lem11  10539  cnegex  11301  zaddcl  12518  rexanre  15256  o1lo1  15446  o1co  15495  rlimcn3  15499  o1of2  15522  lo1add  15536  lo1mul  15537  summo  15626  ntrivcvgmul  15811  prodmolem2  15844  prodmo  15845  dvds2lem  16181  odd2np1  16254  opoe  16276  omoe  16277  opeo  16278  omeo  16279  bezoutlem4  16455  gcddiv  16464  divgcdcoprmex  16579  pcqmul  16767  pcadd  16803  mul4sq  16868  4sqlem12  16870  prmgaplem7  16971  cyccom  19117  gaorber  19222  psgneu  19420  lsmsubm  19567  pj1eu  19610  efgredlem  19661  efgrelexlemb  19664  qusabl  19779  dprdsubg  19940  dvdsrtr  20288  unitgrp  20303  lss1d  20898  lsmspsn  21020  lspsolvlem  21081  lbsextlem2  21098  znfld  21499  cygznlem3  21508  psgnghm  21519  tgcl  22885  restbas  23074  ordtbas2  23107  uncmp  23319  txuni2  23481  txbas  23483  ptbasin  23493  txcnp  23536  txlly  23552  txnlly  23553  tx1stc  23566  tx2ndc  23567  fbasrn  23800  rnelfmlem  23868  fmfnfmlem3  23872  txflf  23922  qustgplem  24037  trust  24145  utoptop  24150  fmucndlem  24206  blin2  24345  metustto  24469  tgqioo  24716  minveclem3b  25356  pmltpc  25379  evthicc2  25389  ovolunlem2  25427  dyaddisj  25525  rolle  25922  dvcvx  25953  itgsubst  25984  plyadd  26150  plymul  26151  coeeu  26158  aalioulem6  26273  dchrptlem2  27204  lgsdchr  27294  mul2sq  27358  2sqlem5  27361  pntibnd  27532  pntlemp  27549  nosupprefixmo  27640  noinfprefixmo  27641  addsproplem2  27914  negsproplem2  27972  mulsuniflem  28089  precsexlem10  28155  zaddscl  28319  zmulscld  28322  zseo  28346  zs12addscl  28388  recut  28399  readdscl  28402  remulscl  28405  cgraswap  28799  cgracom  28801  cgratr  28802  flatcgra  28803  dfcgra2  28809  acopyeu  28813  ax5seg  28918  axpasch  28921  axeuclid  28943  axcontlem4  28947  axcontlem9  28952  uhgr2edg  29188  2pthon3v  29923  pjhthmo  31284  superpos  32336  chirredi  32376  cdjreui  32414  cdj3i  32423  xrofsup  32754  archiabllem2c  33171  ccfldextdgrr  33706  ordtconnlem1  33958  dya2iocnrect  34315  txpconn  35297  cvmlift2lem10  35377  cvmlift3lem7  35390  msubco  35596  mclsppslem  35648  altopelaltxp  36041  funtransport  36096  btwnconn1lem13  36164  btwnconn1lem14  36165  segletr  36179  segleantisym  36180  funray  36205  funline  36207  tailfb  36442  mblfinlem3  37719  ismblfin  37721  itg2addnc  37734  ftc1anclem6  37758  heibor1lem  37869  crngohomfo  38066  ispridlc  38130  prter1  38998  hl2at  39524  cdlemn11pre  41329  dihord2pre  41344  dihord4  41377  dihmeetlem20N  41445  mapdpglem32  41824  diophin  42889  diophun  42890  iunrelexpuztr  43836  mullimc  45740  mullimcf  45747  addlimc  45770  fourierdlem42  46271  fourierdlem80  46308  sge0resplit  46528  hoiqssbllem3  46746