Metamath Proof Explorer


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 B
Assertion sssymdifcl x A y A x y y x A

Proof

Step Hyp Ref Expression
1 ssficl.a A = z | z B
2 vex x V
3 2 difexi x y V
4 vex y V
5 4 difexi y x V
6 3 5 unex x y y x V
7 sseq1 z = x y y x z B x y y x B
8 sseq1 z = x z B x B
9 sseq1 z = y z B y B
10 ssdifss x B x y B
11 ssdifss y B y x B
12 unss x y B y x B x y y x B
13 12 biimpi x y B y x B x y y x B
14 10 11 13 syl2an x B y B x y y x B
15 1 6 7 8 9 14 cllem0 x A y A x y y x A