MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ssid Structured version   Visualization version   GIF version

Theorem ssid 3622
Description: Any class is a subclass of itself. Exercise 10 of [TakeutiZaring] p. 18. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Andrew Salmon, 14-Jun-2011.)
Assertion
Ref Expression
ssid 𝐴𝐴

Proof of Theorem ssid
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 id 22 . 2 (𝑥𝐴𝑥𝐴)
21ssriv 3605 1 𝐴𝐴
Colors of variables: wff setvar class
Syntax hints:  wcel 1989  wss 3572
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1485  df-ex 1704  df-nf 1709  df-sb 1880  df-clab 2608  df-cleq 2614  df-clel 2617  df-in 3579  df-ss 3586
This theorem is referenced by:  eqimssi  3657  eqimss2i  3658  nsspssun  3855  difid  3946  inv1  3968  disjpss  4026  pwidg  4171  elssuni  4465  unimax  4471  intmin  4495  rintn0  4617  sseliALT  4789  xpss1  5226  xpss2  5227  residm  5428  resdm  5439  resmpt3  5448  ssrnres  5570  ordunidif  5771  dffn3  6052  fdmrn  6062  fvreseq1  6316  fimacnv  6345  iunpw  6975  onsucuni  7025  tfisi  7055  fparlem3  7276  fparlem4  7277  funsssuppss  7318  suppofss1d  7329  suppofss2d  7330  tfrlem1  7469  tz7.48-2  7534  oaordi  7623  omwordi  7648  omass  7657  nnaordi  7695  nnmwordi  7712  fpmg  7880  ralxpmap  7904  boxcutc  7948  domss2  8116  0fin  8185  en1eqsn  8187  findcard2d  8199  fimax2g  8203  domunfican  8230  pwfi  8258  fissuni  8268  fipreima  8269  fsuppmptif  8302  fsuppco2  8305  fsuppcor  8306  mapfienlem1  8307  mapfienlem2  8308  fimin2g  8400  wofib  8447  wemapso  8453  noinfep  8554  cantnfval2  8563  cantnfp1lem3  8574  cantnflem1  8583  tcidm  8619  tc0  8620  r1rankidb  8664  r1pw  8705  rankr1id  8722  scott0  8746  htalem  8756  xpomen  8835  infpwfien  8882  alephsmo  8922  dfac12lem3  8964  ackbij2lem4  9061  cflem  9065  cflecard  9072  cflim2  9082  cfslb  9085  fin4en1  9128  fin23lem13  9151  fin23lem15  9153  fin23lem36  9167  isf32lem1  9172  fin67  9214  dcomex  9266  zorn2lem4  9318  alephexp2  9400  fpwwe2lem13  9461  canthnumlem  9467  wunex2  9557  wuncidm  9565  eltsk2g  9570  axgroth6  9647  axgroth3  9650  xrsup  12662  expcl  12873  hashcard  13141  hashf1lem2  13235  xptrrel  13713  cotrtrclfv  13747  rtrclreclem1  13792  rtrclreclem2  13793  lo1eq  14293  rlimeq  14294  serclim0  14302  isercolllem2  14390  isercoll  14392  summolem3  14439  isum  14444  fsumser  14455  fsumcl  14458  fsum2d  14496  fsumabs  14527  fsumrlim  14537  fsumo1  14538  fsumiun  14547  flo1  14580  prodmolem3  14657  iprod  14662  iprodn0  14664  fprodss  14672  fprodcl  14676  fprod2d  14705  fprodclf  14717  risefaccl  14740  fallfaccl  14741  eflt  14841  rpnnen2lem3  14939  rpnnen2lem5  14941  rpnnen2lem11  14947  rpnnen2lem12  14948  rexpen  14951  eulerthlem2  15481  ressid  15929  ressinbas  15930  mremre  16258  catsubcat  16493  yon11  16898  yon12  16899  yon2  16900  yonpropd  16902  oppcyon  16903  yonffth  16918  oduclatb  17138  ipopos  17154  fpwipodrs  17158  submid  17345  mulgnncl  17550  mulgnnclOLD  17551  mulgnn0cl  17552  mulgcl  17553  subgid  17590  ghmghmrn  17673  cntrnsg  17768  symggen  17884  sylow3lem5  18040  lsmss1  18073  lsmss2  18075  gsumzres  18304  gsumzcl2  18305  gsumzf1o  18307  gsumadd  18317  gsumzmhm  18331  gsumzoppg  18338  gsum2dlem1  18363  gsum2dlem2  18364  gsum2d  18365  dprdfinv  18412  dprdf1  18426  dmdprdsplitlem  18430  dprd2db  18436  dpjidcl  18451  ablfac1eulem  18465  ablfac1eu  18466  ablfaclem2  18479  gsumdixp  18603  subrgid  18776  lcomfsupp  18897  lss1  18933  lbsextlem1  19152  rlmval2  19188  rlmbas  19189  rlmplusg  19190  rlm0  19191  rlmmulr  19193  rlmsca  19194  rlmsca2  19195  rlmvsca  19196  rlmtopn  19197  rlmds  19198  psrass1lem  19371  mplsubglem  19428  mpllsslem  19429  mplsubrglem  19433  mplcoe1  19459  mplcoe5  19462  mplbas2  19464  evlslem4  19502  psrbagev1  19504  evlslem2  19506  znf1o  19894  zntoslem  19899  regsumsupp  19962  css0  20027  uvcresum  20126  frlmsslsp  20129  frlmlbs  20130  frlmup1  20131  mamures  20190  mdetrsca2  20404  mdetrlin2  20407  mdetunilem5  20416  mdetunilem9  20420  smadiadetglem1  20471  smadiadetglem2  20472  pmatcollpw3  20583  cpmadumatpolylem2  20681  topopn  20705  fiinbas  20750  topbas  20770  topcld  20833  clstop  20867  ntrtop  20868  opnneissb  20912  opnssneib  20913  opnneiid  20924  neiptopuni  20928  neiptoptop  20929  maxlp  20945  isperf2  20950  restopn2  20975  restperf  20982  idcn  21055  cnconst2  21081  lmres  21098  rncmp  21193  fiuncmp  21201  cmpfi  21205  conncn  21223  1stcelcls  21258  llyidm  21285  nllyidm  21286  toplly  21287  ssref  21309  refref  21310  kgentopon  21335  kgencn2  21354  ptpjpre1  21368  ptbasfi  21378  ptcld  21410  xkopt  21452  elqtop2  21498  qtopuni  21499  ptcmpfi  21610  fbssfi  21635  opnfbas  21640  filtop  21653  isfil2  21654  isfild  21656  fsubbas  21665  ssfg  21670  filssufilg  21709  ufileu  21717  imaelfm  21749  rnelfm  21751  fmfnfmlem4  21755  neiflim  21772  supnfcls  21818  fclscf  21823  flimfnfcls  21826  tsmsfbas  21925  utopbas  22033  xpsxmet  22179  xpsdsval  22180  xpsmet  22181  tmsxms  22285  tmsms  22286  imasf1oxms  22288  imasf1oms  22289  prdsxms  22329  prdsms  22330  tmsxpsval  22337  retopbas  22558  cnngp  22577  cnopn  22584  cnperf  22617  retopconn  22626  fsumcn  22667  abscncf  22698  recncf  22699  imcncf  22700  cjcncf  22701  mulc1cncf  22702  cncfcn1  22707  cncfmpt2f  22711  cncfmpt2ss  22712  addccncf  22713  cdivcncf  22714  negcncf  22715  negfcncf  22716  abscncfALT  22717  cnmpt2pc  22721  xrhmeo  22739  oprpiece1res1  22744  oprpiece1res2  22745  cnrehmeo  22746  iscau3  23070  caubl  23100  caublcls  23101  rrxcph  23174  rrxmval  23182  rrxdstprj1  23186  evthicc2  23223  ovolre  23287  volsuplem  23317  uniiccdif  23340  uniioovol  23341  uniiccvol  23342  uniioombllem3  23347  uniioombllem4  23348  uniioombllem5  23349  dyadmbllem  23361  volcn  23368  volivth  23369  itgfsum  23587  iblabslem  23588  iblabs  23589  bddmulibl  23599  cnlimc  23646  cnlimci  23647  dvres3  23671  dvres3a  23672  dvidlem  23673  dvcnp2  23677  dvcn  23678  dvnadd  23686  dvnres  23688  cpnord  23692  cpnres  23694  dvaddbr  23695  dvmulbr  23696  dvcmul  23701  dvcmulf  23702  dvcobr  23703  dvcjbr  23706  dvrec  23712  dvmptntr  23728  dvmptfsum  23732  dveflem  23736  dvef  23737  rolle  23747  dvlipcn  23751  c1liplem1  23753  dvgt0lem2  23760  dvivth  23767  lhop1lem  23770  dvfsumabs  23780  ftc1a  23794  ftc1cn  23800  ftc2  23801  deg1mul3le  23870  plyssc  23950  plyeq0  23961  coeeulem  23974  0dgr  23995  coemulc  24005  coe0  24006  coesub  24007  coe1termlem  24008  dgrmulc  24021  dgrsub  24022  dgrcolem1  24023  dgrcolem2  24024  dvnply2  24036  plycpn  24038  plyremlem  24053  fta1lem  24056  vieta1lem2  24060  aalioulem3  24083  dvntaylp  24119  taylthlem1  24121  taylthlem2  24122  ulmcn  24147  psercn  24174  pserdv  24177  abelth  24189  efcn  24191  efcvx  24197  pige3  24263  dvrelog  24377  logcn  24387  dvloglem  24388  dvlog  24391  dvlog2  24393  efopnlem2  24397  logccv  24403  cxpcn  24480  cxpcn2  24481  cxpcn3  24483  resqrtcn  24484  sqrtcn  24485  loglesqrt  24493  atancn  24657  rlimcnp3  24688  jensen  24709  lgamgulmlem2  24750  ftalem3  24795  basellem2  24802  dchrfi  24974  dchrisumlema  25171  pntrsumo1  25248  pntrsumbnd  25249  pntlem3  25292  uhgrsubgrself  26166  uhgrspansubgr  26177  nbupgr  26234  nbumgrvtx  26236  nbgr2vtx1edg  26240  cusgrexilem2  26332  ifpsnprss  26512  umgr2adedgwlk  26835  umgr2adedgwlkon  26836  umgr2adedgspth  26838  upgr1wlkdlem2  26999  1pthon2ve  27007  sspid  27564  ssps  27569  helch  28084  hhssnv  28105  hhsssh  28110  shintcl  28173  chintcl  28175  shlesb1i  28229  omlsi  28247  chlejb1i  28319  chm0i  28333  chabs1  28359  chabs2  28360  spanun  28388  cmidi  28453  pjidmcoi  29020  csmdsymi  29177  sumdmdlem2  29262  dmdbr5ati  29265  mdcompli  29272  dmdcompli  29273  disjdifprg  29372  fcoinver  29402  xppreima  29433  padct  29482  xrinfm  29504  clatp0cl  29656  clatp1cl  29657  xrsmulgzz  29663  xrsp0  29666  xrsp1  29667  gsumle  29764  gsummpt2co  29765  gsumvsca1  29767  gsumvsca2  29768  mdetpmtr1  29874  reff  29891  locfinreflem  29892  pnfneige0  29982  esumsnf  30111  esumcvg  30133  pwsiga  30178  sigagenid  30199  baselcarsg  30353  iblidicc  30655  cxpcncf1  30658  efmul2picn  30659  fdvposlt  30662  fdvneggt  30663  fdvposle  30664  fdvnegge  30665  reprfz1  30687  breprexplemc  30695  circlemeth  30703  circlevma  30705  circlemethhgt  30706  logdivsqrle  30713  hgt750lemb  30719  hgt750lema  30720  hgt750leme  30721  tgoldbachgtde  30723  bnj1253  31070  cvmlift2lem6  31275  mrsubrn  31395  mrsubff1  31396  mrsub0  31398  mrsubccat  31400  mrsubcn  31401  elmrsubrn  31402  elmsubrn  31410  msubrn  31411  msubff1  31438  mthmpps  31464  trpredtr  31714  trpredpo  31719  wzel  31755  wzelOLD  31756  frrlem5c  31770  frrlem10  31775  nosupbnd1lem1  31838  imagesset  32044  ivthALT  32314  fness  32328  fneref  32329  refssfne  32337  fnemeet1  32345  fnejoin2  32348  filnetlem2  32358  filnetlem4  32360  ontgval  32414  knoppcnlem10  32476  knoppcnlem11  32477  knoppndvlem6  32492  knoppndv  32509  bj-rabtr  32910  bj-rabtrALTALT  32912  bj-rabtrAUTO  32913  bj-disj2r  32997  bj-restsnid  33024  bj-restpw  33029  bj-restb  33031  bj-resta  33033  bj-restuni2  33035  elxp8  33199  mblfinlem3  33428  mblfinlem4  33429  ismblfin  33430  ovoliunnfl  33431  voliunnfl  33433  volsupnfl  33434  mbfposadd  33437  ftc1cnnclem  33463  ftc1cnnc  33464  ftc1anc  33473  ftc2nc  33474  areacirclem2  33481  areacirclem3  33482  areacirclem4  33483  areacirc  33485  welb  33511  caures  33536  constcncf  33538  idcncf  33539  sub1cncf  33540  sub2cncf  33541  cnresima  33543  rngoidl  33803  atpsubN  34865  pol1N  35022  1psubclN  35056  cdlemefrs32fva  35514  dia2dimlem13  36191  dibord  36274  dochvalr  36472  hdmapevec  36953  ismrcd1  37087  ismrc  37090  incssnn0  37100  mzpclall  37116  rmydioph  37407  rmxdioph  37409  expdiophlem2  37415  expdioph  37416  aomclem6  37455  kelac1  37459  gicabl  37495  rgspnid  37568  itgpowd  37626  arearect  37627  areaquad  37628  clcnvlem  37756  cnvtrucl0  37757  cnvtrcl0  37759  fvilbd  37807  relexp0a  37834  brfvrtrcld  37852  corcltrcl  37857  clsk3nimkb  38164  clsk1indlem2  38166  ntrclskb  38193  k0004ss2  38276  wnefimgd  38286  wfximgfd  38289  extoimad  38290  funfvima2d  38295  nzss  38342  lhe4.4ex1a  38354  dvsconst  38355  dvsid  38356  dvsef  38357  dvconstbi  38359  binomcxplemnn0  38374  onfrALTlem3  38585  onfrALTlem3VD  38949  unisn0  39048  ssinc  39090  ssdec  39091  founiiun  39182  founiiun0  39199  choicefi  39214  evthiccabs  39527  islptre  39657  climconstmpt  39696  fnlimfvre  39712  cncfshift  39856  addccncf2  39858  fsumcncf  39860  cncfperiod  39861  negcncfg  39863  cncfcompt  39865  ioccncflimc  39867  cncfuni  39868  icccncfext  39869  cncficcgt0  39870  icocncflimc  39871  cncfiooicclem1  39875  cncfiooicc  39876  cncfiooiccre  39877  cxpcncf2  39882  fprodcncf  39883  add1cncf  39884  add2cncf  39885  sub1cncfd  39886  sub2cncfd  39887  dvcosre  39895  dvcnre  39899  fperdvper  39902  dvmptresicc  39903  dvmptfprod  39929  itgsinexplem1  39938  itgcoscmulx  39954  ibliooicc  39956  itgsincmulx  39959  itgsubsticclem  39960  itgiccshift  39965  itgperiod  39966  itgsbtaddcnst  39967  dirkeritg  40088  dirkercncflem2  40090  dirkercncflem4  40092  fourierdlem16  40109  fourierdlem18  40111  fourierdlem21  40114  fourierdlem22  40115  fourierdlem23  40116  fourierdlem32  40125  fourierdlem33  40126  fourierdlem39  40132  fourierdlem40  40133  fourierdlem57  40149  fourierdlem58  40150  fourierdlem59  40151  fourierdlem62  40154  fourierdlem68  40160  fourierdlem72  40164  fourierdlem73  40165  fourierdlem74  40166  fourierdlem75  40167  fourierdlem76  40168  fourierdlem78  40170  fourierdlem83  40175  fourierdlem84  40176  fourierdlem85  40177  fourierdlem88  40180  fourierdlem93  40185  fourierdlem94  40186  fourierdlem95  40187  fourierdlem97  40189  fourierdlem101  40193  fourierdlem103  40195  fourierdlem104  40196  fourierdlem111  40203  fourierdlem112  40204  fourierdlem113  40205  sqwvfoura  40214  sqwvfourb  40215  fouriersw  40217  fouriercn  40218  etransclem18  40238  etransclem22  40242  etransclem34  40254  etransclem46  40266  etransclem47  40267  sge0fsum  40373  meaiininclem  40469  hoidmvlelem2  40579  hspdifhsp  40599  hspmbllem2  40610  hspmbl  40612  iinhoiicclem  40656  pimgtmnf2  40693  smflimsuplem1  40795  smflimsuplem6  40800  funresfunco  40974  submgmid  41564  rnghmsscmap2  41744  rhmsscmap2  41790  srhmsubc  41847  fldhmsubc  41855  srhmsubcALTV  41865  fldhmsubcALTV  41873  elbigolo1  42122
  Copyright terms: Public domain W3C validator