Theorem 3sstr4i 4020

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 4007	. 2 ⊢ (𝐶 ⊆ 𝐷 ↔ 𝐴 ⊆ 𝐵)
5	1, 4	mpbir 230	1 ⊢ 𝐶 ⊆ 𝐷

Syntax hints:   = wceq 1533   ⊆ wss 3943

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2704  df-cleq 2718  df-clel 2804  df-v 3470  df-in 3950  df-ss 3960

This theorem is referenced by:  relopabiv  5813  rncoss  5964  imassrn  6063  rnin  6139  inimass  6147  f1ossf1o  7121  ssoprab2i  7514  omopthlem2  8658  1sdom2dom  9246  rankval4  9861  cardf2  9937  r0weon  10006  dcomex  10441  axdc2lem  10442  fpwwe2lem1  10625  canthwe  10645  recmulnq  10958  npex  10980  axresscn  11142  mpoaddf  11203  mpomulf  11204  trclublem  14945  bpoly4  16006  2strop1  17178  odlem1  19452  gexlem1  19496  pzriprnglem4  21366  psrbagsn  21961  bwth  23264  2ndcctbss  23309  uniioombllem4  25465  uniioombllem5  25466  eff1olem  26432  birthdaylem1  26833  nvss  30350  lediri  31294  lejdiri  31296  sshhococi  31303  mayetes3i  31486  disjxpin  32323  imadifxp  32336  sxbrsigalem5  33816  eulerpartlemmf  33903  kur14lem6  34729  cvmlift2lem12  34832  bj-xpcossxp  36576  bj-rrhatsscchat  36623  mblfinlem4  37040  lclkrs2  40923  areaquad  42523  corclrcl  43016  corcltrcl  43048  relopabVD  44220  ovolval5lem3  45924