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

Theorem cbvrexv 2765
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 1605 . 2  |-  F/ y
ph
2 nfv 1605 . 2  |-  F/ x ps
3 cbvralv.1 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
41, 2, 3cbvrex 2761 1  |-  ( E. x  e.  A  ph  <->  E. y  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176   E.wrex 2544
This theorem is referenced by:  cbvrex2v  2773  reu7  2960  reusv3  4542  funcnvuni  5317  fun11iun  5493  fliftfun  5811  grpridd  6060  tfrlem3  6393  abianfp  6471  nneob  6650  pssnn  7081  frfi  7102  finsschain  7162  marypha1lem  7186  supmo  7203  suplub2  7212  ordtypelem3  7235  ordtypelem9  7241  wemaplem1  7261  brwdom3  7296  unwdomg  7298  cantnf  7395  trcl  7410  infxpenc2  7649  aceq2  7746  dfac5lem4  7753  kmlem9  7784  kmlem14  7789  fin23lem26  7951  fin1a2lem13  8038  axdc3lem3  8078  winainflem  8315  axgroth4  8454  suprlub  9716  supmul1  9719  supmullem1  9720  supmullem2  9721  supmul  9722  ublbneg  10302  zsupss  10307  xrsupsslem  10625  xrinfmsslem  10626  rexanre  11830  rexuzre  11836  rexico  11837  caurcvg2  12150  caucvgb  12152  summolem2  12189  summo  12190  mertens  12342  odd2np1lem  12586  gcdcllem1  12690  pceu  12899  4sqlem12  13003  vdwlem10  13037  vdwlem13  13040  vdwnn  13045  drsdirfi  14072  gaorb  14761  pj1eu  15005  efgsfo  15048  cyggeninv  15170  cygabl  15177  pgpfac1lem5  15314  pgpfac1  15315  pgpfaclem2  15317  lss1d  15720  lspsneq  15875  lspsolvlem  15895  lbsextlem2  15912  cygznlem3  16523  ordtrest2lem  16933  cnprest  17017  1stcfb  17171  1stcelcls  17187  elpt  17267  fbssfi  17532  fgcl  17573  rnelfmlem  17647  fmfnfmlem3  17651  txflf  17701  alexsubb  17740  alexsubALTlem4  17744  icccmplem2  18328  ply1divex  19522  coeeu  19607  plydivex  19677  aannenlem2  19709  ulmcau  19772  ulmbdd  19775  dchrptlem2  20504  bposlem9  20531  pntibndlem3  20741  pntlemi  20753  pntlemp  20759  pntleml  20760  pnt3  20761  isgrpo2  20864  grpoidinvlem3  20873  isgrp2d  20902  isgrpda  20964  ubthlem3  21451  norm1exi  21829  pjhthmo  21881  cdjreui  23012  cdj3i  23021  lmxrge0  23375  esumcvg  23454  conpcon  23766  cvmlift2lem12  23845  cvmlift2lem13  23846  cvmlift3lem2  23851  cvmlift3lem7  23856  cvmlift3  23859  poseq  24253  soseq  24254  funtransport  24654  funray  24763  funline  24765  intopcoaconb  25540  islimrs4  25582  fnessref  26293  neibastop2  26310  unirep  26349  filbcmb  26432  sdclem1  26453  sdc  26454  fdc  26455  incsequz  26458  heibor1lem  26533  heiborlem10  26544  isdrngo2  26589  prnc  26692  prtlem13  26736  prtlem15  26743  mzpcompact2lem  26829  eldioph3  26845  diophrex  26855  rexrabdioph  26875  eldioph4i  26895  aomclem8  27159  hbtlem2  27328  rngunsnply  27378  psgnunilem3  27419  psgnunilem4  27420  psgneu  27429  dvconstbi  27551  expgrowth  27552  lshpsmreu  29299  lshpkrlem1  29300  lshpkrlem3  29302  pclfinN  30089  4atex  30265  dihglblem2N  31484  lcfl7N  31691  lcf1o  31741
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ral 2548  df-rex 2549
  Copyright terms: Public domain W3C validator