Theorem psdmullem

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

	Ref	Expression
Hypotheses	psdmullem.cb	|- ( ph -> C C_ B )
	psdmullem.ba	|- ( ph -> B C_ A )
Assertion	psdmullem	|- ( ph -> ( ( A \ B ) u. ( B \ C ) ) = ( A \ C ) )

Proof

Step	Hyp	Ref	Expression
1		psdmullem.cb	|- ( ph -> C C_ B )
2		psdmullem.ba	|- ( ph -> B C_ A )
3		undif3	|- ( ( A \ B ) u. ( B \ C ) ) = ( ( ( A \ B ) u. B ) \ ( C \ ( A \ B ) ) )
4		undifr	|- ( B C_ A <-> ( ( A \ B ) u. B ) = A )
5	2 4	sylib	|- ( ph -> ( ( A \ B ) u. B ) = A )
6		difdif2	|- ( C \ ( A \ B ) ) = ( ( C \ A ) u. ( C i^i B ) )
7	1 2	sstrd	|- ( ph -> C C_ A )
8		ssdif0	|- ( C C_ A <-> ( C \ A ) = (/) )
9	7 8	sylib	|- ( ph -> ( C \ A ) = (/) )
10		dfss2	|- ( C C_ B <-> ( C i^i B ) = C )
11	1 10	sylib	|- ( ph -> ( C i^i B ) = C )
12	9 11	uneq12d	|- ( ph -> ( ( C \ A ) u. ( C i^i B ) ) = ( (/) u. C ) )
13		0un	|- ( (/) u. C ) = C
14	12 13	eqtrdi	|- ( ph -> ( ( C \ A ) u. ( C i^i B ) ) = C )
15	6 14	eqtrid	|- ( ph -> ( C \ ( A \ B ) ) = C )
16	5 15	difeq12d	|- ( ph -> ( ( ( A \ B ) u. B ) \ ( C \ ( A \ B ) ) ) = ( A \ C ) )
17	3 16	eqtrid	|- ( ph -> ( ( A \ B ) u. ( B \ C ) ) = ( A \ C ) )