Theorem elpwinss 45290

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

Syntax hints:   → wi 4   ∈ wcel 2113   ∩ cin 3900   ⊆ wss 3901  𝒫 cpw 4554

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-in 3908  df-ss 3918  df-pw 4556

This theorem is referenced by:  sge0z  46615  sge0revalmpt  46618  sge0f1o  46622  sge0rnbnd  46633  sge0pnffigt  46636  sge0lefi  46638  sge0ltfirp  46640  sge0gerpmpt  46642  sge0le  46647  sge0ltfirpmpt  46648  sge0iunmptlemre  46655  sge0rpcpnf  46661  sge0lefimpt  46663  sge0ltfirpmpt2  46666  sge0isum  46667  sge0xaddlem1  46673  sge0xaddlem2  46674  sge0pnffigtmpt  46680  sge0pnffsumgt  46682  sge0gtfsumgt  46683  sge0uzfsumgt  46684  sge0seq  46686  sge0reuz  46687  omeiunltfirp  46759  carageniuncllem2  46762  caratheodorylem2  46767