Theorem eqsstrri 3991

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

Syntax hints:   = wceq 1540   ⊆ wss 3911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ss 3928

This theorem is referenced by:  3sstr3i  3994  inss2  4197  dmv  5876  idssxp  6009  ofrfvalg  7641  ofval  7644  ofrval  7645  off  7651  ofres  7652  ofco  7658  dftpos4  8201  smores2  8300  dmttrcl  9650  rnttrcl  9651  onwf  9759  r0weon  9941  dju1dif  10102  unctb  10133  infmap2  10146  itunitc  10350  axcclem  10386  dfnn3  12176  cotr2  14919  ressbasssg  17183  ressbasssOLD  17186  prdsle  17401  prdsless  17402  cntrss  19239  dprd2da  19950  opsrle  21930  indiscld  22954  leordtval2  23075  fiuncmp  23267  prdstopn  23491  ustneism  24087  icchmeo  24814  itg1addlem4  25576  itg1addlem5  25577  aannenlem3  26214  efifo  26432  konigsbergssiedgw  30152  pjoml4i  31489  5oai  31563  3oai  31570  bdopssadj  31983  xrge00  32926  xrge0mulc1cn  33904  esumdivc  34046  rpsqrtcn  34557  subfacp1lem5  35144  filnetlem3  36341  filnetlem4  36342  mblfinlem4  37627  itg2gt0cn  37642  psubspset  39711  psubclsetN  39903  dvrelog2  42025  dvrelog3  42026  readvrec2  42322  relexpaddss  43680  corcltrcl  43701  relopabVD  44863  cncfiooicc  45865  amgmwlem  49764