Theorem reeanv 3369

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 3367	1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐵 𝜓))

Syntax hints:   ↔ wb 208   ∧ wa 398   ∈ wcel 2114  ∃wrex 3141

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 209  df-an 399  df-ex 1781  df-ral 3145  df-rex 3146

This theorem is referenced by:  3reeanv  3370  2ralor  3371  2reu4lem  4467  disjxiun  5065  fliftfun  7067  tfrlem5  8018  uniinqs  8379  eroveu  8394  erovlem  8395  xpf1o  8681  unxpdomlem3  8726  unfi  8787  finsschain  8833  dffi3  8897  rankxplim3  9312  xpnum  9382  kmlem9  9586  sornom  9701  fpwwe2lem12  10065  cnegex  10823  zaddcl  12025  rexanre  14708  o1lo1  14896  o1co  14945  rlimcn2  14949  o1of2  14971  lo1add  14985  lo1mul  14986  summo  15076  ntrivcvgmul  15260  prodmolem2  15291  prodmo  15292  dvds2lem  15624  odd2np1  15692  opoe  15714  omoe  15715  opeo  15716  omeo  15717  bezoutlem4  15892  gcddiv  15901  divgcdcoprmex  16012  pcqmul  16192  pcadd  16227  mul4sq  16292  4sqlem12  16294  prmgaplem7  16395  cyccom  18348  gaorber  18440  psgneu  18636  lsmsubm  18780  pj1eu  18824  efgredlem  18875  efgrelexlemb  18878  qusabl  18987  cygablOLD  19013  dprdsubg  19148  dvdsrtr  19404  unitgrp  19419  lss1d  19737  lsmspsn  19858  lspsolvlem  19916  lbsextlem2  19933  znfld  20709  cygznlem3  20718  psgnghm  20726  tgcl  21579  restbas  21768  ordtbas2  21801  uncmp  22013  txuni2  22175  txbas  22177  ptbasin  22187  txcnp  22230  txlly  22246  txnlly  22247  tx1stc  22260  tx2ndc  22261  fbasrn  22494  rnelfmlem  22562  fmfnfmlem3  22566  txflf  22616  qustgplem  22731  trust  22840  utoptop  22845  fmucndlem  22902  blin2  23041  metustto  23165  tgqioo  23410  minveclem3b  24033  pmltpc  24053  evthicc2  24063  ovolunlem2  24101  dyaddisj  24199  rolle  24589  dvcvx  24619  itgsubst  24648  plyadd  24809  plymul  24810  coeeu  24817  aalioulem6  24928  dchrptlem2  25843  lgsdchr  25933  mul2sq  25997  2sqlem5  26000  pntibnd  26171  pntlemp  26188  cgraswap  26608  cgracom  26610  cgratr  26611  flatcgra  26612  dfcgra2  26618  acopyeu  26622  ax5seg  26726  axpasch  26729  axeuclid  26751  axcontlem4  26755  axcontlem9  26760  uhgr2edg  26992  2pthon3v  27724  pjhthmo  29081  superpos  30133  chirredi  30173  cdjreui  30211  cdj3i  30220  xrofsup  30494  archiabllem2c  30826  ccfldextdgrr  31059  ordtconnlem1  31169  dya2iocnrect  31541  txpconn  32481  cvmlift2lem10  32561  cvmlift3lem7  32574  msubco  32780  mclsppslem  32832  poseq  33097  soseq  33098  frrlem9  33133  noprefixmo  33204  altopelaltxp  33439  funtransport  33494  btwnconn1lem13  33562  btwnconn1lem14  33563  segletr  33577  segleantisym  33578  funray  33603  funline  33605  tailfb  33727  mblfinlem3  34933  ismblfin  34935  itg2addnc  34948  ftc1anclem6  34974  heibor1lem  35089  crngohomfo  35286  ispridlc  35350  prter1  36017  hl2at  36543  cdlemn11pre  38348  dihord2pre  38363  dihord4  38396  dihmeetlem20N  38464  mapdpglem32  38843  diophin  39376  diophun  39377  iunrelexpuztr  40071  mullimc  41904  mullimcf  41911  addlimc  41936  fourierdlem42  42441  fourierdlem80  42478  sge0resplit  42695  hoiqssbllem3  42913