Theorem eqsstrri 4018

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

Syntax hints:   = wceq 1542   ⊆ wss 3949

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966

This theorem is referenced by:  inss2  4230  dmv  5923  idssxp  6049  ofrfvalg  7678  ofval  7681  ofrval  7682  off  7688  ofres  7689  ofco  7693  dftpos4  8230  smores2  8354  dmttrcl  9716  rnttrcl  9717  onwf  9825  r0weon  10007  dju1dif  10167  unctb  10200  infmap2  10213  itunitc  10416  axcclem  10452  dfnn3  12226  cotr2  14924  ressbasssg  17181  ressbasssOLD  17184  prdsle  17408  prdsless  17409  cntrss  19195  dprd2da  19912  opsrle  21602  indiscld  22595  leordtval2  22716  fiuncmp  22908  prdstopn  23132  ustneism  23728  itg1addlem4  25216  itg1addlem4OLD  25217  itg1addlem5  25218  tdeglem4OLD  25578  aannenlem3  25843  efifo  26056  konigsbergssiedgw  29503  pjoml4i  30840  5oai  30914  3oai  30921  bdopssadj  31334  xrge00  32187  xrge0mulc1cn  32921  esumdivc  33081  rpsqrtcn  33605  subfacp1lem5  34175  gg-icchmeo  35170  filnetlem3  35265  filnetlem4  35266  mblfinlem4  36528  itg2gt0cn  36543  psubspset  38615  psubclsetN  38807  dvrelog2  40929  dvrelog3  40930  relexpaddss  42469  corcltrcl  42490  relopabVD  43662  cncfiooicc  44610  amgmwlem  47849