Theorem eqsstrri 3981

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 3980	1 ⊢ 𝐴 ⊆ 𝐶

Syntax hints:   = wceq 1541   ⊆ wss 3901

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 2708

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

This theorem is referenced by:  3sstr3i  3984  inss2  4190  dmv  5871  idssxp  6008  ofrfvalg  7630  ofval  7633  ofrval  7634  off  7640  ofres  7641  ofco  7647  dftpos4  8187  smores2  8286  dmttrcl  9630  rnttrcl  9631  onwf  9742  r0weon  9922  dju1dif  10083  unctb  10114  infmap2  10127  itunitc  10331  axcclem  10367  dfnn3  12159  cotr2  14900  ressbasssg  17164  ressbasssOLD  17167  prdsle  17382  prdsless  17383  cntrss  19260  dprd2da  19973  opsrle  22002  indiscld  23035  leordtval2  23156  fiuncmp  23348  prdstopn  23572  ustneism  24168  icchmeo  24894  itg1addlem4  25656  itg1addlem5  25657  aannenlem3  26294  efifo  26512  konigsbergssiedgw  30325  pjoml4i  31662  5oai  31736  3oai  31743  bdopssadj  32156  xrge00  33096  xrge0mulc1cn  34098  esumdivc  34240  rpsqrtcn  34750  subfacp1lem5  35378  filnetlem3  36574  filnetlem4  36575  mblfinlem4  37861  itg2gt0cn  37876  psubspset  40004  psubclsetN  40196  dvrelog2  42318  dvrelog3  42319  readvrec2  42616  relexpaddss  43959  corcltrcl  43980  relopabVD  45141  cncfiooicc  46138  amgmwlem  50047