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

Theorem elpwd 4564
Description: Membership in a power class. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
Hypotheses
Ref Expression
elpwd.1 (𝜑𝐴𝑉)
elpwd.2 (𝜑𝐴𝐵)
Assertion
Ref Expression
elpwd (𝜑𝐴 ∈ 𝒫 𝐵)

Proof of Theorem elpwd
StepHypRef Expression
1 elpwd.2 . 2 (𝜑𝐴𝐵)
2 elpwd.1 . . 3 (𝜑𝐴𝑉)
3 elpwg 4561 . . 3 (𝐴𝑉 → (𝐴 ∈ 𝒫 𝐵𝐴𝐵))
42, 3syl 17 . 2 (𝜑 → (𝐴 ∈ 𝒫 𝐵𝐴𝐵))
51, 4mpbird 256 1 (𝜑𝐴 ∈ 𝒫 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wcel 2106  wss 3908  𝒫 cpw 4558
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 2708
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3445  df-in 3915  df-ss 3925  df-pw 4560
This theorem is referenced by:  sselpwd  5281  pwel  5334  frd  5590  f1opw2  7600  pwuncl  7696  f1opwfi  9258  ackbij1lem6  10119  ackbij1lem11  10124  mreacs  17497  sylow3lem3  19369  sylow3lem6  19372  cmpcov  22691  tgqtop  23014  filss  23155  scutval  27090  madecut  27162  cofcut1  27187  fnpreimac  31414  pcmplfin  32244  rspectopn  32251  zarclsint  32256  zarcmplem  32265  indval  32415  reprval  33026  naddunif  34240  bj-sselpwuni  35452  bj-discrmoore  35513  dmvolss  44120  sge0xaddlem1  44568  meadjuni  44592  ovnval2b  44687  ovnsubadd2lem  44780  vonvolmbllem  44795  vonvolmbl  44796  smfresal  44923  smfpimbor1lem1  44933  sprsymrelfvlem  45576  lindslinindsimp1  46432  lindslinindimp2lem4  46436  lincresunit3  46456  iscnrm3llem1  46876
  Copyright terms: Public domain W3C validator