MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  reeanv Structured version   Visualization version   GIF version

Theorem reeanv 3216
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
StepHypRef Expression
1 exdistrv 1960 . 2 (∃𝑥𝑦((𝑥𝐴𝜑) ∧ (𝑦𝐵𝜓)) ↔ (∃𝑥(𝑥𝐴𝜑) ∧ ∃𝑦(𝑦𝐵𝜓)))
21reeanlem 3215 1 (∃𝑥𝐴𝑦𝐵 (𝜑𝜓) ↔ (∃𝑥𝐴 𝜑 ∧ ∃𝑦𝐵 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 397  wcel 2107  wrex 3070
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 398  df-ex 1783  df-ral 3062  df-rex 3071
This theorem is referenced by:  3reeanv  3217  2ralorOLD  3219  2reu4lem  4484  disjxiun  5103  fliftfun  7258  poseq  8091  soseq  8092  frrlem9  8226  tfrlem5  8327  uniinqs  8739  eroveu  8754  erovlem  8755  xpf1o  9086  unxpdomlem3  9199  unfiOLD  9260  finsschain  9306  dffi3  9372  ttrcltr  9657  rankxplim3  9822  xpnum  9892  kmlem9  10099  sornom  10218  fpwwe2lem11  10582  cnegex  11341  zaddcl  12548  rexanre  15237  o1lo1  15425  o1co  15474  rlimcn3  15478  o1of2  15501  lo1add  15515  lo1mul  15516  summo  15607  ntrivcvgmul  15792  prodmolem2  15823  prodmo  15824  dvds2lem  16156  odd2np1  16228  opoe  16250  omoe  16251  opeo  16252  omeo  16253  bezoutlem4  16428  gcddiv  16437  divgcdcoprmex  16547  pcqmul  16730  pcadd  16766  mul4sq  16831  4sqlem12  16833  prmgaplem7  16934  cyccom  19001  gaorber  19093  psgneu  19293  lsmsubm  19440  pj1eu  19483  efgredlem  19534  efgrelexlemb  19537  qusabl  19648  dprdsubg  19808  dvdsrtr  20086  unitgrp  20101  lss1d  20439  lsmspsn  20560  lspsolvlem  20619  lbsextlem2  20636  znfld  20983  cygznlem3  20992  psgnghm  21000  tgcl  22335  restbas  22525  ordtbas2  22558  uncmp  22770  txuni2  22932  txbas  22934  ptbasin  22944  txcnp  22987  txlly  23003  txnlly  23004  tx1stc  23017  tx2ndc  23018  fbasrn  23251  rnelfmlem  23319  fmfnfmlem3  23323  txflf  23373  qustgplem  23488  trust  23597  utoptop  23602  fmucndlem  23659  blin2  23798  metustto  23925  tgqioo  24179  minveclem3b  24808  pmltpc  24830  evthicc2  24840  ovolunlem2  24878  dyaddisj  24976  rolle  25370  dvcvx  25400  itgsubst  25429  plyadd  25594  plymul  25595  coeeu  25602  aalioulem6  25713  dchrptlem2  26629  lgsdchr  26719  mul2sq  26783  2sqlem5  26786  pntibnd  26957  pntlemp  26974  nosupprefixmo  27064  noinfprefixmo  27065  addsproplem2  27304  negsproplem2  27349  cgraswap  27804  cgracom  27806  cgratr  27807  flatcgra  27808  dfcgra2  27814  acopyeu  27818  ax5seg  27929  axpasch  27932  axeuclid  27954  axcontlem4  27958  axcontlem9  27963  uhgr2edg  28198  2pthon3v  28930  pjhthmo  30286  superpos  31338  chirredi  31378  cdjreui  31416  cdj3i  31425  xrofsup  31719  archiabllem2c  32080  ccfldextdgrr  32413  ordtconnlem1  32562  dya2iocnrect  32938  txpconn  33883  cvmlift2lem10  33963  cvmlift3lem7  33976  msubco  34182  mclsppslem  34234  altopelaltxp  34607  funtransport  34662  btwnconn1lem13  34730  btwnconn1lem14  34731  segletr  34745  segleantisym  34746  funray  34771  funline  34773  tailfb  34895  mblfinlem3  36163  ismblfin  36165  itg2addnc  36178  ftc1anclem6  36202  heibor1lem  36314  crngohomfo  36511  ispridlc  36575  prter1  37387  hl2at  37914  cdlemn11pre  39719  dihord2pre  39734  dihord4  39767  dihmeetlem20N  39835  mapdpglem32  40214  diophin  41138  diophun  41139  iunrelexpuztr  42079  mullimc  43943  mullimcf  43950  addlimc  43975  fourierdlem42  44476  fourierdlem80  44513  sge0resplit  44733  hoiqssbllem3  44951
  Copyright terms: Public domain W3C validator