Theorem ssid 3268

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

This proof depends on syntax axioms:   ∈ wcel 2209   ⊆ wss 3220

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-in 3226  df-ss 3233

This theorem is used by:  ssidd  3269  eqimssi  3304  eqimss2i  3305  inv1  3559  difid  3594  disjdif  3599  undifabs  3604  pwidg  3706  elssuni  3963  unimax  3969  intmin  3990  rintm  4105  iunpw  4626  sucprcreg  4696  tfisi  4734  peano5  4745  xpss1  4885  xpss2  4886  residm  5095  resdm  5102  resmpt3  5112  ssrnres  5230  cocnvss  5313  dffn3  5544  fimacnv  5837  foima2  5957  fdmrn  6034  tfrlem1  6579  rdgss  6654  fpmg  6955  findcard2d  7195  findcard2sd  7196  f1finf1o  7264  fidcenumlemr  7272  casef  7429  nnnninf  7467  1idprl  7958  1idpru  7959  ltexprlemm  7968  suplocexprlemmu  8086  indconst1  9306  elq  10032  expcl  11008  serclim0  12089  fsum2d  12220  fsumabs  12250  fsumiun  12262  fprod2d  12408  reef11  12484  ghmghmrn  14117  subrgid  14582  znf1o  15037  topopn  15161  fiinbas  15202  topbas  15220  topcld  15262  ntrtop  15281  opnneissb  15308  opnssneib  15309  opnneiid  15317  idcn  15365  cnconst2  15386  lmres  15401  retopbas  15676  cnopncntop  15697  cnopn  15698  abscncf  15738  recncf  15739  imcncf  15740  cjcncf  15741  mulc1cncf  15742  cncfcn1cntop  15747  cncfmpt2fcntop  15752  addccncf  15753  idcncf  15754  sub1cncf  15755  sub2cncf  15756  cdivcncfap  15757  negfcncf  15759  expcncf  15762  cnrehmeocntop  15763  maxcncf  15768  mincncf  15769  ivthreinc  15798  hovercncf  15799  cnlimcim  15824  cnlimc  15825  cnlimci  15826  dvcnp2cntop  15852  dvcn  15853  dvmptfsum  15878  dvef  15880  plyssc  15892  efcn  15921  uhgrsubgrself  16629  uhgrspansubgr  16640  domomsubct  17153