Theorem 3sstr4i 3998

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

Syntax hints:   = wceq 1540   ⊆ wss 3914

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ss 3931

This theorem is referenced by:  relopabiv  5783  rncoss  5939  imassrn  6042  rnin  6119  inimass  6128  f1ossf1o  7100  ssoprab2i  7500  omopthlem2  8624  1sdom2dom  9194  rankval4  9820  cardf2  9896  r0weon  9965  dcomex  10400  axdc2lem  10401  fpwwe2lem1  10584  canthwe  10604  recmulnq  10917  npex  10939  axresscn  11101  mpoaddf  11162  mpomulf  11163  trclublem  14961  bpoly4  16025  2strop  17199  odlem1  19465  gexlem1  19509  pzriprnglem4  21394  psrbagsn  21970  bwth  23297  2ndcctbss  23342  uniioombllem4  25487  uniioombllem5  25488  eff1olem  26457  birthdaylem1  26861  zssno  28269  nvss  30522  lediri  31466  lejdiri  31468  sshhococi  31475  mayetes3i  31658  disjxpin  32517  imadifxp  32530  constrextdg2  33739  sxbrsigalem5  34279  eulerpartlemmf  34366  kur14lem6  35198  cvmlift2lem12  35301  bj-xpcossxp  37177  bj-rrhatsscchat  37224  mblfinlem4  37654  lclkrs2  41534  areaquad  43205  corclrcl  43696  corcltrcl  43728  relopabVD  44890  ovolval5lem3  46652  uspgrlimlem4  47990  setc1onsubc  49591