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

Theorem reeanv 3245
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 nfv 1992 . 2 𝑦𝜑
2 nfv 1992 . 2 𝑥𝜓
31, 2reean 3244 1 (∃𝑥𝐴𝑦𝐵 (𝜑𝜓) ↔ (∃𝑥𝐴 𝜑 ∧ ∃𝑦𝐵 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 383  wrex 3051
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-10 2168  ax-11 2183  ax-12 2196
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-ral 3055  df-rex 3056
This theorem is referenced by:  3reeanv  3246  2ralor  3247  disjxiun  4801  fliftfun  6725  tfrlem5  7645  uniinqs  7994  eroveu  8009  erovlem  8010  xpf1o  8287  unxpdomlem3  8331  unfi  8392  finsschain  8438  dffi3  8502  rankxplim3  8917  xpnum  8967  kmlem9  9172  sornom  9291  fpwwe2lem12  9655  cnegex  10409  zaddcl  11609  rexanre  14285  o1lo1  14467  o1co  14516  rlimcn2  14520  o1of2  14542  lo1add  14556  lo1mul  14557  summo  14647  ntrivcvgmul  14833  prodmolem2  14864  prodmo  14865  dvds2lem  15196  odd2np1  15267  opoe  15289  omoe  15290  opeo  15291  omeo  15292  bezoutlem4  15461  gcddiv  15470  divgcdcoprmex  15582  pcqmul  15760  pcadd  15795  mul4sq  15860  4sqlem12  15862  prmgaplem7  15963  gaorber  17941  psgneu  18126  lsmsubm  18268  pj1eu  18309  efgredlem  18360  efgrelexlemb  18363  qusabl  18468  cygabl  18492  dprdsubg  18623  dvdsrtr  18852  unitgrp  18867  lss1d  19165  lsmspsn  19286  lspsolvlem  19344  lbsextlem2  19361  znfld  20111  cygznlem3  20120  psgnghm  20128  tgcl  20975  restbas  21164  ordtbas2  21197  uncmp  21408  txuni2  21570  txbas  21572  ptbasin  21582  txcnp  21625  txlly  21641  txnlly  21642  tx1stc  21655  tx2ndc  21656  fbasrn  21889  rnelfmlem  21957  fmfnfmlem3  21961  txflf  22011  qustgplem  22125  trust  22234  utoptop  22239  fmucndlem  22296  blin2  22435  metustto  22559  tgqioo  22804  minveclem3b  23399  pmltpc  23419  evthicc2  23429  ovolunlem2  23466  dyaddisj  23564  rolle  23952  dvcvx  23982  itgsubst  24011  plyadd  24172  plymul  24173  coeeu  24180  aalioulem6  24291  dchrptlem2  25189  lgsdchr  25279  mul2sq  25343  2sqlem5  25346  pntibnd  25481  pntlemp  25498  cgraswap  25911  cgracom  25913  cgratr  25914  dfcgra2  25920  acopyeu  25924  ax5seg  26017  axpasch  26020  axeuclid  26042  axcontlem4  26046  axcontlem9  26051  uhgr2edg  26299  2pthon3v  27063  pjhthmo  28470  superpos  29522  chirredi  29562  cdjreui  29600  cdj3i  29609  xrofsup  29842  archiabllem2c  30058  ordtconnlem1  30279  dya2iocnrect  30652  txpconn  31521  cvmlift2lem10  31601  cvmlift3lem7  31614  msubco  31735  mclsppslem  31787  poseq  32059  soseq  32060  noprefixmo  32154  altopelaltxp  32389  funtransport  32444  btwnconn1lem13  32512  btwnconn1lem14  32513  segletr  32527  segleantisym  32528  funray  32553  funline  32555  tailfb  32678  mblfinlem3  33761  ismblfin  33763  itg2addnc  33777  ftc1anclem6  33803  heibor1lem  33921  crngohomfo  34118  ispridlc  34182  prter1  34668  hl2at  35194  cdlemn11pre  37001  dihord2pre  37016  dihord4  37049  dihmeetlem20N  37117  mapdpglem32  37496  diophin  37838  diophun  37839  iunrelexpuztr  38513  mullimc  40351  mullimcf  40358  addlimc  40383  fourierdlem42  40869  fourierdlem80  40906  sge0resplit  41126  hoiqssbllem3  41344  2reu4a  41695
  Copyright terms: Public domain W3C validator