Theorem 3sstr4i 3973

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

Syntax hints:   = wceq 1542   ⊆ wss 3889

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728  df-ss 3906

This theorem is referenced by:  relopabiv  5776  rncoss  5932  imassrn  6036  rnin  6110  inimass  6119  f1ossf1o  7081  ssoprab2i  7478  omopthlem2  8596  enssdom  8923  1sdom2dom  9164  rankval4  9791  cardf2  9867  r0weon  9934  dcomex  10369  axdc2lem  10370  fpwwe2lem1  10554  canthwe  10574  recmulnq  10887  npex  10909  axresscn  11071  mpoaddf  11132  mpomulf  11133  trclublem  14957  bpoly4  16024  2strop  17199  odlem1  19510  gexlem1  19554  pzriprnglem4  21464  psrbagsn  22041  bwth  23375  2ndcctbss  23420  uniioombllem4  25553  uniioombllem5  25554  eff1olem  26512  birthdaylem1  26915  zssno  28373  nvss  30664  lediri  31608  lejdiri  31610  sshhococi  31617  mayetes3i  31800  disjxpin  32658  imadifxp  32671  constrextdg2  33893  sxbrsigalem5  34432  eulerpartlemmf  34519  kur14lem6  35393  cvmlift2lem12  35496  bj-xpcossxp  37503  bj-rrhatsscchat  37550  mblfinlem4  37981  lclkrs2  41986  areaquad  43644  corclrcl  44134  corcltrcl  44166  relopabVD  45327  ovolval5lem3  47082  uspgrlimlem4  48467  setc1onsubc  50077