Theorem elpwinss 45593

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

Syntax hints:   → wi 4   ∈ wcel 2141   ∩ cin 3903   ⊆ wss 3904  𝒫 cpw 4554

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-in 3911  df-ss 3921  df-pw 4556

This theorem is referenced by:  sge0z  46913  sge0revalmpt  46916  sge0f1o  46920  sge0rnbnd  46931  sge0pnffigt  46934  sge0lefi  46936  sge0ltfirp  46938  sge0gerpmpt  46940  sge0le  46945  sge0ltfirpmpt  46946  sge0iunmptlemre  46953  sge0rpcpnf  46959  sge0lefimpt  46961  sge0ltfirpmpt2  46964  sge0isum  46965  sge0xaddlem1  46971  sge0xaddlem2  46972  sge0pnffigtmpt  46978  sge0pnffsumgt  46980  sge0gtfsumgt  46981  sge0uzfsumgt  46982  sge0seq  46984  sge0reuz  46985  omeiunltfirp  47057  carageniuncllem2  47060  caratheodorylem2  47065