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

Theorem elpw2g 5251
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 4536 . 2 (𝐴 ∈ 𝒫 𝐵𝐴𝐵)
2 ssexg 5230 . . . 4 ((𝐴𝐵𝐵𝑉) → 𝐴 ∈ V)
3 elpwg 4530 . . . . 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 3420  wss 3880  𝒫 cpw 4527
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2113  ax-9 2121  ax-ext 2709  ax-sep 5206
This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2072  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3071  df-v 3422  df-in 3887  df-ss 3897  df-pw 4529
This theorem is referenced by:  elpw2  5252  elpwi2OLD  5254  pwnss  5255  difelpw  5257  rabelpw  5258  pw2f1olem  8771  fineqvlem  8916  elfir  9055  r1sscl  9425  tskwe  9590  dfac8alem  9667  acni2  9684  fin1ai  9931  fin2i  9933  fin23lem7  9954  fin23lem11  9955  isfin2-2  9957  fin23lem39  9988  isf34lem1  10010  isf34lem2  10011  isf34lem4  10015  isf34lem5  10016  fin1a2lem12  10049  canthnumlem  10286  tsken  10392  tskss  10396  gruss  10434  ismre  17117  mreintcl  17122  mremre  17131  submre  17132  mrcval  17137  mrccl  17138  mrcun  17149  ismri  17158  acsfiel  17181  isacs1i  17184  catcoppccl  17647  catcoppcclOLD  17648  acsdrsel  18073  acsdrscl  18076  acsficl  18077  pmtrval  18867  pmtrrn  18873  istopg  21816  uniopn  21818  iscld  21948  ntrval  21957  clsval  21958  discld  22010  mretopd  22013  neival  22023  isnei  22024  lpval  22060  restdis  22099  ordtbaslem  22109  ordtuni  22111  cndis  22212  tgcmp  22322  hauscmplem  22327  comppfsc  22453  elkgen  22457  xkoopn  22510  elqtop  22618  kqffn  22646  isfbas  22750  filss  22774  snfbas  22787  elfg  22792  ufilss  22826  fixufil  22843  cfinufil  22849  ufinffr  22850  ufilen  22851  fin1aufil  22853  flimclslem  22905  hauspwpwf1  22908  supnfcls  22941  flimfnfcls  22949  ptcmplem1  22973  tsmsfbas  23049  blfvalps  23305  blfps  23328  blf  23329  bcthlem5  24249  minveclem3b  24349  sigaclcuni  31822  sigaclcu2  31824  pwsiga  31834  erdsze2lem2  32902  cvmsval  32964  cvmsss2  32972  neibastop2lem  34312  tailf  34327  pibt2  35351  fin2so  35527  sdclem1  35664  elrfirn  40248  elrfirn2  40249  istopclsd  40253  nacsfix  40265  dnnumch1  40600  inpw  45865
  Copyright terms: Public domain W3C validator