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

Theorem cbvabv 2402
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 1605 . 2  |-  F/ y
ph
2 nfv 1605 . 2  |-  F/ x ps
3 cbvabv.1 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
41, 2, 3cbvab 2401 1  |-  { x  |  ph }  =  {
y  |  ps }
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    = wceq 1623   {cab 2269
This theorem is referenced by:  cdeqab1  2983  difjust  3154  unjust  3156  injust  3158  uniiunlem  3260  dfif3  3575  pwjust  3626  snjust  3645  intab  3892  intabs  4172  iotajust  5218  tfrlem3a  6394  sbth  6981  cardprc  7613  iunfictbso  7741  aceq3lem  7747  isf33lem  7992  axdc3  8080  axdclem  8146  axdc  8148  genpv  8623  ltexpri  8667  recexpr  8675  supsr  8734  hashf1lem2  11394  mertens  12342  4sq  13011  ballotlemfmpn  23053  subfacp1lem6  23716  subfacp1  23717  dfon2lem3  24141  dfon2lem7  24145  wfrlem1  24256  frrlem1  24281  bpolyval  24784  eldioph3  26845  diophrex  26855  bnj66  28892  bnj1234  29043  glbconxN  29567
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276
  Copyright terms: Public domain W3C validator