Theorem 3sstr4i 3988

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

Syntax hints:   = wceq 1570   ⊆ wss 3905

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-ss 3922

This theorem is referenced by:  relopabiv  5807  rncoss  5967  imassrn  6073  rninOLD  6144  inimass  6152  f1ossf1o  7124  ssoprab2i  7521  omopthlem2  8642  enssdom  8969  1sdom2dom  9210  rankval4  9835  cardf2  9925  r0weon  9992  dcomex  10426  axdc2lem  10427  fpwwe2lem1  10611  canthwe  10631  recmulnq  10944  npex  10966  axresscn  11128  mpoaddf  11189  mpomulf  11190  trclublem  15028  bpoly4  16108  2strop  17284  odlem1  19600  gexlem1  19644  pzriprnglem4  21634  psrbagsn  22214  bwth  23567  2ndcctbss  23612  uniioombllem4  25745  uniioombllem5  25746  eff1olem  26713  birthdaylem1  27116  zssno  28574  nvss  30945  lediri  31889  lejdiri  31891  sshhococi  31898  mayetes3i  32081  disjxpin  32933  imadifxp  32946  constrextdg2  34139  sxbrsigalem5  34678  eulerpartlemmf  34765  kur14lem6  35703  cvmlift2lem12  35806  bj-xpcossxp  37833  bj-rrhatsscchat  37880  mblfinlem4  38311  lclkrs2  42314  areaquad  43943  corclrcl  44433  corcltrcl  44465  relopabVD  45609  ovolval5lem3  47368  uspgrlimlem4  48756  setc1onsubc  50380