Theorem eqsstr3i 3339

Description: Substitution of equality into a subclass relationship. (Contributed by NM, 19-Oct-1999.)

Hypotheses

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

Assertion

Ref	Expression
eqsstr3i	|- A C_ C

Proof of Theorem eqsstr3i

Step	Hyp	Ref	Expression
1		eqsstr3.1	. . 3 |- B = A
2	1	eqcomi 2408	. 2 |- A = B
3		eqsstr3.2	. 2 |- B C_ C
4	2, 3	eqsstri 3338	1 |- A C_ C

Syntax hints:   = wceq 1649   C_ wss 3280

This theorem is referenced by:  inss2  3522  dmv  5044  ofrfval  6272  ofval  6273  ofrval  6274  off  6279  ofres  6280  ofco  6283  dftpos4  6457  smores2  6575  onwf  7712  r0weon  7850  cda1dif  8012  unctb  8041  infmap2  8054  itunitc  8257  axcclem  8293  dfnn3  9970  bcm1k  11561  bcpasc  11567  ressbasss  13476  strlemor1  13511  prdsle  13639  prdsless  13640  dprd2da  15555  opsrle  16491  indiscld  17110  leordtval2  17230  fiuncmp  17421  prdstopn  17613  ustneism  18206  itg1addlem4  19544  itg1addlem5  19545  tdeglem4  19936  aannenlem3  20200  efifo  20402  advlogexp  20499  pjoml4i  23042  5oai  23116  3oai  23123  bdopssadj  23537  suppss2f  24002  xrge00  24161  xrge0mulc1cn  24280  esumdivc  24426  ballotlemodife  24708  subfacp1lem5  24823  mblfinlem3  26145  itg2gt0cn  26159  filnetlem3  26299  filnetlem4  26300  stoweidlem34  27650  relopabVD  28722  psubspset  30226  psubclsetN  30418

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-in 3287  df-ss 3294