Theorem elpwinss 41304

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 4553	1 ⊢ (𝐴 ∈ (𝒫 𝐵 ∩ 𝐶) → 𝐴 ⊆ 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2110   ∩ 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 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2156  ax-12 2172  ax-ext 2793

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

This theorem is referenced by:  sge0z  42650  sge0revalmpt  42653  sge0f1o  42657  sge0rnbnd  42668  sge0pnffigt  42671  sge0lefi  42673  sge0ltfirp  42675  sge0gerpmpt  42677  sge0le  42682  sge0ltfirpmpt  42683  sge0iunmptlemre  42690  sge0rpcpnf  42696  sge0lefimpt  42698  sge0ltfirpmpt2  42701  sge0isum  42702  sge0xaddlem1  42708  sge0xaddlem2  42709  sge0pnffigtmpt  42715  sge0pnffsumgt  42717  sge0gtfsumgt  42718  sge0uzfsumgt  42719  sge0seq  42721  sge0reuz  42722  omeiunltfirp  42794  carageniuncllem2  42797  caratheodorylem2  42802