Theorem elpwinss 44988

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 4210	. 2 ⊢ (𝐴 ∈ (𝒫 𝐵 ∩ 𝐶) → 𝐴 ∈ 𝒫 𝐵)
2	1	elpwid 4613	1 ⊢ (𝐴 ∈ (𝒫 𝐵 ∩ 𝐶) → 𝐴 ⊆ 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2105   ∩ cin 3961   ⊆ wss 3962  𝒫 cpw 4604

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-in 3969  df-ss 3979  df-pw 4606

This theorem is referenced by:  sge0z  46330  sge0revalmpt  46333  sge0f1o  46337  sge0rnbnd  46348  sge0pnffigt  46351  sge0lefi  46353  sge0ltfirp  46355  sge0gerpmpt  46357  sge0le  46362  sge0ltfirpmpt  46363  sge0iunmptlemre  46370  sge0rpcpnf  46376  sge0lefimpt  46378  sge0ltfirpmpt2  46381  sge0isum  46382  sge0xaddlem1  46388  sge0xaddlem2  46389  sge0pnffigtmpt  46395  sge0pnffsumgt  46397  sge0gtfsumgt  46398  sge0uzfsumgt  46399  sge0seq  46401  sge0reuz  46402  omeiunltfirp  46474  carageniuncllem2  46477  caratheodorylem2  46482