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

Theorem cbvabv 2610
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 1683 . 2  |-  F/ y
ph
2 nfv 1683 . 2  |-  F/ x ps
3 cbvabv.1 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
41, 2, 3cbvab 2608 1  |-  { x  |  ph }  =  {
y  |  ps }
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1379   {cab 2452
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459
This theorem is referenced by:  cdeqab1  3323  difjust  3478  unjust  3480  injust  3482  uniiunlem  3588  dfif3  3953  pwjust  4011  snjust  4026  intab  4312  intabs  4608  iotajust  5550  sbth  7637  cardprc  8361  iunfictbso  8495  aceq3lem  8501  isf33lem  8746  axdc3  8834  axdclem  8899  axdc  8901  genpv  9377  ltexpri  9421  recexpr  9429  supsr  9489  hashf1lem2  12471  mertens  13658  4sq  14341  nbgraf1olem5  24149  eulerpart  27989  ballotlemfmpn  28101  subfacp1lem6  28297  subfacp1  28298  dfon2lem3  28822  dfon2lem7  28826  wfrlem1  28948  frrlem1  28992  ismblfin  29660  eldioph3  30331  diophrex  30341  ssfiunibd  31114  isuhgr  31861  isushgr  31862  bnj66  33015  bnj1234  33166  glbconxN  34192
  Copyright terms: Public domain W3C validator