Theorem 3sstr4i 4035

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

Syntax hints:   = wceq 1540   ⊆ wss 3951

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-ss 3968

This theorem is referenced by:  relopabiv  5830  rncoss  5986  imassrn  6089  rnin  6166  inimass  6175  f1ossf1o  7148  ssoprab2i  7544  omopthlem2  8698  1sdom2dom  9283  rankval4  9907  cardf2  9983  r0weon  10052  dcomex  10487  axdc2lem  10488  fpwwe2lem1  10671  canthwe  10691  recmulnq  11004  npex  11026  axresscn  11188  mpoaddf  11249  mpomulf  11250  trclublem  15034  bpoly4  16095  2strop1  17273  odlem1  19553  gexlem1  19597  pzriprnglem4  21495  psrbagsn  22087  bwth  23418  2ndcctbss  23463  uniioombllem4  25621  uniioombllem5  25622  eff1olem  26590  birthdaylem1  26994  zssno  28367  nvss  30612  lediri  31556  lejdiri  31558  sshhococi  31565  mayetes3i  31748  disjxpin  32601  imadifxp  32614  constrextdg2  33790  sxbrsigalem5  34290  eulerpartlemmf  34377  kur14lem6  35216  cvmlift2lem12  35319  bj-xpcossxp  37190  bj-rrhatsscchat  37237  mblfinlem4  37667  lclkrs2  41542  areaquad  43228  corclrcl  43720  corcltrcl  43752  relopabVD  44921  ovolval5lem3  46669  uspgrlimlem4  47958