Theorem eqsstrri 3960

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

This proof depends on syntax axioms:   = wceq 1570   ⊆ wss 3900

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-ss 3901

This theorem is used by:  3sstr3i  3963  inss2  4137  dmv  5916  idssxp  6059  ofrfvalg  7733  ofval  7736  ofrval  7737  off  7743  ofres  7744  ofco  7750  dftpos4  8300  smores2  8400  dmttrcl  9759  rnttrcl  9760  onwf  9877  r0weon  10130  dju1dif  10290  unctb  10321  infmap2  10334  itunitc  10538  axcclem  10574  dfnn3  12389  cotr2  15173  ressbasssg  17459  ressbasssOLD  17462  prdsle  17683  prdsless  17684  cntrss  19596  dprd2da  20309  opsrle  22411  indiscld  23464  leordtval2  23585  fiuncmp  23777  prdstopn  24002  ustneism  24598  icchmeo  25317  itg1addlem4  26075  itg1addlem5  26076  aannenlem3  26714  efifo  26932  konigsbergssiedgw  30908  pjoml4i  32246  5oai  32320  3oai  32327  bdopssadj  32740  xrge00  33674  xrge0mulc1cn  34684  esumdivc  34826  rpsqrtcn  35333  j0ltalephlem  36048  subfacp1lem5  36157  filnetlem3  37383  filnetlem4  37384  cossididres  38224  mblfinlem4  38846  itg2gt0cn  38861  psubspset  41067  psubclsetN  41259  dvrelog2  43380  dvrelog3  43381  readvrec2  43678  relexpaddss  44979  corcltrcl  45000  relopabVD  46143  cncfiooicc  47177  amgmwlem  51415