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

Theorem elpw2 4563
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 4562 . 2  |-  ( B  e.  _V  ->  ( A  e.  ~P B  <->  A 
C_  B ) )
31, 2ax-mp 5 1  |-  ( A  e.  ~P B  <->  A  C_  B
)
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    e. wcel 1758   _Vcvv 3076    C_ wss 3435   ~Pcpw 3967
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4520
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3078  df-in 3442  df-ss 3449  df-pw 3969
This theorem is referenced by:  axpweq  4576  knatar  6156  canth  6157  dffi3  7791  marypha1lem  7793  r1pwss  8101  rankr1bg  8120  pwwf  8124  unwf  8127  rankval2  8135  uniwf  8136  rankpwi  8140  aceq3lem  8400  dfac2a  8409  dfac12lem2  8423  axdc3lem4  8732  axdc4lem  8734  axdclem  8798  grothpw  9103  uzf  10974  ixxf  11420  fzf  11557  incexclem  13416  rpnnen2lem1  13614  rpnnen2lem2  13615  bitsf  13740  sadfval  13765  smufval  13790  smupf  13791  vdwapf  14150  prdsval  14511  prdsds  14520  prdshom  14523  mreacs  14714  acsfn  14715  wunnat  14984  lubeldm  15269  lubval  15272  glbeldm  15282  glbval  15285  clatlem  15399  clatlubcl2  15401  clatglbcl2  15403  issubm  15593  issubg  15799  cntzval  15957  sylow1lem2  16218  lsmvalx  16258  pj1fval  16311  issubrg  16987  islss  17138  lspval  17178  lspcl  17179  islbs  17279  lbsextlem1  17361  lbsextlem3  17363  lbsextlem4  17364  sraval  17379  aspval  17521  ocvfval  18215  ocvval  18216  isobs  18269  islinds  18362  leordtval2  18947  cnpfval  18969  iscnp2  18974  uncmp  19137  cmpfi  19142  cmpfii  19143  2ndc1stc  19186  1stcrest  19188  islly2  19219  hausllycmp  19229  lly1stc  19231  1stckgenlem  19257  xkotf  19289  txlly  19340  txnlly  19341  tx1stc  19354  basqtop  19415  tgqtop  19416  alexsubALTlem3  19752  alexsubALTlem4  19753  alexsubALT  19754  sszcld  20525  cncfval  20595  cnllycmp  20659  bndth  20661  ishtpy  20675  ovolficcss  21084  ovolval  21088  ovolicc2  21136  ismbl  21140  mblsplit  21146  voliunlem3  21165  vitalilem4  21223  vitalilem5  21224  dvfval  21504  dvnfval  21528  cpnfval  21538  plyval  21793  dmarea  22483  wilthlem2  22539  umgrabi  23755  issh  24761  ocval  24834  spanval  24887  hsupval  24888  sshjval  24904  sshjval3  24908  sigagensiga  26728  dya2iocuni  26841  ballotlemelo  27013  ballotlem2  27014  ballotth  27063  erdszelem1  27222  kur14lem9  27245  kur14  27247  cnllyscon  27277  cover2  28754  cntotbnd  28842  heibor1lem  28855  heibor  28867  isidl  28961  igenval  29008  elmzpcl  29209  eldiophb  29242  rpnnen3  29528  islssfgi  29572  hbt  29633  elmnc  29640  itgoval  29665  itgocn  29668  rgspnval  29672  paddval  33765  pclvalN  33857  polvalN  33872  docavalN  35091  djavalN  35103  dicval  35144  dochval  35319  djhval  35366  lpolconN  35455
  Copyright terms: Public domain W3C validator