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	⊢ 𝐷 = ( 𝑂 ‘ 𝐵 )
	ntrclsbex.r	⊢ ( 𝜑 → 𝐼 𝐷 𝐾 )
Assertion	ntrclsrcomplex	⊢ ( 𝜑 → ( 𝐵 ∖ 𝑆 ) ∈ 𝒫 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		ntrclsbex.d	⊢ 𝐷 = ( 𝑂 ‘ 𝐵 )
2		ntrclsbex.r	⊢ ( 𝜑 → 𝐼 𝐷 𝐾 )
3	1 2	ntrclsbex	⊢ ( 𝜑 → 𝐵 ∈ V )
4		difssd	⊢ ( 𝜑 → ( 𝐵 ∖ 𝑆 ) ⊆ 𝐵 )
5	3 4	sselpwd	⊢ ( 𝜑 → ( 𝐵 ∖ 𝑆 ) ∈ 𝒫 𝐵 )