Theorem elpwinss 45054

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

Syntax hints:   → wi 4   ∈ wcel 2108   ∩ cin 3950   ⊆ wss 3951  𝒫 cpw 4600

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-in 3958  df-ss 3968  df-pw 4602

This theorem is referenced by:  sge0z  46390  sge0revalmpt  46393  sge0f1o  46397  sge0rnbnd  46408  sge0pnffigt  46411  sge0lefi  46413  sge0ltfirp  46415  sge0gerpmpt  46417  sge0le  46422  sge0ltfirpmpt  46423  sge0iunmptlemre  46430  sge0rpcpnf  46436  sge0lefimpt  46438  sge0ltfirpmpt2  46441  sge0isum  46442  sge0xaddlem1  46448  sge0xaddlem2  46449  sge0pnffigtmpt  46455  sge0pnffsumgt  46457  sge0gtfsumgt  46458  sge0uzfsumgt  46459  sge0seq  46461  sge0reuz  46462  omeiunltfirp  46534  carageniuncllem2  46537  caratheodorylem2  46542