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

Theorem cbvrabv 2955
Description: Rule to change the bound variable in a restricted class abstraction, using implicit substitution. (Contributed by NM, 26-May-1999.)
Hypothesis
Ref Expression
cbvrabv.1  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
Assertion
Ref Expression
cbvrabv  |-  { x  e.  A  |  ph }  =  { y  e.  A  |  ps }
Distinct variable groups:    x, y, A    ph, y    ps, x
Allowed substitution hints:    ph( x)    ps( y)

Proof of Theorem cbvrabv
StepHypRef Expression
1 nfcv 2572 . 2  |-  F/_ x A
2 nfcv 2572 . 2  |-  F/_ y A
3 nfv 1629 . 2  |-  F/ y
ph
4 nfv 1629 . 2  |-  F/ x ps
5 cbvrabv.1 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
61, 2, 3, 4, 5cbvrab 2954 1  |-  { x  e.  A  |  ph }  =  { y  e.  A  |  ps }
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    = wceq 1652   {crab 2709
This theorem is referenced by:  pwnss  4365  knatar  6080  oeeulem  6844  ordtypecbv  7486  ordtypelem9  7495  inf3lema  7579  oemapso  7638  oemapvali  7640  tz9.12lem3  7715  cofsmo  8149  enfin2i  8201  fin23lem33  8225  isf32lem11  8243  zorn2g  8383  pwfseqlem1  8533  pwfseqlem3  8535  zsupss  10565  zmin  10570  reexALT  10606  hashbc  11702  sqrlem7  12054  rpnnen  12826  divalglem5  12917  bitsfzolem  12946  smupp1  12992  gcdcllem3  13013  bezout  13042  eulerth  13172  odzval  13177  pcprecl  13213  pcprendvds  13214  pcpremul  13217  pceulem  13219  prmreclem1  13284  prmreclem5  13288  prmreclem6  13289  4sqlem19  13331  vdwnn  13366  hashbcval  13370  gsumvalx  14774  efgsdm  15362  efgsfo  15371  ablfaclem3  15645  ltbwe  16533  coe1mul2lem2  16661  pptbas  17072  concompss  17496  ptcmplem5  18087  ustuqtop  18276  utopsnneip  18278  icccmplem2  18854  minveclem5  19334  ivth  19351  ovolicc2lem5  19417  ovolicc  19419  opnmbllem  19493  vitali  19505  itg2monolem3  19644  elqaa  20239  radcnvle  20336  pserdvlem2  20344  wilth  20854  ftalem6  20860  nbgraf1olem1  21451  nbgraf1o  21457  cusgraexg  21478  cusgrafi  21491  ubthlem3  22374  htth  22421  ballotlemelo  24745  ballotleme  24754  ballotlem7  24793  lgamgulmlem5  24817  lgamcvglem  24824  subfacp1lem6  24871  erdsze  24888  cvmscbv  24945  cvmsiota  24964  cvmlift2lem13  25002  axcontlem11  25913  mblfinlem1  26243  mblfinlem2  26244  neibastop2  26390  eldioph4i  26873  stoweidlem49  27774  frgraregorufr0  28441  usgreghash2spot  28458  lclkrs2  32338
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-rab 2714
  Copyright terms: Public domain W3C validator