Theorem ntrclsrcomplex

Description: The relative complement of the class S exists as a subset of the base set. (Contributed by RP, 25-Jun-2021)

	Ref	Expression
Hypotheses	ntrclsbex.d	|- D = ( O ` B )
	ntrclsbex.r	|- ( ph -> I D K )
Assertion	ntrclsrcomplex	|- ( ph -> ( B \ S ) e. ~P B )

Proof

Step	Hyp	Ref	Expression
1		ntrclsbex.d	|- D = ( O ` B )
2		ntrclsbex.r	|- ( ph -> I D K )
3	1 2	ntrclsbex	|- ( ph -> B e. _V )
4		difssd	|- ( ph -> ( B \ S ) C_ B )
5	3 4	sselpwd	|- ( ph -> ( B \ S ) e. ~P B )