Theorem elpwinss 45480

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-in 3896  df-ss 3906  df-pw 4543

This theorem is referenced by:  sge0z  46803  sge0revalmpt  46806  sge0f1o  46810  sge0rnbnd  46821  sge0pnffigt  46824  sge0lefi  46826  sge0ltfirp  46828  sge0gerpmpt  46830  sge0le  46835  sge0ltfirpmpt  46836  sge0iunmptlemre  46843  sge0rpcpnf  46849  sge0lefimpt  46851  sge0ltfirpmpt2  46854  sge0isum  46855  sge0xaddlem1  46861  sge0xaddlem2  46862  sge0pnffigtmpt  46868  sge0pnffsumgt  46870  sge0gtfsumgt  46871  sge0uzfsumgt  46872  sge0seq  46874  sge0reuz  46875  omeiunltfirp  46947  carageniuncllem2  46950  caratheodorylem2  46955