Theorem eqsstrri 4009

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

Syntax hints:   = wceq 1533   ⊆ wss 3940

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-v 3468  df-in 3947  df-ss 3957

This theorem is referenced by:  inss2  4221  dmv  5912  idssxp  6038  ofrfvalg  7671  ofval  7674  ofrval  7675  off  7681  ofres  7682  ofco  7686  dftpos4  8225  smores2  8349  dmttrcl  9711  rnttrcl  9712  onwf  9820  r0weon  10002  dju1dif  10162  unctb  10195  infmap2  10208  itunitc  10411  axcclem  10447  dfnn3  12222  cotr2  14920  ressbasssg  17179  ressbasssOLD  17182  prdsle  17406  prdsless  17407  cntrss  19236  dprd2da  19953  opsrle  21911  indiscld  22916  leordtval2  23037  fiuncmp  23229  prdstopn  23453  ustneism  24049  icchmeo  24786  itg1addlem4  25549  itg1addlem4OLD  25550  itg1addlem5  25551  tdeglem4OLD  25917  aannenlem3  26183  efifo  26397  konigsbergssiedgw  29938  pjoml4i  31275  5oai  31349  3oai  31356  bdopssadj  31769  xrge00  32618  xrge0mulc1cn  33376  esumdivc  33536  rpsqrtcn  34060  subfacp1lem5  34630  filnetlem3  35721  filnetlem4  35722  mblfinlem4  36984  itg2gt0cn  36999  psubspset  39071  psubclsetN  39263  dvrelog2  41388  dvrelog3  41389  relexpaddss  42924  corcltrcl  42945  relopabVD  44117  cncfiooicc  45061  amgmwlem  48003