Theorem difres

Description: Case when class difference in unaffected by restriction. (Contributed by Thierry Arnoux, 1-Jan-2020)

	Ref	Expression
Assertion	difres	$$⊢A\subseteq B\times \mathrm{V}\to A\setminus \left({C\upharpoonright }_B\right)=A\setminus C$$

Proof

Step	Hyp	Ref	Expression
1		df-res	$$⊢{C\upharpoonright }_B=C\cap \left(B\times \mathrm{V}\right)$$
2	1	difeq2i	$$⊢A\setminus \left({C\upharpoonright }_B\right)=A\setminus \left(C\cap \left(B\times \mathrm{V}\right)\right)$$
3		difindi	$$⊢A\setminus \left(C\cap \left(B\times \mathrm{V}\right)\right)=\left(A\setminus C\right)\cup \left(A\setminus \left(B\times \mathrm{V}\right)\right)$$
4		ssdif	$$⊢A\subseteq B\times \mathrm{V}\to A\setminus \left(B\times \mathrm{V}\right)\subseteq \left(B\times \mathrm{V}\right)\setminus \left(B\times \mathrm{V}\right)$$
5		difid	$$⊢\left(B\times \mathrm{V}\right)\setminus \left(B\times \mathrm{V}\right)=\varnothing$$
6	4 5	sseqtrdi	$$⊢A\subseteq B\times \mathrm{V}\to A\setminus \left(B\times \mathrm{V}\right)\subseteq \varnothing$$
7		ss0	$$⊢A\setminus \left(B\times \mathrm{V}\right)\subseteq \varnothing \to A\setminus \left(B\times \mathrm{V}\right)=\varnothing$$
8	6 7	syl	$$⊢A\subseteq B\times \mathrm{V}\to A\setminus \left(B\times \mathrm{V}\right)=\varnothing$$
9	8	uneq2d	$$⊢A\subseteq B\times \mathrm{V}\to \left(A\setminus C\right)\cup \left(A\setminus \left(B\times \mathrm{V}\right)\right)=\left(A\setminus C\right)\cup \varnothing$$
10	3 9	eqtrid	$$⊢A\subseteq B\times \mathrm{V}\to A\setminus \left(C\cap \left(B\times \mathrm{V}\right)\right)=\left(A\setminus C\right)\cup \varnothing$$
11		un0	$$⊢\left(A\setminus C\right)\cup \varnothing =A\setminus C$$
12	10 11	eqtrdi	$$⊢A\subseteq B\times \mathrm{V}\to A\setminus \left(C\cap \left(B\times \mathrm{V}\right)\right)=A\setminus C$$
13	2 12	eqtrid	$$⊢A\subseteq B\times \mathrm{V}\to A\setminus \left({C\upharpoonright }_B\right)=A\setminus C$$