ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  cbvabv Unicode version

Theorem cbvabv 2177
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 1437 . 2  |-  F/ y
ph
2 nfv 1437 . 2  |-  F/ x ps
3 cbvabv.1 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
41, 2, 3cbvab 2176 1  |-  { x  |  ph }  =  {
y  |  ps }
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 102    = wceq 1259   {cab 2042
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-io 640  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-10 1412  ax-11 1413  ax-i12 1414  ax-bndl 1415  ax-4 1416  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038
This theorem depends on definitions:  df-bi 114  df-nf 1366  df-sb 1662  df-clab 2043  df-cleq 2049
This theorem is referenced by:  cdeqab1  2778  difjust  2946  unjust  2948  injust  2950  uniiunlem  3055  dfif3  3370  pwjust  3387  snjust  3407  intab  3671  iotajust  4893  tfrlemi1  5976  frecsuc  6021  nqprlu  6702  recexpr  6793  caucvgprprlemval  6843  caucvgprprlemnbj  6848  caucvgprprlemaddq  6863  caucvgprprlem1  6864  caucvgprprlem2  6865  axcaucvg  7031  bds  10337
  Copyright terms: Public domain W3C validator