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

Theorem elpw2g 4063
Description: Membership in a power class. Theorem 86 of [Suppes] p. 47. (Contributed by NM, 7-Aug-2000.)
Assertion
Ref Expression
elpw2g  |-  ( B  e.  V  ->  ( A  e.  ~P B  <->  A 
C_  B ) )

Proof of Theorem elpw2g
StepHypRef Expression
1 elpwi 3538 . 2  |-  ( A  e.  ~P B  ->  A  C_  B )
2 ssexg 4057 . . . 4  |-  ( ( A  C_  B  /\  B  e.  V )  ->  A  e.  _V )
3 elpwg 3537 . . . . 5  |-  ( A  e.  _V  ->  ( A  e.  ~P B  <->  A 
C_  B ) )
43biimparc 475 . . . 4  |-  ( ( A  C_  B  /\  A  e.  _V )  ->  A  e.  ~P B
)
52, 4syldan 458 . . 3  |-  ( ( A  C_  B  /\  B  e.  V )  ->  A  e.  ~P B
)
65expcom 426 . 2  |-  ( B  e.  V  ->  ( A  C_  B  ->  A  e.  ~P B ) )
71, 6impbid2 197 1  |-  ( B  e.  V  ->  ( A  e.  ~P B  <->  A 
C_  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 6    <-> wb 178    e. wcel 1621   _Vcvv 2727    C_ wss 3078   ~Pcpw 3530
This theorem is referenced by:  elpw2  4064  knatar  5709  pwnss  6183  pw2f1olem  6851  fineqvlem  6962  elfir  7053  marypha1  7071  r1sscl  7341  tskwe  7467  dfac8alem  7540  acni2  7557  fin1ai  7803  fin2i  7805  fin23lem7  7826  fin23lem11  7827  isfin2-2  7829  fin23lem39  7860  isf34lem1  7882  isf34lem2  7883  isf34lem4  7887  isf34lem5  7888  fin1a2lem7  7916  fin1a2lem12  7921  canthnumlem  8150  canthp1lem2  8155  wunss  8214  tsken  8256  tskss  8260  gruss  8298  ramub1lem1  12947  ismre  13364  mreintcl  13369  mremre  13378  submre  13379  mrcval  13384  mrccl  13385  mrcun  13396  acsfiel  13401  isacs1i  13403  catcoppccl  13784  acsdrsel  14114  acsdrscl  14117  acsficl  14118  opsrval  16048  istopg  16473  uniopn  16475  iscld  16596  ntrval  16605  clsval  16606  discld  16658  mretopd  16661  neiss2  16670  neival  16671  isnei  16672  lpval  16703  restdis  16741  ordtbaslem  16750  ordtuni  16752  cncls  16835  cndis  16851  tgcmp  16960  hauscmplem  16965  elkgen  17063  xkoopn  17116  elqtop  17220  kqffn  17248  isfbas  17356  filss  17380  snfbas  17393  elfg  17398  fbasrn  17411  ufilss  17432  fixufil  17449  cfinufil  17455  ufinffr  17456  ufilen  17457  fin1aufil  17459  rnelfmlem  17479  flimclslem  17511  hauspwpwf1  17514  supnfcls  17547  flimfnfcls  17555  ptcmplem1  17578  tsmsfbas  17642  blfval  17779  blf  17793  bcthlem5  18582  minveclem3b  18624  erdsze2lem2  22906  cvmsval  22968  cvmsss2  22976  ump  24211  islimrs  24746  comppfsc  25473  neibastop2lem  25475  tailf  25490  sdclem1  25619  elrfirn  25936  elrfirn2  25937  istopclsd  25941  nacsfix  25953  dnnumch1  26307  pmtrval  26560  pmtrrn  26565
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1926  ax-ext 2234  ax-sep 4038
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-v 2729  df-in 3085  df-ss 3089  df-pw 3532
  Copyright terms: Public domain W3C validator