Theorem elpwinss 45092

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

Syntax hints:   → wi 4   ∈ wcel 2111   ∩ cin 3901   ⊆ wss 3902  𝒫 cpw 4550

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 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-in 3909  df-ss 3919  df-pw 4552

This theorem is referenced by:  sge0z  46419  sge0revalmpt  46422  sge0f1o  46426  sge0rnbnd  46437  sge0pnffigt  46440  sge0lefi  46442  sge0ltfirp  46444  sge0gerpmpt  46446  sge0le  46451  sge0ltfirpmpt  46452  sge0iunmptlemre  46459  sge0rpcpnf  46465  sge0lefimpt  46467  sge0ltfirpmpt2  46470  sge0isum  46471  sge0xaddlem1  46477  sge0xaddlem2  46478  sge0pnffigtmpt  46484  sge0pnffsumgt  46486  sge0gtfsumgt  46487  sge0uzfsumgt  46488  sge0seq  46490  sge0reuz  46491  omeiunltfirp  46563  carageniuncllem2  46566  caratheodorylem2  46571