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