Theorem eqsstr3i 3449

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 2480	. 2 |- A = B
3		eqsstr3.2	. 2 |- B C_ C
4	2, 3	eqsstri 3448	1 |- A C_ C

Syntax hints:   = wceq 1452   C_ wss 3390

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451

This theorem depends on definitions:  df-bi 190  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-in 3397  df-ss 3404

This theorem is referenced by:  inss2  3644  dmv  5056  ofrfval  6558  ofval  6559  ofrval  6560  off  6565  ofres  6566  ofco  6570  dftpos4  7010  smores2  7091  onwf  8319  r0weon  8461  cda1dif  8624  unctb  8653  infmap2  8666  itunitc  8869  axcclem  8905  dfnn3  10645  bcm1k  12538  bcpasc  12544  cotr2  13116  ressbasss  15259  strlemor1  15295  prdsle  15438  prdsless  15439  dprd2da  17753  opsrle  18776  indiscld  20184  leordtval2  20305  fiuncmp  20496  prdstopn  20720  ustneism  21316  itg1addlem4  22736  itg1addlem5  22737  tdeglem4  23088  aannenlem3  23365  efifo  23575  advlogexp  23679  pjoml4i  27321  5oai  27395  3oai  27402  bdopssadj  27815  suppss2fOLD  28313  xrge00  28523  xrge0mulc1cn  28821  esumdivc  28978  ballotlemodife  29403  subfacp1lem5  29979  filnetlem3  31107  filnetlem4  31108  mblfinlem4  32044  itg2gt0cn  32061  psubspset  33380  psubclsetN  33572  relexpaddss  36381  corcltrcl  36402  relopabVD  37361  cncfiooicc  37869  stoweidlem34  38007  konigsbergssiedgw  40163