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\left(B\right)$$
	ntrclsbex.r	$$⊢\phi \to IDK$$
Assertion	ntrclsrcomplex	$$⊢\phi \to B\setminus S\in 𝒫B$$

Proof

Step	Hyp	Ref	Expression
1		ntrclsbex.d	$$⊢D=O\left(B\right)$$
2		ntrclsbex.r	$$⊢\phi \to IDK$$
3	1 2	ntrclsbex	$$⊢\phi \to B\in \mathrm{V}$$
4		difssd	$$⊢\phi \to B\setminus S\subseteq B$$
5	3 4	sselpwd	$$⊢\phi \to B\setminus S\in 𝒫B$$