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

Syntax hints:   = wceq 1541   ⊆ wss 3891

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1544  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3432  df-in 3898  df-ss 3908

This theorem is referenced by:  inss2  4168  dmv  5828  idssxp  5953  ofrfvalg  7532  ofval  7535  ofrval  7536  off  7542  ofres  7543  ofco  7547  dftpos4  8045  smores2  8169  dmttrcl  9440  rnttrcl  9441  onwf  9572  r0weon  9752  dju1dif  9912  unctb  9945  infmap2  9958  itunitc  10161  axcclem  10197  dfnn3  11970  cotr2  14669  ressbasss  16931  prdsle  17154  prdsless  17155  cntrss  18917  dprd2da  19626  opsrle  21229  indiscld  22223  leordtval2  22344  fiuncmp  22536  prdstopn  22760  ustneism  23356  itg1addlem4  24844  itg1addlem4OLD  24845  itg1addlem5  24846  tdeglem4OLD  25206  aannenlem3  25471  efifo  25684  konigsbergssiedgw  28593  pjoml4i  29928  5oai  30002  3oai  30009  bdopssadj  30422  xrge00  31274  xrge0mulc1cn  31870  esumdivc  32030  rpsqrtcn  32552  subfacp1lem5  33125  filnetlem3  34548  filnetlem4  34549  mblfinlem4  35796  itg2gt0cn  35811  psubspset  37737  psubclsetN  37929  dvrelog2  40052  dvrelog3  40053  relexpaddss  41279  corcltrcl  41300  relopabVD  42474  cncfiooicc  43389  amgmwlem  46458