Theorem elpwinss 44039

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

Syntax hints:   → wi 4   ∈ wcel 2105   ∩ cin 3948   ⊆ wss 3949  𝒫 cpw 4603

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3475  df-in 3956  df-ss 3966  df-pw 4605

This theorem is referenced by:  sge0z  45391  sge0revalmpt  45394  sge0f1o  45398  sge0rnbnd  45409  sge0pnffigt  45412  sge0lefi  45414  sge0ltfirp  45416  sge0gerpmpt  45418  sge0le  45423  sge0ltfirpmpt  45424  sge0iunmptlemre  45431  sge0rpcpnf  45437  sge0lefimpt  45439  sge0ltfirpmpt2  45442  sge0isum  45443  sge0xaddlem1  45449  sge0xaddlem2  45450  sge0pnffigtmpt  45456  sge0pnffsumgt  45458  sge0gtfsumgt  45459  sge0uzfsumgt  45460  sge0seq  45462  sge0reuz  45463  omeiunltfirp  45535  carageniuncllem2  45538  caratheodorylem2  45543