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  7428  nnnninf  7466  1idprl  7957  1idpru  7958  ltexprlemm  7967  suplocexprlemmu  8085  indconst1  9304  elq  10024  expcl  10996  serclim0  12073  fsum2d  12204  fsumabs  12234  fsumiun  12246  fprod2d  12392  reef11  12468  ghmghmrn  14068  subrgid  14533  znf1o  14988  topopn  15111  fiinbas  15152  topbas  15170  topcld  15212  ntrtop  15231  opnneissb  15258  opnssneib  15259  opnneiid  15267  idcn  15315  cnconst2  15336  lmres  15351  retopbas  15626  cnopncntop  15647  cnopn  15648  abscncf  15688  recncf  15689  imcncf  15690  cjcncf  15691  mulc1cncf  15692  cncfcn1cntop  15697  cncfmpt2fcntop  15702  addccncf  15703  idcncf  15704  sub1cncf  15705  sub2cncf  15706  cdivcncfap  15707  negfcncf  15709  expcncf  15712  cnrehmeocntop  15713  maxcncf  15718  mincncf  15719  ivthreinc  15748  hovercncf  15749  cnlimcim  15774  cnlimc  15775  cnlimci  15776  dvcnp2cntop  15802  dvcn  15803  dvmptfsum  15828  dvef  15830  plyssc  15842  efcn  15871  uhgrsubgrself  16519  uhgrspansubgr  16530  domomsubct  17043