Theorem eqsstrri 3961

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

Syntax hints:   = wceq 1539   ⊆ wss 3892

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3439  df-in 3899  df-ss 3909

This theorem is referenced by:  inss2  4169  dmv  5844  idssxp  5968  ofrfvalg  7573  ofval  7576  ofrval  7577  off  7583  ofres  7584  ofco  7588  dftpos4  8092  smores2  8216  dmttrcl  9523  rnttrcl  9524  onwf  9632  r0weon  9814  dju1dif  9974  unctb  10007  infmap2  10020  itunitc  10223  axcclem  10259  dfnn3  12033  cotr2  14733  ressbasss  16995  prdsle  17218  prdsless  17219  cntrss  18981  dprd2da  19690  opsrle  21293  indiscld  22287  leordtval2  22408  fiuncmp  22600  prdstopn  22824  ustneism  23420  itg1addlem4  24908  itg1addlem4OLD  24909  itg1addlem5  24910  tdeglem4OLD  25270  aannenlem3  25535  efifo  25748  konigsbergssiedgw  28659  pjoml4i  29994  5oai  30068  3oai  30075  bdopssadj  30488  xrge00  31340  xrge0mulc1cn  31936  esumdivc  32096  rpsqrtcn  32618  subfacp1lem5  33191  filnetlem3  34614  filnetlem4  34615  mblfinlem4  35861  itg2gt0cn  35876  psubspset  37800  psubclsetN  37992  dvrelog2  40114  dvrelog3  40115  relexpaddss  41364  corcltrcl  41385  relopabVD  42559  cncfiooicc  43484  amgmwlem  46564