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

Metamath Proof Explorer

Theorem psdmullem

Description: Lemma for psdmul . Transitive law for union of class difference. (Contributed by SN, 5-May-2025)

Ref Expression
Hypotheses psdmullem.cb ⊢ φ → C ⊆ B
psdmullem.ba ⊢ φ → B ⊆ A
Assertion psdmullem ⊢ φ → A ∖ B ∪ B ∖ C = A ∖ C

Proof

Step Hyp Ref Expression
1 psdmullem.cb ⊢ φ → C ⊆ B
2 psdmullem.ba ⊢ φ → B ⊆ A
3 undif3 ⊢ A ∖ B ∪ B ∖ C = A ∖ B ∪ B ∖ C ∖ A ∖ B
4 undifr ⊢ B ⊆ A ↔ A ∖ B ∪ B = A
5 2 4 sylib ⊢ φ → A ∖ B ∪ B = A
6 difdif2 ⊢ C ∖ A ∖ B = C ∖ A ∪ C ∩ B
7 1 2 sstrd ⊢ φ → C ⊆ A
8 ssdif0 ⊢ C ⊆ A ↔ C ∖ A = ∅
9 7 8 sylib ⊢ φ → C ∖ A = ∅
10 dfss2 ⊢ C ⊆ B ↔ C ∩ B = C
11 1 10 sylib ⊢ φ → C ∩ B = C
12 9 11 uneq12d ⊢ φ → C ∖ A ∪ C ∩ B = ∅ ∪ C
13 0un ⊢ ∅ ∪ C = C
14 12 13 eqtrdi ⊢ φ → C ∖ A ∪ C ∩ B = C
15 6 14 eqtrid ⊢ φ → C ∖ A ∖ B = C
16 5 15 difeq12d ⊢ φ → A ∖ B ∪ B ∖ C ∖ A ∖ B = A ∖ C
17 3 16 eqtrid ⊢ φ → A ∖ B ∪ B ∖ C = A ∖ C