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

Theorem elpwi 3972
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 3971 . 2  |-  ( A  e.  ~P B  -> 
( A  e.  ~P B 
<->  A  C_  B )
)
21ibi 249 1  |-  ( A  e.  ~P B  ->  A  C_  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1898    C_ wss 3416   ~Pcpw 3963
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-v 3059  df-in 3423  df-ss 3430  df-pw 3965
This theorem is referenced by:  elpwid  3973  elelpwi  3974  elpwunsn  4024  elpw2g  4580  f1opw2  6549  eldifpw  6630  iunpw  6632  f1opwfi  7904  fi0  7960  fiin  7962  marypha1lem  7973  marypha1  7974  marypha2  7979  brwdom2  8114  brwdom3  8123  r1pwss  8281  rankpwi  8320  acndom  8508  acnnum  8509  dfac12r  8602  ackbij2lem1  8675  ackbij1lem6  8681  ackbij1b  8695  isfin2-2  8775  ssfin2  8776  enfin2i  8777  compsscnvlem  8826  compssiso  8830  fin11a  8839  enfin1ai  8840  fin12  8869  fin1a2s  8870  fin1a2  8871  hsmexlem2  8883  tskwe2  9224  inttsk  9225  inatsk  9229  hashbclem  12648  pr2pwpr  12669  elss2prb  12676  qshash  13934  incexclem  13943  incexc  13944  incexc2  13945  rpnnen2  14327  smupf  14501  ramval  15009  ramvalOLD  15010  ramlb  15026  mrcflem  15561  isacs2  15608  mreacs  15613  acsfn  15614  acsfn1  15616  acsfn2  15618  sscpwex  15769  fpwipodrs  16459  isacs3lem  16461  isacs4lem  16463  isacs5lem  16464  isacs5  16467  pmtrfrn  17148  oppglsm  17343  lspf  18246  pptbas  20072  clsf  20112  mretopd  20157  neiptopuni  20195  cncls2  20338  cncls  20339  cnntr  20340  restcnrm  20427  cncmp  20456  tgcmp  20465  uncmp  20467  sscmp  20469  hauscmplem  20470  cmpfi  20472  1stcrest  20517  dis2ndc  20524  lly1stc  20560  dislly  20561  comppfsc  20596  kgentopon  20602  kgen2ss  20619  kgencn  20620  kgencn2  20621  kgencn3  20622  txcmplem2  20706  txcmp  20707  tx1stc  20714  txkgen  20716  xkopt  20719  xkococnlem  20723  xkococn  20724  kqnrmlem1  20807  kqnrmlem2  20808  hmphdis  20860  isfil2  20920  isfild  20922  fbasfip  20932  neifil  20944  trfil2  20951  trufil  20974  fixufil  20986  cfinufil  20992  fin1aufil  20996  fclscmp  21094  alexsubALTlem2  21112  alexsubALTlem3  21113  alexsubALTlem4  21114  ptcmplem5  21120  tgpconcompeqg  21175  imasf1oxms  21553  met2ndc  21587  zdis  21883  icccmp  21892  ovolf  22484  ismbl2  22530  cmmbl  22537  nulmbl  22538  nulmbl2  22539  unmbl  22540  shftmbl  22541  voliunlem2  22553  ioombl1  22564  uniioombl  22596  sqff1o  24158  musum  24169  eengtrkg  25064  usgrares1  25187  rabfodom  28189  elpwincl1  28203  fpwrelmap  28367  cmpcref  28726  pcmplfinf  28737  esumcst  28933  esumfsup  28940  esum2d  28963  dmvlsiga  29000  pwsiga  29001  sigaclci  29003  sigainb  29007  insiga  29008  pwldsys  29028  ldgenpisyslem1  29034  ldgenpisyslem3  29036  measinb  29092  measres  29093  cntmeas  29097  volmeas  29103  ddemeas  29108  dya2iocucvr  29155  sxbrsigalem1  29156  omscl  29168  omsf  29169  omsclOLD  29172  omsfOLD  29173  omsmon  29175  oms0OLD  29178  omsmonOLD  29179  baselcarsg  29187  difelcarsg  29191  carsgsiga  29203  omsmeas  29204  omsmeasOLD  29205  coinflippv  29365  kur14  29988  conpcon  30007  cvmsi  30037  neibastop1  31064  neibastop2lem  31065  neibastop3  31067  onsucsuccmpi  31152  limsucncmpi  31154  ismblfin  32026  cover2  32085  sstotbnd3  32153  heibor1  32187  heibor  32198  pclvalN  33500  pclfinN  33510  pclcmpatN  33511  dochfN  34969  elrfi  35581  cmpfiiin  35584  ismrcd2  35586  isnacs3  35597  aomclem2  35958  islssfg  35973  lmhmfgsplit  35989  lnrfg  36023  acsfn1p  36110  sspwtr  37249  sspwtrALT  37250  sspwtrALT2  37259  pwtrVD  37260  pwtrrVD  37261  sspwimp  37355  sspwimpVD  37356  sspwimpcf  37357  sspwimpcfVD  37358  sspwimpALT  37362  sspwimpALT2  37365  pwssfi  37419  elpwinss  37425  ssnnf1octb  37508  dvdmsscn  37849  dvnmptconst  37854  dvnxpaek  37855  dvnmul  37856  dvnprodlem3  37861  stoweidlem57  37956  pwsal  38214  prsal  38217  intsal  38227  salexct  38231  sge0rnre  38244  sge0tsms  38260  sge0cl  38261  sge0fsum  38267  sge0sup  38271  sge0less  38272  sge0gerp  38275  sge0resplit  38286  sge0split  38289  nnfoctbdj  38332  ismeannd  38343  psmeasure  38347  caragen0  38365  caragenunidm  38367  caragenuncl  38372  caragendifcl  38373  omeiunle  38376  carageniuncl  38382  caragensal  38384  caratheodorylem2  38386  0ome  38388  isomennd  38390  caragenel2d  38391  caragencmpl  38394  ovnf  38423  ovn02  38428  ovnsubaddlem1  38430  ovnsubaddlem2  38431  ovnsubadd  38432  hspmbl  38489  edgassv2  39329  umgrres1lem  39427  upgrres1  39430  uhgrvd00  39621  uhgraedgrnv  39936  edgssv2ALT  39986  edgssv2  39987  lincdifsn  40490  lcosslsp  40504  lindslinindsimp1  40523  lincresunit3lem1  40545  lincresunit3lem2  40546  lincresunit3  40547  aacllem  40813
  Copyright terms: Public domain W3C validator