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  5871  idssxp  6008  ofrfvalg  7632  ofval  7635  ofrval  7636  off  7642  ofres  7643  ofco  7649  dftpos4  8188  smores2  8287  dmttrcl  9633  rnttrcl  9634  onwf  9745  r0weon  9925  dju1dif  10086  unctb  10117  infmap2  10130  itunitc  10334  axcclem  10370  dfnn3  12179  cotr2  14930  ressbasssg  17198  ressbasssOLD  17201  prdsle  17416  prdsless  17417  cntrss  19297  dprd2da  20010  opsrle  22035  indiscld  23066  leordtval2  23187  fiuncmp  23379  prdstopn  23603  ustneism  24199  icchmeo  24918  itg1addlem4  25676  itg1addlem5  25677  aannenlem3  26307  efifo  26524  konigsbergssiedgw  30335  pjoml4i  31673  5oai  31747  3oai  31754  bdopssadj  32167  xrge00  33089  xrge0mulc1cn  34101  esumdivc  34243  rpsqrtcn  34753  subfacp1lem5  35382  filnetlem3  36578  filnetlem4  36579  mblfinlem4  37995  itg2gt0cn  38010  psubspset  40204  psubclsetN  40396  dvrelog2  42517  dvrelog3  42518  readvrec2  42807  relexpaddss  44163  corcltrcl  44184  relopabVD  45345  cncfiooicc  46340  amgmwlem  50289