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

Theorem cbvabv 2506
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 1626 . 2  |-  F/ y
ph
2 nfv 1626 . 2  |-  F/ x ps
3 cbvabv.1 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
41, 2, 3cbvab 2505 1  |-  { x  |  ph }  =  {
y  |  ps }
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    = wceq 1649   {cab 2373
This theorem is referenced by:  cdeqab1  3096  difjust  3265  unjust  3267  injust  3269  uniiunlem  3374  dfif3  3692  pwjust  3743  snjust  3762  intab  4022  intabs  4302  iotajust  5357  tfrlem3a  6575  sbth  7163  cardprc  7800  iunfictbso  7928  aceq3lem  7934  isf33lem  8179  axdc3  8267  axdclem  8332  axdc  8334  genpv  8809  ltexpri  8853  recexpr  8861  supsr  8920  hashf1lem2  11632  mertens  12590  4sq  13259  nbgraf1olem5  21321  ballotlemfmpn  24531  subfacp1lem6  24650  subfacp1  24651  dfon2lem3  25165  dfon2lem7  25169  wfrlem1  25280  frrlem1  25305  bpolyval  25809  eldioph3  26515  diophrex  26525  bnj66  28569  bnj1234  28720  glbconxN  29492
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2374  df-cleq 2380
  Copyright terms: Public domain W3C validator