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

Theorem elpw2g 5211
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 4506 . 2 (𝐴 ∈ 𝒫 𝐵𝐴𝐵)
2 ssexg 5191 . . . 4 ((𝐴𝐵𝐵𝑉) → 𝐴 ∈ V)
3 elpwg 4500 . . . . 5 (𝐴 ∈ V → (𝐴 ∈ 𝒫 𝐵𝐴𝐵))
43biimparc 483 . . . 4 ((𝐴𝐵𝐴 ∈ V) → 𝐴 ∈ 𝒫 𝐵)
52, 4syldan 594 . . 3 ((𝐴𝐵𝐵𝑉) → 𝐴 ∈ 𝒫 𝐵)
65expcom 417 . 2 (𝐵𝑉 → (𝐴𝐵𝐴 ∈ 𝒫 𝐵))
71, 6impbid2 229 1 (𝐵𝑉 → (𝐴 ∈ 𝒫 𝐵𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wcel 2111  Vcvv 3441  wss 3881  𝒫 cpw 4497
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770  ax-sep 5167
This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-rab 3115  df-v 3443  df-in 3888  df-ss 3898  df-pw 4499
This theorem is referenced by:  elpw2  5212  elpwi2OLD  5214  pwnss  5215  difelpw  5217  rabelpw  5218  pw2f1olem  8604  fineqvlem  8716  elfir  8863  r1sscl  9198  tskwe  9363  dfac8alem  9440  acni2  9457  fin1ai  9704  fin2i  9706  fin23lem7  9727  fin23lem11  9728  isfin2-2  9730  fin23lem39  9761  isf34lem1  9783  isf34lem2  9784  isf34lem4  9788  isf34lem5  9789  fin1a2lem12  9822  canthnumlem  10059  tsken  10165  tskss  10169  gruss  10207  ismre  16853  mreintcl  16858  mremre  16867  submre  16868  mrcval  16873  mrccl  16874  mrcun  16885  ismri  16894  acsfiel  16917  isacs1i  16920  catcoppccl  17360  acsdrsel  17769  acsdrscl  17772  acsficl  17773  pmtrval  18571  pmtrrn  18577  istopg  21500  uniopn  21502  iscld  21632  ntrval  21641  clsval  21642  discld  21694  mretopd  21697  neival  21707  isnei  21708  lpval  21744  restdis  21783  ordtbaslem  21793  ordtuni  21795  cndis  21896  tgcmp  22006  hauscmplem  22011  comppfsc  22137  elkgen  22141  xkoopn  22194  elqtop  22302  kqffn  22330  isfbas  22434  filss  22458  snfbas  22471  elfg  22476  ufilss  22510  fixufil  22527  cfinufil  22533  ufinffr  22534  ufilen  22535  fin1aufil  22537  flimclslem  22589  hauspwpwf1  22592  supnfcls  22625  flimfnfcls  22633  ptcmplem1  22657  tsmsfbas  22733  blfvalps  22990  blfps  23013  blf  23014  bcthlem5  23932  minveclem3b  24032  sigaclcuni  31487  sigaclcu2  31489  pwsiga  31499  erdsze2lem2  32564  cvmsval  32626  cvmsss2  32634  neibastop2lem  33821  tailf  33836  pibt2  34834  fin2so  35044  sdclem1  35181  elrfirn  39634  elrfirn2  39635  istopclsd  39639  nacsfix  39651  dnnumch1  39986
  Copyright terms: Public domain W3C validator