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

Metamath Proof Explorer

Theorem sbceqg

Description: Distribute proper substitution through an equality relation. (Contributed by NM, 10-Nov-2005) (Proof shortened by Andrew Salmon, 29-Jun-2011)

Ref Expression
Assertion sbceqg 
|- ( A e. V -> ( [. A / x ]. B = C <-> [_ A / x ]_ B = [_ A / x ]_ C ) )

Proof

Step Hyp Ref Expression
1 dfsbcq2 
 |-  ( z = A -> ( [ z / x ] B = C <-> [. A / x ]. B = C ) )
2 dfsbcq2 
 |-  ( z = A -> ( [ z / x ] y e. B <-> [. A / x ]. y e. B ) )
3 2 abbidv 
 |-  ( z = A -> { y | [ z / x ] y e. B } = { y | [. A / x ]. y e. B } )
4 dfsbcq2 
 |-  ( z = A -> ( [ z / x ] y e. C <-> [. A / x ]. y e. C ) )
5 4 abbidv 
 |-  ( z = A -> { y | [ z / x ] y e. C } = { y | [. A / x ]. y e. C } )
6 3 5 eqeq12d 
 |-  ( z = A -> ( { y | [ z / x ] y e. B } = { y | [ z / x ] y e. C } <-> { y | [. A / x ]. y e. B } = { y | [. A / x ]. y e. C } ) )
7 nfs1v 
 |-  F/ x [ z / x ] y e. B
8 7 nfab 
 |-  F/_ x { y | [ z / x ] y e. B }
9 nfs1v 
 |-  F/ x [ z / x ] y e. C
10 9 nfab 
 |-  F/_ x { y | [ z / x ] y e. C }
11 8 10 nfeq 
 |-  F/ x { y | [ z / x ] y e. B } = { y | [ z / x ] y e. C }
12 sbab 
 |-  ( x = z -> B = { y | [ z / x ] y e. B } )
13 sbab 
 |-  ( x = z -> C = { y | [ z / x ] y e. C } )
14 12 13 eqeq12d 
 |-  ( x = z -> ( B = C <-> { y | [ z / x ] y e. B } = { y | [ z / x ] y e. C } ) )
15 11 14 sbiev 
 |-  ( [ z / x ] B = C <-> { y | [ z / x ] y e. B } = { y | [ z / x ] y e. C } )
16 1 6 15 vtoclbg 
 |-  ( A e. V -> ( [. A / x ]. B = C <-> { y | [. A / x ]. y e. B } = { y | [. A / x ]. y e. C } ) )
17 df-csb 
 |-  [_ A / x ]_ B = { y | [. A / x ]. y e. B }
18 df-csb 
 |-  [_ A / x ]_ C = { y | [. A / x ]. y e. C }
19 17 18 eqeq12i 
 |-  ( [_ A / x ]_ B = [_ A / x ]_ C <-> { y | [. A / x ]. y e. B } = { y | [. A / x ]. y e. C } )
20 16 19 bitr4di 
 |-  ( A e. V -> ( [. A / x ]. B = C <-> [_ A / x ]_ B = [_ A / x ]_ C ) )