Metamath Proof Explorer


Theorem csbdif

Description: Distribution of class substitution over difference of two classes. (Contributed by ML, 14-Jul-2020)

Ref Expression
Assertion csbdif 𝐴 / 𝑥 ( 𝐵𝐶 ) = ( 𝐴 / 𝑥 𝐵 𝐴 / 𝑥 𝐶 )

Proof

Step Hyp Ref Expression
1 csbeq1 ( 𝑦 = 𝐴 𝑦 / 𝑥 ( 𝐵𝐶 ) = 𝐴 / 𝑥 ( 𝐵𝐶 ) )
2 csbeq1 ( 𝑦 = 𝐴 𝑦 / 𝑥 𝐵 = 𝐴 / 𝑥 𝐵 )
3 csbeq1 ( 𝑦 = 𝐴 𝑦 / 𝑥 𝐶 = 𝐴 / 𝑥 𝐶 )
4 2 3 difeq12d ( 𝑦 = 𝐴 → ( 𝑦 / 𝑥 𝐵 𝑦 / 𝑥 𝐶 ) = ( 𝐴 / 𝑥 𝐵 𝐴 / 𝑥 𝐶 ) )
5 1 4 eqeq12d ( 𝑦 = 𝐴 → ( 𝑦 / 𝑥 ( 𝐵𝐶 ) = ( 𝑦 / 𝑥 𝐵 𝑦 / 𝑥 𝐶 ) ↔ 𝐴 / 𝑥 ( 𝐵𝐶 ) = ( 𝐴 / 𝑥 𝐵 𝐴 / 𝑥 𝐶 ) ) )
6 vex 𝑦 ∈ V
7 nfcsb1v 𝑥 𝑦 / 𝑥 𝐵
8 nfcsb1v 𝑥 𝑦 / 𝑥 𝐶
9 7 8 nfdif 𝑥 ( 𝑦 / 𝑥 𝐵 𝑦 / 𝑥 𝐶 )
10 csbeq1a ( 𝑥 = 𝑦𝐵 = 𝑦 / 𝑥 𝐵 )
11 csbeq1a ( 𝑥 = 𝑦𝐶 = 𝑦 / 𝑥 𝐶 )
12 10 11 difeq12d ( 𝑥 = 𝑦 → ( 𝐵𝐶 ) = ( 𝑦 / 𝑥 𝐵 𝑦 / 𝑥 𝐶 ) )
13 6 9 12 csbief 𝑦 / 𝑥 ( 𝐵𝐶 ) = ( 𝑦 / 𝑥 𝐵 𝑦 / 𝑥 𝐶 )
14 5 13 vtoclg ( 𝐴 ∈ V → 𝐴 / 𝑥 ( 𝐵𝐶 ) = ( 𝐴 / 𝑥 𝐵 𝐴 / 𝑥 𝐶 ) )
15 dif0 ( ∅ ∖ ∅ ) = ∅
16 15 a1i ( ¬ 𝐴 ∈ V → ( ∅ ∖ ∅ ) = ∅ )
17 csbprc ( ¬ 𝐴 ∈ V → 𝐴 / 𝑥 𝐵 = ∅ )
18 csbprc ( ¬ 𝐴 ∈ V → 𝐴 / 𝑥 𝐶 = ∅ )
19 17 18 difeq12d ( ¬ 𝐴 ∈ V → ( 𝐴 / 𝑥 𝐵 𝐴 / 𝑥 𝐶 ) = ( ∅ ∖ ∅ ) )
20 csbprc ( ¬ 𝐴 ∈ V → 𝐴 / 𝑥 ( 𝐵𝐶 ) = ∅ )
21 16 19 20 3eqtr4rd ( ¬ 𝐴 ∈ V → 𝐴 / 𝑥 ( 𝐵𝐶 ) = ( 𝐴 / 𝑥 𝐵 𝐴 / 𝑥 𝐶 ) )
22 14 21 pm2.61i 𝐴 / 𝑥 ( 𝐵𝐶 ) = ( 𝐴 / 𝑥 𝐵 𝐴 / 𝑥 𝐶 )