Theorem 3sstr4i 3982

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

This proof depends on syntax axioms:   = wceq 1570   ⊆ wss 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-ss 3916

This theorem is used by:  relopabiv  5798  rncoss  5959  imassrnOLD  6069  rninOLD  6138  inimass  6145  f1ossf1o  7127  ssoprab2i  7529  omopthlem2  8662  enssdom  8996  1sdom2dom  9238  rankval4  9877  cardf2  10017  r0weon  10084  dcomex  10518  axdc2lem  10519  fpwwe2lem1  10709  canthwe  10729  recmulnq  11042  npex  11064  axresscn  11226  mpoaddf  11287  mpomulf  11288  trclublem  15141  bpoly4  16218  2strop  17400  odlem1  19742  gexlem1  19786  pzriprnglem4  21783  psrbagsn  22365  bwth  23721  2ndcctbss  23767  uniioombllem4  25900  uniioombllem5  25901  eff1olem  26869  birthdaylem1  27272  zssno  28760  nvss  31188  lediri  32132  lejdiri  32134  sshhococi  32141  mayetes3i  32324  disjxpin  33175  imadifxp  33188  constrextdg2  34374  sxbrsigalem5  34913  eulerpartlemmf  35000  kur14lem6  35955  cvmlift2lem12  36058  bj-xpcossxp  38090  bj-rrhatsscchat  38137  mblfinlem4  38558  lclkrs2  42577  areaquad  44202  corclrcl  44692  corcltrcl  44724  relopabVD  45868  ovolval5lem3  47633  uspgrlimlem4  49058  setc1onsubc  50679