Theorem sselpwd

Description: Elementhood to a power set. (Contributed by Thierry Arnoux, 18-May-2020)

	Ref	Expression
Hypotheses	sselpwd.1	|- ( ph -> B e. V )
	sselpwd.2	|- ( ph -> A C_ B )
Assertion	sselpwd	|- ( ph -> A e. ~P B )

Proof

Step	Hyp	Ref	Expression
1		sselpwd.1	|- ( ph -> B e. V )
2		sselpwd.2	|- ( ph -> A C_ B )
3	1 2	ssexd	|- ( ph -> A e. _V )
4	3 2	elpwd	|- ( ph -> A e. ~P B )