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

Theorem elpw2g 4857
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 4201 . 2 (𝐴 ∈ 𝒫 𝐵𝐴𝐵)
2 ssexg 4837 . . . 4 ((𝐴𝐵𝐵𝑉) → 𝐴 ∈ V)
3 elpwg 4199 . . . . 5 (𝐴 ∈ V → (𝐴 ∈ 𝒫 𝐵𝐴𝐵))
43biimparc 503 . . . 4 ((𝐴𝐵𝐴 ∈ V) → 𝐴 ∈ 𝒫 𝐵)
52, 4syldan 486 . . 3 ((𝐴𝐵𝐵𝑉) → 𝐴 ∈ 𝒫 𝐵)
65expcom 450 . 2 (𝐵𝑉 → (𝐴𝐵𝐴 ∈ 𝒫 𝐵))
71, 6impbid2 216 1 (𝐵𝑉 → (𝐴 ∈ 𝒫 𝐵𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wcel 2030  Vcvv 3231  wss 3607  𝒫 cpw 4191
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-in 3614  df-ss 3621  df-pw 4193
This theorem is referenced by:  elpw2  4858  elpwi2  4859  pwnss  4860  pw2f1olem  8105  fineqvlem  8215  elfir  8362  marypha1  8381  r1sscl  8686  tskwe  8814  dfac8alem  8890  acni2  8907  fin1ai  9153  fin2i  9155  fin23lem7  9176  fin23lem11  9177  isfin2-2  9179  fin23lem39  9210  isf34lem1  9232  isf34lem2  9233  isf34lem4  9237  isf34lem5  9238  fin1a2lem12  9271  canthnumlem  9508  canthp1lem2  9513  tsken  9614  tskss  9618  gruss  9656  ramub1lem1  15777  ismre  16297  mreintcl  16302  mremre  16311  submre  16312  mrcval  16317  mrccl  16318  mrcun  16329  ismri  16338  mreexexlem4d  16354  acsfiel  16362  isacs1i  16365  catcoppccl  16805  acsdrsel  17214  acsdrscl  17217  acsficl  17218  pmtrval  17917  pmtrrn  17923  opsrval  19522  istopg  20748  uniopn  20750  iscld  20879  ntrval  20888  clsval  20889  discld  20941  mretopd  20944  neival  20954  isnei  20955  lpval  20991  restdis  21030  ordtbaslem  21040  ordtuni  21042  cncls  21126  cndis  21143  tgcmp  21252  hauscmplem  21257  comppfsc  21383  elkgen  21387  xkoopn  21440  elqtop  21548  kqffn  21576  isfbas  21680  filss  21704  snfbas  21717  elfg  21722  fbasrn  21735  ufilss  21756  fixufil  21773  cfinufil  21779  ufinffr  21780  ufilen  21781  fin1aufil  21783  rnelfmlem  21803  flimclslem  21835  hauspwpwf1  21838  supnfcls  21871  flimfnfcls  21879  ptcmplem1  21903  tsmsfbas  21978  blfvalps  22235  blfps  22258  blf  22259  bcthlem5  23171  minveclem3b  23245  sigaclcuni  30309  sigaclcu2  30311  pwsiga  30321  erdsze2lem2  31312  cvmsval  31374  cvmsss2  31382  neibastop2lem  32480  tailf  32495  bj-ismoored  33187  fin2so  33526  sdclem1  33669  elrfirn  37575  elrfirn2  37576  istopclsd  37580  nacsfix  37592  dnnumch1  37931
  Copyright terms: Public domain W3C validator