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

Theorem csbeq1d 3056
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 3052 . 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 1348   [_csb 3049
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 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-11 1499  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152
This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-sbc 2956  df-csb 3050
This theorem is referenced by:  csbidmg  3105  csbco3g  3107  fmptcof  5663  mpomptsx  6176  dmmpossx  6178  fmpox  6179  fmpoco  6195  xpf1o  6822  summodclem3  11343  summodclem2a  11344  summodc  11346  zsumdc  11347  fsum3  11350  sumsnf  11372  fsumcnv  11400  fisumcom2  11401  fsumshftm  11408  fisum0diag2  11410  prodmodclem3  11538  prodmodclem2a  11539  prodmodc  11541  zproddc  11542  fprodseq  11546  prodsnf  11555  fprodcnv  11588  fprodcom2fi  11589  pcmpt  12295  ctiunctlemu1st  12389  ctiunctlemu2nd  12390  ctiunctlemudc  12392  ctiunctlemfo  12394
  Copyright terms: Public domain W3C validator