Theorem 3sstr4i 3982

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

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

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 2155  ax-ext 2732

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

This theorem is used by:  relopabiv  5801  rncoss  5961  imassrn  6067  rninOLD  6138  inimass  6146  f1ossf1o  7122  ssoprab2i  7524  omopthlem2  8648  enssdom  8982  1sdom2dom  9224  rankval4  9849  cardf2  9948  r0weon  10015  dcomex  10449  axdc2lem  10450  fpwwe2lem1  10640  canthwe  10660  recmulnq  10973  npex  10995  axresscn  11157  mpoaddf  11218  mpomulf  11219  trclublem  15068  bpoly4  16145  2strop  17321  odlem1  19662  gexlem1  19706  pzriprnglem4  21697  psrbagsn  22279  bwth  23635  2ndcctbss  23681  uniioombllem4  25814  uniioombllem5  25815  eff1olem  26785  birthdaylem1  27188  zssno  28646  nvss  31074  lediri  32018  lejdiri  32020  sshhococi  32027  mayetes3i  32210  disjxpin  33061  imadifxp  33074  constrextdg2  34259  sxbrsigalem5  34799  eulerpartlemmf  34886  kur14lem6  35790  cvmlift2lem12  35893  bj-xpcossxp  37941  bj-rrhatsscchat  37988  mblfinlem4  38409  lclkrs2  42413  areaquad  44057  corclrcl  44547  corcltrcl  44579  relopabVD  45723  ovolval5lem3  47482  uspgrlimlem4  48907  setc1onsubc  50528