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

Theorem cbvabv 2554
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 1629 . 2  |-  F/ y
ph
2 nfv 1629 . 2  |-  F/ x ps
3 cbvabv.1 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
41, 2, 3cbvab 2553 1  |-  { x  |  ph }  =  {
y  |  ps }
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    = wceq 1652   {cab 2421
This theorem is referenced by:  cdeqab1  3145  difjust  3314  unjust  3316  injust  3318  uniiunlem  3423  dfif3  3741  pwjust  3792  snjust  3811  intab  4072  intabs  4353  iotajust  5409  tfrlem3a  6631  sbth  7219  cardprc  7859  iunfictbso  7987  aceq3lem  7993  isf33lem  8238  axdc3  8326  axdclem  8391  axdc  8393  genpv  8868  ltexpri  8912  recexpr  8920  supsr  8979  hashf1lem2  11697  mertens  12655  4sq  13324  nbgraf1olem5  21447  ballotlemfmpn  24744  subfacp1lem6  24863  subfacp1  24864  dfon2lem3  25404  dfon2lem7  25408  wfrlem1  25530  frrlem1  25574  ismblfin  26237  eldioph3  26815  diophrex  26825  bnj66  29168  bnj1234  29319  glbconxN  30112
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 2416
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428
  Copyright terms: Public domain W3C validator