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 2770	. 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 2733

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

This theorem is used by:  3sstr3i  3981  inss2  4183  dmv  5904  idssxp  6041  ofrfvalg  7699  ofval  7702  ofrval  7703  off  7709  ofres  7710  ofco  7716  dftpos4  8255  smores2  8355  dmttrcl  9715  rnttrcl  9716  onwf  9833  r0weon  10084  dju1dif  10244  unctb  10275  infmap2  10288  itunitc  10492  axcclem  10528  dfnn3  12342  cotr2  15123  ressbasssg  17408  ressbasssOLD  17411  prdsle  17626  prdsless  17627  cntrss  19538  dprd2da  20251  opsrle  22349  indiscld  23402  leordtval2  23523  fiuncmp  23715  prdstopn  23940  ustneism  24536  icchmeo  25255  itg1addlem4  26013  itg1addlem5  26014  aannenlem3  26650  efifo  26868  konigsbergssiedgw  30844  pjoml4i  32182  5oai  32256  3oai  32263  bdopssadj  32676  xrge00  33568  xrge0mulc1cn  34566  esumdivc  34708  rpsqrtcn  35215  subfacp1lem5  35928  filnetlem3  37148  filnetlem4  37149  mblfinlem4  38558  itg2gt0cn  38573  psubspset  40781  psubclsetN  40973  dvrelog2  43094  dvrelog3  43095  readvrec2  43392  relexpaddss  44703  corcltrcl  44724  relopabVD  45868  cncfiooicc  46873  amgmwlem  50956