Metamath Proof Explorer

Theorem csbeq2dv

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

Ref Expression
Hypothesis csbeq2dv.1 
|- ( ph -> B = C )
Assertion csbeq2dv 
|- ( ph -> [_ A / x ]_ B = [_ A / x ]_ C )

Proof

Step Hyp Ref Expression
1 csbeq2dv.1 
 |-  ( ph -> B = C )
2 nfv 
 |-  F/ x ph
3 2 1 csbeq2d 
 |-  ( ph -> [_ A / x ]_ B = [_ A / x ]_ C )