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 1 eleq2d
 |-  ( ph -> ( y e. B <-> y e. C ) )
3 2 sbcbidv
 |-  ( ph -> ( [. A / x ]. y e. B <-> [. A / x ]. y e. C ) )
4 3 abbidv
 |-  ( ph -> { y | [. A / x ]. y e. B } = { y | [. A / x ]. y e. C } )
5 df-csb
 |-  [_ A / x ]_ B = { y | [. A / x ]. y e. B }
6 df-csb
 |-  [_ A / x ]_ C = { y | [. A / x ]. y e. C }
7 4 5 6 3eqtr4g
 |-  ( ph -> [_ A / x ]_ B = [_ A / x ]_ C )