Theorem elpwinss 44951

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

Syntax hints:   → wi 4   ∈ wcel 2108   ∩ cin 3975   ⊆ wss 3976  𝒫 cpw 4622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-in 3983  df-ss 3993  df-pw 4624

This theorem is referenced by:  sge0z  46296  sge0revalmpt  46299  sge0f1o  46303  sge0rnbnd  46314  sge0pnffigt  46317  sge0lefi  46319  sge0ltfirp  46321  sge0gerpmpt  46323  sge0le  46328  sge0ltfirpmpt  46329  sge0iunmptlemre  46336  sge0rpcpnf  46342  sge0lefimpt  46344  sge0ltfirpmpt2  46347  sge0isum  46348  sge0xaddlem1  46354  sge0xaddlem2  46355  sge0pnffigtmpt  46361  sge0pnffsumgt  46363  sge0gtfsumgt  46364  sge0uzfsumgt  46365  sge0seq  46367  sge0reuz  46368  omeiunltfirp  46440  carageniuncllem2  46443  caratheodorylem2  46448