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

Theorem elpw2g 4127
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 3593 . 2  |-  ( A  e.  ~P B  ->  A  C_  B )
2 ssexg 4120 . . . 4  |-  ( ( A  C_  B  /\  B  e.  V )  ->  A  e.  _V )
3 elpwg 3592 . . . . 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 2757    C_ wss 3113   ~Pcpw 3585
This theorem is referenced by:  elpw2  4128  knatar  5777  pwnss  6251  pw2f1olem  6920  fineqvlem  7031  elfir  7123  marypha1  7141  r1sscl  7411  tskwe  7537  dfac8alem  7610  acni2  7627  fin1ai  7873  fin2i  7875  fin23lem7  7896  fin23lem11  7897  isfin2-2  7899  fin23lem39  7930  isf34lem1  7952  isf34lem2  7953  isf34lem4  7957  isf34lem5  7958  fin1a2lem7  7986  fin1a2lem12  7991  canthnumlem  8224  canthp1lem2  8229  wunss  8288  tsken  8330  tskss  8334  gruss  8372  ramub1lem1  13021  ismre  13440  mreintcl  13445  mremre  13454  submre  13455  mrcval  13460  mrccl  13461  mrcun  13472  ismri  13481  mreexd  13492  mreexexlem4d  13497  acsfiel  13504  isacs1i  13507  catcoppccl  13888  acsdrsel  14218  acsdrscl  14221  acsficl  14222  opsrval  16164  istopg  16589  uniopn  16591  iscld  16712  ntrval  16721  clsval  16722  discld  16774  mretopd  16777  neiss2  16786  neival  16787  isnei  16788  lpval  16819  restdis  16857  ordtbaslem  16866  ordtuni  16868  cncls  16951  cndis  16967  tgcmp  17076  hauscmplem  17081  elkgen  17179  xkoopn  17232  elqtop  17336  kqffn  17364  isfbas  17472  filss  17496  snfbas  17509  elfg  17514  fbasrn  17527  ufilss  17548  fixufil  17565  cfinufil  17571  ufinffr  17572  ufilen  17573  fin1aufil  17575  rnelfmlem  17595  flimclslem  17627  hauspwpwf1  17630  supnfcls  17663  flimfnfcls  17671  ptcmplem1  17694  tsmsfbas  17758  blfval  17895  blf  17909  bcthlem5  18698  minveclem3b  18740  erdsze2lem2  23093  cvmsval  23155  cvmsss2  23163  ump  24398  islimrs  24933  comppfsc  25660  neibastop2lem  25662  tailf  25677  sdclem1  25806  elrfirn  26123  elrfirn2  26124  istopclsd  26128  nacsfix  26140  dnnumch1  26494  pmtrval  26747  pmtrrn  26752
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 1927  ax-ext 2237  ax-sep 4101
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 1884  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-v 2759  df-in 3120  df-ss 3127  df-pw 3587
  Copyright terms: Public domain W3C validator