Theorem eqimss 2105

Description: Equality implies the subclass relation.

Assertion

Ref	Expression
eqimss	|- (A = B -> A (_ B)

Proof of Theorem eqimss

Step	Hyp	Ref	Expression
1		ssid 2076	. 2 |- A (_ A
2		sseq2 2079	. 2 |- (A = B -> (A (_ A <-> A (_ B))
3	1, 2	mpbii 193	1 |- (A = B -> A (_ B)

Syntax hints:   -> wi 3   = wceq 954   (_ wss 2043

This theorem is referenced by:  eqimss2 2106  sspss 2141  uneqin 2252  pwpw0 2465  sssn 2469  eqsn 2470  sspr 2471  snsspw 2475  elpwuni 2756  pwssun 2822  ordsseleq 2971  ordsson 2986  trsucss 3051  suceloni 3057  suc11 3088  dmxpss 3465  rnxpss 3466  xp11 3468  fnresdm 3588  ffdm 3630  fconst 3649  fof 3663  f1o2 3684  f1o3 3685  f1ofv 3868  tfrlem11 3912  oewordi 4208  oewordri 4209  r1ord3 4637  rankxplim3 4694  carddom 4816  cflim 4889  cfsuc 4895  istps2 7557  chsupsn 9250  chlejb1 9337  atsseq 10211  trnij 10517

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