MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elpwi2 Structured version   Visualization version   GIF version

Theorem elpwi2 5240
Description: Membership in a power class. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
Hypotheses
Ref Expression
elpwi2.1 𝐵𝑉
elpwi2.2 𝐴𝐵
Assertion
Ref Expression
elpwi2 𝐴 ∈ 𝒫 𝐵

Proof of Theorem elpwi2
StepHypRef Expression
1 elpwi2.2 . 2 𝐴𝐵
2 elpwi2.1 . . 3 𝐵𝑉
3 elpw2g 5238 . . 3 (𝐵𝑉 → (𝐴 ∈ 𝒫 𝐵𝐴𝐵))
42, 3ax-mp 5 . 2 (𝐴 ∈ 𝒫 𝐵𝐴𝐵)
51, 4mpbir 232 1 𝐴 ∈ 𝒫 𝐵
Colors of variables: wff setvar class
Syntax hints:  wb 207  wcel 2105  wss 3933  𝒫 cpw 4535
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-rab 3144  df-v 3494  df-in 3940  df-ss 3949  df-pw 4537
This theorem is referenced by:  canth  7100  aceq3lem  9534  axdc3lem4  9863  uzf  12234  ixxf  12736  fzf  12884  bitsf  15764  prdsval  16716  prdsds  16725  wunnat  17214  ocvfval  20738  leordtval2  21748  cnpfval  21770  iscnp2  21775  islly2  22020  xkotf  22121  alexsubALTlem4  22586  sszcld  23352  bndth  23489  ishtpy  23503  fpwrelmap  30395  ballotlem2  31645  satfrnmapom  32514  cover2  34870  clsk1indlem1  40273  sprsymrelfolem1  43531
  Copyright terms: Public domain W3C validator