Theorem eqsstrri 3983

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

Syntax hints:   = wceq 1542   ⊆ wss 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ss 3920

This theorem is referenced by:  3sstr3i  3986  inss2  4192  dmv  5879  idssxp  6016  ofrfvalg  7640  ofval  7643  ofrval  7644  off  7650  ofres  7651  ofco  7657  dftpos4  8197  smores2  8296  dmttrcl  9642  rnttrcl  9643  onwf  9754  r0weon  9934  dju1dif  10095  unctb  10126  infmap2  10139  itunitc  10343  axcclem  10379  dfnn3  12171  cotr2  14912  ressbasssg  17176  ressbasssOLD  17179  prdsle  17394  prdsless  17395  cntrss  19272  dprd2da  19985  opsrle  22014  indiscld  23047  leordtval2  23168  fiuncmp  23360  prdstopn  23584  ustneism  24180  icchmeo  24906  itg1addlem4  25668  itg1addlem5  25669  aannenlem3  26306  efifo  26524  konigsbergssiedgw  30337  pjoml4i  31675  5oai  31749  3oai  31756  bdopssadj  32169  xrge00  33107  xrge0mulc1cn  34119  esumdivc  34261  rpsqrtcn  34771  subfacp1lem5  35400  filnetlem3  36596  filnetlem4  36597  mblfinlem4  37911  itg2gt0cn  37926  psubspset  40120  psubclsetN  40312  dvrelog2  42434  dvrelog3  42435  readvrec2  42731  relexpaddss  44074  corcltrcl  44095  relopabVD  45256  cncfiooicc  46252  amgmwlem  50161