This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

Proof

Step Hyp Ref Expression
1 dfsbcq2 ⊢ ( 𝑧 = 𝐴 → ( [ 𝑧 / 𝑥 ] 𝐵 = 𝐶 ↔ [ 𝐴 / 𝑥 ] 𝐵 = 𝐶 ) )
2 dfsbcq2 ⊢ ( 𝑧 = 𝐴 → ( [ 𝑧 / 𝑥 ] 𝑦 ∈ 𝐵 ↔ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 ) )
3 2 abbidv ⊢ ( 𝑧 = 𝐴 → { 𝑦 ∣ [ 𝑧 / 𝑥 ] 𝑦 ∈ 𝐵 } = { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 } )
4 dfsbcq2 ⊢ ( 𝑧 = 𝐴 → ( [ 𝑧 / 𝑥 ] 𝑦 ∈ 𝐶 ↔ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐶 ) )
5 4 abbidv ⊢ ( 𝑧 = 𝐴 → { 𝑦 ∣ [ 𝑧 / 𝑥 ] 𝑦 ∈ 𝐶 } = { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐶 } )
6 3 5 eqeq12d ⊢ ( 𝑧 = 𝐴 → ( { 𝑦 ∣ [ 𝑧 / 𝑥 ] 𝑦 ∈ 𝐵 } = { 𝑦 ∣ [ 𝑧 / 𝑥 ] 𝑦 ∈ 𝐶 } ↔ { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 } = { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐶 } ) )
7 nfs1v ⊢ Ⅎ 𝑥 [ 𝑧 / 𝑥 ] 𝑦 ∈ 𝐵
8 7 nfab ⊢ Ⅎ 𝑥 { 𝑦 ∣ [ 𝑧 / 𝑥 ] 𝑦 ∈ 𝐵 }
9 nfs1v ⊢ Ⅎ 𝑥 [ 𝑧 / 𝑥 ] 𝑦 ∈ 𝐶
10 9 nfab ⊢ Ⅎ 𝑥 { 𝑦 ∣ [ 𝑧 / 𝑥 ] 𝑦 ∈ 𝐶 }
11 8 10 nfeq ⊢ Ⅎ 𝑥 { 𝑦 ∣ [ 𝑧 / 𝑥 ] 𝑦 ∈ 𝐵 } = { 𝑦 ∣ [ 𝑧 / 𝑥 ] 𝑦 ∈ 𝐶 }
12 sbab ⊢ ( 𝑥 = 𝑧 → 𝐵 = { 𝑦 ∣ [ 𝑧 / 𝑥 ] 𝑦 ∈ 𝐵 } )
13 sbab ⊢ ( 𝑥 = 𝑧 → 𝐶 = { 𝑦 ∣ [ 𝑧 / 𝑥 ] 𝑦 ∈ 𝐶 } )
14 12 13 eqeq12d ⊢ ( 𝑥 = 𝑧 → ( 𝐵 = 𝐶 ↔ { 𝑦 ∣ [ 𝑧 / 𝑥 ] 𝑦 ∈ 𝐵 } = { 𝑦 ∣ [ 𝑧 / 𝑥 ] 𝑦 ∈ 𝐶 } ) )
15 11 14 sbiev ⊢ ( [ 𝑧 / 𝑥 ] 𝐵 = 𝐶 ↔ { 𝑦 ∣ [ 𝑧 / 𝑥 ] 𝑦 ∈ 𝐵 } = { 𝑦 ∣ [ 𝑧 / 𝑥 ] 𝑦 ∈ 𝐶 } )
16 1 6 15 vtoclbg ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] 𝐵 = 𝐶 ↔ { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 } = { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐶 } ) )
17 df-csb ⊢ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 }
18 df-csb ⊢ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 = { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐶 }
19 17 18 eqeq12i ⊢ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ↔ { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 } = { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐶 } )
20 16 19 bitr4di ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] 𝐵 = 𝐶 ↔ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) )