Theorem sssymdifcl

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

	Ref	Expression
Hypothesis	ssficl.a	$$⊢A=\left\{z|z\subseteq B\right\}$$
Assertion	sssymdifcl	$$⊢\forall x\in A\forall y\in A\left(x\setminus y\right)\cup \left(y\setminus x\right)\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		vex	$$⊢y\in \mathrm{V}$$
5	4	difexi	$$⊢y\setminus x\in \mathrm{V}$$
6	3 5	unex	$$⊢\left(x\setminus y\right)\cup \left(y\setminus x\right)\in \mathrm{V}$$
7		sseq1	$$⊢z=\left(x\setminus y\right)\cup \left(y\setminus x\right)\to \left(z\subseteq B\leftrightarrow \left(x\setminus y\right)\cup \left(y\setminus x\right)\subseteq B\right)$$
8		sseq1	$$⊢z=x\to \left(z\subseteq B\leftrightarrow x\subseteq B\right)$$
9		sseq1	$$⊢z=y\to \left(z\subseteq B\leftrightarrow y\subseteq B\right)$$
10		ssdifss	$$⊢x\subseteq B\to x\setminus y\subseteq B$$
11		ssdifss	$$⊢y\subseteq B\to y\setminus x\subseteq B$$
12		unss	$$⊢\left(x\setminus y\subseteq B\wedge y\setminus x\subseteq B\right)\leftrightarrow \left(x\setminus y\right)\cup \left(y\setminus x\right)\subseteq B$$
13	12	biimpi	$$⊢\left(x\setminus y\subseteq B\wedge y\setminus x\subseteq B\right)\to \left(x\setminus y\right)\cup \left(y\setminus x\right)\subseteq B$$
14	10 11 13	syl2an	$$⊢\left(x\subseteq B\wedge y\subseteq B\right)\to \left(x\setminus y\right)\cup \left(y\setminus x\right)\subseteq B$$
15	1 6 7 8 9 14	cllem0	$$⊢\forall x\in A\forall y\in A\left(x\setminus y\right)\cup \left(y\setminus x\right)\in A$$