Theorem eqsstr3i 3520

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

Syntax hints:   = wceq 1383   C_ wss 3461

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-in 3468  df-ss 3475

This theorem is referenced by:  inss2  3704  dmv  5208  ofrfval  6533  ofval  6534  ofrval  6535  off  6539  ofres  6540  ofco  6545  dftpos4  6976  smores2  7027  onwf  8251  r0weon  8393  cda1dif  8559  unctb  8588  infmap2  8601  itunitc  8804  axcclem  8840  dfnn3  10557  bcm1k  12374  bcpasc  12380  ressbasss  14670  strlemor1  14705  prdsle  14840  prdsless  14841  dprd2da  17069  opsrle  18118  indiscld  19569  leordtval2  19690  fiuncmp  19881  prdstopn  20106  ustneism  20703  itg1addlem4  22083  itg1addlem5  22084  tdeglem4  22435  aannenlem3  22702  efifo  22910  advlogexp  23012  pjoml4i  26481  5oai  26555  3oai  26562  bdopssadj  26976  suppss2f  27453  xrge00  27651  xrge0mulc1cn  27900  esumdivc  28066  ballotlemodife  28413  subfacp1lem5  28605  mblfinlem4  30029  itg2gt0cn  30045  filnetlem3  30173  filnetlem4  30174  cncfiooicc  31604  stoweidlem34  31705  relopabVD  33434  psubspset  35208  psubclsetN  35400  cotr2  37480