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

Theorem csbeq1d 3038
Description: Equality deduction for proper substitution into a class. (Contributed by NM, 3-Dec-2005.)
Hypothesis
Ref Expression
csbeq1d.1  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
csbeq1d  |-  ( ph  ->  [_ A  /  x ]_ C  =  [_ B  /  x ]_ C )

Proof of Theorem csbeq1d
StepHypRef Expression
1 csbeq1d.1 . 2  |-  ( ph  ->  A  =  B )
2 csbeq1 3034 . 2  |-  ( A  =  B  ->  [_ A  /  x ]_ C  = 
[_ B  /  x ]_ C )
31, 2syl 14 1  |-  ( ph  ->  [_ A  /  x ]_ C  =  [_ B  /  x ]_ C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1335   [_csb 3031
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-11 1486  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2139
This theorem depends on definitions:  df-bi 116  df-tru 1338  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-sbc 2938  df-csb 3032
This theorem is referenced by:  csbidmg  3087  csbco3g  3089  fmptcof  5635  mpomptsx  6146  dmmpossx  6148  fmpox  6149  fmpoco  6164  xpf1o  6790  summodclem3  11281  summodclem2a  11282  summodc  11284  zsumdc  11285  fsum3  11288  sumsnf  11310  fsumcnv  11338  fisumcom2  11339  fsumshftm  11346  fisum0diag2  11348  prodmodclem3  11476  prodmodclem2a  11477  prodmodc  11479  zproddc  11480  fprodseq  11484  prodsnf  11493  fprodcnv  11526  fprodcom2fi  11527  ctiunctlemu1st  12205  ctiunctlemu2nd  12206  ctiunctlemudc  12208  ctiunctlemfo  12210
  Copyright terms: Public domain W3C validator