Theorem eqsstrri 3992

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

Syntax hints:   = wceq 1567   ⊆ wss 3913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-ss 3930

This theorem is referenced by:  3sstr3i  3995  inss2  4198  dmv  5910  idssxp  6049  ofrfvalg  7680  ofval  7683  ofrval  7684  off  7690  ofres  7691  ofco  7697  dftpos4  8237  smores2  8337  dmttrcl  9686  rnttrcl  9687  onwf  9798  r0weon  9992  dju1dif  10152  unctb  10183  infmap2  10196  itunitc  10401  axcclem  10437  dfnn3  12243  cotr2  15010  ressbasssg  17293  ressbasssOLD  17296  prdsle  17511  prdsless  17512  cntrss  19397  dprd2da  20110  opsrle  22163  indiscld  23213  leordtval2  23334  fiuncmp  23526  prdstopn  23750  ustneism  24346  icchmeo  25065  itg1addlem4  25823  itg1addlem5  25824  aannenlem3  26456  efifo  26674  konigsbergssiedgw  30538  pjoml4i  31876  5oai  31950  3oai  31957  bdopssadj  32370  xrge00  33271  xrge0mulc1cn  34272  esumdivc  34414  rpsqrtcn  34921  subfacp1lem5  35571  filnetlem3  36776  filnetlem4  36777  mblfinlem4  38194  itg2gt0cn  38209  psubspset  40403  psubclsetN  40595  dvrelog2  42716  dvrelog3  42717  readvrec2  43007  relexpaddss  44331  corcltrcl  44352  relopabVD  45496  cncfiooicc  46495  amgmwlem  50471