Theorem ssid 3910

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 3892	1 ⊢ 𝐴 ⊆ 𝐴

Syntax hints:   ∈ wcel 2112   ⊆ wss 3854

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-ext 2730

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1542  df-ex 1783  df-sb 2071  df-clab 2737  df-cleq 2751  df-clel 2831  df-v 3409  df-in 3861  df-ss 3871

This theorem is referenced by:  ssidd  3911  eqimssi  3946  eqimss2i  3947  nsspssun  4158  difid  4263  inv1  4284  disjpss  4350  pwidg  4509  elssuni  4823  unimax  4829  intmin  4851  rintn0  4989  sseliALT  5172  inxpssres  5534  xpss1  5536  xpss2  5537  residm  5849  resdm  5861  resmpt3  5871  cnvrescnv  6017  ordunidif  6210  funresfunco  6369  dffn3  6503  fdmrn  6516  fvreseq1  6793  fimacnv  6823  iunpw  7485  onsucuni  7535  tfisi  7565  fparlem3  7807  fparlem4  7808  funsssuppss  7857  tfrlem1  8015  tz7.48-2  8081  oaordi  8175  omwordi  8200  omass  8209  nnaordi  8247  nnmwordi  8264  fpmg  8443  boxcutc  8516  domss2  8690  0fin  8760  en1eqsn  8762  findcard2d  8778  fimax2g  8782  domunfican  8809  pwfi  8837  fipreima  8848  fimin2g  8979  wofib  9027  wemapso  9033  noinfep  9141  cantnfval2  9150  tcidm  9206  tc0  9207  r1rankidb  9251  r1pw  9292  rankr1id  9309  scott0  9333  xpomen  9460  infpwfien  9507  alephsmo  9547  dfac12lem3  9590  cflem  9691  cflecard  9698  cfslb  9711  fin4en1  9754  fin23lem13  9777  fin23lem36  9793  isf32lem1  9798  fin67  9840  dcomex  9892  zorn2lem4  9944  alephexp2  10026  fpwwe2lem12  10087  canthnumlem  10093  wuncidm  10191  eltsk2g  10196  axgroth6  10273  axgroth3  10276  xrsup  13270  expcl  13482  hashcard  13751  hashf1lem2  13851  xptrrel  14372  cotrtrclfv  14404  rtrclreclem2  14451  lo1eq  14958  rlimeq  14959  serclim0  14967  isercolllem2  15055  isercoll  15057  fsum2d  15159  fsumabs  15189  fsumrlim  15199  fsumo1  15200  fsumiun  15209  fprod2d  15368  risefaccl  15402  fallfaccl  15403  eflt  15503  rpnnen2lem3  15602  rpnnen2lem5  15604  rpnnen2lem12  15611  rexpen  15614  ressid  16602  ressinbas  16603  oduclatb  17805  ipopos  17821  fpwipodrs  17825  ghmghmrn  18429  cntrnsg  18524  0symgefmndeq  18574  sylow3lem5  18808  lsmss1  18843  lsmss2  18845  cntrcmnd  19015  cntrabl  19016  gsumzres  19082  gsumzcl2  19083  gsumzf1o  19085  gsumadd  19096  gsumzmhm  19110  gsumzoppg  19117  dprdf1  19208  ablfac1eulem  19247  subrgid  19590  lbsextlem1  19983  rlmval2  20019  znf1o  20304  zntoslem  20309  css0  20439  uvcresum  20543  frlmlbs  20547  psrass1lemOLD  20687  psrass1lem  20690  mdetrsca2  21289  mdetrlin2  21292  mdetunilem5  21301  mdetunilem9  21305  smadiadetglem1  21356  smadiadetglem2  21357  pmatcollpw3  21469  topopn  21591  fiinbas  21637  topbas  21657  topcld  21720  ntrtop  21755  opnneissb  21799  opnssneib  21800  opnneiid  21811  maxlp  21832  isperf2  21837  restperf  21869  idcn  21942  cnconst2  21968  lmres  21985  fiuncmp  22089  1stcelcls  22146  ssref  22197  refref  22198  kgencn2  22242  ptpjpre1  22256  ptbasfi  22266  xkopt  22340  elqtop2  22386  ptcmpfi  22498  fbssfi  22522  opnfbas  22527  filtop  22540  isfil2  22541  isfild  22543  fsubbas  22552  ssfg  22557  filssufilg  22596  ufileu  22604  imaelfm  22636  rnelfm  22638  fmfnfmlem4  22642  neiflim  22659  fclscf  22710  flimfnfcls  22713  tsmsfbas  22813  xpsxmet  23067  xpsdsval  23068  xpsmet  23069  tmsxms  23173  tmsms  23174  imasf1oxms  23176  imasf1oms  23177  prdsxms  23217  prdsms  23218  tmsxpsval  23225  retopbas  23447  cnngp  23466  cnopn  23473  cnperf  23506  retopconn  23515  fsumcn  23556  abscncf  23587  recncf  23588  imcncf  23589  cjcncf  23590  mulc1cncf  23591  cncfcn1  23597  cncfmpt2f  23601  cncfmpt2ss  23602  addccncf  23603  idcncf  23604  sub1cncf  23605  sub2cncf  23606  cdivcncf  23607  negcncf  23608  negfcncf  23609  abscncfALT  23610  cnmpopc  23614  xrhmeo  23632  oprpiece1res1  23637  oprpiece1res2  23638  cnrehmeo  23639  iscau3  23963  caubl  23993  caublcls  23994  evthicc2  24145  ovolre  24210  volsuplem  24240  uniiccdif  24263  uniioovol  24264  uniiccvol  24265  uniioombllem3  24270  uniioombllem4  24271  uniioombllem5  24272  dyadmbllem  24284  volivth  24292  itgfsum  24511  iblabslem  24512  iblabs  24513  bddmulibl  24523  cnlimc  24572  cnlimci  24573  dvcnp2  24604  dvcn  24605  cpnord  24619  cpnres  24621  dvmptntr  24655  dvmptfsum  24659  rolle  24674  dvlipcn  24678  c1liplem1  24680  dvivth  24694  dvfsumabs  24707  ftc1a  24721  ftc1cn  24727  plyssc  24881  plyeq0  24892  0dgr  24926  coemulc  24936  coe0  24937  coesub  24938  coe1termlem  24939  dgrmulc  24952  dgrsub  24953  dvnply2  24967  plycpn  24969  plyremlem  24984  fta1lem  24987  vieta1lem2  24991  aalioulem3  25014  taylthlem1  25052  taylthlem2  25053  ulmcn  25078  psercn  25105  abelth  25120  efcn  25122  efcvx  25128  dvrelog  25312  logcn  25322  dvloglem  25323  dvlog  25326  dvlog2  25328  efopnlem2  25332  logccv  25338  cxpcn  25418  cxpcn3  25421  resqrtcn  25422  sqrtcn  25423  loglesqrt  25431  atancn  25606  jensen  25658  ftalem3  25744  dchrfi  25923  dchrisumlema  26156  pntlem3  26277  uhgrsubgrself  27154  uhgrspansubgr  27165  umgr2adedgwlk  27815  umgr2adedgwlkon  27816  umgr2adedgspth  27818  upgr1wlkdlem2  28015  sspid  28592  ssps  28597  helch  29110  hhssnv  29131  hhsssh  29136  shintcl  29197  chintcl  29199  shlesb1i  29253  omlsi  29271  chlejb1i  29343  chm0i  29357  chabs1  29383  chabs2  29384  spanun  29412  cmidi  29477  pjidmcoi  30044  csmdsymi  30201  sumdmdlem2  30286  dmdbr5ati  30289  mdcompli  30296  dmdcompli  30297  disjdifprg  30421  fcoinver  30453  f1rnen  30471  xppreima  30491  padct  30563  xrinfm  30586  clatp0cl  30765  clatp1cl  30766  xrsp0  30801  xrsp1  30802  cntrcrng  30833  gsumle  30861  cycpmconjslem1  30932  cycpmconjslem2  30933  gsumvsca1  30990  gsumvsca2  30991  qusxpid  31065  ellspds  31070  rspidlid  31076  reff  31295  locfinreflem  31296  esumsnf  31536  esumcvg  31558  sigagenid  31623  iblidicc  32076  cxpcncf1  32079  fdvposlt  32083  fdvneggt  32084  fdvposle  32085  fdvnegge  32086  logdivsqrle  32134  bnj1253  32502  cvmlift2lem6  32771  satfun  32874  mrsubrn  32976  elmrsubrn  32983  elmsubrn  32991  msubrn  32992  onelssex  33164  trpredtr  33301  madebday  33622  imagesset  33789  ivthALT  34058  fness  34072  fneref  34073  refssfne  34081  fnemeet1  34089  fnejoin2  34092  filnetlem2  34102  filnetlem4  34104  ontgval  34154  knoppcnlem10  34216  knoppcnlem11  34217  bj-rabtr  34638  bj-rabtrAUTO  34640  bj-disj2r  34730  bj-restsnid  34767  bj-resta  34776  bj-imdirco  34870  elxp8  35053  finorwe  35064  mblfinlem3  35361  mblfinlem4  35362  ismblfin  35363  ovoliunnfl  35364  voliunnfl  35366  volsupnfl  35367  mbfposadd  35369  ftc1cnnclem  35393  ftc1cnnc  35394  ftc1anc  35403  ftc2nc  35404  areacirclem2  35411  areacirclem4  35413  areacirc  35415  caures  35463  constcncf  35465  brssrid  36167  brcnvssrid  36172  refrelid  36186  n0eldmqs  36308  atpsubN  37314  pol1N  37471  dia2dimlem13  38637  dibord  38720  dochvalr  38918  hdmapevec  39396  lcmineqlem10  39590  lcmineqlem12  39592  ismrcd1  39997  ismrc  40000  incssnn0  40010  mzpclall  40026  rmydioph  40313  rmxdioph  40315  expdiophlem2  40321  expdioph  40322  aomclem6  40361  kelac1  40365  gicabl  40401  arearect  40523  areaquad  40524  clcnvlem  40681  cnvtrcl0  40684  fvilbd  40748  relexp0a  40775  corcltrcl  40798  clsk1indlem2  41103  ntrclskb  41130  wnefimgd  41223  mnuprdlem4  41341  nzss  41379  lhe4.4ex1a  41391  dvsconst  41392  dvsid  41393  dvsef  41394  binomcxplemnn0  41411  onfrALTlem3  41608  onfrALTlem3VD  41951  unisn0  42046  founiiun0  42172  evthiccabs  42484  climconstmpt  42651  cncfshift  42867  addccncf2  42869  cncfcompt  42876  ioccncflimc  42878  icocncflimc  42882  cncfiooicclem1  42886  cncfiooicc  42887  cncfiooiccre  42888  cxpcncf2  42892  add1cncf  42894  add2cncf  42895  sub1cncfd  42896  sub2cncfd  42897  dvcosre  42905  dvmptfprod  42938  ibliooicc  42964  itgsincmulx  42967  itgsubsticclem  42968  itgiccshift  42973  itgperiod  42974  itgsbtaddcnst  42975  dirkeritg  43095  dirkercncflem2  43097  dirkercncflem4  43099  fourierdlem16  43116  fourierdlem18  43118  fourierdlem21  43121  fourierdlem22  43122  fourierdlem23  43123  fourierdlem32  43132  fourierdlem33  43133  fourierdlem39  43139  fourierdlem40  43140  fourierdlem57  43156  fourierdlem58  43157  fourierdlem59  43158  fourierdlem62  43161  fourierdlem68  43167  fourierdlem72  43171  fourierdlem73  43172  fourierdlem74  43173  fourierdlem75  43174  fourierdlem76  43175  fourierdlem78  43177  fourierdlem83  43182  fourierdlem84  43183  fourierdlem85  43184  fourierdlem88  43187  fourierdlem93  43192  fourierdlem94  43193  fourierdlem95  43194  fourierdlem97  43196  fourierdlem101  43200  fourierdlem103  43202  fourierdlem104  43203  fourierdlem111  43210  fourierdlem112  43211  fourierdlem113  43212  sqwvfoura  43221  sqwvfourb  43222  fouriersw  43224  fouriercn  43225  etransclem18  43245  etransclem22  43249  etransclem34  43261  etransclem46  43273  etransclem47  43274  sge0fsum  43377  meaiininclem  43476  hoidmvlelem2  43586  hspdifhsp  43606  hspmbllem2  43617  hspmbl  43619  iinhoiicclem  43663  pimgtmnf2  43700  smflimsuplem1  43802  smflimsuplem6  43807  srhmsubc  45052  srhmsubcALTV  45070