Theorem 3sstr4i 3981

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

Syntax hints:   = wceq 1541   ⊆ wss 3897

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 2121  ax-ext 2703

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

This theorem is referenced by:  relopabiv  5759  rncoss  5915  imassrn  6019  rnin  6093  inimass  6102  f1ossf1o  7061  ssoprab2i  7457  omopthlem2  8575  1sdom2dom  9138  rankval4  9760  cardf2  9836  r0weon  9903  dcomex  10338  axdc2lem  10339  fpwwe2lem1  10522  canthwe  10542  recmulnq  10855  npex  10877  axresscn  11039  mpoaddf  11100  mpomulf  11101  trclublem  14902  bpoly4  15966  2strop  17140  odlem1  19447  gexlem1  19491  pzriprnglem4  21421  psrbagsn  21998  bwth  23325  2ndcctbss  23370  uniioombllem4  25514  uniioombllem5  25515  eff1olem  26484  birthdaylem1  26888  zssno  28305  nvss  30573  lediri  31517  lejdiri  31519  sshhococi  31526  mayetes3i  31709  disjxpin  32568  imadifxp  32581  constrextdg2  33762  sxbrsigalem5  34301  eulerpartlemmf  34388  kur14lem6  35255  cvmlift2lem12  35358  bj-xpcossxp  37231  bj-rrhatsscchat  37278  mblfinlem4  37708  lclkrs2  41587  areaquad  43257  corclrcl  43748  corcltrcl  43780  relopabVD  44941  ovolval5lem3  46700  uspgrlimlem4  48030  setc1onsubc  49642