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

Theorem reeanv 3101
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 1840 . 2 𝑦𝜑
2 nfv 1840 . 2 𝑥𝜓
31, 2reean 3100 1 (∃𝑥𝐴𝑦𝐵 (𝜑𝜓) ↔ (∃𝑥𝐴 𝜑 ∧ ∃𝑦𝐵 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 384  wrex 2909
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-10 2016  ax-11 2031  ax-12 2044
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-ral 2913  df-rex 2914
This theorem is referenced by:  3reeanv  3102  2ralor  3103  disjxiun  4619  disjxiunOLD  4620  fliftfun  6527  tfrlem5  7436  uniinqs  7787  eroveu  7802  erovlem  7803  xpf1o  8082  unxpdomlem3  8126  unfi  8187  finsschain  8233  dffi3  8297  rankxplim3  8704  xpnum  8737  kmlem9  8940  sornom  9059  fpwwe2lem12  9423  cnegex  10177  zaddcl  11377  rexanre  14036  o1lo1  14218  o1co  14267  rlimcn2  14271  o1of2  14293  lo1add  14307  lo1mul  14308  summo  14397  ntrivcvgmul  14578  prodmolem2  14609  prodmo  14610  dvds2lem  14937  odd2np1  15008  opoe  15030  omoe  15031  opeo  15032  omeo  15033  bezoutlem4  15202  gcddiv  15211  divgcdcoprmex  15323  pcqmul  15501  pcadd  15536  mul4sq  15601  4sqlem12  15603  prmgaplem7  15704  gaorber  17681  psgneu  17866  lsmsubm  18008  pj1eu  18049  efgredlem  18100  efgrelexlemb  18103  qusabl  18208  cygabl  18232  dprdsubg  18363  dvdsrtr  18592  unitgrp  18607  lss1d  18903  lsmspsn  19024  lspsolvlem  19082  lbsextlem2  19099  znfld  19849  cygznlem3  19858  psgnghm  19866  tgcl  20713  restbas  20902  ordtbas2  20935  uncmp  21146  txuni2  21308  txbas  21310  ptbasin  21320  txcnp  21363  txlly  21379  txnlly  21380  tx1stc  21393  tx2ndc  21394  fbasrn  21628  rnelfmlem  21696  fmfnfmlem3  21700  txflf  21750  qustgplem  21864  trust  21973  utoptop  21978  fmucndlem  22035  blin2  22174  metustto  22298  tgqioo  22543  minveclem3b  23139  pmltpc  23159  evthicc2  23169  ovolunlem2  23206  dyaddisj  23304  rolle  23691  dvcvx  23721  itgsubst  23750  plyadd  23911  plymul  23912  coeeu  23919  aalioulem6  24030  dchrptlem2  24924  lgsdchr  25014  mul2sq  25078  2sqlem5  25081  pntibnd  25216  pntlemp  25233  cgraswap  25646  cgracom  25648  cgratr  25649  dfcgra2  25655  acopyeu  25659  ax5seg  25752  axpasch  25755  axeuclid  25777  axcontlem4  25781  axcontlem9  25786  uhgr2edg  26027  2pthon3v  26742  frgrwopreglem5  27077  pjhthmo  28049  superpos  29101  chirredi  29141  cdjreui  29179  cdj3i  29188  xrofsup  29418  archiabllem2c  29576  ordtconnlem1  29794  dya2iocnrect  30166  txpconn  30975  cvmlift2lem10  31055  cvmlift3lem7  31068  msubco  31189  mclsppslem  31241  poseq  31504  soseq  31505  noprefixmo  31626  altopelaltxp  31778  funtransport  31833  btwnconn1lem13  31901  btwnconn1lem14  31902  segletr  31916  segleantisym  31917  funray  31942  funline  31944  tailfb  32067  mblfinlem3  33119  ismblfin  33121  itg2addnc  33135  ftc1anclem6  33161  heibor1lem  33279  crngohomfo  33476  ispridlc  33540  prter1  33683  hl2at  34210  cdlemn11pre  36018  dihord2pre  36033  dihord4  36066  dihmeetlem20N  36134  mapdpglem32  36513  diophin  36855  diophun  36856  iunrelexpuztr  37531  mullimc  39284  mullimcf  39291  addlimc  39316  fourierdlem42  39703  fourierdlem80  39740  sge0resplit  39960  hoiqssbllem3  40175  2reu4a  40523
  Copyright terms: Public domain W3C validator