Theorem elpwdifcl

Description: Closure of class difference with regard to elementhood to a power set. (Contributed by Thierry Arnoux, 18-May-2020)

	Ref	Expression
Hypothesis	elpwincl.1	|- ( ph -> A e. ~P C )
Assertion	elpwdifcl	|- ( ph -> ( A \ B ) e. ~P C )

Proof

Step	Hyp	Ref	Expression
1		elpwincl.1	|- ( ph -> A e. ~P C )
2	1	elpwid	|- ( ph -> A C_ C )
3	2	ssdifssd	|- ( ph -> ( A \ B ) C_ C )
4		difexg	|- ( A e. ~P C -> ( A \ B ) e. _V )
5		elpwg	|- ( ( A \ B ) e. _V -> ( ( A \ B ) e. ~P C <-> ( A \ B ) C_ C ) )
6	1 4 5	3syl	|- ( ph -> ( ( A \ B ) e. ~P C <-> ( A \ B ) C_ C ) )
7	3 6	mpbird	|- ( ph -> ( A \ B ) e. ~P C )