Theorem eqsstrri 3970

Description: Substitution of equality into a subclass relationship. (Contributed by NM, 19-Oct-1999.)

Hypotheses

Ref	Expression
eqsstr3.1	⊢ 𝐵 = 𝐴
eqsstr3.2	⊢ 𝐵 ⊆ 𝐶

Assertion

Ref	Expression
eqsstrri	⊢ 𝐴 ⊆ 𝐶

Proof of Theorem eqsstrri

Step	Hyp	Ref	Expression
1		eqsstr3.1	. . 3 ⊢ 𝐵 = 𝐴
2	1	eqcomi 2746	. 2 ⊢ 𝐴 = 𝐵
3		eqsstr3.2	. 2 ⊢ 𝐵 ⊆ 𝐶
4	2, 3	eqsstri 3969	1 ⊢ 𝐴 ⊆ 𝐶

Syntax hints:   = wceq 1542   ⊆ wss 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ss 3907

This theorem is referenced by:  3sstr3i  3973  inss2  4179  dmv  5869  idssxp  6006  ofrfvalg  7630  ofval  7633  ofrval  7634  off  7640  ofres  7641  ofco  7647  dftpos4  8186  smores2  8285  dmttrcl  9631  rnttrcl  9632  onwf  9743  r0weon  9923  dju1dif  10084  unctb  10115  infmap2  10128  itunitc  10332  axcclem  10368  dfnn3  12177  cotr2  14928  ressbasssg  17196  ressbasssOLD  17199  prdsle  17414  prdsless  17415  cntrss  19295  dprd2da  20008  opsrle  22034  indiscld  23065  leordtval2  23186  fiuncmp  23378  prdstopn  23602  ustneism  24198  icchmeo  24917  itg1addlem4  25675  itg1addlem5  25676  aannenlem3  26309  efifo  26527  konigsbergssiedgw  30340  pjoml4i  31678  5oai  31752  3oai  31759  bdopssadj  32172  xrge00  33094  xrge0mulc1cn  34106  esumdivc  34248  rpsqrtcn  34758  subfacp1lem5  35387  filnetlem3  36583  filnetlem4  36584  mblfinlem4  37992  itg2gt0cn  38007  psubspset  40201  psubclsetN  40393  dvrelog2  42514  dvrelog3  42515  readvrec2  42804  relexpaddss  44160  corcltrcl  44181  relopabVD  45342  cncfiooicc  46337  amgmwlem  50274