Theorem elpwinss 42597

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

Syntax hints:   → wi 4   ∈ wcel 2106   ∩ cin 3886   ⊆ wss 3887  𝒫 cpw 4533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-in 3894  df-ss 3904  df-pw 4535

This theorem is referenced by:  sge0z  43913  sge0revalmpt  43916  sge0f1o  43920  sge0rnbnd  43931  sge0pnffigt  43934  sge0lefi  43936  sge0ltfirp  43938  sge0gerpmpt  43940  sge0le  43945  sge0ltfirpmpt  43946  sge0iunmptlemre  43953  sge0rpcpnf  43959  sge0lefimpt  43961  sge0ltfirpmpt2  43964  sge0isum  43965  sge0xaddlem1  43971  sge0xaddlem2  43972  sge0pnffigtmpt  43978  sge0pnffsumgt  43980  sge0gtfsumgt  43981  sge0uzfsumgt  43982  sge0seq  43984  sge0reuz  43985  omeiunltfirp  44057  carageniuncllem2  44060  caratheodorylem2  44065