Theorem 3sstr4i 4010

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 4005	. 2 ⊢ 𝐶 ⊆ 𝐵
4		3sstr4.3	. 2 ⊢ 𝐷 = 𝐵
5	3, 4	sseqtrri 4008	1 ⊢ 𝐶 ⊆ 𝐷

Syntax hints:   = wceq 1540   ⊆ wss 3926

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 2007  ax-9 2118  ax-ext 2707

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

This theorem is referenced by:  relopabiv  5799  rncoss  5955  imassrn  6058  rnin  6135  inimass  6144  f1ossf1o  7118  ssoprab2i  7518  omopthlem2  8672  1sdom2dom  9255  rankval4  9881  cardf2  9957  r0weon  10026  dcomex  10461  axdc2lem  10462  fpwwe2lem1  10645  canthwe  10665  recmulnq  10978  npex  11000  axresscn  11162  mpoaddf  11223  mpomulf  11224  trclublem  15014  bpoly4  16075  2strop  17250  odlem1  19516  gexlem1  19560  pzriprnglem4  21445  psrbagsn  22021  bwth  23348  2ndcctbss  23393  uniioombllem4  25539  uniioombllem5  25540  eff1olem  26509  birthdaylem1  26913  zssno  28321  nvss  30574  lediri  31518  lejdiri  31520  sshhococi  31527  mayetes3i  31710  disjxpin  32569  imadifxp  32582  constrextdg2  33783  sxbrsigalem5  34320  eulerpartlemmf  34407  kur14lem6  35233  cvmlift2lem12  35336  bj-xpcossxp  37207  bj-rrhatsscchat  37254  mblfinlem4  37684  lclkrs2  41559  areaquad  43240  corclrcl  43731  corcltrcl  43763  relopabVD  44925  ovolval5lem3  46683  uspgrlimlem4  48003  setc1onsubc  49479