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

Theorem cbvrabv 2800
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 2432 . 2  |-  F/_ x A
2 nfcv 2432 . 2  |-  F/_ y A
3 nfv 1609 . 2  |-  F/ y
ph
4 nfv 1609 . 2  |-  F/ x ps
5 cbvrabv.1 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
61, 2, 3, 4, 5cbvrab 2799 1  |-  { x  e.  A  |  ph }  =  { y  e.  A  |  ps }
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    = wceq 1632   {crab 2560
This theorem is referenced by:  pwnss  4192  knatar  5873  oeeulem  6615  ordtypecbv  7248  ordtypelem9  7257  inf3lema  7341  oemapso  7400  oemapvali  7402  tz9.12lem3  7477  cofsmo  7911  enfin2i  7963  fin23lem33  7987  isf32lem11  8005  zorn2g  8146  pwfseqlem1  8296  pwfseqlem3  8298  zsupss  10323  zmin  10328  reexALT  10364  hashbc  11407  sqrlem7  11750  rpnnen  12521  divalglem5  12612  bitsfzolem  12641  smupp1  12687  gcdcllem3  12708  bezout  12737  eulerth  12867  odzval  12872  pcprecl  12908  pcprendvds  12909  pcpremul  12912  pceulem  12914  prmreclem1  12979  prmreclem5  12983  prmreclem6  12984  4sqlem19  13026  vdwnn  13061  hashbcval  13065  gsumvalx  14467  efgsdm  15055  efgsfo  15064  ablfaclem3  15338  ltbwe  16230  coe1mul2lem2  16361  pptbas  16761  concompss  17175  ptcmplem5  17766  icccmplem2  18344  minveclem5  18813  ivth  18830  ovolicc2lem5  18896  ovolicc  18898  opnmbllem  18972  vitali  18984  itg2monolem3  19123  elqaa  19718  radcnvle  19812  pserdvlem2  19820  wilth  20325  ftalem6  20331  ubthlem3  21467  htth  21514  ballotlem7  23110  subfacp1lem6  23731  erdsze  23748  cvmscbv  23804  cvmsiota  23823  cvmlift2lem13  23861  axcontlem11  24674  neibastop2  26413  eldioph4i  26998  lclkrs2  32352
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rab 2565
  Copyright terms: Public domain W3C validator