Theorem eqsstrri 3981

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 3980	1 ⊢ 𝐴 ⊆ 𝐶

Syntax hints:   = wceq 1559   ⊆ wss 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753  df-ss 3919

This theorem is referenced by:  3sstr3i  3984  inss2  4187  dmv  5894  idssxp  6034  ofrfvalg  7663  ofval  7666  ofrval  7667  off  7673  ofres  7674  ofco  7680  dftpos4  8219  smores2  8319  dmttrcl  9670  rnttrcl  9671  onwf  9782  r0weon  9962  dju1dif  10123  unctb  10154  infmap2  10167  itunitc  10372  axcclem  10408  dfnn3  12218  cotr2  14984  ressbasssg  17264  ressbasssOLD  17267  prdsle  17482  prdsless  17483  cntrss  19362  dprd2da  20075  opsrle  22088  indiscld  23139  leordtval2  23260  fiuncmp  23452  prdstopn  23676  ustneism  24272  icchmeo  24991  itg1addlem4  25749  itg1addlem5  25750  aannenlem3  26382  efifo  26600  konigsbergssiedgw  30409  pjoml4i  31747  5oai  31821  3oai  31828  bdopssadj  32241  xrge00  33153  xrge0mulc1cn  34199  esumdivc  34341  rpsqrtcn  34848  subfacp1lem5  35495  filnetlem3  36701  filnetlem4  36702  mblfinlem4  38120  itg2gt0cn  38135  psubspset  40329  psubclsetN  40521  dvrelog2  42642  dvrelog3  42643  readvrec2  42931  relexpaddss  44255  corcltrcl  44276  relopabVD  45437  cncfiooicc  46429  amgmwlem  50384