Theorem 3sstr4i 3983

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

Syntax hints:   = wceq 1541   ⊆ wss 3899

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2726  df-ss 3916

This theorem is referenced by:  relopabiv  5767  rncoss  5924  imassrn  6028  rnin  6102  inimass  6111  f1ossf1o  7071  ssoprab2i  7467  omopthlem2  8586  enssdom  8911  1sdom2dom  9152  rankval4  9777  cardf2  9853  r0weon  9920  dcomex  10355  axdc2lem  10356  fpwwe2lem1  10540  canthwe  10560  recmulnq  10873  npex  10895  axresscn  11057  mpoaddf  11118  mpomulf  11119  trclublem  14916  bpoly4  15980  2strop  17154  odlem1  19462  gexlem1  19506  pzriprnglem4  21437  psrbagsn  22016  bwth  23352  2ndcctbss  23397  uniioombllem4  25541  uniioombllem5  25542  eff1olem  26511  birthdaylem1  26915  zssno  28339  nvss  30617  lediri  31561  lejdiri  31563  sshhococi  31570  mayetes3i  31753  disjxpin  32612  imadifxp  32625  constrextdg2  33855  sxbrsigalem5  34394  eulerpartlemmf  34481  kur14lem6  35354  cvmlift2lem12  35457  bj-xpcossxp  37333  bj-rrhatsscchat  37380  mblfinlem4  37800  lclkrs2  41739  areaquad  43400  corclrcl  43890  corcltrcl  43922  relopabVD  45083  ovolval5lem3  46840  uspgrlimlem4  48179  setc1onsubc  49789