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

Theorem elpw2g 4749
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 4117 . 2 (𝐴 ∈ 𝒫 𝐵𝐴𝐵)
2 ssexg 4727 . . . 4 ((𝐴𝐵𝐵𝑉) → 𝐴 ∈ V)
3 elpwg 4116 . . . . 5 (𝐴 ∈ V → (𝐴 ∈ 𝒫 𝐵𝐴𝐵))
43biimparc 503 . . . 4 ((𝐴𝐵𝐴 ∈ V) → 𝐴 ∈ 𝒫 𝐵)
52, 4syldan 486 . . 3 ((𝐴𝐵𝐵𝑉) → 𝐴 ∈ 𝒫 𝐵)
65expcom 450 . 2 (𝐵𝑉 → (𝐴𝐵𝐴 ∈ 𝒫 𝐵))
71, 6impbid2 215 1 (𝐵𝑉 → (𝐴 ∈ 𝒫 𝐵𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195  wcel 1977  Vcvv 3173  wss 3540  𝒫 cpw 4108
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4704
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-in 3547  df-ss 3554  df-pw 4110
This theorem is referenced by:  elpw2  4750  pwnss  4751  knatar  6485  pw2f1olem  7927  fineqvlem  8037  elfir  8182  marypha1  8201  r1sscl  8509  tskwe  8637  dfac8alem  8713  acni2  8730  fin1ai  8976  fin2i  8978  fin23lem7  8999  fin23lem11  9000  isfin2-2  9002  fin23lem39  9033  isf34lem1  9055  isf34lem2  9056  isf34lem4  9060  isf34lem5  9061  fin1a2lem12  9094  canthnumlem  9327  canthp1lem2  9332  wunss  9391  tsken  9433  tskss  9437  gruss  9475  ramub1lem1  15517  ismre  16022  mreintcl  16027  mremre  16036  submre  16037  mrcval  16042  mrccl  16043  mrcun  16054  ismri  16063  mreexd  16074  mreexexlem4d  16079  acsfiel  16087  isacs1i  16090  catcoppccl  16530  acsdrsel  16939  acsdrscl  16942  acsficl  16943  pmtrval  17643  pmtrrn  17649  opsrval  19244  istopg  20473  uniopn  20475  iscld  20589  ntrval  20598  clsval  20599  discld  20651  mretopd  20654  neival  20664  isnei  20665  lpval  20701  restdis  20740  ordtbaslem  20750  ordtuni  20752  cncls  20836  cndis  20853  tgcmp  20962  hauscmplem  20967  comppfsc  21093  elkgen  21097  xkoopn  21150  elqtop  21258  kqffn  21286  isfbas  21391  filss  21415  snfbas  21428  elfg  21433  fbasrn  21446  ufilss  21467  fixufil  21484  cfinufil  21490  ufinffr  21491  ufilen  21492  fin1aufil  21494  rnelfmlem  21514  flimclslem  21546  hauspwpwf1  21549  supnfcls  21582  flimfnfcls  21590  ptcmplem1  21614  tsmsfbas  21689  blfvalps  21946  blfps  21969  blf  21970  bcthlem5  22878  minveclem3b  22952  sigaclcuni  29302  sigaclcu2  29304  pwsiga  29314  erdsze2lem2  30234  cvmsval  30296  cvmsss2  30304  neibastop2lem  31319  tailf  31334  fin2so  32360  sdclem1  32503  elrfirn  36070  elrfirn2  36071  istopclsd  36075  nacsfix  36087  dnnumch1  36426  elpwi2  38085
  Copyright terms: Public domain W3C validator