Theorem eqsstr3i 3387

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

Syntax hints:   = wceq 1369   C_ wss 3328

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-in 3335  df-ss 3342

This theorem is referenced by:  inss2  3571  dmv  5055  ofrfval  6328  ofval  6329  ofrval  6330  off  6334  ofres  6335  ofco  6340  dftpos4  6764  smores2  6815  onwf  8037  r0weon  8179  cda1dif  8345  unctb  8374  infmap2  8387  itunitc  8590  axcclem  8626  dfnn3  10336  bcm1k  12091  bcpasc  12097  ressbasss  14230  strlemor1  14265  prdsle  14400  prdsless  14401  dprd2da  16541  opsrle  17557  indiscld  18695  leordtval2  18816  fiuncmp  19007  prdstopn  19201  ustneism  19798  itg1addlem4  21177  itg1addlem5  21178  tdeglem4  21529  aannenlem3  21796  efifo  22003  advlogexp  22100  pjoml4i  24990  5oai  25064  3oai  25071  bdopssadj  25485  suppss2f  25954  xrge00  26147  xrge0mulc1cn  26371  esumdivc  26532  ballotlemodife  26880  subfacp1lem5  27072  mblfinlem4  28431  itg2gt0cn  28447  filnetlem3  28601  filnetlem4  28602  stoweidlem34  29829  relopabVD  31637  psubspset  33388  psubclsetN  33580