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

Theorem elpwd 4508
 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 4503 . . 3 (𝐴𝑉 → (𝐴 ∈ 𝒫 𝐵𝐴𝐵))
42, 3syl 17 . 2 (𝜑 → (𝐴 ∈ 𝒫 𝐵𝐴𝐵))
51, 4mpbird 260 1 (𝜑𝐴 ∈ 𝒫 𝐵)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∈ wcel 2111   ⊆ wss 3883  𝒫 cpw 4500 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 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3444  df-in 3890  df-ss 3900  df-pw 4502 This theorem is referenced by:  sselpwd  5198  pwel  5251  f1opw2  7391  pwuncl  7485  f1opwfi  8830  ackbij1lem6  9654  ackbij1lem11  9659  mreacs  16941  sylow3lem3  18767  sylow3lem6  18770  cmpcov  22035  tgqtop  22358  filss  22499  fnpreimac  30478  pcmplfin  31279  rspectopn  31286  zarclsint  31291  zarcmplem  31300  indval  31448  reprval  32057  scutval  33478  madecut  33543  bj-sselpwuni  34618  bj-discrmoore  34677  dmvolss  42795  sge0xaddlem1  43240  meadjuni  43264  ovnval2b  43359  ovnsubadd2lem  43452  vonvolmbllem  43467  vonvolmbl  43468  smfresal  43588  smfpimbor1lem1  43598  sprsymrelfvlem  44175  lindslinindsimp1  45032  lindslinindimp2lem4  45036  lincresunit3  45056
 Copyright terms: Public domain W3C validator