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 φCB
psdmullem.ba φBA
Assertion psdmullem φABBC=AC

Proof

Step Hyp Ref Expression
1 psdmullem.cb φCB
2 psdmullem.ba φBA
3 undif3 ABBC=ABBCAB
4 undifr BAABB=A
5 2 4 sylib φABB=A
6 difdif2 CAB=CACB
7 1 2 sstrd φCA
8 ssdif0 CACA=
9 7 8 sylib φCA=
10 dfss2 CBCB=C
11 1 10 sylib φCB=C
12 9 11 uneq12d φCACB=C
13 0un C=C
14 12 13 eqtrdi φCACB=C
15 6 14 eqtrid φCAB=C
16 5 15 difeq12d φABBCAB=AC
17 3 16 eqtrid φABBC=AC