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

Theorem elpwi 3633
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 3632 . 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 1684    C_ wss 3152   ~Pcpw 3625
This theorem is referenced by:  elpwid  3634  elelpwi  3635  elpw2g  4174  eldifpw  4566  elpwunsn  4568  iunpw  4570  f1opw2  6071  f1opwfi  7159  fival  7166  fi0  7173  fiin  7175  dffi2  7176  elfiun  7183  marypha1lem  7186  marypha1  7187  marypha2  7192  brwdom2  7287  brwdom3  7296  r1pwss  7456  rankpwi  7495  tskwe  7583  acndom  7678  acnnum  7679  acndom2  7681  fodomfi2  7687  infpwfien  7689  dfac12lem2  7770  dfac12r  7772  ackbij2lem1  7845  ackbij1lem6  7851  ackbij1lem9  7854  ackbij1lem10  7855  ackbij1lem11  7856  ackbij1lem16  7861  ackbij1b  7865  cfss  7891  fin23lem7  7942  fin23lem11  7943  isfin2-2  7945  ssfin2  7946  enfin2i  7947  isf32lem8  7986  compsscnvlem  7996  compssiso  8000  isf34lem4  8003  isf34lem7  8005  isf34lem6  8006  fin11a  8009  enfin1ai  8010  fin12  8039  fin1a2s  8040  fin1a2  8041  hsmexlem2  8053  ttukeylem6  8141  tskwe2  8395  inttsk  8396  inatsk  8400  uzssz  10247  elfzoelz  10875  hashbclem  11390  qshash  12285  ackbijnn  12286  incexclem  12295  incexc  12296  incexc2  12297  rpnnen2  12504  smupf  12669  smuval2  12673  smupvallem  12674  smueqlem  12681  ramval  13055  ramlb  13066  ramub1lem1  13073  ramub1lem2  13074  restid2  13335  mress  13495  mrcflem  13508  mrcuni  13523  isacs2  13555  mreacs  13560  acsfn  13561  acsfn1  13563  acsfn2  13565  sscpwex  13692  isdrs2  14073  fpwipodrs  14267  ipodrsima  14268  isacs3lem  14269  isacs4lem  14271  isacs5lem  14272  isacs5  14275  lagsubg2  14678  cntzrcl  14803  sylow1lem2  14910  sylow1lem3  14911  sylow1lem4  14912  sylow2alem2  14929  sylow2a  14930  oppglsm  14953  lsmpropd  14986  lssacs  15724  lspf  15731  lbsextlem2  15912  lbsextlem3  15913  lbsextlem4  15914  elocv  16568  ppttop  16744  pptbas  16745  epttop  16746  clsf  16785  clsval2  16787  mretopd  16829  ordtbas  16922  subbascn  16984  cncls2  17002  cncls  17003  cnntr  17004  restcnrm  17090  cncmp  17119  discmp  17125  tgcmp  17128  uncmp  17130  sscmp  17132  hauscmplem  17133  cmpfi  17135  concompcon  17158  1stcfb  17171  1stcrest  17179  2ndcdisj  17182  dis2ndc  17186  restnlly  17208  nllyrest  17212  nllyidm  17215  cldllycmp  17221  lly1stc  17222  dislly  17223  kgentopon  17233  1stckgenlem  17248  kgen2ss  17250  kgencn  17251  kgencn2  17252  kgencn3  17253  dfac14  17312  xkoccn  17313  txnlly  17331  txcmplem2  17336  txcmp  17337  tx1stc  17344  txkgen  17346  xkopt  17349  xkoco2cn  17352  xkococnlem  17353  xkococn  17354  xkoinjcn  17381  tgqtop  17403  kqnrmlem1  17434  kqnrmlem2  17435  nrmhmph  17485  hmphdis  17487  fbelss  17528  fbssfi  17532  isfil2  17551  isfild  17553  infil  17558  fbasfip  17563  neifil  17575  trfil2  17582  isufil2  17603  trufil  17605  fixufil  17617  cfinufil  17623  fin1aufil  17627  fclscmp  17725  alexsubALTlem2  17742  alexsubALTlem3  17743  alexsubALTlem4  17744  ptcmplem5  17750  tgpconcompeqg  17794  blssm  17968  blin2  17975  imasf1oxms  18035  met2ndc  18069  zdis  18322  icccmplem2  18328  icccmp  18330  cncfrss  18395  cncfrss2  18396  bndth  18456  lebnum  18462  ovolf  18841  ovolicc2  18881  ismbl2  18886  cmmbl  18892  nulmbl  18893  nulmbl2  18894  unmbl  18895  shftmbl  18896  voliunlem2  18908  ioombl1  18919  uniioombl  18944  vitalilem5  18967  i1fd  19036  dvbsss  19252  perfdvf  19253  plybss  19576  wilthlem2  20307  sqff1o  20420  musum  20431  ubthlem1  21449  ssnnssfz  23277  esumval  23425  esumcst  23436  esumpcvgval  23446  esumcvg  23454  elsigass  23486  dmvlsiga  23490  sigaclci  23493  sigainb  23497  insiga  23498  measinb  23548  measres  23549  cntmeas  23553  coinflippv  23684  kur14  23747  conpcon  23766  cvmsi  23796  cvmliftmolem2  23813  cvmlift3lem8  23857  umgrass  23871  eupath2  23904  onsucsuccmpi  24882  limsucncmpi  24884  inpws1  25042  iscst4  25177  imtr  25398  prsubrtr  25399  basexre  25522  intrr  25699  isconcl3b  26099  comppfsc  26307  neibastop1  26308  neibastop2lem  26309  neibastop2  26310  neibastop3  26311  filnetlem4  26330  cover2  26358  sstotbnd3  26500  heibor1  26534  heiborlem3  26537  heiborlem5  26539  heiborlem6  26540  heiborlem10  26544  heibor  26545  elrfi  26769  elrfirn  26770  elrfirn2  26771  cmpfiiin  26772  ismrcd2  26774  istopclsd  26775  mrefg3  26783  isnacs3  26785  aomclem2  27152  islssfg  27168  lsmfgcl  27172  lmhmfgima  27182  lmhmfgsplit  27184  lnrfg  27323  elmnc  27341  pmtrfrn  27400  acsfn1p  27507  stoweidlem39  27788  stoweidlem50  27799  stoweidlem57  27806  sspwtr  28595  sspwtrALT  28596  sspwtrALT2  28597  pwtrVD  28598  pwtrOLD  28599  pwtrrVD  28600  pwtrrOLD  28601  sspwimp  28694  sspwimpVD  28695  sspwimpcf  28696  sspwimpcfVD  28697  sspwimpALT  28701  sspwimpALT2  28705  pclvalN  30079  pclfinN  30089  pclcmpatN  30090  dochfN  31546  mapd1o  31838
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-in 3159  df-ss 3166  df-pw 3627
  Copyright terms: Public domain W3C validator