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

Theorem cbvabv 2565
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 1751 . 2  |-  F/ y
ph
2 nfv 1751 . 2  |-  F/ x ps
3 cbvabv.1 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
41, 2, 3cbvab 2563 1  |-  { x  |  ph }  =  {
y  |  ps }
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    = wceq 1437   {cab 2407
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2408  df-cleq 2414
This theorem is referenced by:  cdeqab1  3291  difjust  3438  unjust  3440  injust  3442  uniiunlem  3549  dfif3  3923  pwjust  3980  snjust  3995  intab  4283  intabs  4581  iotajust  5560  wfrlem1  7039  sbth  7694  cardprc  8415  iunfictbso  8545  aceq3lem  8551  isf33lem  8796  axdc3  8884  axdclem  8949  axdc  8951  genpv  9424  ltexpri  9468  recexpr  9476  supsr  9536  hashf1lem2  12616  cvbtrcl  13042  mertens  13927  4sq  14899  nbgraf1olem5  25156  dispcmp  28679  eulerpart  29208  ballotlemfmpn  29320  bnj66  29664  bnj1234  29815  subfacp1lem6  29901  subfacp1  29902  dfon2lem3  30423  dfon2lem7  30427  frrlem1  30506  f1omptsn  31677  ismblfin  31892  glbconxN  32859  eldioph3  35524  diophrex  35534  ssfiunibd  37366  isuhgr  38806  isushgr  38807  isumgr  38829  isuhgrALTV  38864  isushgrALTV  38865
  Copyright terms: Public domain W3C validator