Theorem eqsstrri 3927

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

Syntax hints:   = wceq 1538   ⊆ wss 3858

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-v 3411  df-in 3865  df-ss 3875

This theorem is referenced by:  inss2  4134  dmv  5763  idssxp  5888  ofrfvalg  7412  ofval  7415  ofrval  7416  off  7422  ofres  7423  ofco  7427  dftpos4  7921  smores2  8001  onwf  9292  r0weon  9472  dju1dif  9632  unctb  9665  infmap2  9678  itunitc  9881  axcclem  9917  dfnn3  11688  cotr2  14384  ressbasss  16614  prdsle  16793  prdsless  16794  cntrss  18527  dprd2da  19232  opsrle  20807  indiscld  21791  leordtval2  21912  fiuncmp  22104  prdstopn  22328  ustneism  22924  itg1addlem4  24399  itg1addlem5  24400  tdeglem4OLD  24760  aannenlem3  25025  efifo  25238  konigsbergssiedgw  28134  pjoml4i  29469  5oai  29543  3oai  29550  bdopssadj  29963  xrge00  30821  xrge0mulc1cn  31412  esumdivc  31570  rpsqrtcn  32092  subfacp1lem5  32662  filnetlem3  34118  filnetlem4  34119  mblfinlem4  35377  itg2gt0cn  35392  psubspset  37320  psubclsetN  37512  dvrelog2  39630  dvrelog3  39631  relexpaddss  40792  corcltrcl  40813  relopabVD  41980  cncfiooicc  42902  amgmwlem  45721