Theorem 3sstr4i 4022

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

Syntax hints:   = wceq 1534   ⊆ wss 3946

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775  df-cleq 2718  df-ss 3963

This theorem is referenced by:  relopabiv  5818  rncoss  5971  imassrn  6072  rnin  6150  inimass  6158  f1ossf1o  7134  ssoprab2i  7528  omopthlem2  8682  1sdom2dom  9274  rankval4  9903  cardf2  9979  r0weon  10048  dcomex  10481  axdc2lem  10482  fpwwe2lem1  10665  canthwe  10685  recmulnq  10998  npex  11020  axresscn  11182  mpoaddf  11243  mpomulf  11244  trclublem  14995  bpoly4  16056  2strop1  17236  odlem1  19529  gexlem1  19573  pzriprnglem4  21470  psrbagsn  22072  bwth  23402  2ndcctbss  23447  uniioombllem4  25603  uniioombllem5  25604  eff1olem  26572  birthdaylem1  26976  zssno  28328  nvss  30523  lediri  31467  lejdiri  31469  sshhococi  31476  mayetes3i  31659  disjxpin  32508  imadifxp  32521  sxbrsigalem5  34135  eulerpartlemmf  34222  kur14lem6  35052  cvmlift2lem12  35155  bj-xpcossxp  36909  bj-rrhatsscchat  36956  mblfinlem4  37374  lclkrs2  41252  areaquad  42918  corclrcl  43411  corcltrcl  43443  relopabVD  44614  ovolval5lem3  46311