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

Syntax hints:   = wceq 1398   C_ wss 3461

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-in 3468  df-ss 3475

This theorem is referenced by:  inss2  3705  dmv  5207  ofrfval  6521  ofval  6522  ofrval  6523  off  6527  ofres  6528  ofco  6533  dftpos4  6966  smores2  7017  onwf  8239  r0weon  8381  cda1dif  8547  unctb  8576  infmap2  8589  itunitc  8792  axcclem  8828  dfnn3  10545  bcm1k  12375  bcpasc  12381  cotr2  12895  ressbasss  14775  strlemor1  14811  prdsle  14951  prdsless  14952  dprd2da  17286  opsrle  18335  indiscld  19759  leordtval2  19880  fiuncmp  20071  prdstopn  20295  ustneism  20892  itg1addlem4  22272  itg1addlem5  22273  tdeglem4  22624  aannenlem3  22892  efifo  23100  advlogexp  23204  pjoml4i  26703  5oai  26777  3oai  26784  bdopssadj  27198  suppss2f  27698  xrge00  27908  xrge0mulc1cn  28158  esumdivc  28312  ballotlemodife  28700  subfacp1lem5  28892  mblfinlem4  30294  itg2gt0cn  30310  filnetlem3  30438  filnetlem4  30439  cncfiooicc  31936  stoweidlem34  32055  relopabVD  34102  psubspset  35865  psubclsetN  36057  relexpaddss  38205  corcltrcl  38231