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 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 B [˙A / x]˙ y B
3 2 abbidv z = A y | z x y B = y | [˙A / x]˙ y B
4 dfsbcq2 z = A z x y C [˙A / x]˙ y C
5 4 abbidv z = A y | z x y C = y | [˙A / x]˙ y C
6 3 5 eqeq12d z = A y | z x y B = y | z x y C y | [˙A / x]˙ y B = y | [˙A / x]˙ y C
7 nfs1v x z x y B
8 7 nfab _ x y | z x y B
9 nfs1v x z x y C
10 9 nfab _ x y | z x y C
11 8 10 nfeq x y | z x y B = y | z x y C
12 sbab x = z B = y | z x y B
13 sbab x = z C = y | z x y C
14 12 13 eqeq12d x = z B = C y | z x y B = y | z x y C
15 11 14 sbiev z x B = C y | z x y B = y | z x y C
16 1 6 15 vtoclbg A V [˙A / x]˙ B = C y | [˙A / x]˙ y B = y | [˙A / x]˙ y C
17 df-csb A / x B = y | [˙A / x]˙ y B
18 df-csb A / x C = y | [˙A / x]˙ y C
19 17 18 eqeq12i A / x B = A / x C y | [˙A / x]˙ y B = y | [˙A / x]˙ y C
20 16 19 bitr4di A V [˙A / x]˙ B = C A / x B = A / x C