Theorem 3sstr4i 3987

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

Syntax hints:   = wceq 1540   ⊆ wss 3903

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 2008  ax-9 2119  ax-ext 2701

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

This theorem is referenced by:  relopabiv  5763  rncoss  5918  imassrn  6022  rnin  6095  inimass  6104  f1ossf1o  7062  ssoprab2i  7460  omopthlem2  8578  1sdom2dom  9143  rankval4  9763  cardf2  9839  r0weon  9906  dcomex  10341  axdc2lem  10342  fpwwe2lem1  10525  canthwe  10545  recmulnq  10858  npex  10880  axresscn  11042  mpoaddf  11103  mpomulf  11104  trclublem  14902  bpoly4  15966  2strop  17140  odlem1  19414  gexlem1  19458  pzriprnglem4  21391  psrbagsn  21968  bwth  23295  2ndcctbss  23340  uniioombllem4  25485  uniioombllem5  25486  eff1olem  26455  birthdaylem1  26859  zssno  28274  nvss  30537  lediri  31481  lejdiri  31483  sshhococi  31490  mayetes3i  31673  disjxpin  32532  imadifxp  32545  constrextdg2  33716  sxbrsigalem5  34256  eulerpartlemmf  34343  kur14lem6  35184  cvmlift2lem12  35287  bj-xpcossxp  37163  bj-rrhatsscchat  37210  mblfinlem4  37640  lclkrs2  41519  areaquad  43189  corclrcl  43680  corcltrcl  43712  relopabVD  44874  ovolval5lem3  46635  uspgrlimlem4  47975  setc1onsubc  49587