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

Theorem elpwi2 5213
Description: Membership in a power class. (Contributed by Glauco Siliprandi, 3-Mar-2021.) (Proof shortened by Wolf Lammen, 26-May-2024.)
Hypotheses
Ref Expression
elpwi2.1 𝐵𝑉
elpwi2.2 𝐴𝐵
Assertion
Ref Expression
elpwi2 𝐴 ∈ 𝒫 𝐵

Proof of Theorem elpwi2
StepHypRef Expression
1 elpwi2.2 . 2 𝐴𝐵
2 elpwi2.1 . . . 4 𝐵𝑉
32elexi 3460 . . 3 𝐵 ∈ V
43elpw2 5212 . 2 (𝐴 ∈ 𝒫 𝐵𝐴𝐵)
51, 4mpbir 234 1 𝐴 ∈ 𝒫 𝐵
Colors of variables: wff setvar class
Syntax hints:  wcel 2111  wss 3881  𝒫 cpw 4497
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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770  ax-sep 5167
This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-rab 3115  df-v 3443  df-in 3888  df-ss 3898  df-pw 4499
This theorem is referenced by:  canth  7090  aceq3lem  9531  axdc3lem4  9864  uzf  12234  ixxf  12736  fzf  12889  bitsf  15766  prdsval  16720  prdsds  16729  wunnat  17218  ocvfval  20355  leordtval2  21817  cnpfval  21839  iscnp2  21844  islly2  22089  xkotf  22190  alexsubALTlem4  22655  sszcld  23422  bndth  23563  ishtpy  23577  fpwrelmap  30495  ballotlem2  31856  satfrnmapom  32730  cover2  35152  clsk1indlem1  40746  sprsymrelfolem1  44007
  Copyright terms: Public domain W3C validator