Theorem 3sstr4i 3960

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

Syntax hints:   = wceq 1539   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900

This theorem is referenced by:  relopabiv  5719  rncoss  5870  imassrn  5969  rnin  6039  inimass  6047  f1ossf1o  6982  ssoprab2i  7363  omopthlem2  8450  rankval4  9556  cardf2  9632  r0weon  9699  dcomex  10134  axdc2lem  10135  fpwwe2lem1  10318  canthwe  10338  recmulnq  10651  npex  10673  axresscn  10835  trclublem  14634  bpoly4  15697  2strop1  16866  odlem1  19058  gexlem1  19099  psrbagsn  21181  bwth  22469  2ndcctbss  22514  uniioombllem4  24655  uniioombllem5  24656  eff1olem  25609  birthdaylem1  26006  nvss  28856  lediri  29800  lejdiri  29802  sshhococi  29809  mayetes3i  29992  disjxpin  30828  imadifxp  30841  sxbrsigalem5  32155  eulerpartlemmf  32242  kur14lem6  33073  cvmlift2lem12  33176  bj-xpcossxp  35287  bj-rrhatsscchat  35334  mblfinlem4  35744  lclkrs2  39481  areaquad  40963  corclrcl  41204  corcltrcl  41236  relopabVD  42410