Metamath Proof Explorer


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 )