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

Theorem elpw2 4746
Description: Membership in a power class. Theorem 86 of [Suppes] p. 47. (Contributed by NM, 11-Oct-2007.)
Hypothesis
Ref Expression
elpw2.1 𝐵 ∈ V
Assertion
Ref Expression
elpw2 (𝐴 ∈ 𝒫 𝐵𝐴𝐵)

Proof of Theorem elpw2
StepHypRef Expression
1 elpw2.1 . 2 𝐵 ∈ V
2 elpw2g 4745 . 2 (𝐵 ∈ V → (𝐴 ∈ 𝒫 𝐵𝐴𝐵))
31, 2ax-mp 5 1 (𝐴 ∈ 𝒫 𝐵𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 194  wcel 1975  Vcvv 3168  wss 3535  𝒫 cpw 4103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585  ax-sep 4699
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-clab 2592  df-cleq 2598  df-clel 2601  df-nfc 2735  df-v 3170  df-in 3542  df-ss 3549  df-pw 4105
This theorem is referenced by:  axpweq  4759  knatar  6481  canth  6482  dffi3  8193  marypha1lem  8195  r1pwss  8503  rankr1bg  8522  pwwf  8526  unwf  8529  rankval2  8537  uniwf  8538  rankpwi  8542  aceq3lem  8799  dfac2a  8808  dfac12lem2  8822  axdc3lem4  9131  axdc4lem  9133  axdclem  9197  grothpw  9500  uzf  11518  ixxf  12008  fzf  12152  incexclem  14349  rpnnen2lem1  14724  rpnnen2lem2  14725  bitsf  14929  sadfval  14954  smufval  14979  smupf  14980  vdwapf  15456  prdsval  15880  prdsds  15889  prdshom  15892  mreacs  16084  acsfn  16085  wunnat  16381  lubeldm  16746  lubval  16749  glbeldm  16759  glbval  16762  clatlem  16876  clatlubcl2  16878  clatglbcl2  16880  issubm  17112  issubg  17359  cntzval  17519  sylow1lem2  17779  lsmvalx  17819  pj1fval  17872  issubrg  18545  islss  18698  lspval  18738  lspcl  18739  islbs  18839  lbsextlem1  18921  lbsextlem3  18923  lbsextlem4  18924  sraval  18939  aspval  19091  ocvfval  19767  ocvval  19768  isobs  19821  islinds  19905  leordtval2  20764  cnpfval  20786  iscnp2  20791  uncmp  20954  cmpfi  20959  cmpfii  20960  2ndc1stc  21002  1stcrest  21004  islly2  21035  hausllycmp  21045  lly1stc  21047  1stckgenlem  21104  xkotf  21136  txlly  21187  txnlly  21188  tx1stc  21201  basqtop  21262  tgqtop  21263  alexsubALTlem3  21601  alexsubALTlem4  21602  alexsubALT  21603  sszcld  22356  cncfval  22426  cnllycmp  22490  bndth  22492  ishtpy  22506  ovolficcss  22958  ovolval  22962  ovolicc2  23010  ismbl  23014  mblsplit  23020  voliunlem3  23040  vitalilem4  23099  vitalilem5  23100  dvfval  23380  dvnfval  23404  cpnfval  23414  plyval  23666  dmarea  24397  wilthlem2  24508  umgrabi  26272  issh  27251  ocval  27325  spanval  27378  hsupval  27379  sshjval  27395  sshjval3  27399  fpwrelmap  28698  sigagensiga  29333  dya2iocuni  29474  coinflippv  29674  ballotlemelo  29678  ballotlem2  29679  ballotth  29728  erdszelem1  30229  kur14lem9  30252  kur14  30254  cnllyscon  30283  elmpst  30489  mclsrcl  30514  mclsval  30516  icoreresf  32175  cover2  32477  cntotbnd  32564  heibor1lem  32577  heibor  32589  isidl  32782  igenval  32829  paddval  33901  pclvalN  33993  polvalN  34008  docavalN  35229  djavalN  35241  dicval  35282  dochval  35457  djhval  35504  lpolconN  35593  elmzpcl  36106  eldiophb  36137  rpnnen3  36416  islssfgi  36459  hbt  36518  elmnc  36524  itgoval  36549  itgocn  36552  rgspnval  36556  issubmgm  41577
  Copyright terms: Public domain W3C validator