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 1560   ⊆ wss 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-cleq 2754  df-ss 3921

This theorem is referenced by:  relopabiv  5793  rncoss  5953  imassrn  6060  rninOLD  6131  inimass  6140  f1ossf1o  7110  ssoprab2i  7507  omopthlem2  8630  enssdom  8957  1sdom2dom  9198  rankval4  9825  cardf2  9901  r0weon  9968  dcomex  10404  axdc2lem  10405  fpwwe2lem1  10589  canthwe  10609  recmulnq  10922  npex  10944  axresscn  11106  mpoaddf  11167  mpomulf  11168  trclublem  15008  bpoly4  16089  2strop  17265  odlem1  19575  gexlem1  19619  pzriprnglem4  21533  psrbagsn  22113  bwth  23467  2ndcctbss  23512  uniioombllem4  25645  uniioombllem5  25646  eff1olem  26610  birthdaylem1  27013  zssno  28471  nvss  30793  lediri  31737  lejdiri  31739  sshhococi  31746  mayetes3i  31929  disjxpin  32785  imadifxp  32798  constrextdg2  34043  sxbrsigalem5  34582  eulerpartlemmf  34669  kur14lem6  35558  cvmlift2lem12  35661  bj-xpcossxp  37678  bj-rrhatsscchat  37725  mblfinlem4  38156  lclkrs2  42161  areaquad  43790  corclrcl  44280  corcltrcl  44312  relopabVD  45473  ovolval5lem3  47225  uspgrlimlem4  48610  setc1onsubc  50220