ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ssid GIF version

Theorem ssid 3117
Description: Any class is a subclass of itself. Exercise 10 of [TakeutiZaring] p. 18. (Contributed by NM, 5-Aug-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 19 . 2 (𝑥𝐴𝑥𝐴)
21ssriv 3101 1 𝐴𝐴
Colors of variables: wff set class
Syntax hints:  wcel 1480  wss 3071
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-11 1484  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121
This theorem depends on definitions:  df-bi 116  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-in 3077  df-ss 3084
This theorem is referenced by:  ssidd  3118  eqimssi  3153  eqimss2i  3154  inv1  3399  difid  3431  undifabs  3439  pwidg  3524  elssuni  3764  unimax  3770  intmin  3791  rintm  3905  iunpw  4401  sucprcreg  4464  tfisi  4501  peano5  4512  xpss1  4649  xpss2  4650  residm  4851  resdm  4858  resmpt3  4868  ssrnres  4981  cocnvss  5064  dffn3  5283  fimacnv  5549  foima2  5653  tfrlem1  6205  rdgss  6280  fpmg  6568  findcard2d  6785  findcard2sd  6786  f1finf1o  6835  fidcenumlemr  6843  casef  6973  nnnninf  7023  1idprl  7405  1idpru  7406  ltexprlemm  7415  suplocexprlemmu  7533  elq  9421  expcl  10318  serclim0  11081  fsum2d  11211  fsumabs  11241  fsumiun  11253  reef11  11413  ressid  12030  topopn  12185  fiinbas  12226  topbas  12246  topcld  12288  ntrtop  12307  opnneissb  12334  opnssneib  12335  opnneiid  12343  idcn  12391  cnconst2  12412  lmres  12427  retopbas  12702  cnopncntop  12716  abscncf  12751  recncf  12752  imcncf  12753  cjcncf  12754  mulc1cncf  12755  cncfcn1cntop  12760  cncfmpt2fcntop  12764  addccncf  12765  cdivcncfap  12766  negfcncf  12768  expcncf  12771  cnrehmeocntop  12772  cnlimcim  12819  cnlimc  12820  cnlimci  12821  dvcnp2cntop  12842  dvcn  12843  dvef  12866  efcn  12867
  Copyright terms: Public domain W3C validator