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

Theorem elpw2 4819
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 4818 . 2 (𝐵 ∈ V → (𝐴 ∈ 𝒫 𝐵𝐴𝐵))
31, 2ax-mp 5 1 (𝐴 ∈ 𝒫 𝐵𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 196  wcel 1988  Vcvv 3195  wss 3567  𝒫 cpw 4149
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-v 3197  df-in 3574  df-ss 3581  df-pw 4151
This theorem is referenced by:  axpweq  4833  knatar  6592  canth  6593  dffi3  8322  marypha1lem  8324  r1pwss  8632  rankr1bg  8651  pwwf  8655  unwf  8658  rankval2  8666  uniwf  8667  rankpwi  8671  aceq3lem  8928  dfac2a  8937  dfac12lem2  8951  axdc3lem4  9260  axdc4lem  9262  axdclem  9326  grothpw  9633  uzf  11675  ixxf  12170  fzf  12315  incexclem  14549  rpnnen2lem1  14924  rpnnen2lem2  14925  bitsf  15130  sadfval  15155  smufval  15180  smupf  15181  vdwapf  15657  prdsval  16096  prdsds  16105  prdshom  16108  mreacs  16300  acsfn  16301  wunnat  16597  lubeldm  16962  lubval  16965  glbeldm  16975  glbval  16978  clatlem  17092  clatlubcl2  17094  clatglbcl2  17096  issubm  17328  issubg  17575  cntzval  17735  sylow1lem2  17995  lsmvalx  18035  pj1fval  18088  issubrg  18761  islss  18916  lspval  18956  lspcl  18957  islbs  19057  lbsextlem1  19139  lbsextlem3  19141  lbsextlem4  19142  sraval  19157  aspval  19309  ocvfval  19991  ocvval  19992  isobs  20045  islinds  20129  leordtval2  20997  cnpfval  21019  iscnp2  21024  uncmp  21187  cmpfi  21192  cmpfii  21193  2ndc1stc  21235  1stcrest  21237  islly2  21268  hausllycmp  21278  lly1stc  21280  1stckgenlem  21337  xkotf  21369  txlly  21420  txnlly  21421  tx1stc  21434  basqtop  21495  tgqtop  21496  alexsubALTlem3  21834  alexsubALTlem4  21835  alexsubALT  21836  sszcld  22601  cncfval  22672  cnllycmp  22736  bndth  22738  ishtpy  22752  ovolficcss  23219  ovolval  23223  ovolicc2  23271  ismbl  23275  mblsplit  23281  voliunlem3  23301  vitalilem4  23361  vitalilem5  23362  dvfval  23642  dvnfval  23666  cpnfval  23676  plyval  23930  dmarea  24665  wilthlem2  24776  issh  28035  ocval  28109  spanval  28162  hsupval  28163  sshjval  28179  sshjval3  28183  fpwrelmap  29482  sigagensiga  30178  dya2iocuni  30319  coinflippv  30519  ballotlemelo  30523  ballotlem2  30524  ballotth  30573  erdszelem1  31147  kur14lem9  31170  kur14  31172  cnllysconn  31201  elmpst  31407  mclsrcl  31432  mclsval  31434  icoreresf  33171  cover2  33479  cntotbnd  33566  heibor1lem  33579  heibor  33591  isidl  33784  igenval  33831  paddval  34903  pclvalN  34995  polvalN  35010  docavalN  36231  djavalN  36243  dicval  36284  dochval  36459  djhval  36506  lpolconN  36595  elmzpcl  37108  eldiophb  37139  rpnnen3  37418  islssfgi  37461  hbt  37519  elmnc  37525  itgoval  37550  itgocn  37553  rgspnval  37557  issubmgm  41554  elpglem2  42220
  Copyright terms: Public domain W3C validator