Theorem elpwinss 41331

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

Syntax hints:   → wi 4   ∈ wcel 2114   ∩ cin 3935   ⊆ wss 3936  𝒫 cpw 4539

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 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-in 3943  df-ss 3952  df-pw 4541

This theorem is referenced by:  sge0z  42677  sge0revalmpt  42680  sge0f1o  42684  sge0rnbnd  42695  sge0pnffigt  42698  sge0lefi  42700  sge0ltfirp  42702  sge0gerpmpt  42704  sge0le  42709  sge0ltfirpmpt  42710  sge0iunmptlemre  42717  sge0rpcpnf  42723  sge0lefimpt  42725  sge0ltfirpmpt2  42728  sge0isum  42729  sge0xaddlem1  42735  sge0xaddlem2  42736  sge0pnffigtmpt  42742  sge0pnffsumgt  42744  sge0gtfsumgt  42745  sge0uzfsumgt  42746  sge0seq  42748  sge0reuz  42749  omeiunltfirp  42821  carageniuncllem2  42824  caratheodorylem2  42829