Theorem sseqtri 2649

Description: Substitution of equality into a subclass relationship.

Hypotheses

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

Assertion

Ref	Expression
sseqtri	|- A C_ C

Proof of Theorem sseqtri

Step	Hyp	Ref	Expression
1		sseqtr.1	. 2 |- A C_ B
2		sseqtr.2	. . 3 |- B = C
3	2	sseq2i 2642	. 2 |- (A C_ B <-> A C_ C)
4	1, 3	mpbi 206	1 |- A C_ C

Syntax hints:   = wceq 1298   C_ wss 2593

This theorem is referenced by:  sseqtr4i 2650  eqimssi 2668  abssi 2682  ssun2 2768  snsspr2 3137  opabssOLD 3398  difex2 3802  unixpss 4094  0ima 4284  oelim2 5270  ecopoprdm 5368  sbthlem7 5516  abfii3 5653  abfii4 5654  rankuni 5809  rankc2 5817  rankxpu 5822  rankxplim 5823  cf0 6058  unirnioo 7571  unbenlem 8773  cncnplem1 9051  nmcn3 9680  abscncfALT 9683  choc1 10924  shlej1i 10981  chub2i 11026  span0 11098  spanuni 11100  sshhococi 11102  chsup0 11104  spansnpji 11134  mayetes3i 11310  nmcopexlem4 11591  nmcfnexlem4 11620  pjimai 11748  pj3i 11781  shatomistici 11933  hatomistici 11934  atcvat4i 11969  divalglem2 13698  divalglem5 13700  nocvxminlem 14028  nocvxmin 14029  axfelem0 14030  axfelem1 14031  dmhmph 14886  dtopcl 14948  ranleqt 15021  reldded 15088  relrded 15089  reldcat 15109  relrcat 15110  hscptsscld 15434  ist1-2 15542  filnet 15645  heiborlem6 15960  heiborlem11 15965  heiborlem12 15966  heiborlem14 15968  heiborlem16 15970  pcocn 16076  pcohtpylem3 16082  isdivrng2 16111

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-10 1308  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-an 242  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-in 2603  df-ss 2605

Copyright terms: Public domain