Theorem elpwinss 42486

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

Syntax hints:   → wi 4   ∈ wcel 2108   ∩ cin 3882   ⊆ wss 3883  𝒫 cpw 4530

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900  df-pw 4532

This theorem is referenced by:  sge0z  43803  sge0revalmpt  43806  sge0f1o  43810  sge0rnbnd  43821  sge0pnffigt  43824  sge0lefi  43826  sge0ltfirp  43828  sge0gerpmpt  43830  sge0le  43835  sge0ltfirpmpt  43836  sge0iunmptlemre  43843  sge0rpcpnf  43849  sge0lefimpt  43851  sge0ltfirpmpt2  43854  sge0isum  43855  sge0xaddlem1  43861  sge0xaddlem2  43862  sge0pnffigtmpt  43868  sge0pnffsumgt  43870  sge0gtfsumgt  43871  sge0uzfsumgt  43872  sge0seq  43874  sge0reuz  43875  omeiunltfirp  43947  carageniuncllem2  43950  caratheodorylem2  43955