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

Theorem csbeq2i 3107
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 3106 . 2  |-  (  T. 
->  [_ A  /  x ]_ B  =  [_ A  /  x ]_ C )
43trud 1314 1  |-  [_ A  /  x ]_ B  = 
[_ A  /  x ]_ C
Colors of variables: wff set class
Syntax hints:    T. wtru 1307    = wceq 1623   [_csb 3081
This theorem is referenced by:  csbvarg  3108  csbnest1g  3133  csbsng  3692  csbunig  3835  csbxpg  4716  csbrng  4923  csbresg  4958  csbima12gALT  5023  csbfv12g  5535  csbfv12gALT  5536  csbnegg  9049  csbcnvg  23198  csbdmg  27980  cdleme31so  30568  cdleme31sn  30569  cdleme31sn1  30570  cdleme31se  30571  cdleme31se2  30572  cdleme31sc  30573  cdleme31sde  30574  cdleme31sn2  30578  cdlemkid3N  31122  cdlemkid4  31123
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-sbc 2992  df-csb 3082
  Copyright terms: Public domain W3C validator