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

Theorem elpwid 4022
Description: An element of a power class is a subclass. Deduction form of elpwi 4021. (Contributed by David Moews, 1-May-2017.)
Hypothesis
Ref Expression
elpwid.1
Assertion
Ref Expression
elpwid

Proof of Theorem elpwid
StepHypRef Expression
1 elpwid.1 . 2
2 elpwi 4021 . 2
31, 2syl 16 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  e.wcel 1818  C_wss 3475  ~Pcpw 4012
This theorem is referenced by:  fopwdom  7645  ssenen  7711  fival  7892  dffi2  7903  elfiun  7910  tskwe  8352  acndom2  8456  fodomfi2  8462  infpwfien  8464  dfac12lem2  8545  ackbij1lem9  8629  ackbij1lem10  8630  ackbij1lem11  8631  ackbij1lem16  8636  ackbij2lem3  8642  cfss  8666  fin23lem7  8717  fin23lem11  8718  enfin2i  8722  isf32lem8  8761  isf34lem4  8778  isf34lem7  8780  isf34lem6  8781  isfin1-3  8787  fin1a2lem13  8813  ttukeylem6  8915  uzssz  11129  elfzoelz  11829  ackbijnn  13640  incexclem  13648  smuval2  14132  smupvallem  14133  smueqlem  14140  ramub1lem1  14544  ramub1lem2  14545  restid2  14828  mress  14990  mrcuni  15018  mreexexlem4d  15044  mreexexd  15045  mreexdomd  15046  acsfn  15056  isdrs2  15568  ipodrsima  15795  isacs3lem  15796  acsfiindd  15807  lagsubg2  16262  cntzrcl  16365  sylow1lem2  16619  sylow1lem3  16620  sylow1lem4  16621  sylow2alem2  16638  sylow2a  16639  lsmpropd  16695  lssacs  17613  lssacsex  17790  lbsextlem2  17805  lbsextlem3  17806  lbsextlem4  17807  elocv  18699  ppttop  19508  epttop  19510  clsval2  19551  mretopd  19593  neiss2  19602  neiptopnei  19633  ordtbas  19693  subbascn  19755  discmp  19898  uncmp  19903  concompcon  19933  1stcfb  19946  2ndcdisj  19957  restnlly  19983  nllyrest  19987  nllyidm  19990  cldllycmp  19996  1stckgenlem  20054  dfac14  20119  xkoccn  20120  txnlly  20138  txkgen  20153  xkopt  20156  xkoco2cn  20159  xkoinjcn  20188  tgqtop  20213  nrmhmph  20295  fbelss  20334  fbssfi  20338  infil  20364  alexsubALTlem3  20549  alexsubALTlem4  20550  ustssxp  20707  trust  20732  utopsnneiplem  20750  blssm  20921  blin2  20932  metustssOLD  21056  metustss  21057  metustfbasOLD  21068  metustfbas  21069  metustOLD  21070  metust  21071  metutopOLD  21085  psmetutop  21086  restmetu  21090  icccmplem2  21328  cncfrss  21395  cncfrss2  21396  bndth  21458  lebnum  21464  ovolicc2  21933  vitalilem5  22021  i1fd  22088  dvbsss  22306  perfdvf  22307  plybss  22591  wilthlem2  23343  f1otrg  24174  uhgrass  24306  umgrass  24319  usgrass  24361  eupath2  24980  ubthlem1  25786  ssnnssfz  27597  indf1ofs  28039  esumval  28057  esumel  28058  gsumesum  28067  esumlub  28068  esumpcvgval  28084  esumcvg  28092  elsigass  28125  ddemeas  28208  br2base  28240  sxbrsigalem0  28242  dya2iocucvr  28255  sxbrsigalem2  28257  sxbrsiga  28261  oms0  28266  omsmon  28267  eulerpartlemgvv  28315  coinfliplem  28417  ballotlemfmpn  28433  cvmliftmolem2  28727  cvmlift3lem8  28771  cnambfre  30063  neibastop1  30177  neibastop2lem  30178  neibastop2  30179  filnetlem4  30199  heiborlem3  30309  heiborlem5  30311  heiborlem6  30312  heiborlem10  30316  heibor  30317  elrfi  30626  elrfirn  30627  elrfirn2  30628  ismrcd1  30630  istopclsd  30632  mrefg3  30640  aomclem2  31001  lsmfgcl  31020  lmhmfgima  31030  elmnc  31085  stoweidlem39  31821  stoweidlem50  31832  uhgss  32369  ssnn0ssfz  32938  mapd1o  37375
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-in 3482  df-ss 3489  df-pw 4014
  Copyright terms: Public domain W3C validator