Theorem elpwinss

Description: An element of the powerset of B intersected with anything, is a subset of B . (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Assertion	elpwinss	|- ( A e. ( ~P B i^i C ) -> A C_ B )

Proof

Step	Hyp	Ref	Expression
1		elinel1	|- ( A e. ( ~P B i^i C ) -> A e. ~P B )
2	1	elpwid	|- ( A e. ( ~P B i^i C ) -> A C_ B )