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

Theorem elpwid 3772
Description: An element of a power class is a subclass. Deduction form of elpwi 3771. (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 3771 . 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 1721    C_ wss 3284   ~Pcpw 3763
This theorem is referenced by:  fopwdom  7179  ssenen  7244  fival  7379  dffi2  7390  elfiun  7397  tskwe  7797  acndom2  7895  fodomfi2  7901  infpwfien  7903  dfac12lem2  7984  ackbij1lem9  8068  ackbij1lem10  8069  ackbij1lem11  8070  ackbij1lem16  8075  ackbij2lem3  8081  cfss  8105  fin23lem7  8156  fin23lem11  8157  enfin2i  8161  isf32lem8  8200  isf34lem4  8217  isf34lem7  8219  isf34lem6  8220  isfin1-3  8226  fin1a2lem13  8252  ttukeylem6  8354  uzssz  10465  elfzoelz  11099  ackbijnn  12566  incexclem  12575  smuval2  12953  smupvallem  12954  smueqlem  12961  ramub1lem1  13353  ramub1lem2  13354  restid2  13617  mress  13777  mrcuni  13805  mreexexlem4d  13831  mreexexd  13832  mreexdomd  13833  acsfn  13843  isdrs2  14355  ipodrsima  14550  isacs3lem  14551  acsfiindd  14562  lagsubg2  14960  cntzrcl  15085  sylow1lem2  15192  sylow1lem3  15193  sylow1lem4  15194  sylow2alem2  15211  sylow2a  15212  lsmpropd  15268  lssacs  16002  lssacsex  16175  lbsextlem2  16190  lbsextlem3  16191  lbsextlem4  16192  elocv  16854  ppttop  17030  epttop  17032  clsval2  17073  mretopd  17115  neiss2  17124  neiptopnei  17155  ordtbas  17214  subbascn  17276  discmp  17419  uncmp  17424  concompcon  17452  1stcfb  17465  2ndcdisj  17476  restnlly  17502  nllyrest  17506  nllyidm  17509  cldllycmp  17515  1stckgenlem  17542  dfac14  17607  xkoccn  17608  txnlly  17626  txkgen  17641  xkopt  17644  xkoco2cn  17647  xkoinjcn  17676  tgqtop  17701  nrmhmph  17783  fbelss  17822  fbssfi  17826  infil  17852  alexsubALTlem3  18037  alexsubALTlem4  18038  ustssxp  18191  trust  18216  utopsnneiplem  18234  blssm  18405  blin2  18416  metustssOLD  18540  metustss  18541  metustfbasOLD  18552  metustfbas  18553  metustOLD  18554  metust  18555  metutopOLD  18569  psmetutop  18570  restmetu  18574  icccmplem2  18811  cncfrss  18878  cncfrss2  18879  bndth  18940  lebnum  18946  ovolicc2  19375  vitalilem5  19461  i1fd  19530  dvbsss  19746  perfdvf  19747  plybss  20070  wilthlem2  20809  uhgrass  21298  umgrass  21311  usgrass  21341  eupath2  21659  ubthlem1  22329  ssnnssfz  24105  indf1ofs  24380  esumval  24398  esumel  24399  gsumesum  24408  esumlub  24409  esumpcvgval  24425  esumcvg  24433  elsigass  24465  br2base  24576  sxbrsigalem0  24578  dya2iocucvr  24591  sxbrsigalem2  24593  sxbrsiga  24597  coinfliplem  24693  ballotlemfmpn  24709  cvmliftmolem2  24926  cvmlift3lem8  24970  cnambfre  26158  neibastop1  26282  neibastop2lem  26283  neibastop2  26284  filnetlem4  26304  heiborlem3  26416  heiborlem5  26418  heiborlem6  26419  heiborlem10  26423  heibor  26424  elrfirn  26643  elrfirn2  26644  ismrcd1  26646  istopclsd  26648  mrefg3  26656  aomclem2  27024  lsmfgcl  27044  lmhmfgima  27054  elmnc  27213  stoweidlem39  27659  stoweidlem50  27670  mapd1o  32135
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2389
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2395  df-cleq 2401  df-clel 2404  df-nfc 2533  df-v 2922  df-in 3291  df-ss 3298  df-pw 3765
  Copyright terms: Public domain W3C validator