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

Theorem elpw2g 4366
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 3809 . 2  |-  ( A  e.  ~P B  ->  A  C_  B )
2 ssexg 4352 . . . 4  |-  ( ( A  C_  B  /\  B  e.  V )  ->  A  e.  _V )
3 elpwg 3808 . . . . 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 4    <-> wb 178    e. wcel 1726   _Vcvv 2958    C_ wss 3322   ~Pcpw 3801
This theorem is referenced by:  elpw2  4367  pwnss  4368  knatar  6083  pw2f1olem  7215  fineqvlem  7326  elfir  7423  marypha1  7442  r1sscl  7714  tskwe  7842  dfac8alem  7915  acni2  7932  fin1ai  8178  fin2i  8180  fin23lem7  8201  fin23lem11  8202  isfin2-2  8204  fin23lem39  8235  isf34lem1  8257  isf34lem2  8258  isf34lem4  8262  isf34lem5  8263  fin1a2lem7  8291  fin1a2lem12  8296  canthnumlem  8528  canthp1lem2  8533  wunss  8592  tsken  8634  tskss  8638  gruss  8676  ramub1lem1  13399  ismre  13820  mreintcl  13825  mremre  13834  submre  13835  mrcval  13840  mrccl  13841  mrcun  13852  ismri  13861  mreexd  13872  mreexexlem4d  13877  acsfiel  13884  isacs1i  13887  catcoppccl  14268  acsdrsel  14598  acsdrscl  14601  acsficl  14602  opsrval  16540  istopg  16973  uniopn  16975  iscld  17096  ntrval  17105  clsval  17106  discld  17158  mretopd  17161  neival  17171  isnei  17172  lpval  17208  restdis  17247  ordtbaslem  17257  ordtuni  17259  cncls  17343  cndis  17360  tgcmp  17469  hauscmplem  17474  elkgen  17573  xkoopn  17626  elqtop  17734  kqffn  17762  isfbas  17866  filss  17890  snfbas  17903  elfg  17908  fbasrn  17921  ufilss  17942  fixufil  17959  cfinufil  17965  ufinffr  17966  ufilen  17967  fin1aufil  17969  rnelfmlem  17989  flimclslem  18021  hauspwpwf1  18024  supnfcls  18057  flimfnfcls  18065  ptcmplem1  18088  tsmsfbas  18162  blfvalps  18418  blfps  18441  blf  18442  bcthlem5  19286  minveclem3b  19334  sigaclcuni  24506  sigaclcu2  24508  pwsiga  24518  erdsze2lem2  24895  cvmsval  24958  cvmsss2  24966  comppfsc  26401  neibastop2lem  26403  tailf  26418  sdclem1  26461  elrfirn  26763  elrfirn2  26764  istopclsd  26768  nacsfix  26780  dnnumch1  27133  pmtrval  27385  pmtrrn  27390
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-sep 4333
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2960  df-in 3329  df-ss 3336  df-pw 3803
  Copyright terms: Public domain W3C validator