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 ( 𝐴𝑉 → ( [ 𝐴 / 𝑥 ] 𝐵 = 𝐶 𝐴 / 𝑥 𝐵 = 𝐴 / 𝑥 𝐶 ) )

Proof

Step Hyp Ref Expression
1 dfcleq ( 𝐵 = 𝐶 ↔ ∀ 𝑦 ( 𝑦𝐵𝑦𝐶 ) )
2 1 sbcth ( 𝐴𝑉[ 𝐴 / 𝑥 ] ( 𝐵 = 𝐶 ↔ ∀ 𝑦 ( 𝑦𝐵𝑦𝐶 ) ) )
3 sbcbig ( 𝐴𝑉 → ( [ 𝐴 / 𝑥 ] ( 𝐵 = 𝐶 ↔ ∀ 𝑦 ( 𝑦𝐵𝑦𝐶 ) ) ↔ ( [ 𝐴 / 𝑥 ] 𝐵 = 𝐶[ 𝐴 / 𝑥 ]𝑦 ( 𝑦𝐵𝑦𝐶 ) ) ) )
4 2 3 mpbid ( 𝐴𝑉 → ( [ 𝐴 / 𝑥 ] 𝐵 = 𝐶[ 𝐴 / 𝑥 ]𝑦 ( 𝑦𝐵𝑦𝐶 ) ) )
5 sbcal ( [ 𝐴 / 𝑥 ]𝑦 ( 𝑦𝐵𝑦𝐶 ) ↔ ∀ 𝑦 [ 𝐴 / 𝑥 ] ( 𝑦𝐵𝑦𝐶 ) )
6 4 5 bitrdi ( 𝐴𝑉 → ( [ 𝐴 / 𝑥 ] 𝐵 = 𝐶 ↔ ∀ 𝑦 [ 𝐴 / 𝑥 ] ( 𝑦𝐵𝑦𝐶 ) ) )
7 sbcbig ( 𝐴𝑉 → ( [ 𝐴 / 𝑥 ] ( 𝑦𝐵𝑦𝐶 ) ↔ ( [ 𝐴 / 𝑥 ] 𝑦𝐵[ 𝐴 / 𝑥 ] 𝑦𝐶 ) ) )
8 7 albidv ( 𝐴𝑉 → ( ∀ 𝑦 [ 𝐴 / 𝑥 ] ( 𝑦𝐵𝑦𝐶 ) ↔ ∀ 𝑦 ( [ 𝐴 / 𝑥 ] 𝑦𝐵[ 𝐴 / 𝑥 ] 𝑦𝐶 ) ) )
9 sbcel2 ( [ 𝐴 / 𝑥 ] 𝑦𝐵𝑦 𝐴 / 𝑥 𝐵 )
10 9 a1i ( 𝐴𝑉 → ( [ 𝐴 / 𝑥 ] 𝑦𝐵𝑦 𝐴 / 𝑥 𝐵 ) )
11 sbcel2 ( [ 𝐴 / 𝑥 ] 𝑦𝐶𝑦 𝐴 / 𝑥 𝐶 )
12 11 a1i ( 𝐴𝑉 → ( [ 𝐴 / 𝑥 ] 𝑦𝐶𝑦 𝐴 / 𝑥 𝐶 ) )
13 10 12 bibi12d ( 𝐴𝑉 → ( ( [ 𝐴 / 𝑥 ] 𝑦𝐵[ 𝐴 / 𝑥 ] 𝑦𝐶 ) ↔ ( 𝑦 𝐴 / 𝑥 𝐵𝑦 𝐴 / 𝑥 𝐶 ) ) )
14 13 albidv ( 𝐴𝑉 → ( ∀ 𝑦 ( [ 𝐴 / 𝑥 ] 𝑦𝐵[ 𝐴 / 𝑥 ] 𝑦𝐶 ) ↔ ∀ 𝑦 ( 𝑦 𝐴 / 𝑥 𝐵𝑦 𝐴 / 𝑥 𝐶 ) ) )
15 6 8 14 3bitrd ( 𝐴𝑉 → ( [ 𝐴 / 𝑥 ] 𝐵 = 𝐶 ↔ ∀ 𝑦 ( 𝑦 𝐴 / 𝑥 𝐵𝑦 𝐴 / 𝑥 𝐶 ) ) )
16 dfcleq ( 𝐴 / 𝑥 𝐵 = 𝐴 / 𝑥 𝐶 ↔ ∀ 𝑦 ( 𝑦 𝐴 / 𝑥 𝐵𝑦 𝐴 / 𝑥 𝐶 ) )
17 15 16 bitr4di ( 𝐴𝑉 → ( [ 𝐴 / 𝑥 ] 𝐵 = 𝐶 𝐴 / 𝑥 𝐵 = 𝐴 / 𝑥 𝐶 ) )