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 43237
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 4154 . 2 (𝐴 ∈ (𝒫 𝐵𝐶) → 𝐴 ∈ 𝒫 𝐵)
21elpwid 4568 1 (𝐴 ∈ (𝒫 𝐵𝐶) → 𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2106  cin 3908  wss 3909  𝒫 cpw 4559
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3446  df-in 3916  df-ss 3926  df-pw 4561
This theorem is referenced by:  sge0z  44586  sge0revalmpt  44589  sge0f1o  44593  sge0rnbnd  44604  sge0pnffigt  44607  sge0lefi  44609  sge0ltfirp  44611  sge0gerpmpt  44613  sge0le  44618  sge0ltfirpmpt  44619  sge0iunmptlemre  44626  sge0rpcpnf  44632  sge0lefimpt  44634  sge0ltfirpmpt2  44637  sge0isum  44638  sge0xaddlem1  44644  sge0xaddlem2  44645  sge0pnffigtmpt  44651  sge0pnffsumgt  44653  sge0gtfsumgt  44654  sge0uzfsumgt  44655  sge0seq  44657  sge0reuz  44658  omeiunltfirp  44730  carageniuncllem2  44733  caratheodorylem2  44738
  Copyright terms: Public domain W3C validator