Theorem eqsstrri 3983

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

Syntax hints:   = wceq 1540   ⊆ wss 3903

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 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ss 3920

This theorem is referenced by:  3sstr3i  3986  inss2  4189  dmv  5865  idssxp  6000  ofrfvalg  7621  ofval  7624  ofrval  7625  off  7631  ofres  7632  ofco  7638  dftpos4  8178  smores2  8277  dmttrcl  9617  rnttrcl  9618  onwf  9726  r0weon  9906  dju1dif  10067  unctb  10098  infmap2  10111  itunitc  10315  axcclem  10351  dfnn3  12142  cotr2  14884  ressbasssg  17148  ressbasssOLD  17151  prdsle  17366  prdsless  17367  cntrss  19210  dprd2da  19923  opsrle  21952  indiscld  22976  leordtval2  23097  fiuncmp  23289  prdstopn  23513  ustneism  24109  icchmeo  24836  itg1addlem4  25598  itg1addlem5  25599  aannenlem3  26236  efifo  26454  konigsbergssiedgw  30194  pjoml4i  31531  5oai  31605  3oai  31612  bdopssadj  32025  xrge00  32968  xrge0mulc1cn  33908  esumdivc  34050  rpsqrtcn  34561  subfacp1lem5  35157  filnetlem3  36354  filnetlem4  36355  mblfinlem4  37640  itg2gt0cn  37655  psubspset  39723  psubclsetN  39915  dvrelog2  42037  dvrelog3  42038  readvrec2  42334  relexpaddss  43691  corcltrcl  43712  relopabVD  44874  cncfiooicc  45875  amgmwlem  49787