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

Theorem elpw2 4108
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 4107 . 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 2740    C_ wss 3094   ~Pcpw 3566
This theorem is referenced by:  axpweq  4125  abexssex  5680  knatar  5756  canth  6225  dffi3  7117  marypha1lem  7119  r1pwss  7389  rankr1bg  7408  pwwf  7412  unwf  7415  rankval2  7423  uniwf  7424  rankpwi  7428  aceq3lem  7680  dfac2a  7689  dfac12lem2  7703  cflim3  7821  cflim2  7822  cfslb  7825  axdc3lem4  8012  axdc4lem  8014  axdclem  8079  grothpw  8381  uzf  10165  ixxf  10597  fzf  10717  rpnnen2lem1  12420  rpnnen2lem2  12421  bitsf  12545  sadfval  12570  smufval  12595  smupf  12596  vdwapf  12946  prdsval  13282  prdsds  13290  prdshom  13293  mreacs  13487  acsfn  13488  wunnat  13757  lubval  14040  glbval  14045  clatlem  14143  issubm  14352  issubg  14548  cntzval  14724  sylow1lem2  14837  lsmvalx  14877  pj1fval  14930  issubrg  15472  islss  15619  lspval  15659  lspcl  15660  islbs  15756  lbsextlem1  15838  lbsextlem3  15840  lbsextlem4  15841  sraval  15856  aspval  15995  ocvfval  16493  ocvval  16494  isobs  16547  leordtval2  16869  cnpfval  16891  iscnp2  16896  uncmp  17057  cmpfi  17062  cmpfii  17063  2ndc1stc  17104  1stcrest  17106  islly2  17137  hausllycmp  17147  lly1stc  17149  1stckgenlem  17175  xkotf  17207  txlly  17257  txnlly  17258  tx1stc  17271  basqtop  17329  tgqtop  17330  alexsubALTlem3  17670  alexsubALTlem4  17671  alexsubALT  17672  cncfval  18319  cnllycmp  18381  bndth  18383  ishtpy  18397  ovolficcss  18756  ovolval  18760  ovolicc2  18808  ismbl  18812  mblsplit  18818  voliunlem2  18835  voliunlem3  18836  vitalilem4  18893  vitalilem5  18894  dvfval  19174  dvnfval  19198  cpnfval  19208  plyval  19502  dmarea  20179  wilthlem2  20234  issh  21712  ocval  21784  spanval  21837  hsupval  21838  sshjval  21854  sshjval3  21858  erdszelem1  23059  kur14lem9  23082  kur14  23084  cnllyscon  23113  umgrabi  23244  isidlNEW  24778  vtarsuelt  25227  cover2  25690  cntotbnd  25852  heibor1lem  25865  heibor  25877  isidl  25971  igenval  26018  elmzpcl  26136  eldiophb  26168  rpnnen3  26457  islssfgi  26502  islinds  26611  hbt  26666  elmnc  26673  itgoval  26698  itgocn  26701  rgspnval  26705  paddval  29117  pclvalN  29209  polvalN  29224  docavalN  30443  djavalN  30455  dicval  30496  dochval  30671  djhval  30718  lpolconN  30807
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 4081
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 2742  df-in 3101  df-ss 3108  df-pw 3568
  Copyright terms: Public domain W3C validator