Theorem psdmullem

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

	Ref	Expression
Hypotheses	psdmullem.cb	$$⊢\phi \to C\subseteq B$$
	psdmullem.ba	$$⊢\phi \to B\subseteq A$$
Assertion	psdmullem	$$⊢\phi \to \left(A\setminus B\right)\cup \left(B\setminus C\right)=A\setminus C$$

Proof

Step	Hyp	Ref	Expression
1		psdmullem.cb	$$⊢\phi \to C\subseteq B$$
2		psdmullem.ba	$$⊢\phi \to B\subseteq A$$
3		undif3	$$⊢\left(A\setminus B\right)\cup \left(B\setminus C\right)=\left(\left(A\setminus B\right)\cup B\right)\setminus \left(C\setminus \left(A\setminus B\right)\right)$$
4		undifr	$$⊢B\subseteq A\leftrightarrow \left(A\setminus B\right)\cup B=A$$
5	2 4	sylib	$$⊢\phi \to \left(A\setminus B\right)\cup B=A$$
6		difdif2	$$⊢C\setminus \left(A\setminus B\right)=\left(C\setminus A\right)\cup \left(C\cap B\right)$$
7	1 2	sstrd	$$⊢\phi \to C\subseteq A$$
8		ssdif0	$$⊢C\subseteq A\leftrightarrow C\setminus A=\varnothing$$
9	7 8	sylib	$$⊢\phi \to C\setminus A=\varnothing$$
10		dfss2	$$⊢C\subseteq B\leftrightarrow C\cap B=C$$
11	1 10	sylib	$$⊢\phi \to C\cap B=C$$
12	9 11	uneq12d	$$⊢\phi \to \left(C\setminus A\right)\cup \left(C\cap B\right)=\varnothing \cup C$$
13		0un	$$⊢\varnothing \cup C=C$$
14	12 13	eqtrdi	$$⊢\phi \to \left(C\setminus A\right)\cup \left(C\cap B\right)=C$$
15	6 14	eqtrid	$$⊢\phi \to C\setminus \left(A\setminus B\right)=C$$
16	5 15	difeq12d	$$⊢\phi \to \left(\left(A\setminus B\right)\cup B\right)\setminus \left(C\setminus \left(A\setminus B\right)\right)=A\setminus C$$
17	3 16	eqtrid	$$⊢\phi \to \left(A\setminus B\right)\cup \left(B\setminus C\right)=A\setminus C$$