Theorem 3sstr4i 4052

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

Syntax hints:   = wceq 1537   ⊆ wss 3976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-ss 3993

This theorem is referenced by:  relopabiv  5844  rncoss  5998  imassrn  6100  rnin  6178  inimass  6186  f1ossf1o  7162  ssoprab2i  7561  omopthlem2  8716  1sdom2dom  9310  rankval4  9936  cardf2  10012  r0weon  10081  dcomex  10516  axdc2lem  10517  fpwwe2lem1  10700  canthwe  10720  recmulnq  11033  npex  11055  axresscn  11217  mpoaddf  11278  mpomulf  11279  trclublem  15044  bpoly4  16107  2strop1  17286  odlem1  19577  gexlem1  19621  pzriprnglem4  21518  psrbagsn  22110  bwth  23439  2ndcctbss  23484  uniioombllem4  25640  uniioombllem5  25641  eff1olem  26608  birthdaylem1  27012  zssno  28385  nvss  30625  lediri  31569  lejdiri  31571  sshhococi  31578  mayetes3i  31761  disjxpin  32610  imadifxp  32623  sxbrsigalem5  34253  eulerpartlemmf  34340  kur14lem6  35179  cvmlift2lem12  35282  bj-xpcossxp  37155  bj-rrhatsscchat  37202  mblfinlem4  37620  lclkrs2  41497  areaquad  43177  corclrcl  43669  corcltrcl  43701  relopabVD  44872  ovolval5lem3  46575  uspgrlimlem4  47815