Theorem sseqtr 2091

Description: Substitution of equality into a subclass relationship.

Hypotheses

Ref	Expression
sseqtr.1	|- A (_ B
sseqtr.2	|- B = C

Assertion

Ref	Expression
sseqtr	|- A (_ C

Proof of Theorem sseqtr

Step	Hyp	Ref	Expression
1		sseqtr.1	. 2 |- A (_ B
2		sseqtr.2	. . 3 |- B = C
3	2	sseq2i 2084	. 2 |- (A (_ B <-> A (_ C)
4	1, 3	mpbi 189	1 |- A (_ C

Syntax hints:   = wceq 955   (_ wss 2045

This theorem is referenced by:  sseqtr4 2092  eqimssi 2109  abssi 2120  ssun2 2192  opabss 2665  unixpss 3255  0ima 3418  oelim2 4219  ecopoprdm 4306  sbthlem7 4446  abfii3 4550  abfii4 4551  rankuni 4685  rankc2 4693  rankxpu 4698  rankxplim 4699  cf0 4897  unirnioo 6353  unbenlem 7483  cncnplem1 7753  nmcn3 8327  abscncfALT 8330  choc1 9279  shlej1 9336  chub2 9381  span0 9453  spanun 9455  sshhococ 9457  chsup0 9459  spansnpj 9491  nmcopexlem4 9945  nmcfnexlem4 9974  pjima 10095  pj3 10127  shatomistic 10279  hatomistic 10280  atcvat4 10315  dmhmph 10513  dtopcl 10566  reldded 10625  relrded 10626  reldcat 10646  relrcat 10647

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