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