Theorem elpwinss 45170

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  46497  sge0revalmpt  46500  sge0f1o  46504  sge0rnbnd  46515  sge0pnffigt  46518  sge0lefi  46520  sge0ltfirp  46522  sge0gerpmpt  46524  sge0le  46529  sge0ltfirpmpt  46530  sge0iunmptlemre  46537  sge0rpcpnf  46543  sge0lefimpt  46545  sge0ltfirpmpt2  46548  sge0isum  46549  sge0xaddlem1  46555  sge0xaddlem2  46556  sge0pnffigtmpt  46562  sge0pnffsumgt  46564  sge0gtfsumgt  46565  sge0uzfsumgt  46566  sge0seq  46568  sge0reuz  46569  omeiunltfirp  46641  carageniuncllem2  46644  caratheodorylem2  46649