Metamath Proof Explorer

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 φ I D K
Assertion ntrclsrcomplex φ B S 𝒫 B


Step Hyp Ref Expression
1 ntrclsbex.d D = O B
2 ntrclsbex.r φ I D K
3 1 2 ntrclsbex φ B V
4 difssd φ B S B
5 3 4 sselpwd φ B S 𝒫 B