Theorem ssid 2076

Description: Any class is a subclass of itself. Exercise 10 of [TakeutiZaring] p. 18.

Assertion

Ref	Expression
ssid	|- A (_ A

Proof of Theorem ssid

Step	Hyp	Ref	Expression
1		eqid 1473	. . 3 |- A = A
2		eqss 2073	. . 3 |- (A = A <-> (A (_ A /\ A (_ A))
3	1, 2	mpbi 189	. 2 |- (A (_ A /\ A (_ A)
4	3	pm3.26i 320	1 |- A (_ A

Syntax hints:   /\ wa 223   = wceq 954   (_ wss 2043

This theorem is referenced by:  eqimss 2105  eqimssi 2107  eqimss2i 2108  nssinpss 2236  nsspssun 2237  inv1 2295  disjpss 2315  difid 2330  pwid 2404  elssuni 2521  unimax 2527  intmin 2548  iunpw 2909  ordunidif 3000  onsucuni 3080  ssres2 3378  residm 3382  resdm 3385  ssrnres 3473  fnfrn 3625  fssxp 3628  funssxp 3629  fimacnv 3801  tfrlem1 3902  tz7.48-2 3948  abianfp 3953  oaordi 4170  omwordi 4192  omass 4201  xpdom3 4431  sucprcreg 4580  noinfep 4620  scott0 4697  htalem 4707  zorn2lem4 4771  cflem 4885  cflecard 4892  axresscn 5248  expclt 6521  clmi1 7032  clm4at 7036  clmi2at 7037  climconst 7039  climunii 7043  climshft 7049  climres 7050  climuz0 7053  climmullem8 7071  serzf0 7113  ser1f0 7114  isumclim4t 7144  negfcncf 7212  abscncflem 7217  cjcncf 7221  mulc1cncf 7222  isupivth 7233  dsupivthlem 7234  efcn 7371  reeff1olem1 7372  reeff1olem1OLD 7374  xpnnen 7449  alephexp2 7536  topopn 7552  topbast 7577  subbas 7594  retopbas 7605  topcld 7625  clstop 7650  ntrtop 7651  opnneissb 7678  opnssneib 7679  opnneiid 7687  islp2 7697  ssblex 7808  opnm 7812  blssopn 7819  blnei 7831  cncfmet1 7858  lmbrf 7882  iscauf 7891  iscau4 7892  iscau5 7893  lmsslem 7903  caussi 7905  lmclimnn 7915  opr1scn 7930  grpidinv2 8010  grpinv 8019  abscncfALT 8291  sspid 8331  ssps 8336  pilem1 8609  efghgrpilem 8653  efifolem1 8656  axgroth3 8718  grothinf 8720  h2hcau 8788  h2hlm 8789  helch 9055  hhssnv 9073  hhsssh 9078  occlt 9121  omls 9184  shintclt 9232  chintclt 9234  shlesb1 9297  chm1 9317  chlejb1 9337  chm0 9351  chabs1t 9377  chabs2t 9378  spanunt 9406  cmid 9493  pjidmco 10043  hst0t 10098  csmdsym 10198  sumdmdlem2 10282  dmdbr5at 10284  mdcompl 10290  dmdcompl 10291  fgsb 10480  efilcp 10481  fgsb2 10485  efilcp2 10486  0alg 10569

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-in 2047  df-ss 2049

Copyright terms: Public domain