Theorem eqsstr3i 3384

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

Syntax hints:   = wceq 1364   C_ wss 3325

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 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-in 3332  df-ss 3339

This theorem is referenced by:  inss2  3568  dmv  5051  ofrfval  6327  ofval  6328  ofrval  6329  off  6333  ofres  6334  ofco  6339  dftpos4  6763  smores2  6811  onwf  8033  r0weon  8175  cda1dif  8341  unctb  8370  infmap2  8383  itunitc  8586  axcclem  8622  dfnn3  10332  bcm1k  12087  bcpasc  12093  ressbasss  14226  strlemor1  14261  prdsle  14396  prdsless  14397  dprd2da  16531  opsrle  17533  indiscld  18654  leordtval2  18775  fiuncmp  18966  prdstopn  19160  ustneism  19757  itg1addlem4  21136  itg1addlem5  21137  tdeglem4  21488  aannenlem3  21755  efifo  21962  advlogexp  22059  pjoml4i  24925  5oai  24999  3oai  25006  bdopssadj  25420  suppss2f  25889  xrge00  26080  xrge0mulc1cn  26307  esumdivc  26468  ballotlemodife  26810  subfacp1lem5  27002  mblfinlem4  28356  itg2gt0cn  28372  filnetlem3  28526  filnetlem4  28527  stoweidlem34  29754  relopabVD  31471  psubspset  33110  psubclsetN  33302