Theorem eqsstrri 3984

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

Syntax hints:   = wceq 1570   ⊆ wss 3905

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-ss 3922

This theorem is referenced by:  3sstr3i  3987  inss2  4190  dmv  5912  idssxp  6051  ofrfvalg  7682  ofval  7685  ofrval  7686  off  7692  ofres  7693  ofco  7699  dftpos4  8237  smores2  8337  dmttrcl  9686  rnttrcl  9687  onwf  9798  r0weon  9992  dju1dif  10152  unctb  10183  infmap2  10196  itunitc  10400  axcclem  10436  dfnn3  12242  cotr2  15010  ressbasssg  17292  ressbasssOLD  17295  prdsle  17510  prdsless  17511  cntrss  19396  dprd2da  20109  opsrle  22198  indiscld  23248  leordtval2  23369  fiuncmp  23561  prdstopn  23785  ustneism  24381  icchmeo  25100  itg1addlem4  25858  itg1addlem5  25859  aannenlem3  26493  efifo  26712  konigsbergssiedgw  30601  pjoml4i  31939  5oai  32013  3oai  32020  bdopssadj  32433  xrge00  33334  xrge0mulc1cn  34331  esumdivc  34473  rpsqrtcn  34980  subfacp1lem5  35676  filnetlem3  36891  filnetlem4  36892  mblfinlem4  38311  itg2gt0cn  38326  psubspset  40518  psubclsetN  40710  dvrelog2  42831  dvrelog3  42832  readvrec2  43122  relexpaddss  44444  corcltrcl  44465  relopabVD  45609  cncfiooicc  46608  amgmwlem  50622