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

Theorem elpw2 5033
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 5032 . 2 (𝐵 ∈ V → (𝐴 ∈ 𝒫 𝐵𝐴𝐵))
31, 2ax-mp 5 1 (𝐴 ∈ 𝒫 𝐵𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 197  wcel 2157  Vcvv 3402  wss 3780  𝒫 cpw 4362
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795  ax-sep 4988
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-v 3404  df-in 3787  df-ss 3794  df-pw 4364
This theorem is referenced by:  axpweq  5047  knatar  6841  canth  6842  dffi3  8586  marypha1lem  8588  r1pwss  8904  rankr1bg  8923  pwwf  8927  unwf  8930  rankval2  8938  uniwf  8939  rankpwi  8943  aceq3lem  9236  dfac2a  9245  dfac12lem2  9261  axdc3lem4  9570  axdc4lem  9572  axdclem  9636  grothpw  9943  uzf  11927  ixxf  12423  fzf  12573  incexclem  14810  rpnnen2lem1  15183  rpnnen2lem2  15184  bitsf  15388  sadfval  15413  smufval  15438  smupf  15439  vdwapf  15913  prdsval  16340  prdsds  16349  prdshom  16352  mreacs  16543  acsfn  16544  wunnat  16840  lubeldm  17206  lubval  17209  glbeldm  17219  glbval  17222  clatlem  17336  clatlubcl2  17338  clatglbcl2  17340  issubm  17572  issubg  17816  cntzval  17975  sylow1lem2  18235  lsmvalx  18275  pj1fval  18328  issubrg  19004  islss  19159  lspval  19202  lspcl  19203  islbs  19303  lbsextlem1  19387  lbsextlem3  19389  lbsextlem4  19390  sraval  19405  aspval  19557  ocvfval  20241  ocvval  20242  isobs  20295  islinds  20379  leordtval2  21251  cnpfval  21273  iscnp2  21278  uncmp  21441  cmpfi  21446  cmpfii  21447  2ndc1stc  21489  1stcrest  21491  islly2  21522  hausllycmp  21532  lly1stc  21534  1stckgenlem  21591  xkotf  21623  txlly  21674  txnlly  21675  tx1stc  21688  basqtop  21749  tgqtop  21750  alexsubALTlem3  22087  alexsubALTlem4  22088  alexsubALT  22089  sszcld  22854  cncfval  22925  cnllycmp  22989  bndth  22991  ishtpy  23005  ovolficcss  23473  ovolval  23477  ovolicc2  23526  ismbl  23530  mblsplit  23536  voliunlem3  23556  vitalilem4  23615  vitalilem5  23616  dvfval  23898  dvnfval  23922  cpnfval  23932  plyval  24186  dmarea  24921  wilthlem2  25032  issh  28416  ocval  28490  spanval  28543  hsupval  28544  sshjval  28560  sshjval3  28564  fpwrelmap  29858  sigagensiga  30552  dya2iocuni  30693  coinflippv  30893  ballotlemelo  30897  ballotlem2  30898  ballotth  30947  erdszelem1  31518  kur14lem9  31541  kur14  31543  cnllysconn  31572  elmpst  31778  mclsrcl  31803  mclsval  31805  icoreresf  33535  cover2  33839  cntotbnd  33925  heibor1lem  33938  heibor  33950  isidl  34143  igenval  34190  paddval  35597  pclvalN  35689  polvalN  35704  docavalN  36922  djavalN  36934  dicval  36975  dochval  37150  djhval  37197  lpolconN  37286  elpwbi  37772  elmzpcl  37809  eldiophb  37840  rpnnen3  38118  islssfgi  38161  hbt  38219  elmnc  38225  itgoval  38250  itgocn  38253  rgspnval  38257  issubmgm  42375  elpglem2  43044
  Copyright terms: Public domain W3C validator