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  7687  ofval  7690  ofrval  7691  off  7697  ofres  7698  ofco  7704  dftpos4  8244  smores2  8344  dmttrcl  9703  rnttrcl  9704  onwf  9815  r0weon  10018  dju1dif  10178  unctb  10209  infmap2  10222  itunitc  10426  axcclem  10462  dfnn3  12274  cotr2  15053  ressbasssg  17332  ressbasssOLD  17335  prdsle  17550  prdsless  17551  cntrss  19461  dprd2da  20174  opsrle  22266  indiscld  23319  leordtval2  23440  fiuncmp  23632  prdstopn  23857  ustneism  24453  icchmeo  25172  itg1addlem4  25930  itg1addlem5  25931  aannenlem3  26569  efifo  26787  konigsbergssiedgw  30733  pjoml4i  32071  5oai  32145  3oai  32152  bdopssadj  32565  xrge00  33457  xrge0mulc1cn  34454  esumdivc  34596  rpsqrtcn  35104  subfacp1lem5  35766  filnetlem3  37002  filnetlem4  37003  mblfinlem4  38412  itg2gt0cn  38427  psubspset  40620  psubclsetN  40812  dvrelog2  42933  dvrelog3  42934  readvrec2  43239  relexpaddss  44561  corcltrcl  44582  relopabVD  45726  cncfiooicc  46725  amgmwlem  50823