Theorem 3sstr4i 3959

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

This proof depends on syntax axioms:   = wceq 1569   ⊆ wss 3895

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-ss 3896

This theorem is used by:  relopabiv  5797  rncoss  5958  imassrnOLD  6068  rninOLD  6137  inimass  6144  f1ossf1o  7129  ssoprab2i  7531  omopthlem2  8669  enssdom  9003  1sdom2dom  9245  rankval4  9884  cardf2  10024  r0weon  10091  dcomex  10525  axdc2lem  10526  fpwwe2lem1  10716  canthwe  10736  recmulnq  11049  npex  11071  axresscn  11233  mpoaddf  11294  mpomulf  11295  trclublem  15148  bpoly4  16225  2strop  17407  odlem1  19749  gexlem1  19793  pzriprnglem4  21790  psrbagsn  22372  bwth  23728  2ndcctbss  23774  uniioombllem4  25907  uniioombllem5  25908  eff1olem  26876  birthdaylem1  27279  zssno  28767  nvss  31195  lediri  32139  lejdiri  32141  sshhococi  32148  mayetes3i  32331  disjxpin  33182  imadifxp  33195  constrextdg2  34381  sxbrsigalem5  34920  eulerpartlemmf  35007  kur14lem6  35976  cvmlift2lem12  36079  bj-xpcossxp  38111  bj-rrhatsscchat  38158  mblfinlem4  38579  lclkrs2  42598  areaquad  44218  corclrcl  44707  corcltrcl  44739  relopabVD  45883  ovolval5lem3  47664  uspgrlimlem4  49089  setc1onsubc  50710