Theorem ssid 2078

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 1475	. . 3 |- A = A
2		eqss 2075	. . 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 955   (_ wss 2045

This theorem is referenced by:  eqimss 2107  eqimssi 2109  eqimss2i 2110  nssinpss 2238  nsspssun 2239  inv1 2297  disjpss 2317  difid 2332  pwid 2406  elssuni 2523  unimax 2529  intmin 2550  iunpw 2911  ordunidif 3002  onsucuni 3082  ssres2 3383  residm 3387  resdm 3390  ssrnres 3478  fnfrn 3631  fssxp 3634  funssxp 3635  fimacnv 3807  tfrlem1 3908  tz7.48-2 3954  abianfp 3959  oaordi 4177  omwordi 4199  omass 4208  xpdom3 4438  sucprcreg 4587  noinfep 4627  scott0 4704  htalem 4714  zorn2lem4 4778  cflem 4892  cflecard 4899  axresscn 5255  expclt 6531  clmi1 7054  clm4at 7058  clmi2at 7059  climconst 7062  climunii 7066  climshft 7072  climres 7073  climuz0 7076  climmullem8 7096  serzf0 7140  ser1f0 7141  isumclim4t 7172  negfcncf 7240  abscncflem 7245  cjcncf 7249  mulc1cncf 7250  isupivth 7261  dsupivthlem 7262  efcn 7399  reeff1olem1 7400  reeff1olem1OLD 7402  xpnnen 7477  alephexp2 7565  topopn 7581  topbast 7606  subbas 7623  retopbas 7634  topcld 7654  clstop 7679  ntrtop 7680  opnneissb 7707  opnssneib 7708  opnneiid 7716  islp2 7726  ssblex 7839  opnm 7843  blssopn 7850  blnei 7862  cncfmet1 7889  lmbrf 7913  iscauf 7922  iscau4 7923  iscau5 7924  iscaunns 7927  lmsslem 7935  caussi 7937  lmclimnn 7947  opr1scn 7963  grpidinv2 8043  grpinv 8052  abscncfALT 8330  sspid 8370  ssps 8375  pilem1 8654  efghgrpilem 8698  efifolem1 8701  axgroth3 8763  grothinf 8765  h2hcau 8833  h2hlm 8834  helch 9104  hhssnv 9122  hhsssh 9127  occlt 9170  omls 9234  shintclt 9282  chintclt 9284  shlesb1 9347  chm1 9367  chlejb1 9387  chm0 9401  chabs1t 9427  chabs2t 9428  spanunt 9456  cmid 9543  pjidmco 10096  hst0t 10151  csmdsym 10252  sumdmdlem2 10337  dmdbr5at 10340  mdcompl 10347  dmdcompl 10348  emfin 10465  fgsb 10538  efilcp 10539  fgsb2 10543  efilcp2 10544  0alg 10640

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-10 965  ax-12 967  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 980  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-in 2049  df-ss 2051

Copyright terms: Public domain