Theorem eqsstrri 4006

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 2744	. 2 ⊢ 𝐴 = 𝐵
3		eqsstr3.2	. 2 ⊢ 𝐵 ⊆ 𝐶
4	2, 3	eqsstri 4005	1 ⊢ 𝐴 ⊆ 𝐶

Syntax hints:   = wceq 1540   ⊆ wss 3926

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2727  df-ss 3943

This theorem is referenced by:  3sstr3i  4009  inss2  4213  dmv  5902  idssxp  6036  ofrfvalg  7679  ofval  7682  ofrval  7683  off  7689  ofres  7690  ofco  7696  dftpos4  8244  smores2  8368  dmttrcl  9735  rnttrcl  9736  onwf  9844  r0weon  10026  dju1dif  10187  unctb  10218  infmap2  10231  itunitc  10435  axcclem  10471  dfnn3  12254  cotr2  14996  ressbasssg  17258  ressbasssOLD  17261  prdsle  17476  prdsless  17477  cntrss  19314  dprd2da  20025  opsrle  22005  indiscld  23029  leordtval2  23150  fiuncmp  23342  prdstopn  23566  ustneism  24162  icchmeo  24889  itg1addlem4  25652  itg1addlem5  25653  aannenlem3  26290  efifo  26508  konigsbergssiedgw  30231  pjoml4i  31568  5oai  31642  3oai  31649  bdopssadj  32062  xrge00  33007  xrge0mulc1cn  33972  esumdivc  34114  rpsqrtcn  34625  subfacp1lem5  35206  filnetlem3  36398  filnetlem4  36399  mblfinlem4  37684  itg2gt0cn  37699  psubspset  39763  psubclsetN  39955  dvrelog2  42077  dvrelog3  42078  readvrec2  42404  relexpaddss  43742  corcltrcl  43763  relopabVD  44925  cncfiooicc  45923  amgmwlem  49666