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

Theorem elpwi 3857
Description: Subset relation implied by membership in a power class. (Contributed by NM, 17-Feb-2007.)
Assertion
Ref Expression
elpwi  |-  ( A  e.  ~P B  ->  A  C_  B )

Proof of Theorem elpwi
StepHypRef Expression
1 elpwg 3856 . 2  |-  ( A  e.  ~P B  -> 
( A  e.  ~P B 
<->  A  C_  B )
)
21ibi 241 1  |-  ( A  e.  ~P B  ->  A  C_  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1755    C_ wss 3316   ~Pcpw 3848
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-v 2964  df-in 3323  df-ss 3330  df-pw 3850
This theorem is referenced by:  elpwid  3858  elelpwi  3859  elpwunsn  3905  elpw2g  4443  f1opw2  6302  eldifpw  6377  iunpw  6379  f1opwfi  7603  fi0  7658  fiin  7660  marypha1lem  7671  marypha1  7672  marypha2  7677  brwdom2  7776  brwdom3  7785  r1pwss  7979  rankpwi  8018  acndom  8209  acnnum  8210  dfac12r  8303  ackbij2lem1  8376  ackbij1lem6  8382  ackbij1b  8396  isfin2-2  8476  ssfin2  8477  enfin2i  8478  compsscnvlem  8527  compssiso  8531  fin11a  8540  enfin1ai  8541  fin12  8570  fin1a2s  8571  fin1a2  8572  hsmexlem2  8584  tskwe2  8927  inttsk  8928  inatsk  8932  pr2pwpr  12166  hashbclem  12188  qshash  13272  incexclem  13281  incexc  13282  incexc2  13283  rpnnen2  13490  smupf  13656  ramval  14051  ramlb  14062  mrcflem  14526  isacs2  14573  mreacs  14578  acsfn  14579  acsfn1  14581  acsfn2  14583  sscpwex  14710  fpwipodrs  15316  isacs3lem  15318  isacs4lem  15320  isacs5lem  15321  isacs5  15324  pmtrfrn  15943  oppglsm  16120  lspf  16976  pptbas  18453  clsf  18493  mretopd  18537  neiptopuni  18575  cncls2  18718  cncls  18719  cnntr  18720  restcnrm  18807  cncmp  18836  tgcmp  18845  uncmp  18847  sscmp  18849  hauscmplem  18850  cmpfi  18852  1stcrest  18898  dis2ndc  18905  lly1stc  18941  dislly  18942  kgentopon  18952  kgen2ss  18969  kgencn  18970  kgencn2  18971  kgencn3  18972  txcmplem2  19056  txcmp  19057  tx1stc  19064  txkgen  19066  xkopt  19069  xkococnlem  19073  xkococn  19074  tgqtop  19126  kqnrmlem1  19157  kqnrmlem2  19158  hmphdis  19210  isfil2  19270  isfild  19272  fbasfip  19282  neifil  19294  trfil2  19301  isufil2  19322  trufil  19324  fixufil  19336  cfinufil  19342  fin1aufil  19346  fclscmp  19444  alexsubALTlem2  19461  alexsubALTlem3  19462  alexsubALTlem4  19463  ptcmplem5  19469  tgpconcompeqg  19523  imasf1oxms  19905  met2ndc  19939  zdis  20234  icccmp  20243  ovolf  20806  ismbl2  20851  cmmbl  20857  nulmbl  20858  nulmbl2  20859  unmbl  20860  shftmbl  20861  voliunlem2  20873  ioombl1  20884  uniioombl  20910  sqff1o  22404  musum  22415  f1otrg  22939  eengtrkg  23053  usgrares1  23145  esumcst  26367  esumfsup  26372  dmvlsiga  26425  pwsiga  26426  sigaclci  26428  sigainb  26432  insiga  26433  measinb  26488  measres  26489  cntmeas  26493  volmeas  26500  ddemeas  26505  dya2iocucvr  26552  sxbrsigalem1  26553  coinflippv  26713  kur14  26951  conpcon  26971  cvmsi  27001  onsucsuccmpi  28136  limsucncmpi  28138  ismblfin  28273  comppfsc  28420  neibastop1  28421  neibastop2lem  28422  neibastop3  28424  cover2  28448  sstotbnd3  28516  heibor1  28550  heibor  28561  elrfi  28872  cmpfiiin  28875  ismrcd2  28877  isnacs3  28888  aomclem2  29250  islssfg  29265  lmhmfgsplit  29281  lnrfg  29317  acsfn1p  29398  stoweidlem57  29695  uhgraedgrnv  30116  lincdifsn  30664  lcosslsp  30678  lindslinindsimp1  30697  lincresunit3lem1  30719  lincresunit3lem2  30720  lincresunit3  30721  sspwtr  31254  sspwtrALT  31255  sspwtrALT2  31258  pwtrVD  31259  pwtrrVD  31260  sspwimp  31353  sspwimpVD  31354  sspwimpcf  31355  sspwimpcfVD  31356  sspwimpALT  31360  sspwimpALT2  31363  pclvalN  33104  pclfinN  33114  pclcmpatN  33115  dochfN  34571
  Copyright terms: Public domain W3C validator