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

Theorem elpw2g 4355
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 3799 . 2  |-  ( A  e.  ~P B  ->  A  C_  B )
2 ssexg 4341 . . . 4  |-  ( ( A  C_  B  /\  B  e.  V )  ->  A  e.  _V )
3 elpwg 3798 . . . . 5  |-  ( A  e.  _V  ->  ( A  e.  ~P B  <->  A 
C_  B ) )
43biimparc 474 . . . 4  |-  ( ( A  C_  B  /\  A  e.  _V )  ->  A  e.  ~P B
)
52, 4syldan 457 . . 3  |-  ( ( A  C_  B  /\  B  e.  V )  ->  A  e.  ~P B
)
65expcom 425 . 2  |-  ( B  e.  V  ->  ( A  C_  B  ->  A  e.  ~P B ) )
71, 6impbid2 196 1  |-  ( B  e.  V  ->  ( A  e.  ~P B  <->  A 
C_  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    e. wcel 1725   _Vcvv 2948    C_ wss 3312   ~Pcpw 3791
This theorem is referenced by:  elpw2  4356  pwnss  4357  knatar  6071  pw2f1olem  7203  fineqvlem  7314  elfir  7411  marypha1  7430  r1sscl  7700  tskwe  7826  dfac8alem  7899  acni2  7916  fin1ai  8162  fin2i  8164  fin23lem7  8185  fin23lem11  8186  isfin2-2  8188  fin23lem39  8219  isf34lem1  8241  isf34lem2  8242  isf34lem4  8246  isf34lem5  8247  fin1a2lem7  8275  fin1a2lem12  8280  canthnumlem  8512  canthp1lem2  8517  wunss  8576  tsken  8618  tskss  8622  gruss  8660  ramub1lem1  13382  ismre  13803  mreintcl  13808  mremre  13817  submre  13818  mrcval  13823  mrccl  13824  mrcun  13835  ismri  13844  mreexd  13855  mreexexlem4d  13860  acsfiel  13867  isacs1i  13870  catcoppccl  14251  acsdrsel  14581  acsdrscl  14584  acsficl  14585  opsrval  16523  istopg  16956  uniopn  16958  iscld  17079  ntrval  17088  clsval  17089  discld  17141  mretopd  17144  neival  17154  isnei  17155  lpval  17191  restdis  17230  ordtbaslem  17240  ordtuni  17242  cncls  17326  cndis  17343  tgcmp  17452  hauscmplem  17457  elkgen  17556  xkoopn  17609  elqtop  17717  kqffn  17745  isfbas  17849  filss  17873  snfbas  17886  elfg  17891  fbasrn  17904  ufilss  17925  fixufil  17942  cfinufil  17948  ufinffr  17949  ufilen  17950  fin1aufil  17952  rnelfmlem  17972  flimclslem  18004  hauspwpwf1  18007  supnfcls  18040  flimfnfcls  18048  ptcmplem1  18071  tsmsfbas  18145  blfvalps  18401  blfps  18424  blf  18425  bcthlem5  19269  minveclem3b  19317  sigaclcuni  24489  sigaclcu2  24491  pwsiga  24501  erdsze2lem2  24878  cvmsval  24941  cvmsss2  24949  comppfsc  26324  neibastop2lem  26326  tailf  26341  sdclem1  26384  elrfirn  26686  elrfirn2  26687  istopclsd  26691  nacsfix  26703  dnnumch1  27056  pmtrval  27309  pmtrrn  27314
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-sep 4322
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-v 2950  df-in 3319  df-ss 3326  df-pw 3793
  Copyright terms: Public domain W3C validator