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