MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cbvrexv Structured version   Unicode version

Theorem cbvrexv 2934
Description: Change the bound variable of a restricted existential quantifier using implicit substitution. (Contributed by NM, 2-Jun-1998.)
Hypothesis
Ref Expression
cbvralv.1  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
Assertion
Ref Expression
cbvrexv  |-  ( E. x  e.  A  ph  <->  E. y  e.  A  ps )
Distinct variable groups:    x, A    y, A    ph, y    ps, x
Allowed substitution hints:    ph( x)    ps( y)

Proof of Theorem cbvrexv
StepHypRef Expression
1 nfv 1630 . 2  |-  F/ y
ph
2 nfv 1630 . 2  |-  F/ x ps
3 cbvralv.1 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
41, 2, 3cbvrex 2930 1  |-  ( E. x  e.  A  ph  <->  E. y  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178   E.wrex 2707
This theorem is referenced by:  cbvrex2v  2942  reu7  3130  reusv3  4732  funcnvuni  5519  fun11iun  5696  fliftfun  6035  grpridd  6288  tfrlem3  6639  abianfp  6717  nneob  6896  pssnn  7328  frfi  7353  finsschain  7414  marypha1lem  7439  supmo  7458  suplub2  7467  ordtypelem3  7490  ordtypelem9  7496  wemaplem1  7516  brwdom3  7551  unwdomg  7553  cantnf  7650  trcl  7665  infxpenc2  7904  aceq2  8001  dfac5lem4  8008  kmlem9  8039  kmlem14  8044  fin23lem26  8206  fin1a2lem13  8293  axdc3lem3  8333  winainflem  8569  axgroth4  8708  suprlub  9971  supmul1  9974  supmullem1  9975  supmullem2  9976  supmul  9977  ublbneg  10561  zsupss  10566  xrsupsslem  10886  xrinfmsslem  10887  rexanre  12151  rexuzre  12157  rexico  12158  caurcvg2  12472  caucvgb  12474  summolem2  12511  summo  12512  mertens  12664  odd2np1lem  12908  gcdcllem1  13012  pceu  13221  4sqlem12  13325  vdwlem10  13359  vdwlem13  13362  vdwnn  13367  drsdirfi  14396  gaorb  15085  pj1eu  15329  efgsfo  15372  cyggeninv  15494  cygabl  15501  pgpfac1lem5  15638  pgpfac1  15639  pgpfaclem2  15641  lss1d  16040  lspsneq  16195  lspsolvlem  16215  lbsextlem2  16232  cygznlem3  16851  ordtrest2lem  17268  cnprest  17354  1stcfb  17509  1stcelcls  17525  elpt  17605  fbssfi  17870  fgcl  17911  rnelfmlem  17985  fmfnfmlem3  17989  txflf  18039  alexsubb  18078  alexsubALTlem4  18082  isucn2  18310  icccmplem2  18855  ply1divex  20060  coeeu  20145  plydivex  20215  aannenlem2  20247  ulmcau  20312  ulmbdd  20315  dchrptlem2  21050  bposlem9  21077  pntibndlem3  21287  pntlemi  21299  pntlemp  21305  pntleml  21306  pnt3  21307  isgrpo2  21786  grpoidinvlem3  21795  isgrp2d  21824  isgrpda  21886  ubthlem3  22375  norm1exi  22753  pjhthmo  22805  cdjreui  23936  cdj3i  23945  lmxrge0  24338  esumcvg  24477  conpcon  24923  cvmlift2lem12  25002  cvmlift2lem13  25003  cvmlift3lem2  25008  cvmlift3lem7  25013  cvmlift3  25016  prodmolem2  25262  prodmo  25263  poseq  25529  soseq  25530  funtransport  25966  funray  26075  funline  26077  supaddc  26238  supadd  26239  ismblfin  26248  volsupnfl  26252  itg2addnclem  26257  fnessref  26374  neibastop2  26391  unirep  26415  filbcmb  26443  sdclem1  26448  sdc  26449  fdc  26450  incsequz  26453  heibor1lem  26519  heiborlem10  26530  isdrngo2  26575  prnc  26678  prtlem13  26718  prtlem15  26725  mzpcompact2lem  26809  eldioph3  26825  diophrex  26835  rexrabdioph  26855  eldioph4i  26874  aomclem8  27137  hbtlem2  27306  rngunsnply  27356  psgnunilem3  27397  psgnunilem4  27398  psgneu  27407  dvconstbi  27529  expgrowth  27530  frgraregorufr0  28442  lshpsmreu  29908  lshpkrlem1  29909  lshpkrlem3  29911  pclfinN  30698  4atex  30874  dihglblem2N  32093  lcfl7N  32300  lcf1o  32350
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2418
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-cleq 2430  df-clel 2433  df-nfc 2562  df-ral 2711  df-rex 2712
  Copyright terms: Public domain W3C validator