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

Theorem elpw2 4128
Description: Membership in a power class. Theorem 86 of [Suppes] p. 47. (Contributed by NM, 11-Oct-2007.)
Hypothesis
Ref Expression
elpw2.1  |-  B  e. 
_V
Assertion
Ref Expression
elpw2  |-  ( A  e.  ~P B  <->  A  C_  B
)

Proof of Theorem elpw2
StepHypRef Expression
1 elpw2.1 . 2  |-  B  e. 
_V
2 elpw2g 4127 . 2  |-  ( B  e.  _V  ->  ( A  e.  ~P B  <->  A 
C_  B ) )
31, 2ax-mp 10 1  |-  ( A  e.  ~P B  <->  A  C_  B
)
Colors of variables: wff set class
Syntax hints:    <-> wb 178    e. wcel 1621   _Vcvv 2757    C_ wss 3113   ~Pcpw 3585
This theorem is referenced by:  axpweq  4145  abexssex  5701  knatar  5777  canth  6246  dffi3  7138  marypha1lem  7140  r1pwss  7410  rankr1bg  7429  pwwf  7433  unwf  7436  rankval2  7444  uniwf  7445  rankpwi  7449  aceq3lem  7701  dfac2a  7710  dfac12lem2  7724  cflim3  7842  cflim2  7843  cfslb  7846  axdc3lem4  8033  axdc4lem  8035  axdclem  8100  grothpw  8402  uzf  10186  ixxf  10618  fzf  10738  rpnnen2lem1  12441  rpnnen2lem2  12442  bitsf  12566  sadfval  12591  smufval  12616  smupf  12617  vdwapf  12967  prdsval  13303  prdsds  13311  prdshom  13314  mreacs  13508  acsfn  13509  wunnat  13778  lubval  14061  glbval  14066  clatlem  14164  issubm  14373  issubg  14569  cntzval  14745  sylow1lem2  14858  lsmvalx  14898  pj1fval  14951  issubrg  15493  islss  15640  lspval  15680  lspcl  15681  islbs  15777  lbsextlem1  15859  lbsextlem3  15861  lbsextlem4  15862  sraval  15877  aspval  16016  ocvfval  16514  ocvval  16515  isobs  16568  leordtval2  16890  cnpfval  16912  iscnp2  16917  uncmp  17078  cmpfi  17083  cmpfii  17084  2ndc1stc  17125  1stcrest  17127  islly2  17158  hausllycmp  17168  lly1stc  17170  1stckgenlem  17196  xkotf  17228  txlly  17278  txnlly  17279  tx1stc  17292  basqtop  17350  tgqtop  17351  alexsubALTlem3  17691  alexsubALTlem4  17692  alexsubALT  17693  cncfval  18340  cnllycmp  18402  bndth  18404  ishtpy  18418  ovolficcss  18777  ovolval  18781  ovolicc2  18829  ismbl  18833  mblsplit  18839  voliunlem2  18856  voliunlem3  18857  vitalilem4  18914  vitalilem5  18915  dvfval  19195  dvnfval  19219  cpnfval  19229  plyval  19523  dmarea  20200  wilthlem2  20255  issh  21733  ocval  21805  spanval  21858  hsupval  21859  sshjval  21875  sshjval3  21879  erdszelem1  23080  kur14lem9  23103  kur14  23105  cnllyscon  23134  umgrabi  23265  isidlNEW  24799  vtarsuelt  25248  cover2  25711  cntotbnd  25873  heibor1lem  25886  heibor  25898  isidl  25992  igenval  26039  elmzpcl  26157  eldiophb  26189  rpnnen3  26478  islssfgi  26523  islinds  26632  hbt  26687  elmnc  26694  itgoval  26719  itgocn  26722  rgspnval  26726  paddval  29138  pclvalN  29230  polvalN  29245  docavalN  30464  djavalN  30476  dicval  30517  dochval  30692  djhval  30739  lpolconN  30828
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