Theorem eqsstrri 3978

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

Syntax hints:   = wceq 1541   ⊆ wss 3898

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2725  df-ss 3915

This theorem is referenced by:  3sstr3i  3981  inss2  4187  dmv  5868  idssxp  6005  ofrfvalg  7627  ofval  7630  ofrval  7631  off  7637  ofres  7638  ofco  7644  dftpos4  8184  smores2  8283  dmttrcl  9622  rnttrcl  9623  onwf  9734  r0weon  9914  dju1dif  10075  unctb  10106  infmap2  10119  itunitc  10323  axcclem  10359  dfnn3  12150  cotr2  14891  ressbasssg  17155  ressbasssOLD  17158  prdsle  17373  prdsless  17374  cntrss  19251  dprd2da  19964  opsrle  21993  indiscld  23026  leordtval2  23147  fiuncmp  23339  prdstopn  23563  ustneism  24159  icchmeo  24885  itg1addlem4  25647  itg1addlem5  25648  aannenlem3  26285  efifo  26503  konigsbergssiedgw  30251  pjoml4i  31588  5oai  31662  3oai  31669  bdopssadj  32082  xrge00  33024  xrge0mulc1cn  34026  esumdivc  34168  rpsqrtcn  34678  subfacp1lem5  35300  filnetlem3  36496  filnetlem4  36497  mblfinlem4  37773  itg2gt0cn  37788  psubspset  39916  psubclsetN  40108  dvrelog2  42230  dvrelog3  42231  readvrec2  42531  relexpaddss  43875  corcltrcl  43896  relopabVD  45057  cncfiooicc  46054  amgmwlem  49963