Theorem elpwinss 45171

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

Assertion

Ref	Expression
elpwinss	⊢ (𝐴 ∈ (𝒫 𝐵 ∩ 𝐶) → 𝐴 ⊆ 𝐵)

Proof of Theorem elpwinss

Step	Hyp	Ref	Expression
1		elinel1 4150	. 2 ⊢ (𝐴 ∈ (𝒫 𝐵 ∩ 𝐶) → 𝐴 ∈ 𝒫 𝐵)
2	1	elpwid 4558	1 ⊢ (𝐴 ∈ (𝒫 𝐵 ∩ 𝐶) → 𝐴 ⊆ 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2113   ∩ cin 3897   ⊆ wss 3898  𝒫 cpw 4549

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-in 3905  df-ss 3915  df-pw 4551

This theorem is referenced by:  sge0z  46498  sge0revalmpt  46501  sge0f1o  46505  sge0rnbnd  46516  sge0pnffigt  46519  sge0lefi  46521  sge0ltfirp  46523  sge0gerpmpt  46525  sge0le  46530  sge0ltfirpmpt  46531  sge0iunmptlemre  46538  sge0rpcpnf  46544  sge0lefimpt  46546  sge0ltfirpmpt2  46549  sge0isum  46550  sge0xaddlem1  46556  sge0xaddlem2  46557  sge0pnffigtmpt  46563  sge0pnffsumgt  46565  sge0gtfsumgt  46566  sge0uzfsumgt  46567  sge0seq  46569  sge0reuz  46570  omeiunltfirp  46642  carageniuncllem2  46645  caratheodorylem2  46650