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

Theorem elpwi 3709
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 3708 . 2  |-  ( A  e.  ~P B  -> 
( A  e.  ~P B 
<->  A  C_  B )
)
21ibi 232 1  |-  ( A  e.  ~P B  ->  A  C_  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1710    C_ wss 3228   ~Pcpw 3701
This theorem is referenced by:  elpwid  3710  elelpwi  3711  elpw2g  4253  eldifpw  4645  elpwunsn  4647  iunpw  4649  f1opw2  6155  f1opwfi  7246  fival  7253  fi0  7260  fiin  7262  dffi2  7263  elfiun  7270  marypha1lem  7273  marypha1  7274  marypha2  7279  brwdom2  7374  brwdom3  7383  r1pwss  7543  rankpwi  7582  tskwe  7670  acndom  7765  acnnum  7766  acndom2  7768  fodomfi2  7774  infpwfien  7776  dfac12lem2  7857  dfac12r  7859  ackbij2lem1  7932  ackbij1lem6  7938  ackbij1lem9  7941  ackbij1lem10  7942  ackbij1lem11  7943  ackbij1lem16  7948  ackbij1b  7952  cfss  7978  fin23lem7  8029  fin23lem11  8030  isfin2-2  8032  ssfin2  8033  enfin2i  8034  isf32lem8  8073  compsscnvlem  8083  compssiso  8087  isf34lem4  8090  isf34lem7  8092  isf34lem6  8093  fin11a  8096  enfin1ai  8097  fin12  8126  fin1a2s  8127  fin1a2  8128  hsmexlem2  8140  ttukeylem6  8228  tskwe2  8482  inttsk  8483  inatsk  8487  uzssz  10336  elfzoelz  10964  hashbclem  11480  qshash  12376  ackbijnn  12377  incexclem  12386  incexc  12387  incexc2  12388  rpnnen2  12595  smupf  12760  smuval2  12764  smupvallem  12765  smueqlem  12772  ramval  13146  ramlb  13157  ramub1lem1  13164  ramub1lem2  13165  restid2  13428  mress  13588  mrcflem  13601  mrcuni  13616  isacs2  13648  mreacs  13653  acsfn  13654  acsfn1  13656  acsfn2  13658  sscpwex  13785  isdrs2  14166  fpwipodrs  14360  ipodrsima  14361  isacs3lem  14362  isacs4lem  14364  isacs5lem  14365  isacs5  14368  lagsubg2  14771  cntzrcl  14896  sylow1lem2  15003  sylow1lem3  15004  sylow1lem4  15005  sylow2alem2  15022  sylow2a  15023  oppglsm  15046  lsmpropd  15079  lssacs  15817  lspf  15824  lbsextlem2  16005  lbsextlem3  16006  lbsextlem4  16007  elocv  16668  ppttop  16844  pptbas  16845  epttop  16846  clsf  16885  clsval2  16887  mretopd  16929  ordtbas  17022  subbascn  17084  cncls2  17102  cncls  17103  cnntr  17104  restcnrm  17190  cncmp  17219  discmp  17225  tgcmp  17228  uncmp  17230  sscmp  17232  hauscmplem  17233  cmpfi  17235  concompcon  17258  1stcfb  17271  1stcrest  17279  2ndcdisj  17282  dis2ndc  17286  restnlly  17308  nllyrest  17312  nllyidm  17315  cldllycmp  17321  lly1stc  17322  dislly  17323  kgentopon  17333  1stckgenlem  17348  kgen2ss  17350  kgencn  17351  kgencn2  17352  kgencn3  17353  dfac14  17412  xkoccn  17413  txnlly  17431  txcmplem2  17436  txcmp  17437  tx1stc  17444  txkgen  17446  xkopt  17449  xkoco2cn  17452  xkococnlem  17453  xkococn  17454  xkoinjcn  17481  tgqtop  17503  kqnrmlem1  17534  kqnrmlem2  17535  nrmhmph  17585  hmphdis  17587  fbelss  17624  fbssfi  17628  isfil2  17647  isfild  17649  infil  17654  fbasfip  17659  neifil  17671  trfil2  17678  isufil2  17699  trufil  17701  fixufil  17713  cfinufil  17719  fin1aufil  17723  fclscmp  17821  alexsubALTlem2  17838  alexsubALTlem3  17839  alexsubALTlem4  17840  ptcmplem5  17846  tgpconcompeqg  17890  blssm  18064  blin2  18071  imasf1oxms  18131  met2ndc  18165  zdis  18418  icccmplem2  18425  icccmp  18427  cncfrss  18492  cncfrss2  18493  bndth  18554  lebnum  18560  ovolf  18939  ovolicc2  18979  ismbl2  18984  cmmbl  18990  nulmbl  18991  nulmbl2  18992  unmbl  18993  shftmbl  18994  voliunlem2  19006  ioombl1  19017  uniioombl  19042  vitalilem5  19065  i1fd  19134  dvbsss  19350  perfdvf  19351  plybss  19674  wilthlem2  20413  sqff1o  20526  musum  20537  ubthlem1  21557  ssnnssfz  23347  neiptopuni  23443  ustrel  23517  esumval  23707  esumlub  23718  esumcst  23721  esumfsup  23726  esumpcvgval  23734  esumcvg  23742  elsigass  23774  dmvlsiga  23778  sigaclci  23781  sigainb  23785  insiga  23786  measinb  23839  measres  23840  cntmeas  23844  volmeas  23851  dya2iocucvr  23898  sxbrsigalem1  23899  coinflippv  23990  kur14  24151  conpcon  24170  cvmsi  24200  cvmliftmolem2  24217  cvmlift3lem8  24261  umgrass  24275  eupath2  24308  onsucsuccmpi  25441  limsucncmpi  25443  comppfsc  25631  neibastop1  25632  neibastop2lem  25633  neibastop2  25634  neibastop3  25635  filnetlem4  25654  cover2  25682  sstotbnd3  25823  heibor1  25857  heiborlem3  25860  heiborlem5  25862  heiborlem6  25863  heiborlem10  25867  heibor  25868  elrfi  26092  elrfirn  26093  elrfirn2  26094  cmpfiiin  26095  ismrcd2  26097  istopclsd  26098  mrefg3  26106  isnacs3  26108  aomclem2  26475  islssfg  26491  lsmfgcl  26495  lmhmfgima  26505  lmhmfgsplit  26507  lnrfg  26646  elmnc  26664  pmtrfrn  26723  acsfn1p  26830  stoweidlem39  27111  stoweidlem50  27122  stoweidlem57  27129  usgrares1  27570  sspwtr  28340  sspwtrALT  28341  sspwtrALT2  28342  pwtrVD  28343  pwtrOLD  28344  pwtrrVD  28345  pwtrrOLD  28346  sspwimp  28439  sspwimpVD  28440  sspwimpcf  28441  sspwimpcfVD  28442  sspwimpALT  28446  sspwimpALT2  28450  pclvalN  30131  pclfinN  30141  pclcmpatN  30142  dochfN  31598  mapd1o  31890
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-v 2866  df-in 3235  df-ss 3242  df-pw 3703
  Copyright terms: Public domain W3C validator