Theorem eqsstr3i 3528

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

Syntax hints:   = wceq 1374   C_ wss 3469

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-in 3476  df-ss 3483

This theorem is referenced by:  inss2  3712  dmv  5209  ofrfval  6523  ofval  6524  ofrval  6525  off  6529  ofres  6530  ofco  6535  dftpos4  6964  smores2  7015  onwf  8237  r0weon  8379  cda1dif  8545  unctb  8574  infmap2  8587  itunitc  8790  axcclem  8826  dfnn3  10539  bcm1k  12348  bcpasc  12354  ressbasss  14536  strlemor1  14571  prdsle  14706  prdsless  14707  dprd2da  16874  opsrle  17904  indiscld  19351  leordtval2  19472  fiuncmp  19663  prdstopn  19857  ustneism  20454  itg1addlem4  21834  itg1addlem5  21835  tdeglem4  22186  aannenlem3  22453  efifo  22660  advlogexp  22757  pjoml4i  26167  5oai  26241  3oai  26248  bdopssadj  26662  suppss2f  27136  xrge00  27322  xrge0mulc1cn  27545  esumdivc  27715  ballotlemodife  28062  subfacp1lem5  28254  mblfinlem4  29618  itg2gt0cn  29634  filnetlem3  29788  filnetlem4  29789  cncfiooicc  31188  stoweidlem34  31289  relopabVD  32656  psubspset  34415  psubclsetN  34607