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

Theorem elpw2 4169
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 4168 . 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 1688   _Vcvv 2789    C_ wss 3153   ~Pcpw 3626
This theorem is referenced by:  axpweq  4186  abexssex  5742  knatar  5818  canth  6287  dffi3  7179  marypha1lem  7181  r1pwss  7451  rankr1bg  7470  pwwf  7474  unwf  7477  rankval2  7485  uniwf  7486  rankpwi  7490  aceq3lem  7742  dfac2a  7751  dfac12lem2  7765  cflim3  7883  cflim2  7884  cfslb  7887  axdc3lem4  8074  axdc4lem  8076  axdclem  8141  grothpw  8443  uzf  10228  ixxf  10660  fzf  10780  incexclem  12289  rpnnen2lem1  12487  rpnnen2lem2  12488  bitsf  12612  sadfval  12637  smufval  12662  smupf  12663  vdwapf  13013  prdsval  13349  prdsds  13357  prdshom  13360  mreacs  13554  acsfn  13555  wunnat  13824  lubval  14107  glbval  14112  clatlem  14210  issubm  14419  issubg  14615  cntzval  14791  sylow1lem2  14904  lsmvalx  14944  pj1fval  14997  issubrg  15539  islss  15686  lspval  15726  lspcl  15727  islbs  15823  lbsextlem1  15905  lbsextlem3  15907  lbsextlem4  15908  sraval  15923  aspval  16062  ocvfval  16560  ocvval  16561  isobs  16614  leordtval2  16936  cnpfval  16958  iscnp2  16963  uncmp  17124  cmpfi  17129  cmpfii  17130  2ndc1stc  17171  1stcrest  17173  islly2  17204  hausllycmp  17214  lly1stc  17216  1stckgenlem  17242  xkotf  17274  txlly  17324  txnlly  17325  tx1stc  17338  basqtop  17396  tgqtop  17397  alexsubALTlem3  17737  alexsubALTlem4  17738  alexsubALT  17739  cncfval  18386  cnllycmp  18448  bndth  18450  ishtpy  18464  ovolficcss  18823  ovolval  18827  ovolicc2  18875  ismbl  18879  mblsplit  18885  voliunlem2  18902  voliunlem3  18903  vitalilem4  18960  vitalilem5  18961  dvfval  19241  dvnfval  19265  cpnfval  19275  plyval  19569  dmarea  20246  wilthlem2  20301  issh  21779  ocval  21851  spanval  21904  hsupval  21905  sshjval  21921  sshjval3  21925  erdszelem1  23126  kur14lem9  23149  kur14  23151  cnllyscon  23180  umgrabi  23311  isidlNEW  24845  vtarsuelt  25294  cover2  25757  cntotbnd  25919  heibor1lem  25932  heibor  25944  isidl  26038  igenval  26085  elmzpcl  26203  eldiophb  26235  rpnnen3  26524  islssfgi  26569  islinds  26678  hbt  26733  elmnc  26740  itgoval  26765  itgocn  26768  rgspnval  26772  paddval  29254  pclvalN  29346  polvalN  29361  docavalN  30580  djavalN  30592  dicval  30633  dochval  30808  djhval  30855  lpolconN  30944
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1538  ax-5 1549  ax-17 1608  ax-9 1641  ax-8 1648  ax-6 1707  ax-7 1712  ax-11 1719  ax-12 1869  ax-ext 2265  ax-sep 4142
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1534  df-nf 1537  df-sb 1636  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-v 2791  df-in 3160  df-ss 3167  df-pw 3628
  Copyright terms: Public domain W3C validator