Theorem ssid 2070

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 1468	. . 3 |- A = A
2		eqss 2067	. . 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 953   (_ wss 2037

This theorem is referenced by:  eqimss 2099  eqimssi 2101  eqimss2i 2102  nssinpss 2230  nsspssun 2231  inv1 2289  disjpss 2309  difid 2324  pwid 2398  elssuni 2516  unimax 2522  intmin 2543  iunpw 2904  ordunidif 2995  onsucuni 3075  ssres2 3370  residm 3374  resdm 3377  ssrnres 3467  fnfrn 3619  fssxp 3622  funssxp 3623  fimacnv 3795  tfrlem1 3896  tz7.48-2 3942  abianfp 3947  oaordi 4164  omwordi 4186  omass 4195  xpdom3 4425  sucprcreg 4572  noinfep 4612  scott0 4689  htalem 4699  zorn2lem4 4763  cflem 4877  cflecard 4884  axresscn 5240  expclt 6513  clmi1 7024  clm4at 7028  clmi2at 7029  climconst 7031  climunii 7035  climshft 7041  climres 7042  climuz0 7045  climmullem8 7063  serzf0 7105  ser1f0 7106  isumclim4t 7136  negfcncf 7204  abscncflem 7209  cjcncf 7213  mulc1cncf 7214  isupivth 7225  dsupivthlem 7226  efcn 7363  reeff1olem1 7364  reeff1olem1OLD 7366  xpnnen 7441  alephexp2 7528  topopn 7544  topbast 7569  subbas 7586  retopbas 7597  topcld 7617  clstop 7642  ntrtop 7643  opnneissb 7669  opnssneib 7670  opnneiid 7678  islp2 7688  ssblex 7796  opnm 7800  blssopn 7807  blnei 7818  cncfmet1 7845  lmbrf 7868  iscauf 7877  iscau5 7878  lmsslem 7887  caussi 7889  lmclimnn 7899  opr1scn 7914  grpidinv2 7994  grpinv 8003  abscncfALT 8278  sspid 8318  ssps 8323  pilem1 8590  efghgrpilem 8634  efifolem1 8637  axgroth3 8718  grothinf 8720  h2hcau 8788  h2hlm 8789  helch 9037  hhssnv 9054  hhsssh 9059  occlt 9098  omls 9161  shintclt 9209  chintclt 9211  shlesb1 9274  chm1 9294  chlejb1 9314  chm0 9328  chabs1t 9354  chabs2t 9355  spanunt 9383  cmid 9470  pjidmco 10016  hst0t 10070  csmdsym 10169  sumdmdlem2 10253  dmdbr5at 10255  mdcompl 10261  dmdcompl 10262  fgsb 10444  efilcp 10445  fgsb2 10449  efilcp2 10450  0alg 10533

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-12 965  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978  df-sb 1168  df-clab 1457  df-cleq 1462  df-clel 1465  df-in 2041  df-ss 2043

Copyright terms: Public domain