Theorem elpwincl1

Description: Closure of intersection 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	elpwincl1	|- ( ph -> ( A i^i B ) e. ~P C )

Proof

Step	Hyp	Ref	Expression
1		elpwincl.1	|- ( ph -> A e. ~P C )
2		elpwi	|- ( A e. ~P C -> A C_ C )
3		ssinss1	|- ( A C_ C -> ( A i^i B ) C_ C )
4	1 2 3	3syl	|- ( ph -> ( A i^i B ) C_ C )
5		inex1g	|- ( A e. ~P C -> ( A i^i B ) e. _V )
6		elpwg	|- ( ( A i^i B ) e. _V -> ( ( A i^i B ) e. ~P C <-> ( A i^i B ) C_ C ) )
7	1 5 6	3syl	|- ( ph -> ( ( A i^i B ) e. ~P C <-> ( A i^i B ) C_ C ) )
8	4 7	mpbird	|- ( ph -> ( A i^i B ) e. ~P C )