Theorem bj-sbeq

Description: Distribute proper substitution through an equality relation. (See sbceqg ). (Contributed by BJ, 6-Oct-2018)

	Ref	Expression
Assertion	bj-sbeq	⊢ ( [ 𝑦 / 𝑥 ] 𝐴 = 𝐵 ↔ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 = ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		dfcleq	⊢ ( 𝐴 = 𝐵 ↔ ∀ 𝑧 ( 𝑧 ∈ 𝐴 ↔ 𝑧 ∈ 𝐵 ) )
2	1	sbbii	⊢ ( [ 𝑦 / 𝑥 ] 𝐴 = 𝐵 ↔ [ 𝑦 / 𝑥 ] ∀ 𝑧 ( 𝑧 ∈ 𝐴 ↔ 𝑧 ∈ 𝐵 ) )
3		sbsbc	⊢ ( [ 𝑦 / 𝑥 ] ∀ 𝑧 ( 𝑧 ∈ 𝐴 ↔ 𝑧 ∈ 𝐵 ) ↔ [ 𝑦 / 𝑥 ] ∀ 𝑧 ( 𝑧 ∈ 𝐴 ↔ 𝑧 ∈ 𝐵 ) )
4		sbcal	⊢ ( [ 𝑦 / 𝑥 ] ∀ 𝑧 ( 𝑧 ∈ 𝐴 ↔ 𝑧 ∈ 𝐵 ) ↔ ∀ 𝑧 [ 𝑦 / 𝑥 ] ( 𝑧 ∈ 𝐴 ↔ 𝑧 ∈ 𝐵 ) )
5	2 3 4	3bitri	⊢ ( [ 𝑦 / 𝑥 ] 𝐴 = 𝐵 ↔ ∀ 𝑧 [ 𝑦 / 𝑥 ] ( 𝑧 ∈ 𝐴 ↔ 𝑧 ∈ 𝐵 ) )
6		sbcbig	⊢ ( 𝑦 ∈ V → ( [ 𝑦 / 𝑥 ] ( 𝑧 ∈ 𝐴 ↔ 𝑧 ∈ 𝐵 ) ↔ ( [ 𝑦 / 𝑥 ] 𝑧 ∈ 𝐴 ↔ [ 𝑦 / 𝑥 ] 𝑧 ∈ 𝐵 ) ) )
7	6	elv	⊢ ( [ 𝑦 / 𝑥 ] ( 𝑧 ∈ 𝐴 ↔ 𝑧 ∈ 𝐵 ) ↔ ( [ 𝑦 / 𝑥 ] 𝑧 ∈ 𝐴 ↔ [ 𝑦 / 𝑥 ] 𝑧 ∈ 𝐵 ) )
8	7	albii	⊢ ( ∀ 𝑧 [ 𝑦 / 𝑥 ] ( 𝑧 ∈ 𝐴 ↔ 𝑧 ∈ 𝐵 ) ↔ ∀ 𝑧 ( [ 𝑦 / 𝑥 ] 𝑧 ∈ 𝐴 ↔ [ 𝑦 / 𝑥 ] 𝑧 ∈ 𝐵 ) )
9		sbcel2	⊢ ( [ 𝑦 / 𝑥 ] 𝑧 ∈ 𝐴 ↔ 𝑧 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 )
10		sbcel2	⊢ ( [ 𝑦 / 𝑥 ] 𝑧 ∈ 𝐵 ↔ 𝑧 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
11	9 10	bibi12i	⊢ ( ( [ 𝑦 / 𝑥 ] 𝑧 ∈ 𝐴 ↔ [ 𝑦 / 𝑥 ] 𝑧 ∈ 𝐵 ) ↔ ( 𝑧 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ↔ 𝑧 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) )
12	11	albii	⊢ ( ∀ 𝑧 ( [ 𝑦 / 𝑥 ] 𝑧 ∈ 𝐴 ↔ [ 𝑦 / 𝑥 ] 𝑧 ∈ 𝐵 ) ↔ ∀ 𝑧 ( 𝑧 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ↔ 𝑧 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) )
13	5 8 12	3bitri	⊢ ( [ 𝑦 / 𝑥 ] 𝐴 = 𝐵 ↔ ∀ 𝑧 ( 𝑧 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ↔ 𝑧 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) )
14		dfcleq	⊢ ( ⦋ 𝑦 / 𝑥 ⦌ 𝐴 = ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ↔ ∀ 𝑧 ( 𝑧 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ↔ 𝑧 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) )
15	13 14	bitr4i	⊢ ( [ 𝑦 / 𝑥 ] 𝐴 = 𝐵 ↔ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 = ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )