Theorem elpwinss 45627

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

Syntax hints:   → wi 4   ∈ wcel 2145   ∩ cin 3906   ⊆ wss 3907  𝒫 cpw 4558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-in 3914  df-ss 3924  df-pw 4560

This theorem is referenced by:  sge0z  46947  sge0revalmpt  46950  sge0f1o  46954  sge0rnbnd  46965  sge0pnffigt  46968  sge0lefi  46970  sge0ltfirp  46972  sge0gerpmpt  46974  sge0le  46979  sge0ltfirpmpt  46980  sge0iunmptlemre  46987  sge0rpcpnf  46993  sge0lefimpt  46995  sge0ltfirpmpt2  46998  sge0isum  46999  sge0xaddlem1  47005  sge0xaddlem2  47006  sge0pnffigtmpt  47012  sge0pnffsumgt  47014  sge0gtfsumgt  47015  sge0uzfsumgt  47016  sge0seq  47018  sge0reuz  47019  omeiunltfirp  47091  carageniuncllem2  47094  caratheodorylem2  47099