Metamath Proof Explorer


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 = z | z B
Assertion ssdifcl x A y A x y A

Proof

Step Hyp Ref Expression
1 ssficl.a A = z | z B
2 vex x V
3 2 difexi x y V
4 sseq1 z = x y z B x y B
5 sseq1 z = x z B x B
6 sseq1 z = y z B y B
7 ssdifss x B x y B
8 7 adantr x B y B x y B
9 1 3 4 5 6 8 cllem0 x A y A x y A