Theorem elpwinss 44037

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

Syntax hints:   → wi 4   ∈ wcel 2104   ∩ cin 3946   ⊆ wss 3947  𝒫 cpw 4601

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-v 3474  df-in 3954  df-ss 3964  df-pw 4603

This theorem is referenced by:  sge0z  45389  sge0revalmpt  45392  sge0f1o  45396  sge0rnbnd  45407  sge0pnffigt  45410  sge0lefi  45412  sge0ltfirp  45414  sge0gerpmpt  45416  sge0le  45421  sge0ltfirpmpt  45422  sge0iunmptlemre  45429  sge0rpcpnf  45435  sge0lefimpt  45437  sge0ltfirpmpt2  45440  sge0isum  45441  sge0xaddlem1  45447  sge0xaddlem2  45448  sge0pnffigtmpt  45454  sge0pnffsumgt  45456  sge0gtfsumgt  45457  sge0uzfsumgt  45458  sge0seq  45460  sge0reuz  45461  omeiunltfirp  45533  carageniuncllem2  45536  caratheodorylem2  45541