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

Theorem cbvabv 2597
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 1712 . 2  |-  F/ y
ph
2 nfv 1712 . 2  |-  F/ x ps
3 cbvabv.1 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
41, 2, 3cbvab 2595 1  |-  { x  |  ph }  =  {
y  |  ps }
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1398   {cab 2439
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446
This theorem is referenced by:  cdeqab1  3316  difjust  3463  unjust  3465  injust  3467  uniiunlem  3574  dfif3  3943  pwjust  4000  snjust  4015  intab  4302  intabs  4598  iotajust  5533  sbth  7630  cardprc  8352  iunfictbso  8486  aceq3lem  8492  isf33lem  8737  axdc3  8825  axdclem  8890  axdc  8892  genpv  9366  ltexpri  9410  recexpr  9418  supsr  9478  hashf1lem2  12489  cvbtrcl  12910  mertens  13777  4sq  14566  nbgraf1olem5  24647  dispcmp  28097  eulerpart  28585  ballotlemfmpn  28697  subfacp1lem6  28893  subfacp1  28894  dfon2lem3  29457  dfon2lem7  29461  wfrlem1  29583  frrlem1  29627  ismblfin  30295  eldioph3  30938  diophrex  30948  ssfiunibd  31748  isuhgr  32738  isushgr  32739  bnj66  34319  bnj1234  34470  glbconxN  35499
  Copyright terms: Public domain W3C validator