Theorem 3sstr4i 3989

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

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

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 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2737

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

This theorem is used by:  relopabiv  5809  rncoss  5969  imassrn  6075  rninOLD  6146  inimass  6154  f1ossf1o  7128  ssoprab2i  7530  omopthlem2  8652  enssdom  8979  1sdom2dom  9221  rankval4  9846  cardf2  9945  r0weon  10012  dcomex  10446  axdc2lem  10447  fpwwe2lem1  10631  canthwe  10651  recmulnq  10964  npex  10986  axresscn  11148  mpoaddf  11209  mpomulf  11210  trclublem  15056  bpoly4  16135  2strop  17311  odlem1  19649  gexlem1  19693  pzriprnglem4  21684  psrbagsn  22264  bwth  23617  2ndcctbss  23663  uniioombllem4  25796  uniioombllem5  25797  eff1olem  26764  birthdaylem1  27167  zssno  28625  nvss  31016  lediri  31960  lejdiri  31962  sshhococi  31969  mayetes3i  32152  disjxpin  33004  imadifxp  33017  constrextdg2  34203  sxbrsigalem5  34743  eulerpartlemmf  34830  kur14lem6  35740  cvmlift2lem12  35843  bj-xpcossxp  37890  bj-rrhatsscchat  37937  mblfinlem4  38368  lclkrs2  42372  areaquad  44001  corclrcl  44491  corcltrcl  44523  relopabVD  45667  ovolval5lem3  47426  uspgrlimlem4  48814  setc1onsubc  50437