Theorem eqsstr3i 3463

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

Syntax hints:   = wceq 1444   C_ wss 3404

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431

This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-in 3411  df-ss 3418

This theorem is referenced by:  inss2  3653  dmv  5050  ofrfval  6539  ofval  6540  ofrval  6541  off  6546  ofres  6547  ofco  6551  dftpos4  6992  smores2  7073  onwf  8301  r0weon  8443  cda1dif  8606  unctb  8635  infmap2  8648  itunitc  8851  axcclem  8887  dfnn3  10623  bcm1k  12500  bcpasc  12506  cotr2  13041  ressbasss  15181  strlemor1  15217  prdsle  15360  prdsless  15361  dprd2da  17675  opsrle  18699  indiscld  20107  leordtval2  20228  fiuncmp  20419  prdstopn  20643  ustneism  21238  itg1addlem4  22657  itg1addlem5  22658  tdeglem4  23009  aannenlem3  23286  efifo  23496  advlogexp  23600  pjoml4i  27240  5oai  27314  3oai  27321  bdopssadj  27734  suppss2fOLD  28237  xrge00  28448  xrge0mulc1cn  28747  esumdivc  28904  ballotlemodife  29330  subfacp1lem5  29907  filnetlem3  31036  filnetlem4  31037  mblfinlem4  31980  itg2gt0cn  31997  psubspset  33309  psubclsetN  33501  relexpaddss  36310  corcltrcl  36331  relopabVD  37298  cncfiooicc  37772  stoweidlem34  37895