Theorem eqsstrri 3969

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

Syntax hints:   = wceq 1542   ⊆ wss 3889

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 2708

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

This theorem is referenced by:  3sstr3i  3972  inss2  4178  dmv  5877  idssxp  6014  ofrfvalg  7639  ofval  7642  ofrval  7643  off  7649  ofres  7650  ofco  7656  dftpos4  8195  smores2  8294  dmttrcl  9642  rnttrcl  9643  onwf  9754  r0weon  9934  dju1dif  10095  unctb  10126  infmap2  10139  itunitc  10343  axcclem  10379  dfnn3  12188  cotr2  14939  ressbasssg  17207  ressbasssOLD  17210  prdsle  17425  prdsless  17426  cntrss  19306  dprd2da  20019  opsrle  22025  indiscld  23056  leordtval2  23177  fiuncmp  23369  prdstopn  23593  ustneism  24189  icchmeo  24908  itg1addlem4  25666  itg1addlem5  25667  aannenlem3  26296  efifo  26511  konigsbergssiedgw  30320  pjoml4i  31658  5oai  31732  3oai  31739  bdopssadj  32152  xrge00  33074  xrge0mulc1cn  34085  esumdivc  34227  rpsqrtcn  34737  subfacp1lem5  35366  filnetlem3  36562  filnetlem4  36563  mblfinlem4  37981  itg2gt0cn  37996  psubspset  40190  psubclsetN  40382  dvrelog2  42503  dvrelog3  42504  readvrec2  42793  relexpaddss  44145  corcltrcl  44166  relopabVD  45327  cncfiooicc  46322  amgmwlem  50277