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

Theorem elpwd 4606
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 4603 . . 3 (𝐴𝑉 → (𝐴 ∈ 𝒫 𝐵𝐴𝐵))
42, 3syl 17 . 2 (𝜑 → (𝐴 ∈ 𝒫 𝐵𝐴𝐵))
51, 4mpbird 257 1 (𝜑𝐴 ∈ 𝒫 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wcel 2108  wss 3951  𝒫 cpw 4600
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ss 3968  df-pw 4602
This theorem is referenced by:  sselpwd  5328  pwel  5381  frd  5641  f1opw2  7688  pwuncl  7790  naddunif  8731  f1opwfi  9396  ackbij1lem6  10264  ackbij1lem11  10269  mreacs  17701  sylow3lem3  19647  sylow3lem6  19650  cmpcov  23397  tgqtop  23720  filss  23861  scutval  27845  madecut  27921  cofcut1  27954  cutlt  27966  elons2d  28282  fnpreimac  32681  indval  32838  exsslsb  33647  pcmplfin  33859  rspectopn  33866  zarclsint  33871  zarcmplem  33880  reprval  34625  bj-sselpwuni  37051  bj-discrmoore  37112  dmvolss  46000  sge0xaddlem1  46448  meadjuni  46472  ovnval2b  46567  ovnsubadd2lem  46660  vonvolmbllem  46675  vonvolmbl  46676  smfresal  46803  smfpimbor1lem1  46813  sprsymrelfvlem  47477  isubgruhgr  47854  grimuhgr  47878  gpgedgel  48007  lindslinindsimp1  48374  lindslinindimp2lem4  48378  lincresunit3  48398  iscnrm3llem1  48846
  Copyright terms: Public domain W3C validator