Theorem eqsstr3i 3636

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

Syntax hints:   = wceq 1483   C_ wss 3574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-in 3581  df-ss 3588

This theorem is referenced by:  inss2  3834  dmv  5341  ofrfval  6905  ofval  6906  ofrval  6907  off  6912  ofres  6913  ofco  6917  dftpos4  7371  smores2  7451  onwf  8693  r0weon  8835  cda1dif  8998  unctb  9027  infmap2  9040  itunitc  9243  axcclem  9279  dfnn3  11034  bcm1k  13102  bcpasc  13108  cotr2  13716  ressbasss  15932  strlemor1OLD  15969  prdsle  16122  prdsless  16123  dprd2da  18441  opsrle  19475  indiscld  20895  leordtval2  21016  fiuncmp  21207  prdstopn  21431  ustneism  22027  itg1addlem4  23466  itg1addlem5  23467  tdeglem4  23820  aannenlem3  24085  efifo  24293  advlogexp  24401  konigsbergssiedgw  27111  pjoml4i  28446  5oai  28520  3oai  28527  bdopssadj  28940  xrge00  29686  xrge0mulc1cn  29987  esumdivc  30145  ballotlemodife  30559  rpsqrtcn  30671  subfacp1lem5  31166  filnetlem3  32375  filnetlem4  32376  mblfinlem4  33449  itg2gt0cn  33465  psubspset  35030  psubclsetN  35222  relexpaddss  38010  corcltrcl  38031  relopabVD  39137  cncfiooicc  40107  stoweidlem34  40251  amgmwlem  42548