Theorem 3sstr4i 3966

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

Syntax hints:   = wceq 1547   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731  df-ss 3900

This theorem is referenced by:  relopabiv  5763  rncoss  5919  imassrn  6023  rnin  6097  inimass  6106  f1ossf1o  7070  ssoprab2i  7467  omopthlem2  8586  enssdom  8913  1sdom2dom  9154  rankval4  9782  cardf2  9858  r0weon  9925  dcomex  10360  axdc2lem  10361  fpwwe2lem1  10545  canthwe  10565  recmulnq  10878  npex  10900  axresscn  11062  mpoaddf  11123  mpomulf  11124  trclublem  14948  bpoly4  16015  2strop  17190  odlem1  19501  gexlem1  19545  pzriprnglem4  21459  psrbagsn  22039  bwth  23393  2ndcctbss  23438  uniioombllem4  25571  uniioombllem5  25572  eff1olem  26530  birthdaylem1  26933  zssno  28391  nvss  30682  lediri  31626  lejdiri  31628  sshhococi  31635  mayetes3i  31818  disjxpin  32677  imadifxp  32690  constrextdg2  33933  sxbrsigalem5  34472  eulerpartlemmf  34559  kur14lem6  35439  cvmlift2lem12  35542  bj-xpcossxp  37549  bj-rrhatsscchat  37596  mblfinlem4  38027  lclkrs2  42032  areaquad  43661  corclrcl  44151  corcltrcl  44183  relopabVD  45344  ovolval5lem3  47097  uspgrlimlem4  48482  setc1onsubc  50092