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

Theorem elpw2g 4174
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 3633 . 2  |-  ( A  e.  ~P B  ->  A  C_  B )
2 ssexg 4160 . . . 4  |-  ( ( A  C_  B  /\  B  e.  V )  ->  A  e.  _V )
3 elpwg 3632 . . . . 5  |-  ( A  e.  _V  ->  ( A  e.  ~P B  <->  A 
C_  B ) )
43biimparc 473 . . . 4  |-  ( ( A  C_  B  /\  A  e.  _V )  ->  A  e.  ~P B
)
52, 4syldan 456 . . 3  |-  ( ( A  C_  B  /\  B  e.  V )  ->  A  e.  ~P B
)
65expcom 424 . 2  |-  ( B  e.  V  ->  ( A  C_  B  ->  A  e.  ~P B ) )
71, 6impbid2 195 1  |-  ( B  e.  V  ->  ( A  e.  ~P B  <->  A 
C_  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    e. wcel 1684   _Vcvv 2788    C_ wss 3152   ~Pcpw 3625
This theorem is referenced by:  elpw2  4175  pwnss  4176  knatar  5857  pw2f1olem  6966  fineqvlem  7077  elfir  7169  marypha1  7187  r1sscl  7457  tskwe  7583  dfac8alem  7656  acni2  7673  fin1ai  7919  fin2i  7921  fin23lem7  7942  fin23lem11  7943  isfin2-2  7945  fin23lem39  7976  isf34lem1  7998  isf34lem2  7999  isf34lem4  8003  isf34lem5  8004  fin1a2lem7  8032  fin1a2lem12  8037  canthnumlem  8270  canthp1lem2  8275  wunss  8334  tsken  8376  tskss  8380  gruss  8418  ramub1lem1  13073  ismre  13492  mreintcl  13497  mremre  13506  submre  13507  mrcval  13512  mrccl  13513  mrcun  13524  ismri  13533  mreexd  13544  mreexexlem4d  13549  acsfiel  13556  isacs1i  13559  catcoppccl  13940  acsdrsel  14270  acsdrscl  14273  acsficl  14274  opsrval  16216  istopg  16641  uniopn  16643  iscld  16764  ntrval  16773  clsval  16774  discld  16826  mretopd  16829  neiss2  16838  neival  16839  isnei  16840  lpval  16871  restdis  16909  ordtbaslem  16918  ordtuni  16920  cncls  17003  cndis  17019  tgcmp  17128  hauscmplem  17133  elkgen  17231  xkoopn  17284  elqtop  17388  kqffn  17416  isfbas  17524  filss  17548  snfbas  17561  elfg  17566  fbasrn  17579  ufilss  17600  fixufil  17617  cfinufil  17623  ufinffr  17624  ufilen  17625  fin1aufil  17627  rnelfmlem  17647  flimclslem  17679  hauspwpwf1  17682  supnfcls  17715  flimfnfcls  17723  ptcmplem1  17746  tsmsfbas  17810  blfval  17947  blf  17961  bcthlem5  18750  minveclem3b  18792  sigaclcuni  23479  sigaclcu2  23481  erdsze2lem2  23735  cvmsval  23797  cvmsss2  23805  ump  25046  islimrs  25580  comppfsc  26307  neibastop2lem  26309  tailf  26324  sdclem1  26453  elrfirn  26770  elrfirn2  26771  istopclsd  26775  nacsfix  26787  dnnumch1  27141  pmtrval  27394  pmtrrn  27399
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-in 3159  df-ss 3166  df-pw 3627
  Copyright terms: Public domain W3C validator