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