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 = { z | z C_ B }
Assertion	sssymdifcl	|- A. x e. A A. y e. A ( ( x \ y ) u. ( y \ x ) ) e. A

Proof

Step	Hyp	Ref	Expression
1		ssficl.a	|- A = { z | z C_ B }
2		vex	|- x e. _V
3	2	difexi	|- ( x \ y ) e. _V
4		vex	|- y e. _V
5	4	difexi	|- ( y \ x ) e. _V
6	3 5	unex	|- ( ( x \ y ) u. ( y \ x ) ) e. _V
7		sseq1	|- ( z = ( ( x \ y ) u. ( y \ x ) ) -> ( z C_ B <-> ( ( x \ y ) u. ( y \ x ) ) C_ B ) )
8		sseq1	|- ( z = x -> ( z C_ B <-> x C_ B ) )
9		sseq1	|- ( z = y -> ( z C_ B <-> y C_ B ) )
10		ssdifss	|- ( x C_ B -> ( x \ y ) C_ B )
11		ssdifss	|- ( y C_ B -> ( y \ x ) C_ B )
12		unss	|- ( ( ( x \ y ) C_ B /\ ( y \ x ) C_ B ) <-> ( ( x \ y ) u. ( y \ x ) ) C_ B )
13	12	biimpi	|- ( ( ( x \ y ) C_ B /\ ( y \ x ) C_ B ) -> ( ( x \ y ) u. ( y \ x ) ) C_ B )
14	10 11 13	syl2an	|- ( ( x C_ B /\ y C_ B ) -> ( ( x \ y ) u. ( y \ x ) ) C_ B )
15	1 6 7 8 9 14	cllem0	|- A. x e. A A. y e. A ( ( x \ y ) u. ( y \ x ) ) e. A