Theorem neicvgrcomplex

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

	Ref	Expression
Hypotheses	neicvgbex.d	$$⊢D=P\left(B\right)$$
	neicvgbex.h	$$⊢H=F\circ \left(D\circ G\right)$$
	neicvgbex.r	$$⊢\phi \to NHM$$
Assertion	neicvgrcomplex	$$⊢\phi \to B\setminus S\in 𝒫B$$

Proof

Step	Hyp	Ref	Expression
1		neicvgbex.d	$$⊢D=P\left(B\right)$$
2		neicvgbex.h	$$⊢H=F\circ \left(D\circ G\right)$$
3		neicvgbex.r	$$⊢\phi \to NHM$$
4	1 2 3	neicvgbex	$$⊢\phi \to B\in \mathrm{V}$$
5		difssd	$$⊢\phi \to B\setminus S\subseteq B$$
6	4 5	sselpwd	$$⊢\phi \to B\setminus S\in 𝒫B$$