Theorem elpwinss 45749

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

Syntax hints:   → wi 4   ∈ wcel 2143   ∩ cin 3905   ⊆ wss 3906  𝒫 cpw 4563

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-in 3913  df-ss 3923  df-pw 4565

This theorem is referenced by:  sge0z  47069  sge0revalmpt  47072  sge0f1o  47076  sge0rnbnd  47087  sge0pnffigt  47090  sge0lefi  47092  sge0ltfirp  47094  sge0gerpmpt  47096  sge0le  47101  sge0ltfirpmpt  47102  sge0iunmptlemre  47109  sge0rpcpnf  47115  sge0lefimpt  47117  sge0ltfirpmpt2  47120  sge0isum  47121  sge0xaddlem1  47127  sge0xaddlem2  47128  sge0pnffigtmpt  47134  sge0pnffsumgt  47136  sge0gtfsumgt  47137  sge0uzfsumgt  47138  sge0seq  47140  sge0reuz  47141  omeiunltfirp  47213  carageniuncllem2  47216  caratheodorylem2  47221