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

Metamath Proof Explorer

Theorem sbcel12

Description: Distribute proper substitution through a membership relation. (Contributed by NM, 10-Nov-2005) (Revised by NM, 18-Aug-2018)

Ref Expression
Assertion sbcel12 ( [ 𝐴 / 𝑥 ] 𝐵 ∈ 𝐶 ↔ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 )

Proof

Step Hyp Ref Expression
1 dfsbcq2 ⊢ ( 𝑧 = 𝐴 → ( [ 𝑧 / 𝑥 ] 𝐵 ∈ 𝐶 ↔ [ 𝐴 / 𝑥 ] 𝐵 ∈ 𝐶 ) )
2 dfsbcq2 ⊢ ( 𝑧 = 𝐴 → ( [ 𝑧 / 𝑥 ] 𝑦 ∈ 𝐵 ↔ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 ) )
3 2 abbidv ⊢ ( 𝑧 = 𝐴 → { 𝑦 ∣ [ 𝑧 / 𝑥 ] 𝑦 ∈ 𝐵 } = { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 } )
4 dfsbcq2 ⊢ ( 𝑧 = 𝐴 → ( [ 𝑧 / 𝑥 ] 𝑦 ∈ 𝐶 ↔ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐶 ) )
5 4 abbidv ⊢ ( 𝑧 = 𝐴 → { 𝑦 ∣ [ 𝑧 / 𝑥 ] 𝑦 ∈ 𝐶 } = { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐶 } )
6 3 5 eleq12d ⊢ ( 𝑧 = 𝐴 → ( { 𝑦 ∣ [ 𝑧 / 𝑥 ] 𝑦 ∈ 𝐵 } ∈ { 𝑦 ∣ [ 𝑧 / 𝑥 ] 𝑦 ∈ 𝐶 } ↔ { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 } ∈ { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐶 } ) )
7 nfs1v ⊢ Ⅎ 𝑥 [ 𝑧 / 𝑥 ] 𝑦 ∈ 𝐵
8 7 nfab ⊢ Ⅎ 𝑥 { 𝑦 ∣ [ 𝑧 / 𝑥 ] 𝑦 ∈ 𝐵 }
9 nfs1v ⊢ Ⅎ 𝑥 [ 𝑧 / 𝑥 ] 𝑦 ∈ 𝐶
10 9 nfab ⊢ Ⅎ 𝑥 { 𝑦 ∣ [ 𝑧 / 𝑥 ] 𝑦 ∈ 𝐶 }
11 8 10 nfel ⊢ Ⅎ 𝑥 { 𝑦 ∣ [ 𝑧 / 𝑥 ] 𝑦 ∈ 𝐵 } ∈ { 𝑦 ∣ [ 𝑧 / 𝑥 ] 𝑦 ∈ 𝐶 }
12 sbab ⊢ ( 𝑥 = 𝑧 → 𝐵 = { 𝑦 ∣ [ 𝑧 / 𝑥 ] 𝑦 ∈ 𝐵 } )
13 sbab ⊢ ( 𝑥 = 𝑧 → 𝐶 = { 𝑦 ∣ [ 𝑧 / 𝑥 ] 𝑦 ∈ 𝐶 } )
14 12 13 eleq12d ⊢ ( 𝑥 = 𝑧 → ( 𝐵 ∈ 𝐶 ↔ { 𝑦 ∣ [ 𝑧 / 𝑥 ] 𝑦 ∈ 𝐵 } ∈ { 𝑦 ∣ [ 𝑧 / 𝑥 ] 𝑦 ∈ 𝐶 } ) )
15 11 14 sbiev ⊢ ( [ 𝑧 / 𝑥 ] 𝐵 ∈ 𝐶 ↔ { 𝑦 ∣ [ 𝑧 / 𝑥 ] 𝑦 ∈ 𝐵 } ∈ { 𝑦 ∣ [ 𝑧 / 𝑥 ] 𝑦 ∈ 𝐶 } )
16 1 6 15 vtoclbg ⊢ ( 𝐴 ∈ V → ( [ 𝐴 / 𝑥 ] 𝐵 ∈ 𝐶 ↔ { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 } ∈ { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐶 } ) )
17 df-csb ⊢ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 }
18 df-csb ⊢ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 = { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐶 }
19 17 18 eleq12i ⊢ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ↔ { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 } ∈ { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐶 } )
20 16 19 bitr4di ⊢ ( 𝐴 ∈ V → ( [ 𝐴 / 𝑥 ] 𝐵 ∈ 𝐶 ↔ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) )
21 sbcex ⊢ ( [ 𝐴 / 𝑥 ] 𝐵 ∈ 𝐶 → 𝐴 ∈ V )
22 21 con3i ⊢ ( ¬ 𝐴 ∈ V → ¬ [ 𝐴 / 𝑥 ] 𝐵 ∈ 𝐶 )
23 noel ⊢ ¬ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∈ ∅
24 csbprc ⊢ ( ¬ 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ 𝐶 = ∅ )
25 24 eleq2d ⊢ ( ¬ 𝐴 ∈ V → ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ↔ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∈ ∅ ) )
26 23 25 mtbiri ⊢ ( ¬ 𝐴 ∈ V → ¬ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 )
27 22 26 2falsed ⊢ ( ¬ 𝐴 ∈ V → ( [ 𝐴 / 𝑥 ] 𝐵 ∈ 𝐶 ↔ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) )
28 20 27 pm2.61i ⊢ ( [ 𝐴 / 𝑥 ] 𝐵 ∈ 𝐶 ↔ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 )