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  4572  sucprcreg  4642  tfisi  4680  peano5  4691  xpss1  4831  xpss2  4832  residm  5040  resdm  5047  resmpt3  5057  ssrnres  5174  cocnvss  5257  dffn3  5487  fimacnv  5769  foima2  5884  tfrlem1  6465  rdgss  6540  fpmg  6834  findcard2d  7066  findcard2sd  7067  f1finf1o  7130  fidcenumlemr  7138  casef  7271  nnnninf  7309  1idprl  7793  1idpru  7794  ltexprlemm  7803  suplocexprlemmu  7921  elq  9834  expcl  10796  serclim0  11837  fsum2d  11967  fsumabs  11997  fsumiun  12009  fprod2d  12155  reef11  12231  ghmghmrn  13821  subrgid  14208  znf1o  14636  topopn  14703  fiinbas  14744  topbas  14762  topcld  14804  ntrtop  14823  opnneissb  14850  opnssneib  14851  opnneiid  14859  idcn  14907  cnconst2  14928  lmres  14943  retopbas  15218  cnopncntop  15239  cnopn  15240  abscncf  15280  recncf  15281  imcncf  15282  cjcncf  15283  mulc1cncf  15284  cncfcn1cntop  15289  cncfmpt2fcntop  15294  addccncf  15295  idcncf  15296  sub1cncf  15297  sub2cncf  15298  cdivcncfap  15299  negfcncf  15301  expcncf  15304  cnrehmeocntop  15305  maxcncf  15310  mincncf  15311  ivthreinc  15340  hovercncf  15341  cnlimcim  15366  cnlimc  15367  cnlimci  15368  dvcnp2cntop  15394  dvcn  15395  dvmptfsum  15420  dvef  15422  plyssc  15434  efcn  15463  domomsubct  16480