Theorem eqimss 2112

Description: Equality implies the subclass relation.

Assertion

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

Proof of Theorem eqimss

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

Syntax hints:   -> wi 3   = wceq 958   (_ wss 2050

This theorem is referenced by:  eqimss2 2113  sspss 2148  uneqin 2259  pwpw0 2473  sssn 2477  eqsn 2478  sspr 2479  snsspw 2483  pwsnALT 2505  elpwuni 2767  pwssun 2833  ordsseleq 2982  ordsson 2997  trsucss 3062  suceloni 3068  suc11 3099  dmxpss 3479  rnxpss 3480  xp11 3482  fnresdm 3602  ffdm 3645  fconst 3664  fof 3678  f1o2 3699  f1o3 3700  f1ofv 3883  tfrlem11 3927  oewordi 4224  oewordri 4225  r1ord3 4667  rankxplim3 4724  carddom 4846  cflim 4921  cfsuc 4927  istps2 7608  chsupsn 9307  chlejb1 9394  atsseq 10269  sfvlim 10576  trnij 10608

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475  df-in 2054  df-ss 2056

Copyright terms: Public domain