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

Theorem elpw2g 5342
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 4607 . 2 (𝐴 ∈ 𝒫 𝐵𝐴𝐵)
2 ssexg 5321 . . . 4 ((𝐴𝐵𝐵𝑉) → 𝐴 ∈ V)
3 elpwg 4603 . . . . 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 3475  wss 3946  𝒫 cpw 4600
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 5297
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 3434  df-v 3477  df-in 3953  df-ss 3963  df-pw 4602
This theorem is referenced by:  elpw2  5343  elpwi2OLD  5345  pwnss  5347  difelpw  5349  rabelpw  5350  pw2f1olem  9071  fineqvlem  9257  elfir  9405  r1sscl  9775  tskwe  9940  dfac8alem  10019  acni2  10036  fin1ai  10283  fin2i  10285  fin23lem7  10306  fin23lem11  10307  isfin2-2  10309  fin23lem39  10340  isf34lem1  10362  isf34lem2  10363  isf34lem4  10367  isf34lem5  10368  fin1a2lem12  10401  canthnumlem  10638  tsken  10744  tskss  10748  gruss  10786  ismre  17529  mreintcl  17534  mremre  17543  submre  17544  mrcval  17549  mrccl  17550  mrcun  17561  ismri  17570  acsfiel  17593  isacs1i  17596  catcoppccl  18062  catcoppcclOLD  18063  acsdrsel  18491  acsdrscl  18494  acsficl  18495  pmtrval  19311  pmtrrn  19317  istopg  22378  uniopn  22380  iscld  22512  ntrval  22521  clsval  22522  discld  22574  mretopd  22577  neival  22587  isnei  22588  lpval  22624  restdis  22663  ordtbaslem  22673  ordtuni  22675  cndis  22776  tgcmp  22886  hauscmplem  22891  comppfsc  23017  elkgen  23021  xkoopn  23074  elqtop  23182  kqffn  23210  isfbas  23314  filss  23338  snfbas  23351  elfg  23356  ufilss  23390  fixufil  23407  cfinufil  23413  ufinffr  23414  ufilen  23415  fin1aufil  23417  flimclslem  23469  hauspwpwf1  23472  supnfcls  23505  flimfnfcls  23513  ptcmplem1  23537  tsmsfbas  23613  blfvalps  23870  blfps  23893  blf  23894  bcthlem5  24826  minveclem3b  24926  sigaclcuni  33053  sigaclcu2  33055  pwsiga  33065  erdsze2lem2  34132  cvmsval  34194  cvmsss2  34202  neibastop2lem  35182  tailf  35197  pibt2  36235  fin2so  36412  sdclem1  36548  elrfirn  41365  elrfirn2  41366  istopclsd  41370  nacsfix  41382  dnnumch1  41718  inpw  47404
  Copyright terms: Public domain W3C validator