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 1542   ⊆ wss 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

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

This theorem is referenced by:  relopabiv  5777  rncoss  5934  imassrn  6038  rnin  6112  inimass  6121  f1ossf1o  7083  ssoprab2i  7479  omopthlem2  8598  enssdom  8925  1sdom2dom  9166  rankval4  9791  cardf2  9867  r0weon  9934  dcomex  10369  axdc2lem  10370  fpwwe2lem1  10554  canthwe  10574  recmulnq  10887  npex  10909  axresscn  11071  mpoaddf  11132  mpomulf  11133  trclublem  14930  bpoly4  15994  2strop  17168  odlem1  19476  gexlem1  19520  pzriprnglem4  21451  psrbagsn  22030  bwth  23366  2ndcctbss  23411  uniioombllem4  25555  uniioombllem5  25556  eff1olem  26525  birthdaylem1  26929  zssno  28389  nvss  30681  lediri  31625  lejdiri  31627  sshhococi  31634  mayetes3i  31817  disjxpin  32675  imadifxp  32688  constrextdg2  33927  sxbrsigalem5  34466  eulerpartlemmf  34553  kur14lem6  35427  cvmlift2lem12  35530  bj-xpcossxp  37444  bj-rrhatsscchat  37491  mblfinlem4  37911  lclkrs2  41916  areaquad  43573  corclrcl  44063  corcltrcl  44095  relopabVD  45256  ovolval5lem3  47012  uspgrlimlem4  48351  setc1onsubc  49961