Theorem eqsstrri 3978

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

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

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 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2732

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

This theorem is used by:  3sstr3i  3981  inss2  4183  dmv  5906  idssxp  6045  ofrfvalg  7686  ofval  7689  ofrval  7690  off  7696  ofres  7697  ofco  7703  dftpos4  8243  smores2  8343  dmttrcl  9700  rnttrcl  9701  onwf  9812  r0weon  10015  dju1dif  10175  unctb  10206  infmap2  10219  itunitc  10423  axcclem  10459  dfnn3  12271  cotr2  15050  ressbasssg  17329  ressbasssOLD  17332  prdsle  17547  prdsless  17548  cntrss  19458  dprd2da  20171  opsrle  22263  indiscld  23316  leordtval2  23437  fiuncmp  23629  prdstopn  23854  ustneism  24450  icchmeo  25169  itg1addlem4  25927  itg1addlem5  25928  aannenlem3  26566  efifo  26784  konigsbergssiedgw  30730  pjoml4i  32068  5oai  32142  3oai  32149  bdopssadj  32562  xrge00  33454  xrge0mulc1cn  34451  esumdivc  34593  rpsqrtcn  35101  subfacp1lem5  35763  filnetlem3  36999  filnetlem4  37000  mblfinlem4  38409  itg2gt0cn  38424  psubspset  40617  psubclsetN  40809  dvrelog2  42930  dvrelog3  42931  readvrec2  43236  relexpaddss  44558  corcltrcl  44579  relopabVD  45723  cncfiooicc  46722  amgmwlem  50820