Theorem ssid 3244

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.

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

Syntax hints:   ∈ wcel 2200   ⊆ wss 3197

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3203  df-ss 3210

This theorem is referenced by:  ssidd  3245  eqimssi  3280  eqimss2i  3281  inv1  3528  difid  3560  undifabs  3568  pwidg  3663  elssuni  3916  unimax  3922  intmin  3943  rintm  4058  iunpw  4571  sucprcreg  4641  tfisi  4679  peano5  4690  xpss1  4829  xpss2  4830  residm  5037  resdm  5044  resmpt3  5054  ssrnres  5171  cocnvss  5254  dffn3  5484  fimacnv  5766  foima2  5881  tfrlem1  6460  rdgss  6535  fpmg  6829  findcard2d  7061  findcard2sd  7062  f1finf1o  7122  fidcenumlemr  7130  casef  7263  nnnninf  7301  1idprl  7785  1idpru  7786  ltexprlemm  7795  suplocexprlemmu  7913  elq  9825  expcl  10787  serclim0  11824  fsum2d  11954  fsumabs  11984  fsumiun  11996  fprod2d  12142  reef11  12218  ghmghmrn  13808  subrgid  14195  znf1o  14623  topopn  14690  fiinbas  14731  topbas  14749  topcld  14791  ntrtop  14810  opnneissb  14837  opnssneib  14838  opnneiid  14846  idcn  14894  cnconst2  14915  lmres  14930  retopbas  15205  cnopncntop  15226  cnopn  15227  abscncf  15267  recncf  15268  imcncf  15269  cjcncf  15270  mulc1cncf  15271  cncfcn1cntop  15276  cncfmpt2fcntop  15281  addccncf  15282  idcncf  15283  sub1cncf  15284  sub2cncf  15285  cdivcncfap  15286  negfcncf  15288  expcncf  15291  cnrehmeocntop  15292  maxcncf  15297  mincncf  15298  ivthreinc  15327  hovercncf  15328  cnlimcim  15353  cnlimc  15354  cnlimci  15355  dvcnp2cntop  15381  dvcn  15382  dvmptfsum  15407  dvef  15409  plyssc  15421  efcn  15450  domomsubct  16396