Theorem 3sstr4i 3974

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

Syntax hints:   = wceq 1542   ⊆ wss 3890

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 3907

This theorem is referenced by:  relopabiv  5770  rncoss  5927  imassrn  6031  rnin  6105  inimass  6114  f1ossf1o  7076  ssoprab2i  7472  omopthlem2  8590  enssdom  8917  1sdom2dom  9158  rankval4  9785  cardf2  9861  r0weon  9928  dcomex  10363  axdc2lem  10364  fpwwe2lem1  10548  canthwe  10568  recmulnq  10881  npex  10903  axresscn  11065  mpoaddf  11126  mpomulf  11127  trclublem  14951  bpoly4  16018  2strop  17193  odlem1  19504  gexlem1  19548  pzriprnglem4  21477  psrbagsn  22054  bwth  23388  2ndcctbss  23433  uniioombllem4  25566  uniioombllem5  25567  eff1olem  26528  birthdaylem1  26931  zssno  28390  nvss  30682  lediri  31626  lejdiri  31628  sshhococi  31635  mayetes3i  31818  disjxpin  32676  imadifxp  32689  constrextdg2  33912  sxbrsigalem5  34451  eulerpartlemmf  34538  kur14lem6  35412  cvmlift2lem12  35515  bj-xpcossxp  37522  bj-rrhatsscchat  37569  mblfinlem4  37998  lclkrs2  42003  areaquad  43665  corclrcl  44155  corcltrcl  44187  relopabVD  45348  ovolval5lem3  47103  uspgrlimlem4  48482  setc1onsubc  50092