This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem csbeq2

Description: Substituting into equivalent classes gives equivalent results. (Contributed by Giovanni Mascellani, 9-Apr-2018)

Ref Expression
Assertion csbeq2 
|- ( A. x B = C -> [_ A / x ]_ B = [_ A / x ]_ C )

Proof

Step Hyp Ref Expression
1 eleq2 
 |-  ( B = C -> ( y e. B <-> y e. C ) )
2 1 alimi 
 |-  ( A. x B = C -> A. x ( y e. B <-> y e. C ) )
3 sbcbi2 
 |-  ( A. x ( y e. B <-> y e. C ) -> ( [. A / x ]. y e. B <-> [. A / x ]. y e. C ) )
4 2 3 syl 
 |-  ( A. x B = C -> ( [. A / x ]. y e. B <-> [. A / x ]. y e. C ) )
5 4 abbidv 
 |-  ( A. x B = C -> { y | [. A / x ]. y e. B } = { y | [. A / x ]. y e. C } )
6 df-csb 
 |-  [_ A / x ]_ B = { y | [. A / x ]. y e. B }
7 df-csb 
 |-  [_ A / x ]_ C = { y | [. A / x ]. y e. C }
8 5 6 7 3eqtr4g 
 |-  ( A. x B = C -> [_ A / x ]_ B = [_ A / x ]_ C )