Theorem ssid 3247

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

Syntax hints:   ∈ wcel 2202   ⊆ wss 3200

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 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3206  df-ss 3213

This theorem is referenced by:  ssidd  3248  eqimssi  3283  eqimss2i  3284  inv1  3531  difid  3563  undifabs  3571  pwidg  3666  elssuni  3921  unimax  3927  intmin  3948  rintm  4063  iunpw  4577  sucprcreg  4647  tfisi  4685  peano5  4696  xpss1  4836  xpss2  4837  residm  5045  resdm  5052  resmpt3  5062  ssrnres  5179  cocnvss  5262  dffn3  5493  fimacnv  5776  foima2  5892  tfrlem1  6474  rdgss  6549  fpmg  6843  findcard2d  7080  findcard2sd  7081  f1finf1o  7146  fidcenumlemr  7154  casef  7287  nnnninf  7325  1idprl  7810  1idpru  7811  ltexprlemm  7820  suplocexprlemmu  7938  elq  9856  expcl  10820  serclim0  11870  fsum2d  12001  fsumabs  12031  fsumiun  12043  fprod2d  12189  reef11  12265  ghmghmrn  13855  subrgid  14243  znf1o  14671  topopn  14738  fiinbas  14779  topbas  14797  topcld  14839  ntrtop  14858  opnneissb  14885  opnssneib  14886  opnneiid  14894  idcn  14942  cnconst2  14963  lmres  14978  retopbas  15253  cnopncntop  15274  cnopn  15275  abscncf  15315  recncf  15316  imcncf  15317  cjcncf  15318  mulc1cncf  15319  cncfcn1cntop  15324  cncfmpt2fcntop  15329  addccncf  15330  idcncf  15331  sub1cncf  15332  sub2cncf  15333  cdivcncfap  15334  negfcncf  15336  expcncf  15339  cnrehmeocntop  15340  maxcncf  15345  mincncf  15346  ivthreinc  15375  hovercncf  15376  cnlimcim  15401  cnlimc  15402  cnlimci  15403  dvcnp2cntop  15429  dvcn  15430  dvmptfsum  15455  dvef  15457  plyssc  15469  efcn  15498  uhgrsubgrself  16123  uhgrspansubgr  16134  domomsubct  16628