Theorem 3sstr4i 3538

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	|- A C_ B
3sstr4.2	|- C = A
3sstr4.3	|- D = B

Assertion

Ref	Expression
3sstr4i	|- C C_ D

Proof of Theorem 3sstr4i

Step	Hyp	Ref	Expression
1		3sstr4.1	. 2 |- A C_ B
2		3sstr4.2	. . 3 |- C = A
3		3sstr4.3	. . 3 |- D = B
4	2, 3	sseq12i 3525	. 2 |- ( C C_ D <-> A C_ B )
5	1, 4	mpbir 209	1 |- C C_ D

Syntax hints:   = wceq 1395   C_ wss 3471

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-in 3478  df-ss 3485

This theorem is referenced by:  brab2a  5058  rncoss  5273  imassrn  5358  rnin  5422  inimass  5429  ssoprab2i  6390  omopthlem2  7323  rankval4  8302  cardf2  8341  r0weon  8407  dcomex  8844  axdc2lem  8845  fpwwe2lem1  9026  canthwe  9046  recmulnq  9359  npex  9381  axresscn  9542  odlem1  16685  gexlem1  16725  psrbagsn  18286  bwth  20036  2ndcctbss  20081  uniioombllem4  22120  uniioombllem5  22121  eff1olem  23060  birthdaylem1  23406  nvss  25612  lediri  26581  lejdiri  26583  sshhococi  26590  mayetes3i  26774  disjxpin  27584  imadifxp  27595  sxbrsigalem5  28420  eulerpartlemmf  28489  kur14lem6  28830  cvmlift2lem12  28934  bpoly4  29983  mblfinlem4  30216  areaquad  31346  relopabVD  33802  bj-rrhatsscchat  34740  lclkrs2  37368  trclubg  37886