Theorem eqsstrri 4016

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

Syntax hints:   = wceq 1539   ⊆ wss 3947

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 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-v 3474  df-in 3954  df-ss 3964

This theorem is referenced by:  inss2  4228  dmv  5921  idssxp  6047  ofrfvalg  7680  ofval  7683  ofrval  7684  off  7690  ofres  7691  ofco  7695  dftpos4  8232  smores2  8356  dmttrcl  9718  rnttrcl  9719  onwf  9827  r0weon  10009  dju1dif  10169  unctb  10202  infmap2  10215  itunitc  10418  axcclem  10454  dfnn3  12230  cotr2  14928  ressbasssg  17185  ressbasssOLD  17188  prdsle  17412  prdsless  17413  cntrss  19236  dprd2da  19953  opsrle  21821  indiscld  22815  leordtval2  22936  fiuncmp  23128  prdstopn  23352  ustneism  23948  icchmeo  24685  itg1addlem4  25448  itg1addlem4OLD  25449  itg1addlem5  25450  tdeglem4OLD  25813  aannenlem3  26079  efifo  26292  konigsbergssiedgw  29770  pjoml4i  31107  5oai  31181  3oai  31188  bdopssadj  31601  xrge00  32454  xrge0mulc1cn  33219  esumdivc  33379  rpsqrtcn  33903  subfacp1lem5  34473  filnetlem3  35568  filnetlem4  35569  mblfinlem4  36831  itg2gt0cn  36846  psubspset  38918  psubclsetN  39110  dvrelog2  41235  dvrelog3  41236  relexpaddss  42771  corcltrcl  42792  relopabVD  43964  cncfiooicc  44908  amgmwlem  47936