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

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