Theorem eqsstrri 3977

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 3976	1 ⊢ 𝐴 ⊆ 𝐶

Syntax hints:   = wceq 1541   ⊆ wss 3897

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 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-ss 3914

This theorem is referenced by:  3sstr3i  3980  inss2  4183  dmv  5857  idssxp  5993  ofrfvalg  7613  ofval  7616  ofrval  7617  off  7623  ofres  7624  ofco  7630  dftpos4  8170  smores2  8269  dmttrcl  9606  rnttrcl  9607  onwf  9718  r0weon  9898  dju1dif  10059  unctb  10090  infmap2  10103  itunitc  10307  axcclem  10343  dfnn3  12134  cotr2  14879  ressbasssg  17143  ressbasssOLD  17146  prdsle  17361  prdsless  17362  cntrss  19238  dprd2da  19951  opsrle  21977  indiscld  23001  leordtval2  23122  fiuncmp  23314  prdstopn  23538  ustneism  24134  icchmeo  24860  itg1addlem4  25622  itg1addlem5  25623  aannenlem3  26260  efifo  26478  konigsbergssiedgw  30222  pjoml4i  31559  5oai  31633  3oai  31640  bdopssadj  32053  xrge00  32987  xrge0mulc1cn  33946  esumdivc  34088  rpsqrtcn  34598  subfacp1lem5  35220  filnetlem3  36414  filnetlem4  36415  mblfinlem4  37700  itg2gt0cn  37715  psubspset  39783  psubclsetN  39975  dvrelog2  42097  dvrelog3  42098  readvrec2  42394  relexpaddss  43751  corcltrcl  43772  relopabVD  44933  cncfiooicc  45932  amgmwlem  49834