Theorem 3sstr4i 4039

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.1	. 2 ⊢ 𝐴 ⊆ 𝐵
2		3sstr4.2	. . 3 ⊢ 𝐶 = 𝐴
3		3sstr4.3	. . 3 ⊢ 𝐷 = 𝐵
4	2, 3	sseq12i 4026	. 2 ⊢ (𝐶 ⊆ 𝐷 ↔ 𝐴 ⊆ 𝐵)
5	1, 4	mpbir 231	1 ⊢ 𝐶 ⊆ 𝐷

Syntax hints:   = wceq 1537   ⊆ wss 3963

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-cleq 2727  df-ss 3980

This theorem is referenced by:  relopabiv  5833  rncoss  5989  imassrn  6091  rnin  6169  inimass  6177  f1ossf1o  7148  ssoprab2i  7544  omopthlem2  8697  1sdom2dom  9281  rankval4  9905  cardf2  9981  r0weon  10050  dcomex  10485  axdc2lem  10486  fpwwe2lem1  10669  canthwe  10689  recmulnq  11002  npex  11024  axresscn  11186  mpoaddf  11247  mpomulf  11248  trclublem  15031  bpoly4  16092  2strop1  17273  odlem1  19568  gexlem1  19612  pzriprnglem4  21513  psrbagsn  22105  bwth  23434  2ndcctbss  23479  uniioombllem4  25635  uniioombllem5  25636  eff1olem  26605  birthdaylem1  27009  zssno  28382  nvss  30622  lediri  31566  lejdiri  31568  sshhococi  31575  mayetes3i  31758  disjxpin  32608  imadifxp  32621  sxbrsigalem5  34270  eulerpartlemmf  34357  kur14lem6  35196  cvmlift2lem12  35299  bj-xpcossxp  37172  bj-rrhatsscchat  37219  mblfinlem4  37647  lclkrs2  41523  areaquad  43205  corclrcl  43697  corcltrcl  43729  relopabVD  44899  ovolval5lem3  46610  uspgrlimlem4  47894