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

Theorem csbeq2i 3193
Description: Formula-building inference rule for class substitution. (Contributed by NM, 10-Nov-2005.) (Revised by Mario Carneiro, 1-Sep-2015.)
Hypothesis
Ref Expression
csbeq2i.1  |-  B  =  C
Assertion
Ref Expression
csbeq2i  |-  [_ A  /  x ]_ B  = 
[_ A  /  x ]_ C

Proof of Theorem csbeq2i
StepHypRef Expression
1 csbeq2i.1 . . . 4  |-  B  =  C
21a1i 10 . . 3  |-  (  T. 
->  B  =  C
)
32csbeq2dv 3192 . 2  |-  (  T. 
->  [_ A  /  x ]_ B  =  [_ A  /  x ]_ C )
43trud 1328 1  |-  [_ A  /  x ]_ B  = 
[_ A  /  x ]_ C
Colors of variables: wff set class
Syntax hints:    T. wtru 1321    = wceq 1647   [_csb 3167
This theorem is referenced by:  csbvarg  3194  csbnest1g  3219  csbsng  3782  csbunig  3937  csbxpg  4819  csbrng  5026  csbresg  5061  csbima12gALT  5126  csbfv12g  5642  csbfv12gALT  5643  csbnegg  9196  csbcnvg  23436  csbdmg  27488  cdleme31so  30639  cdleme31sn  30640  cdleme31sn1  30641  cdleme31se  30642  cdleme31se2  30643  cdleme31sc  30644  cdleme31sde  30645  cdleme31sn2  30649  cdlemkid3N  31193  cdlemkid4  31194
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-clab 2353  df-cleq 2359  df-clel 2362  df-sbc 3078  df-csb 3168
  Copyright terms: Public domain W3C validator