Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  elpwinss Structured version   Visualization version   GIF version

Theorem elpwinss 38738
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
StepHypRef Expression
1 elinel1 3783 . 2 (𝐴 ∈ (𝒫 𝐵𝐶) → 𝐴 ∈ 𝒫 𝐵)
21elpwid 4148 1 (𝐴 ∈ (𝒫 𝐵𝐶) → 𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1987  cin 3559  wss 3560  𝒫 cpw 4136
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-v 3192  df-in 3567  df-ss 3574  df-pw 4138
This theorem is referenced by:  sge0z  39929  sge0revalmpt  39932  sge0f1o  39936  sge0rnbnd  39947  sge0pnffigt  39950  sge0lefi  39952  sge0ltfirp  39954  sge0gerpmpt  39956  sge0le  39961  sge0ltfirpmpt  39962  sge0iunmptlemre  39969  sge0rpcpnf  39975  sge0lefimpt  39977  sge0ltfirpmpt2  39980  sge0isum  39981  sge0xaddlem1  39987  sge0xaddlem2  39988  sge0pnffigtmpt  39994  sge0pnffsumgt  39996  sge0gtfsumgt  39997  sge0uzfsumgt  39998  sge0seq  40000  sge0reuz  40001  omeiunltfirp  40070  carageniuncllem2  40073  caratheodorylem2  40078
  Copyright terms: Public domain W3C validator