Metamath Proof Explorer


Theorem bj-sbceqgALT

Description: Distribute proper substitution through an equality relation. Alternate proof of sbceqg . (Contributed by BJ, 6-Oct-2018) Proof modification is discouraged to avoid using sbceqg , but the Metamath program "MM-PA> MINIMIZE__WITH * / EXCEPT sbceqg" command is ok. (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion bj-sbceqgALT A V [˙A / x]˙ B = C A / x B = A / x C

Proof

Step Hyp Ref Expression
1 dfcleq B = C y y B y C
2 1 sbcth A V [˙A / x]˙ B = C y y B y C
3 sbcbig A V [˙A / x]˙ B = C y y B y C [˙A / x]˙ B = C [˙A / x]˙ y y B y C
4 2 3 mpbid A V [˙A / x]˙ B = C [˙A / x]˙ y y B y C
5 sbcal [˙A / x]˙ y y B y C y [˙A / x]˙ y B y C
6 4 5 bitrdi A V [˙A / x]˙ B = C y [˙A / x]˙ y B y C
7 sbcbig A V [˙A / x]˙ y B y C [˙A / x]˙ y B [˙A / x]˙ y C
8 7 albidv A V y [˙A / x]˙ y B y C y [˙A / x]˙ y B [˙A / x]˙ y C
9 sbcel2 [˙A / x]˙ y B y A / x B
10 9 a1i A V [˙A / x]˙ y B y A / x B
11 sbcel2 [˙A / x]˙ y C y A / x C
12 11 a1i A V [˙A / x]˙ y C y A / x C
13 10 12 bibi12d A V [˙A / x]˙ y B [˙A / x]˙ y C y A / x B y A / x C
14 13 albidv A V y [˙A / x]˙ y B [˙A / x]˙ y C y y A / x B y A / x C
15 6 8 14 3bitrd A V [˙A / x]˙ B = C y y A / x B y A / x C
16 dfcleq A / x B = A / x C y y A / x B y A / x C
17 15 16 bitr4di A V [˙A / x]˙ B = C A / x B = A / x C