Theorem 3sstr4i 4017

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

Syntax hints:   = wceq 1533   ⊆ wss 3940

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 2695

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-v 3468  df-in 3947  df-ss 3957

This theorem is referenced by:  relopabiv  5810  rncoss  5961  imassrn  6060  rnin  6136  inimass  6144  f1ossf1o  7118  ssoprab2i  7511  omopthlem2  8654  1sdom2dom  9242  rankval4  9857  cardf2  9933  r0weon  10002  dcomex  10437  axdc2lem  10438  fpwwe2lem1  10621  canthwe  10641  recmulnq  10954  npex  10976  axresscn  11138  mpomulf  11199  trclublem  14938  bpoly4  15999  2strop1  17168  odlem1  19440  gexlem1  19484  pzriprnglem4  21334  psrbagsn  21925  bwth  23224  2ndcctbss  23269  uniioombllem4  25425  uniioombllem5  25426  eff1olem  26387  birthdaylem1  26787  nvss  30270  lediri  31214  lejdiri  31216  sshhococi  31223  mayetes3i  31406  disjxpin  32243  imadifxp  32256  sxbrsigalem5  33742  eulerpartlemmf  33829  kur14lem6  34657  cvmlift2lem12  34760  mpoaddf  35624  bj-xpcossxp  36526  bj-rrhatsscchat  36573  mblfinlem4  36984  lclkrs2  40867  areaquad  42420  corclrcl  42913  corcltrcl  42945  relopabVD  44117  ovolval5lem3  45821