Metamath Proof Explorer

Theorem csbin

Description: Distribute proper substitution into a class through an intersection relation. (Contributed by Alan Sare, 22-Jul-2012) (Revised by NM, 18-Aug-2018)

Ref Expression
Assertion csbin ⦋ 𝐴 / 𝑥 ⦌ ( 𝐵 ∩ 𝐶 ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 )

Proof

Step Hyp Ref Expression
1 csbeq1 ⊢ ( 𝑦 = 𝐴 → ⦋ 𝑦 / 𝑥 ⦌ ( 𝐵 ∩ 𝐶 ) = ⦋ 𝐴 / 𝑥 ⦌ ( 𝐵 ∩ 𝐶 ) )
2 csbeq1 ⊢ ( 𝑦 = 𝐴 → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 = ⦋ 𝐴 / 𝑥 ⦌ 𝐵 )
3 csbeq1 ⊢ ( 𝑦 = 𝐴 → ⦋ 𝑦 / 𝑥 ⦌ 𝐶 = ⦋ 𝐴 / 𝑥 ⦌ 𝐶 )
4 2 3 ineq12d ⊢ ( 𝑦 = 𝐴 → ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) )
5 1 4 eqeq12d ⊢ ( 𝑦 = 𝐴 → ( ⦋ 𝑦 / 𝑥 ⦌ ( 𝐵 ∩ 𝐶 ) = ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) ↔ ⦋ 𝐴 / 𝑥 ⦌ ( 𝐵 ∩ 𝐶 ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) )
6 vex ⊢ 𝑦 ∈ V
7 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐵
8 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐶
9 7 8 nfin ⊢ Ⅎ 𝑥 ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 )
10 csbeq1a ⊢ ( 𝑥 = 𝑦 → 𝐵 = ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
11 csbeq1a ⊢ ( 𝑥 = 𝑦 → 𝐶 = ⦋ 𝑦 / 𝑥 ⦌ 𝐶 )
12 10 11 ineq12d ⊢ ( 𝑥 = 𝑦 → ( 𝐵 ∩ 𝐶 ) = ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) )
13 6 9 12 csbief ⊢ ⦋ 𝑦 / 𝑥 ⦌ ( 𝐵 ∩ 𝐶 ) = ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 )
14 5 13 vtoclg ⊢ ( 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ ( 𝐵 ∩ 𝐶 ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) )
15 csbprc ⊢ ( ¬ 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ ( 𝐵 ∩ 𝐶 ) = ∅ )
16 csbprc ⊢ ( ¬ 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = ∅ )
17 csbprc ⊢ ( ¬ 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ 𝐶 = ∅ )
18 16 17 ineq12d ⊢ ( ¬ 𝐴 ∈ V → ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) = ( ∅ ∩ ∅ ) )
19 in0 ⊢ ( ∅ ∩ ∅ ) = ∅
20 18 19 eqtr2di ⊢ ( ¬ 𝐴 ∈ V → ∅ = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) )
21 15 20 eqtrd ⊢ ( ¬ 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ ( 𝐵 ∩ 𝐶 ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) )
22 14 21 pm2.61i ⊢ ⦋ 𝐴 / 𝑥 ⦌ ( 𝐵 ∩ 𝐶 ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 )