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

Theorem cbvrexv 2893
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 1626 . 2  |-  F/ y
ph
2 nfv 1626 . 2  |-  F/ x ps
3 cbvralv.1 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
41, 2, 3cbvrex 2889 1  |-  ( E. x  e.  A  ph  <->  E. y  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177   E.wrex 2667
This theorem is referenced by:  cbvrex2v  2901  reu7  3089  reusv3  4690  funcnvuni  5477  fun11iun  5654  fliftfun  5993  grpridd  6246  tfrlem3  6597  abianfp  6675  nneob  6854  pssnn  7286  frfi  7311  finsschain  7371  marypha1lem  7396  supmo  7413  suplub2  7422  ordtypelem3  7445  ordtypelem9  7451  wemaplem1  7471  brwdom3  7506  unwdomg  7508  cantnf  7605  trcl  7620  infxpenc2  7859  aceq2  7956  dfac5lem4  7963  kmlem9  7994  kmlem14  7999  fin23lem26  8161  fin1a2lem13  8248  axdc3lem3  8288  winainflem  8524  axgroth4  8663  suprlub  9926  supmul1  9929  supmullem1  9930  supmullem2  9931  supmul  9932  ublbneg  10516  zsupss  10521  xrsupsslem  10841  xrinfmsslem  10842  rexanre  12105  rexuzre  12111  rexico  12112  caurcvg2  12426  caucvgb  12428  summolem2  12465  summo  12466  mertens  12618  odd2np1lem  12862  gcdcllem1  12966  pceu  13175  4sqlem12  13279  vdwlem10  13313  vdwlem13  13316  vdwnn  13321  drsdirfi  14350  gaorb  15039  pj1eu  15283  efgsfo  15326  cyggeninv  15448  cygabl  15455  pgpfac1lem5  15592  pgpfac1  15593  pgpfaclem2  15595  lss1d  15994  lspsneq  16149  lspsolvlem  16169  lbsextlem2  16186  cygznlem3  16805  ordtrest2lem  17221  cnprest  17307  1stcfb  17461  1stcelcls  17477  elpt  17557  fbssfi  17822  fgcl  17863  rnelfmlem  17937  fmfnfmlem3  17941  txflf  17991  alexsubb  18030  alexsubALTlem4  18034  isucn2  18262  icccmplem2  18807  ply1divex  20012  coeeu  20097  plydivex  20167  aannenlem2  20199  ulmcau  20264  ulmbdd  20267  dchrptlem2  21002  bposlem9  21029  pntibndlem3  21239  pntlemi  21251  pntlemp  21257  pntleml  21258  pnt3  21259  isgrpo2  21738  grpoidinvlem3  21747  isgrp2d  21776  isgrpda  21838  ubthlem3  22327  norm1exi  22705  pjhthmo  22757  cdjreui  23888  cdj3i  23897  lmxrge0  24290  esumcvg  24429  conpcon  24875  cvmlift2lem12  24954  cvmlift2lem13  24955  cvmlift3lem2  24960  cvmlift3lem7  24965  cvmlift3  24968  prodmolem2  25214  prodmo  25215  poseq  25467  soseq  25468  funtransport  25869  funray  25978  funline  25980  supaddc  26137  supadd  26138  ismblfin  26146  volsupnfl  26150  itg2addnclem  26155  fnessref  26263  neibastop2  26280  unirep  26304  filbcmb  26332  sdclem1  26337  sdc  26338  fdc  26339  incsequz  26342  heibor1lem  26408  heiborlem10  26419  isdrngo2  26464  prnc  26567  prtlem13  26607  prtlem15  26614  mzpcompact2lem  26698  eldioph3  26714  diophrex  26724  rexrabdioph  26744  eldioph4i  26763  aomclem8  27027  hbtlem2  27196  rngunsnply  27246  psgnunilem3  27287  psgnunilem4  27288  psgneu  27297  dvconstbi  27419  expgrowth  27420  frgraregorufr0  28155  lshpsmreu  29592  lshpkrlem1  29593  lshpkrlem3  29595  pclfinN  30382  4atex  30558  dihglblem2N  31777  lcfl7N  31984  lcf1o  32034
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ral 2671  df-rex 2672
  Copyright terms: Public domain W3C validator