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

Theorem elpwid 3810
Description: An element of a power class is a subclass. Deduction form of elpwi 3809. (Contributed by David Moews, 1-May-2017.)
Hypothesis
Ref Expression
elpwid.1  |-  ( ph  ->  A  e.  ~P B
)
Assertion
Ref Expression
elpwid  |-  ( ph  ->  A  C_  B )

Proof of Theorem elpwid
StepHypRef Expression
1 elpwid.1 . 2  |-  ( ph  ->  A  e.  ~P B
)
2 elpwi 3809 . 2  |-  ( A  e.  ~P B  ->  A  C_  B )
31, 2syl 16 1  |-  ( ph  ->  A  C_  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1726    C_ wss 3322   ~Pcpw 3801
This theorem is referenced by:  fopwdom  7218  ssenen  7283  fival  7419  dffi2  7430  elfiun  7437  tskwe  7839  acndom2  7937  fodomfi2  7943  infpwfien  7945  dfac12lem2  8026  ackbij1lem9  8110  ackbij1lem10  8111  ackbij1lem11  8112  ackbij1lem16  8117  ackbij2lem3  8123  cfss  8147  fin23lem7  8198  fin23lem11  8199  enfin2i  8203  isf32lem8  8242  isf34lem4  8259  isf34lem7  8261  isf34lem6  8262  isfin1-3  8268  fin1a2lem13  8294  ttukeylem6  8396  uzssz  10507  elfzoelz  11142  ackbijnn  12609  incexclem  12618  smuval2  12996  smupvallem  12997  smueqlem  13004  ramub1lem1  13396  ramub1lem2  13397  restid2  13660  mress  13820  mrcuni  13848  mreexexlem4d  13874  mreexexd  13875  mreexdomd  13876  acsfn  13886  isdrs2  14398  ipodrsima  14593  isacs3lem  14594  acsfiindd  14605  lagsubg2  15003  cntzrcl  15128  sylow1lem2  15235  sylow1lem3  15236  sylow1lem4  15237  sylow2alem2  15254  sylow2a  15255  lsmpropd  15311  lssacs  16045  lssacsex  16218  lbsextlem2  16233  lbsextlem3  16234  lbsextlem4  16235  elocv  16897  ppttop  17073  epttop  17075  clsval2  17116  mretopd  17158  neiss2  17167  neiptopnei  17198  ordtbas  17258  subbascn  17320  discmp  17463  uncmp  17468  concompcon  17497  1stcfb  17510  2ndcdisj  17521  restnlly  17547  nllyrest  17551  nllyidm  17554  cldllycmp  17560  1stckgenlem  17587  dfac14  17652  xkoccn  17653  txnlly  17671  txkgen  17686  xkopt  17689  xkoco2cn  17692  xkoinjcn  17721  tgqtop  17746  nrmhmph  17828  fbelss  17867  fbssfi  17871  infil  17897  alexsubALTlem3  18082  alexsubALTlem4  18083  ustssxp  18236  trust  18261  utopsnneiplem  18279  blssm  18450  blin2  18461  metustssOLD  18585  metustss  18586  metustfbasOLD  18597  metustfbas  18598  metustOLD  18599  metust  18600  metutopOLD  18614  psmetutop  18615  restmetu  18619  icccmplem2  18856  cncfrss  18923  cncfrss2  18924  bndth  18985  lebnum  18991  ovolicc2  19420  vitalilem5  19506  i1fd  19575  dvbsss  19791  perfdvf  19792  plybss  20115  wilthlem2  20854  uhgrass  21343  umgrass  21356  usgrass  21386  eupath2  21704  ubthlem1  22374  ssnnssfz  24150  indf1ofs  24425  esumval  24443  esumel  24444  gsumesum  24453  esumlub  24454  esumpcvgval  24470  esumcvg  24478  elsigass  24510  br2base  24621  sxbrsigalem0  24623  dya2iocucvr  24636  sxbrsigalem2  24638  sxbrsiga  24642  coinfliplem  24738  ballotlemfmpn  24754  cvmliftmolem2  24971  cvmlift3lem8  25015  cnambfre  26257  neibastop1  26390  neibastop2lem  26391  neibastop2  26392  filnetlem4  26412  heiborlem3  26524  heiborlem5  26526  heiborlem6  26527  heiborlem10  26531  heibor  26532  elrfirn  26751  elrfirn2  26752  ismrcd1  26754  istopclsd  26756  mrefg3  26764  aomclem2  27132  lsmfgcl  27151  lmhmfgima  27161  elmnc  27320  stoweidlem39  27766  stoweidlem50  27777  mapd1o  32508
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2960  df-in 3329  df-ss 3336  df-pw 3803
  Copyright terms: Public domain W3C validator