Metamath Proof Explorer

Theorem csbeq2i

Description: Formula-building inference for class substitution. (Contributed by NM, 10-Nov-2005) (Revised by Mario Carneiro, 1-Sep-2015)

Ref Expression
Hypothesis csbeq2i.1 
|- B = C
Assertion csbeq2i 
|- [_ A / x ]_ B = [_ A / x ]_ C

Proof

Step Hyp Ref Expression
1 csbeq2i.1 
 |-  B = C
2 1 a1i 
 |-  ( T. -> B = C )
3 2 csbeq2dv 
 |-  ( T. -> [_ A / x ]_ B = [_ A / x ]_ C )
4 3 mptru 
 |-  [_ A / x ]_ B = [_ A / x ]_ C