Theorem 3sstr4i 4001

Description: Substitution of equality in both sides of a subclass relationship. (Contributed by NM, 13-Jan-1996.) (Proof shortened by Eric Schmidt, 26-Jan-2007.)

Hypotheses

Ref	Expression
3sstr4.1	⊢ 𝐴 ⊆ 𝐵
3sstr4.2	⊢ 𝐶 = 𝐴
3sstr4.3	⊢ 𝐷 = 𝐵

Assertion

Ref	Expression
3sstr4i	⊢ 𝐶 ⊆ 𝐷

Proof of Theorem 3sstr4i

Step	Hyp	Ref	Expression
1		3sstr4.2	. . 3 ⊢ 𝐶 = 𝐴
2		3sstr4.1	. . 3 ⊢ 𝐴 ⊆ 𝐵
3	1, 2	eqsstri 3996	. 2 ⊢ 𝐶 ⊆ 𝐵
4		3sstr4.3	. 2 ⊢ 𝐷 = 𝐵
5	3, 4	sseqtrri 3999	1 ⊢ 𝐶 ⊆ 𝐷

Syntax hints:   = wceq 1540   ⊆ wss 3917

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 2702

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

This theorem is referenced by:  relopabiv  5786  rncoss  5942  imassrn  6045  rnin  6122  inimass  6131  f1ossf1o  7103  ssoprab2i  7503  omopthlem2  8627  1sdom2dom  9201  rankval4  9827  cardf2  9903  r0weon  9972  dcomex  10407  axdc2lem  10408  fpwwe2lem1  10591  canthwe  10611  recmulnq  10924  npex  10946  axresscn  11108  mpoaddf  11169  mpomulf  11170  trclublem  14968  bpoly4  16032  2strop  17206  odlem1  19472  gexlem1  19516  pzriprnglem4  21401  psrbagsn  21977  bwth  23304  2ndcctbss  23349  uniioombllem4  25494  uniioombllem5  25495  eff1olem  26464  birthdaylem1  26868  zssno  28276  nvss  30529  lediri  31473  lejdiri  31475  sshhococi  31482  mayetes3i  31665  disjxpin  32524  imadifxp  32537  constrextdg2  33746  sxbrsigalem5  34286  eulerpartlemmf  34373  kur14lem6  35205  cvmlift2lem12  35308  bj-xpcossxp  37184  bj-rrhatsscchat  37231  mblfinlem4  37661  lclkrs2  41541  areaquad  43212  corclrcl  43703  corcltrcl  43735  relopabVD  44897  ovolval5lem3  46659  uspgrlimlem4  47994  setc1onsubc  49595