Theorem ssid 3958

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.

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐴)
2	1	ssriv 3940	1 ⊢ 𝐴 ⊆ 𝐴

Syntax hints:   ∈ wcel 2141   ⊆ wss 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814

This theorem depends on definitions:  df-bi 209  df-ss 3921

This theorem is referenced by:  ssidd  3959  eqimssd  3992  eqimsscd  3993  eqimssi  3996  eqimss2i  3997  nsspssun  4220  difidALT  4329  inv1  4351  disjpss  4414  pwidgOLD  4575  elssuni  4896  unimax  4902  intmin  4925  rintn0  5065  sseliALT  5258  inxpssres  5662  xpss1  5664  xpss2  5665  residm  5994  resdm  6010  resmpt3  6024  cnvrescnv  6178  onelssex  6391  ordunidif  6392  funresfunco  6558  dffn3  6700  fdmrn  6719  fvreseq1  7016  iunpw  7750  onsucuni  7804  tfisi  7835  fparlem3  8088  fparlem4  8089  funsssuppss  8165  tfrlem1  8341  tz7.48-2  8408  oaordi  8510  omwordi  8535  omass  8544  nnaordi  8583  nnmwordi  8600  naddunif  8659  fpmg  8846  boxcutc  8919  domss2  9104  findcard2d  9131  fimax2g  9226  domunfican  9262  fipreima  9298  fimin2g  9442  wofib  9490  wemapso  9496  noinfep  9612  cantnfval2  9621  tcidm  9696  tc0  9697  r1rankidb  9759  r1pw  9800  rankr1id  9817  scott0  9841  xpomen  9968  infpwfien  10015  alephsmo  10055  dfac12lem3  10099  cflem  10198  cflemOLD  10199  cflecard  10206  cfslb  10220  fin4en1  10263  fin23lem13  10286  fin23lem36  10302  isf32lem1  10307  fin67  10349  dcomex  10401  zorn2lem4  10453  alephexp2  10536  fpwwe2lem12  10597  canthnumlem  10603  wuncidm  10701  eltsk2g  10706  axgroth6  10783  axgroth3  10786  indconst1  12205  xrsup  13875  expcl  14089  hashcard  14365  hashf1lem2  14466  xptrrel  14990  cotrtrclfv  15022  rtrclreclem2  15069  lo1eq  15578  rlimeq  15579  serclim0  15587  isercolllem2  15676  isercoll  15678  fsum2d  15781  fsumabs  15812  fsumrlim  15822  fsumo1  15823  fsumiun  15832  fprod2d  15994  risefaccl  16028  fallfaccl  16029  eflt  16132  rpnnen2lem3  16231  rpnnen2lem5  16233  rpnnen2lem12  16240  rexpen  16243  ressbasssg  17256  ressid  17263  ressinbas  17264  oduclatb  18522  ipopos  18551  fpwipodrs  18555  ghmghmrn  19258  elcntr  19353  cntrnsg  19367  0symgefmndeq  19417  sylow3lem5  19654  lsmss1  19688  lsmss2  19690  cmnbascntr  19828  cntrcmnd  19865  cntrabl  19866  gsumzres  19932  gsumzcl2  19933  gsumzf1o  19935  gsumadd  19946  gsumzmhm  19960  gsumzoppg  19967  dprdf1  20058  ablfac1eulem  20097  gsumle  20168  subrgid  20602  srhmsubc  20709  lbsextlem1  21208  rlmval2  21239  znf1o  21583  zntoslem  21588  css0  21721  uvcresum  21825  frlmlbs  21829  psrass1lem  21965  mdetrsca2  22644  mdetrlin2  22647  mdetunilem5  22656  mdetunilem9  22660  smadiadetglem1  22711  smadiadetglem2  22712  pmatcollpw3  22824  topopn  22946  fiinbas  22992  topbas  23012  topcld  23075  ntrtop  23110  opnneissb  23154  opnssneib  23155  opnneiid  23166  maxlp  23187  isperf2  23192  restperf  23224  idcn  23297  cnconst2  23323  lmres  23340  fiuncmp  23444  1stcelcls  23501  ssref  23552  refref  23553  kgencn2  23597  ptpjpre1  23611  ptbasfi  23621  xkopt  23695  elqtop2  23741  ptcmpfi  23853  fbssfi  23877  opnfbas  23882  filtop  23895  isfil2  23896  isfild  23898  fsubbas  23907  ssfg  23912  filssufilg  23951  ufileu  23959  imaelfm  23991  rnelfm  23993  fmfnfmlem4  23997  neiflim  24014  fclscf  24065  flimfnfcls  24068  tsmsfbas  24168  xpsxmet  24420  xpsdsval  24421  xpsmet  24422  tmsxms  24526  tmsms  24527  imasf1oxms  24529  imasf1oms  24530  prdsxms  24570  prdsms  24571  tmsxpsval  24578  retopbas  24800  cnngp  24819  cnopn  24826  cnperf  24861  retopconn  24870  fsumcn  24912  abscncf  24943  recncf  24944  imcncf  24945  cjcncf  24946  mulc1cncf  24947  cncfcn1  24953  cncfmpt2f  24957  cncfmpt2ss  24958  addccncf  24959  idcncf  24960  sub1cncf  24961  sub2cncf  24962  cdivcncf  24963  negcncf  24964  negfcncf  24965  abscncfALT  24966  cnmpopc  24970  xrhmeo  24988  oprpiece1res1  24993  oprpiece1res2  24994  cnrehmeo  24995  iscau3  25320  caubl  25350  caublcls  25351  mulcncf  25488  evthicc2  25502  ovolre  25567  volsuplem  25597  uniiccdif  25620  uniioovol  25621  uniiccvol  25622  uniioombllem3  25627  uniioombllem4  25628  uniioombllem5  25629  dyadmbllem  25641  volivth  25649  itgfsum  25869  iblabslem  25870  iblabs  25871  bddmulibl  25881  cnlimc  25930  cnlimci  25931  dvcnp2  25962  dvcn  25963  cpnord  25977  cpnres  25979  dvmptntr  26013  dvmptfsum  26017  rolle  26032  dvlipcn  26036  c1liplem1  26038  dvivth  26052  dvfsumabs  26065  ftc1a  26079  ftc1cn  26085  plyssc  26240  plyeq0  26251  0dgr  26285  coemulc  26295  coe0  26296  coesub  26297  coe1termlem  26298  dgrmulc  26311  dgrsub  26312  dvnply2  26328  plycpn  26330  plyremlem  26345  fta1lem  26348  vieta1lem2  26352  aalioulem3  26375  taylthlem1  26413  taylthlem2  26414  ulmcn  26439  psercn  26466  abelth  26481  efcn  26483  efcvx  26489  dvrelog  26679  logcn  26689  dvloglem  26690  dvlog  26693  dvlog2  26695  efopnlem2  26699  logccv  26705  cxpcn  26787  cxpcn3  26790  resqrtcn  26791  sqrtcn  26792  loglesqrt  26803  atancn  26978  jensen  27030  ftalem3  27116  dchrfi  27296  dchrisumlema  27529  pntlem3  27650  madebday  27970  expscl  28501  bdaypw2n0bndlem  28533  uhgrsubgrself  29427  uhgrspansubgr  29438  umgr2adedgwlk  30091  umgr2adedgwlkon  30092  umgr2adedgspth  30094  upgr1wlkdlem2  30294  sspid  30874  ssps  30879  helch  31392  hhssnv  31413  hhsssh  31418  shintcl  31479  chintcl  31481  shlesb1i  31535  omlsi  31553  chlejb1i  31625  chm0i  31639  chabs1  31665  chabs2  31666  spanun  31694  cmidi  31759  pjidmcoi  32326  csmdsymi  32483  sumdmdlem2  32568  dmdbr5ati  32571  mdcompli  32578  dmdcompli  32579  disjdifprg  32724  fcoinver  32753  f1rnen  32780  xppreima  32797  padct  32870  xrinfm  32907  clatp0cl  33115  clatp1cl  33116  xrsp0  33151  xrsp1  33152  cntrcrng  33222  cycpmconjslem1  33295  cycpmconjslem2  33296  gsumvsca1  33367  gsumvsca2  33368  qusxpid  33510  ellspds  33515  rspidlid  33522  rlmdim  33868  reff  34097  locfinreflem  34098  esumsnf  34322  esumcvg  34344  sigagenid  34409  iblidicc  34850  cxpcncf1  34853  fdvposlt  34857  fdvneggt  34858  fdvposle  34859  fdvnegge  34860  logdivsqrle  34908  bnj1253  35276  fineqvac  35376  fineqvnttrclse  35384  noinfepfnregs  35392  cvmlift2lem6  35622  satfun  35725  mrsubrn  35827  elmrsubrn  35834  elmsubrn  35842  msubrn  35843  imagesset  36267  ivthALT  36659  fness  36673  fneref  36674  refssfne  36682  fnemeet1  36690  fnejoin2  36693  filnetlem2  36703  filnetlem4  36705  ontgval  36755  ttctrid  36826  knoppcnlem10  36904  knoppcnlem11  36905  bj-rabtr  37379  bj-rabtrAUTO  37381  bj-disj2r  37477  bj-restsnid  37541  bj-resta  37550  bj-imdirco  37646  elxp8  37829  finorwe  37840  mblfinlem3  38122  mblfinlem4  38123  ismblfin  38124  ovoliunnfl  38125  voliunnfl  38127  volsupnfl  38128  mbfposadd  38130  ftc1cnnclem  38154  ftc1cnnc  38155  ftc1anc  38164  ftc2nc  38165  areacirclem2  38172  areacirclem4  38174  areacirc  38176  caures  38223  constcncf  38225  brssrid  39045  brcnvssrid  39050  refrelid  39065  n0eldmqs  39195  atpsubN  40341  pol1N  40498  dia2dimlem13  41664  dibord  41747  dochvalr  41945  hdmapevec  42423  lcmineqlem10  42619  lcmineqlem12  42621  ismrcd1  43243  ismrc  43246  incssnn0  43256  mzpclall  43272  rmydioph  43555  rmxdioph  43557  expdiophlem2  43563  expdioph  43564  aomclem6  43600  kelac1  43604  gicabl  43640  arearect  43756  areaquad  43757  unielid  43760  oege2  43848  oacl2g  43871  ofoaf  43896  clcnvlem  44163  cnvtrcl0  44166  fvilbd  44229  relexp0a  44256  corcltrcl  44279  clsk1indlem2  44582  ntrclskb  44609  wnefimgd  44701  mnuprdlem4  44815  nzss  44857  lhe4.4ex1a  44869  dvsconst  44870  dvsid  44871  dvsef  44872  binomcxplemnn0  44889  onfrALTlem3  45084  onfrALTlem3VD  45426  unisn0  45598  founiiun0  45732  evthiccabs  46036  climconstmpt  46196  cncfshift  46412  addccncf2  46414  cncfcompt  46421  ioccncflimc  46423  icocncflimc  46427  cncfiooicclem1  46431  cncfiooicc  46432  cncfiooiccre  46433  cxpcncf2  46437  add1cncf  46439  add2cncf  46440  sub1cncfd  46441  sub2cncfd  46442  dvcosre  46450  dvmptfprod  46483  ibliooicc  46509  itgsincmulx  46512  itgsubsticclem  46513  itgiccshift  46518  itgperiod  46519  itgsbtaddcnst  46520  dirkeritg  46640  dirkercncflem2  46642  dirkercncflem4  46644  fourierdlem16  46661  fourierdlem18  46663  fourierdlem21  46666  fourierdlem22  46667  fourierdlem23  46668  fourierdlem32  46677  fourierdlem33  46678  fourierdlem39  46684  fourierdlem40  46685  fourierdlem57  46701  fourierdlem58  46702  fourierdlem59  46703  fourierdlem62  46706  fourierdlem68  46712  fourierdlem72  46716  fourierdlem73  46717  fourierdlem74  46718  fourierdlem75  46719  fourierdlem76  46720  fourierdlem78  46722  fourierdlem83  46727  fourierdlem84  46728  fourierdlem85  46729  fourierdlem88  46732  fourierdlem93  46737  fourierdlem94  46738  fourierdlem95  46739  fourierdlem97  46741  fourierdlem101  46745  fourierdlem103  46747  fourierdlem104  46748  fourierdlem111  46755  fourierdlem112  46756  sqwvfoura  46766  sqwvfourb  46767  fouriersw  46769  fouriercn  46770  etransclem18  46790  etransclem22  46794  etransclem34  46806  etransclem46  46818  etransclem47  46819  sge0fsum  46925  meaiininclem  47024  hoidmvlelem2  47134  hspdifhsp  47154  hspmbllem2  47165  hspmbl  47167  iinhoiicclem  47211  pimgtmnf2  47252  smflimsuplem1  47358  smflimsuplem6  47363  cjnpoly  47447  srhmsubcALTV  48911  imaidfu2lem  49694  imaidfu  49695  imaidfu2  49696  setc1onsubc  50187