Theorem ssid 2634

Description: Any class is a subclass of itself. Exercise 10 of [TakeutiZaring] p. 18. (The proof was shortened by Andrew Salmon, 14-Jun-2011.)

Assertion

Ref	Expression
ssid	|- A C_ A

Proof of Theorem ssid

Step	Hyp	Ref	Expression
1		id 73	. 2 |- (x e. A -> x e. A)
2	1	ssriv 2621	1 |- A C_ A

Syntax hints:   e. wcel 1300   C_ wss 2593

This theorem is referenced by:  eqimssOLD 2666  eqimssi 2668  eqimss2i 2669  nssinpssOLD 2825  nsspssun 2826  inv1 2898  disjpss 2924  difid 2942  pwid 3042  elssuni 3206  unimax 3212  intmin 3237  intminOLD 3238  ssbri 3379  axpweq 3480  ordunidif 3712  iunpw 3858  onsucuni 3907  xpss1 4091  xpss2 4092  ssres2OLD 4241  residm 4246  resdm 4249  ssrnres 4354  dffn3 4570  fssxpOLD 4576  funssxp 4577  fimacnv 4783  tfrlem1 5119  tz7.48-2 5166  abianfp 5171  oaordi 5227  omwordi 5250  omass 5259  xpdom3 5504  unifi 5648  pwfi 5661  ordtypelem4 5687  sucprcreg 5703  noinfep 5747  scott0 5847  htalem 5857  zorn2lem4 5953  cflem 6053  cflecard 6060  axresscnOLD 6421  expcl 7824  clmi1i 8346  clm4a 8350  clmi2a 8351  climconsti 8354  climunii 8358  climshfti 8364  climresi 8365  climuz0i 8368  climmullem8 8387  serzf0i 8429  isumclim4 8462  negfcncfi 8531  abscncflem 8536  cjcncf 8540  mulc1cncf 8541  isupivthi 8552  dsupivthlem 8553  efcn 8688  reeff1olem1 8689  xpnnen 8768  alephexp2 8855  topopn 8871  fiinbas 8885  topbas 8897  subbas 8914  retopbas 8925  topcld 8951  clstop 8976  ntrtop 8977  opnneissb 9004  opnssneib 9005  opnneiid 9013  islp2 9023  ssblex 9133  opnm 9137  blssopn 9144  blnei 9156  cncfmet1 9184  lmbrf 9208  iscauf 9217  iscau4 9218  iscau5 9219  iscaunns 9222  lmsslem 9230  caussi 9232  lmclimnn 9242  opr1scn 9258  grprlidrid 9337  grpidinv2 9344  grpinv 9353  abscncfALT 9683  sspid 9723  ssps 9728  pilem1 10020  efghgrpilem 10073  efifolem1 10076  grothpw 10134  grothomex 10136  axgroth6 10137  axgroth3 10138  emfin 10165  setwoe 10170  filfbas 10276  fsubbas 10281  fbssfg 10285  fgfil 10290  extbas2 10292  h2hcau 10481  h2hlm 10482  helch 10749  hhssnv 10767  hhsssh 10772  occl 10815  omlsi 10879  shintcl 10927  chintcl 10929  shlesb1i 10992  chm1i 11012  chlejb1i 11032  chm0i 11046  chabs1 11072  chabs2 11073  spanun 11101  cmidi 11186  pjidmcoi 11749  hst0 11805  csmdsymi 11906  sumdmdlem2 11991  dmdbr5ati 11994  mdcompli 12001  dmdcompli 12002  bnj1253 13470  bnj1283 13476  residcp 14392  set2elt 14408  prl2 14514  inpc 14619  inposet 14620  dominc 14622  rninc 14623  domncnt 14624  ranncnt 14625  dfps2 14634  toplat 14638  osneisi 14875  fgsb 14921  efilcp 14922  fgsb2 14925  efilcp2 14926  limfilnei 14943  clindistop 14962  0alg 15103  catsbc 15197  taralt 15211  inacint 15221  tareltsuc 15275  fictblem 15370  ordtypelem4OLD 15378  cncls 15419  hscptsscld 15434  alexsublem4 15440  retopcon 15452  ivthALT 15454  fness 15491  ssref 15492  fneref 15493  refref 15494  refssfne 15504  comppfsc 15517  neibastop2lem4 15522  neibastop2 15523  neibastop3 15524  fnemeet1 15528  fnemeet2 15529  fnejoin1 15530  opnfbas 15557  supfil 15560  filssufil 15571  ufileu 15573  ufinffr 15578  ufilen 15579  neiplim 15586  cnpfillim 15589  imaelfm 15591  rnelfm 15593  fmfnfmlem4 15597  fcluscf 15612  flimfnfcls 15615  filnetlem1 15640  filnetlem4 15643  filnetlem5 15644  difxp 15690  fimax 15746  welb 15759  frfi 15771  oprpiece1res1 15880  oprpiece1res2 15881  addccncf 15883  sub1cncf 15885  sub2cncf 15886  cnimass 15888  cncfres 15895  heiborlem9 15963  heiborlem13 15967  heiborlem33 15987  heiborlem41 15995  phtpycom 16050  phtpycolem3 16053  phtpycolem4 16054  reparphtlem2 16064  pcocn 16076  pcohtpylem3 16082  pcopt 16084  pcoass 16085  pcorevlem 16086  rngidl 16172  p0le 16845  ple1 16846  grpidinv2NEW 17119  grpinvNEW 17128  atpsub 17233  pol1 17323  1psubcl 17353

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-10 1308  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-an 242  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-in 2603  df-ss 2605

Copyright terms: Public domain