Theorem 3sstr4i 4026

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

Syntax hints:   = wceq 1542   ⊆ wss 3949

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966

This theorem is referenced by:  relopabiv  5821  rncoss  5972  imassrn  6071  rnin  6147  inimass  6155  f1ossf1o  7126  ssoprab2i  7519  omopthlem2  8659  1sdom2dom  9247  rankval4  9862  cardf2  9938  r0weon  10007  dcomex  10442  axdc2lem  10443  fpwwe2lem1  10626  canthwe  10646  recmulnq  10959  npex  10981  axresscn  11143  trclublem  14942  bpoly4  16003  2strop1  17172  odlem1  19403  gexlem1  19447  psrbagsn  21624  bwth  22914  2ndcctbss  22959  uniioombllem4  25103  uniioombllem5  25104  eff1olem  26057  birthdaylem1  26456  nvss  29846  lediri  30790  lejdiri  30792  sshhococi  30799  mayetes3i  30982  disjxpin  31819  imadifxp  31832  sxbrsigalem5  33287  eulerpartlemmf  33374  kur14lem6  34202  cvmlift2lem12  34305  mpomulf  35159  bj-xpcossxp  36070  bj-rrhatsscchat  36117  mblfinlem4  36528  lclkrs2  40411  areaquad  41965  corclrcl  42458  corcltrcl  42490  relopabVD  43662  ovolval5lem3  45370  pzriprnglem4  46808