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

Theorem elpw2g 5305
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 4571 . 2 (𝐴 ∈ 𝒫 𝐵𝐴𝐵)
2 ssexg 5284 . . . 4 ((𝐴𝐵𝐵𝑉) → 𝐴 ∈ V)
3 elpwg 4567 . . . . 5 (𝐴 ∈ V → (𝐴 ∈ 𝒫 𝐵𝐴𝐵))
43biimparc 481 . . . 4 ((𝐴𝐵𝐴 ∈ V) → 𝐴 ∈ 𝒫 𝐵)
52, 4syldan 592 . . 3 ((𝐴𝐵𝐵𝑉) → 𝐴 ∈ 𝒫 𝐵)
65expcom 415 . 2 (𝐵𝑉 → (𝐴𝐵𝐴 ∈ 𝒫 𝐵))
71, 6impbid2 225 1 (𝐵𝑉 → (𝐴 ∈ 𝒫 𝐵𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wcel 2107  Vcvv 3447  wss 3914  𝒫 cpw 4564
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5260
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3407  df-v 3449  df-in 3921  df-ss 3931  df-pw 4566
This theorem is referenced by:  elpw2  5306  elpwi2OLD  5308  pwnss  5310  difelpw  5312  rabelpw  5313  pw2f1olem  9026  fineqvlem  9212  elfir  9359  r1sscl  9729  tskwe  9894  dfac8alem  9973  acni2  9990  fin1ai  10237  fin2i  10239  fin23lem7  10260  fin23lem11  10261  isfin2-2  10263  fin23lem39  10294  isf34lem1  10316  isf34lem2  10317  isf34lem4  10321  isf34lem5  10322  fin1a2lem12  10355  canthnumlem  10592  tsken  10698  tskss  10702  gruss  10740  ismre  17478  mreintcl  17483  mremre  17492  submre  17493  mrcval  17498  mrccl  17499  mrcun  17510  ismri  17519  acsfiel  17542  isacs1i  17545  catcoppccl  18011  catcoppcclOLD  18012  acsdrsel  18440  acsdrscl  18443  acsficl  18444  pmtrval  19241  pmtrrn  19247  istopg  22267  uniopn  22269  iscld  22401  ntrval  22410  clsval  22411  discld  22463  mretopd  22466  neival  22476  isnei  22477  lpval  22513  restdis  22552  ordtbaslem  22562  ordtuni  22564  cndis  22665  tgcmp  22775  hauscmplem  22780  comppfsc  22906  elkgen  22910  xkoopn  22963  elqtop  23071  kqffn  23099  isfbas  23203  filss  23227  snfbas  23240  elfg  23245  ufilss  23279  fixufil  23296  cfinufil  23302  ufinffr  23303  ufilen  23304  fin1aufil  23306  flimclslem  23358  hauspwpwf1  23361  supnfcls  23394  flimfnfcls  23402  ptcmplem1  23426  tsmsfbas  23502  blfvalps  23759  blfps  23782  blf  23783  bcthlem5  24715  minveclem3b  24815  sigaclcuni  32781  sigaclcu2  32783  pwsiga  32793  erdsze2lem2  33862  cvmsval  33924  cvmsss2  33932  neibastop2lem  34885  tailf  34900  pibt2  35938  fin2so  36115  sdclem1  36252  elrfirn  41065  elrfirn2  41066  istopclsd  41070  nacsfix  41082  dnnumch1  41418  inpw  46993
  Copyright terms: Public domain W3C validator