Theorem eqsstrri 4018

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

Syntax hints:   = wceq 1540   ⊆ wss 3949

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3475  df-in 3956  df-ss 3966

This theorem is referenced by:  inss2  4230  dmv  5923  idssxp  6049  ofrfvalg  7681  ofval  7684  ofrval  7685  off  7691  ofres  7692  ofco  7696  dftpos4  8233  smores2  8357  dmttrcl  9719  rnttrcl  9720  onwf  9828  r0weon  10010  dju1dif  10170  unctb  10203  infmap2  10216  itunitc  10419  axcclem  10455  dfnn3  12231  cotr2  14929  ressbasssg  17186  ressbasssOLD  17189  prdsle  17413  prdsless  17414  cntrss  19237  dprd2da  19954  opsrle  21822  indiscld  22816  leordtval2  22937  fiuncmp  23129  prdstopn  23353  ustneism  23949  icchmeo  24686  itg1addlem4  25449  itg1addlem4OLD  25450  itg1addlem5  25451  tdeglem4OLD  25811  aannenlem3  26076  efifo  26289  konigsbergssiedgw  29767  pjoml4i  31104  5oai  31178  3oai  31185  bdopssadj  31598  xrge00  32451  xrge0mulc1cn  33216  esumdivc  33376  rpsqrtcn  33900  subfacp1lem5  34470  filnetlem3  35569  filnetlem4  35570  mblfinlem4  36832  itg2gt0cn  36847  psubspset  38919  psubclsetN  39111  dvrelog2  41236  dvrelog3  41237  relexpaddss  42772  corcltrcl  42793  relopabVD  43965  cncfiooicc  44910  amgmwlem  47938