Theorem elpwinss 45498

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

Syntax hints:   → wi 4   ∈ wcel 2114   ∩ cin 3889   ⊆ wss 3890  𝒫 cpw 4542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-in 3897  df-ss 3907  df-pw 4544

This theorem is referenced by:  sge0z  46821  sge0revalmpt  46824  sge0f1o  46828  sge0rnbnd  46839  sge0pnffigt  46842  sge0lefi  46844  sge0ltfirp  46846  sge0gerpmpt  46848  sge0le  46853  sge0ltfirpmpt  46854  sge0iunmptlemre  46861  sge0rpcpnf  46867  sge0lefimpt  46869  sge0ltfirpmpt2  46872  sge0isum  46873  sge0xaddlem1  46879  sge0xaddlem2  46880  sge0pnffigtmpt  46886  sge0pnffsumgt  46888  sge0gtfsumgt  46889  sge0uzfsumgt  46890  sge0seq  46892  sge0reuz  46893  omeiunltfirp  46965  carageniuncllem2  46968  caratheodorylem2  46973