Theorem 3sstr4i 3960

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

This proof depends on syntax axioms:   = wceq 1569   ⊆ wss 3896

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-ss 3897

This theorem is used by:  relopabiv  5799  rncoss  5960  imassrnOLD  6071  rninOLD  6140  inimass  6147  f1ossf1o  7134  ssoprab2i  7535  omopthlem2  8677  enssdom  9011  1sdom2dom  9253  rankval4  9891  cardf2  10031  r0weon  10098  dcomex  10532  axdc2lem  10533  fpwwe2lem1  10723  canthwe  10743  recmulnq  11056  npex  11078  axresscn  11240  mpoaddf  11301  mpomulf  11302  trclublem  15157  bpoly4  16234  2strop  17416  odlem1  19758  gexlem1  19802  pzriprnglem4  21799  psrbagsn  22381  bwth  23737  2ndcctbss  23783  uniioombllem4  25916  uniioombllem5  25917  eff1olem  26885  birthdaylem1  27288  zssno  28776  nvss  31204  lediri  32148  lejdiri  32150  sshhococi  32157  mayetes3i  32340  disjxpin  33233  imadifxp  33246  constrextdg2  34431  sxbrsigalem5  34970  eulerpartlemmf  35057  kur14lem6  36094  cvmlift2lem12  36197  onprcr  36580  bj-xpcossxp  38247  bj-rrhatsscchat  38294  mblfinlem4  38715  lclkrs2  42734  areaquad  44355  corclrcl  44844  corcltrcl  44876  relopabVD  46019  ovolval5lem3  47800  uspgrlimlem4  49225  setc1onsubc  50876