Theorem 3sstr4i 3996

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

Syntax hints:   = wceq 1567   ⊆ wss 3913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-ss 3930

This theorem is referenced by:  relopabiv  5808  rncoss  5968  imassrn  6074  rninOLD  6145  inimass  6153  f1ossf1o  7125  ssoprab2i  7522  omopthlem2  8645  enssdom  8972  1sdom2dom  9213  rankval4  9838  cardf2  9928  r0weon  9995  dcomex  10430  axdc2lem  10431  fpwwe2lem1  10615  canthwe  10635  recmulnq  10948  npex  10970  axresscn  11132  mpoaddf  11193  mpomulf  11194  trclublem  15031  bpoly4  16112  2strop  17288  odlem1  19604  gexlem1  19648  pzriprnglem4  21602  psrbagsn  22182  bwth  23535  2ndcctbss  23580  uniioombllem4  25713  uniioombllem5  25714  eff1olem  26678  birthdaylem1  27081  zssno  28539  nvss  30885  lediri  31829  lejdiri  31831  sshhococi  31838  mayetes3i  32021  disjxpin  32873  imadifxp  32886  constrextdg2  34083  sxbrsigalem5  34622  eulerpartlemmf  34709  kur14lem6  35601  cvmlift2lem12  35704  bj-xpcossxp  37720  bj-rrhatsscchat  37767  mblfinlem4  38198  lclkrs2  42203  areaquad  43834  corclrcl  44324  corcltrcl  44356  relopabVD  45500  ovolval5lem3  47259  uspgrlimlem4  48644  setc1onsubc  50264