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

Theorem reeanv 3372
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 1949 . 2 (∃𝑥𝑦((𝑥𝐴𝜑) ∧ (𝑦𝐵𝜓)) ↔ (∃𝑥(𝑥𝐴𝜑) ∧ ∃𝑦(𝑦𝐵𝜓)))
21reeanlem 3370 1 (∃𝑥𝐴𝑦𝐵 (𝜑𝜓) ↔ (∃𝑥𝐴 𝜑 ∧ ∃𝑦𝐵 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 207  wa 396  wcel 2106  wrex 3143
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1774  df-ral 3147  df-rex 3148
This theorem is referenced by:  3reeanv  3373  2ralor  3374  2reu4lem  4467  disjxiun  5059  fliftfun  7060  tfrlem5  8010  uniinqs  8370  eroveu  8385  erovlem  8386  xpf1o  8671  unxpdomlem3  8716  unfi  8777  finsschain  8823  dffi3  8887  rankxplim3  9302  xpnum  9372  kmlem9  9576  sornom  9691  fpwwe2lem12  10055  cnegex  10813  zaddcl  12014  rexanre  14699  o1lo1  14887  o1co  14936  rlimcn2  14940  o1of2  14962  lo1add  14976  lo1mul  14977  summo  15066  ntrivcvgmul  15250  prodmolem2  15281  prodmo  15282  dvds2lem  15614  odd2np1  15682  opoe  15704  omoe  15705  opeo  15706  omeo  15707  bezoutlem4  15882  gcddiv  15891  divgcdcoprmex  16002  pcqmul  16182  pcadd  16217  mul4sq  16282  4sqlem12  16284  prmgaplem7  16385  cyccom  18278  gaorber  18370  psgneu  18556  lsmsubm  18700  pj1eu  18744  efgredlem  18795  efgrelexlemb  18798  qusabl  18907  cygablOLD  18933  dprdsubg  19068  dvdsrtr  19324  unitgrp  19339  lss1d  19657  lsmspsn  19778  lspsolvlem  19836  lbsextlem2  19853  znfld  20623  cygznlem3  20632  psgnghm  20640  tgcl  21493  restbas  21682  ordtbas2  21715  uncmp  21927  txuni2  22089  txbas  22091  ptbasin  22101  txcnp  22144  txlly  22160  txnlly  22161  tx1stc  22174  tx2ndc  22175  fbasrn  22408  rnelfmlem  22476  fmfnfmlem3  22480  txflf  22530  qustgplem  22644  trust  22753  utoptop  22758  fmucndlem  22815  blin2  22954  metustto  23078  tgqioo  23323  minveclem3b  23946  pmltpc  23966  evthicc2  23976  ovolunlem2  24014  dyaddisj  24112  rolle  24502  dvcvx  24532  itgsubst  24561  plyadd  24722  plymul  24723  coeeu  24730  aalioulem6  24841  dchrptlem2  25755  lgsdchr  25845  mul2sq  25909  2sqlem5  25912  pntibnd  26083  pntlemp  26100  cgraswap  26520  cgracom  26522  cgratr  26523  flatcgra  26524  dfcgra2  26530  acopyeu  26535  ax5seg  26639  axpasch  26642  axeuclid  26664  axcontlem4  26668  axcontlem9  26673  uhgr2edg  26905  2pthon3v  27637  pjhthmo  28994  superpos  30046  chirredi  30086  cdjreui  30124  cdj3i  30133  xrofsup  30406  archiabllem2c  30739  ccfldextdgrr  30944  ordtconnlem1  31054  dya2iocnrect  31426  txpconn  32364  cvmlift2lem10  32444  cvmlift3lem7  32457  msubco  32663  mclsppslem  32715  poseq  32980  soseq  32981  frrlem9  33016  noprefixmo  33087  altopelaltxp  33322  funtransport  33377  btwnconn1lem13  33445  btwnconn1lem14  33446  segletr  33460  segleantisym  33461  funray  33486  funline  33488  tailfb  33610  mblfinlem3  34799  ismblfin  34801  itg2addnc  34814  ftc1anclem6  34840  heibor1lem  34956  crngohomfo  35153  ispridlc  35217  prter1  35883  hl2at  36409  cdlemn11pre  38214  dihord2pre  38229  dihord4  38262  dihmeetlem20N  38330  mapdpglem32  38709  diophin  39231  diophun  39232  iunrelexpuztr  39926  mullimc  41759  mullimcf  41766  addlimc  41791  fourierdlem42  42297  fourierdlem80  42334  sge0resplit  42551  hoiqssbllem3  42769
  Copyright terms: Public domain W3C validator