Theorem ssid 3262

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

Syntax hints:   ∈ wcel 2205   ⊆ wss 3214

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-in 3220  df-ss 3227

This theorem is referenced by:  ssidd  3263  eqimssi  3298  eqimss2i  3299  inv1  3549  difid  3581  undifabs  3590  pwidg  3691  elssuni  3947  unimax  3953  intmin  3974  rintm  4089  iunpw  4606  sucprcreg  4676  tfisi  4714  peano5  4725  xpss1  4865  xpss2  4866  residm  5075  resdm  5082  resmpt3  5092  ssrnres  5210  cocnvss  5293  dffn3  5524  fimacnv  5811  foima2  5930  fdmrn  6007  tfrlem1  6552  rdgss  6627  fpmg  6921  findcard2d  7161  findcard2sd  7162  f1finf1o  7230  fidcenumlemr  7238  casef  7392  nnnninf  7430  1idprl  7921  1idpru  7922  ltexprlemm  7931  suplocexprlemmu  8049  elq  9975  expcl  10946  serclim0  12019  fsum2d  12150  fsumabs  12180  fsumiun  12192  fprod2d  12338  reef11  12414  ghmghmrn  14020  subrgid  14473  znf1o  14929  topopn  15003  fiinbas  15044  topbas  15062  topcld  15104  ntrtop  15123  opnneissb  15150  opnssneib  15151  opnneiid  15159  idcn  15207  cnconst2  15228  lmres  15243  retopbas  15518  cnopncntop  15539  cnopn  15540  abscncf  15580  recncf  15581  imcncf  15582  cjcncf  15583  mulc1cncf  15584  cncfcn1cntop  15589  cncfmpt2fcntop  15594  addccncf  15595  idcncf  15596  sub1cncf  15597  sub2cncf  15598  cdivcncfap  15599  negfcncf  15601  expcncf  15604  cnrehmeocntop  15605  maxcncf  15610  mincncf  15611  ivthreinc  15640  hovercncf  15641  cnlimcim  15666  cnlimc  15667  cnlimci  15668  dvcnp2cntop  15694  dvcn  15695  dvmptfsum  15720  dvef  15722  plyssc  15734  efcn  15763  uhgrsubgrself  16391  uhgrspansubgr  16402  domomsubct  16915