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

Theorem elpw2g 5032
Description: Membership in a power class. Theorem 86 of [Suppes] p. 47. (Contributed by NM, 7-Aug-2000.)
Assertion
Ref Expression
elpw2g (𝐵𝑉 → (𝐴 ∈ 𝒫 𝐵𝐴𝐵))

Proof of Theorem elpw2g
StepHypRef Expression
1 elpwi 4372 . 2 (𝐴 ∈ 𝒫 𝐵𝐴𝐵)
2 ssexg 5012 . . . 4 ((𝐴𝐵𝐵𝑉) → 𝐴 ∈ V)
3 elpwg 4370 . . . . 5 (𝐴 ∈ V → (𝐴 ∈ 𝒫 𝐵𝐴𝐵))
43biimparc 467 . . . 4 ((𝐴𝐵𝐴 ∈ V) → 𝐴 ∈ 𝒫 𝐵)
52, 4syldan 581 . . 3 ((𝐴𝐵𝐵𝑉) → 𝐴 ∈ 𝒫 𝐵)
65expcom 400 . 2 (𝐵𝑉 → (𝐴𝐵𝐴 ∈ 𝒫 𝐵))
71, 6impbid2 217 1 (𝐵𝑉 → (𝐴 ∈ 𝒫 𝐵𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  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:  elpw2  5033  elpwi2  5034  pwnss  5035  pw2f1olem  8313  fineqvlem  8423  elfir  8570  marypha1  8589  r1sscl  8905  tskwe  9069  dfac8alem  9145  acni2  9162  fin1ai  9410  fin2i  9412  fin23lem7  9433  fin23lem11  9434  isfin2-2  9436  fin23lem39  9467  isf34lem1  9489  isf34lem2  9490  isf34lem4  9494  isf34lem5  9495  fin1a2lem12  9528  canthnumlem  9765  canthp1lem2  9770  tsken  9871  tskss  9875  gruss  9913  ramub1lem1  15967  ismre  16475  mreintcl  16480  mremre  16489  submre  16490  mrcval  16495  mrccl  16496  mrcun  16507  ismri  16516  mreexexlem4d  16532  acsfiel  16539  isacs1i  16542  catcoppccl  16982  acsdrsel  17392  acsdrscl  17395  acsficl  17396  pmtrval  18092  pmtrrn  18098  opsrval  19703  istopg  20934  uniopn  20936  iscld  21066  ntrval  21075  clsval  21076  discld  21128  mretopd  21131  neival  21141  isnei  21142  lpval  21178  restdis  21217  ordtbaslem  21227  ordtuni  21229  cncls  21313  cndis  21330  tgcmp  21439  hauscmplem  21444  comppfsc  21570  elkgen  21574  xkoopn  21627  elqtop  21735  kqffn  21763  isfbas  21867  filss  21891  snfbas  21904  elfg  21909  fbasrn  21922  ufilss  21943  fixufil  21960  cfinufil  21966  ufinffr  21967  ufilen  21968  fin1aufil  21970  rnelfmlem  21990  flimclslem  22022  hauspwpwf1  22025  supnfcls  22058  flimfnfcls  22066  ptcmplem1  22090  tsmsfbas  22165  blfvalps  22422  blfps  22445  blf  22446  bcthlem5  23359  minveclem3b  23434  sigaclcuni  30529  sigaclcu2  30531  pwsiga  30541  erdsze2lem2  31531  cvmsval  31593  cvmsss2  31601  neibastop2lem  32698  tailf  32713  bj-ismoored  33392  fin2so  33728  sdclem1  33869  elrfirn  37778  elrfirn2  37779  istopclsd  37783  nacsfix  37795  dnnumch1  38133
  Copyright terms: Public domain W3C validator