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

Theorem cbvabv 2415
Description: Rule used to change bound variables, using implicit substitution. (Contributed by NM, 26-May-1999.)
Hypothesis
Ref Expression
cbvabv.1  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
Assertion
Ref Expression
cbvabv  |-  { x  |  ph }  =  {
y  |  ps }
Distinct variable groups:    ph, y    ps, x
Allowed substitution hints:    ph( x)    ps( y)

Proof of Theorem cbvabv
StepHypRef Expression
1 nfv 1609 . 2  |-  F/ y
ph
2 nfv 1609 . 2  |-  F/ x ps
3 cbvabv.1 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
41, 2, 3cbvab 2414 1  |-  { x  |  ph }  =  {
y  |  ps }
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    = wceq 1632   {cab 2282
This theorem is referenced by:  cdeqab1  2996  difjust  3167  unjust  3169  injust  3171  uniiunlem  3273  dfif3  3588  pwjust  3639  snjust  3658  intab  3908  intabs  4188  iotajust  5234  tfrlem3a  6410  sbth  6997  cardprc  7629  iunfictbso  7757  aceq3lem  7763  isf33lem  8008  axdc3  8096  axdclem  8162  axdc  8164  genpv  8639  ltexpri  8683  recexpr  8691  supsr  8750  hashf1lem2  11410  mertens  12358  4sq  13027  ballotlemfmpn  23069  subfacp1lem6  23731  subfacp1  23732  dfon2lem3  24212  dfon2lem7  24216  wfrlem1  24327  frrlem1  24352  bpolyval  24856  eldioph3  26948  diophrex  26958  bnj66  29208  bnj1234  29359  glbconxN  30189
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
  Copyright terms: Public domain W3C validator