Description: Lemma for psdmul . Transitive law for union of class difference. (Contributed by SN, 5-May-2025)
Ref | Expression | ||
---|---|---|---|
Hypotheses | psdmullem.cb | |
|
psdmullem.ba | |
||
Assertion | psdmullem | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | psdmullem.cb | |
|
2 | psdmullem.ba | |
|
3 | undif3 | |
|
4 | undifr | |
|
5 | 2 4 | sylib | |
6 | difdif2 | |
|
7 | 1 2 | sstrd | |
8 | ssdif0 | |
|
9 | 7 8 | sylib | |
10 | dfss2 | |
|
11 | 1 10 | sylib | |
12 | 9 11 | uneq12d | |
13 | 0un | |
|
14 | 12 13 | eqtrdi | |
15 | 6 14 | eqtrid | |
16 | 5 15 | difeq12d | |
17 | 3 16 | eqtrid | |