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 C_ B }
Assertion	ssdifcl	|- A. x e. A A. y e. A ( x \ y ) 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		sseq1	|- ( z = ( x \ y ) -> ( z C_ B <-> ( x \ y ) C_ B ) )
5		sseq1	|- ( z = x -> ( z C_ B <-> x C_ B ) )
6		sseq1	|- ( z = y -> ( z C_ B <-> y C_ B ) )
7		ssdifss	|- ( x C_ B -> ( x \ y ) C_ B )
8	7	adantr	|- ( ( x C_ B /\ y C_ B ) -> ( x \ y ) C_ B )
9	1 3 4 5 6 8	cllem0	|- A. x e. A A. y e. A ( x \ y ) e. A