Theorem 3sstr4i 3964

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

Syntax hints:   = wceq 1539   ⊆ wss 3887

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-in 3894  df-ss 3904

This theorem is referenced by:  relopabiv  5730  rncoss  5881  imassrn  5980  rnin  6050  inimass  6058  f1ossf1o  7000  ssoprab2i  7385  omopthlem2  8490  rankval4  9625  cardf2  9701  r0weon  9768  dcomex  10203  axdc2lem  10204  fpwwe2lem1  10387  canthwe  10407  recmulnq  10720  npex  10742  axresscn  10904  trclublem  14706  bpoly4  15769  2strop1  16940  odlem1  19143  gexlem1  19184  psrbagsn  21271  bwth  22561  2ndcctbss  22606  uniioombllem4  24750  uniioombllem5  24751  eff1olem  25704  birthdaylem1  26101  nvss  28955  lediri  29899  lejdiri  29901  sshhococi  29908  mayetes3i  30091  disjxpin  30927  imadifxp  30940  sxbrsigalem5  32255  eulerpartlemmf  32342  kur14lem6  33173  cvmlift2lem12  33276  bj-xpcossxp  35360  bj-rrhatsscchat  35407  mblfinlem4  35817  lclkrs2  39554  areaquad  41047  corclrcl  41315  corcltrcl  41347  relopabVD  42521