Theorem ssdifcl

Description: The class of all subsets of a class is closed under class difference. (Contributed by RP, 3-Jan-2020)

	Ref	Expression
Hypothesis	ssficl.a	$$⊢A=\left\{z|z\subseteq B\right\}$$
Assertion	ssdifcl	$$⊢\forall x\in A\forall y\in Ax\setminus y\in A$$

Proof

Step	Hyp	Ref	Expression
1		ssficl.a	$$⊢A=\left\{z|z\subseteq B\right\}$$
2		vex	$$⊢x\in \mathrm{V}$$
3	2	difexi	$$⊢x\setminus y\in \mathrm{V}$$
4		sseq1	$$⊢z=x\setminus y\to \left(z\subseteq B\leftrightarrow x\setminus y\subseteq B\right)$$
5		sseq1	$$⊢z=x\to \left(z\subseteq B\leftrightarrow x\subseteq B\right)$$
6		sseq1	$$⊢z=y\to \left(z\subseteq B\leftrightarrow y\subseteq B\right)$$
7		ssdifss	$$⊢x\subseteq B\to x\setminus y\subseteq B$$
8	7	adantr	$$⊢\left(x\subseteq B\wedge y\subseteq B\right)\to x\setminus y\subseteq B$$
9	1 3 4 5 6 8	cllem0	$$⊢\forall x\in A\forall y\in Ax\setminus y\in A$$