Theorem 3sstr4i 3995

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

Syntax hints:   = wceq 1540   ⊆ wss 3911

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 3928

This theorem is referenced by:  relopabiv  5774  rncoss  5928  imassrn  6031  rnin  6107  inimass  6116  f1ossf1o  7082  ssoprab2i  7480  omopthlem2  8601  1sdom2dom  9170  rankval4  9796  cardf2  9872  r0weon  9941  dcomex  10376  axdc2lem  10377  fpwwe2lem1  10560  canthwe  10580  recmulnq  10893  npex  10915  axresscn  11077  mpoaddf  11138  mpomulf  11139  trclublem  14937  bpoly4  16001  2strop  17175  odlem1  19441  gexlem1  19485  pzriprnglem4  21370  psrbagsn  21946  bwth  23273  2ndcctbss  23318  uniioombllem4  25463  uniioombllem5  25464  eff1olem  26433  birthdaylem1  26837  zssno  28245  nvss  30495  lediri  31439  lejdiri  31441  sshhococi  31448  mayetes3i  31631  disjxpin  32490  imadifxp  32503  constrextdg2  33712  sxbrsigalem5  34252  eulerpartlemmf  34339  kur14lem6  35171  cvmlift2lem12  35274  bj-xpcossxp  37150  bj-rrhatsscchat  37197  mblfinlem4  37627  lclkrs2  41507  areaquad  43178  corclrcl  43669  corcltrcl  43701  relopabVD  44863  ovolval5lem3  46625  uspgrlimlem4  47963  setc1onsubc  49564