Theorem 3sstr4i 3964

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

This proof depends on syntax axioms:   = wceq 1570   ⊆ wss 3900

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-ss 3901

This theorem is used by:  relopabiv  5807  relopabi  5809  rncoss  5971  imassrnOLD  6087  rninOLD  6156  inimass  6163  f1ossf1o  7161  ssoprab2i  7562  onprcr  7825  omopthlem2  8707  enssdom  9041  1sdom2dom  9283  rankval4  9921  cardf2  10061  r0weon  10130  dcomex  10564  axdc2lem  10565  fpwwe2lem1  10755  canthwe  10775  recmulnq  11088  npex  11110  axresscn  11272  mpoaddf  11333  mpomulf  11334  trclublem  15191  bpoly4  16269  2strop  17451  odlem1  19800  gexlem1  19844  pzriprnglem4  21845  psrbagsn  22427  bwth  23783  2ndcctbss  23829  uniioombllem4  25962  uniioombllem5  25963  eff1olem  26933  birthdaylem1  27336  zssno  28824  nvss  31252  lediri  32196  lejdiri  32198  sshhococi  32205  mayetes3i  32388  disjxpin  33280  imadifxp  33293  constrextdg2  34492  sxbrsigalem5  35031  eulerpartlemmf  35118  kur14lem6  36184  cvmlift2lem12  36287  bj-xpcossxp  38378  bj-rrhatsscchat  38425  mblfinlem4  38846  lclkrs2  42863  areaquad  44479  corclrcl  44968  corcltrcl  45000  relopabVD  46143  ovolval5lem3  47937  uspgrlimlem4  49362  setc1onsubc  51071