Theorem 3sstr4i 3506

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 3493	. 2 |- ( C C_ D <-> A C_ B )
5	1, 4	mpbir 209	1 |- C C_ D

Syntax hints:   = wceq 1370   C_ wss 3439

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-in 3446  df-ss 3453

This theorem is referenced by:  brab2a  4999  rncoss  5211  imassrn  5291  rnin  5357  inimass  5364  ssoprab2i  6292  omopthlem2  7208  rankval4  8188  cardf2  8227  r0weon  8293  dcomex  8730  axdc2lem  8731  fpwwe2lem1  8912  canthwe  8932  recmulnq  9247  npex  9269  axresscn  9429  odlem1  16162  gexlem1  16202  psrbagsn  17704  bwth  19148  2ndcctbss  19194  uniioombllem4  21202  uniioombllem5  21203  eff1olem  22140  birthdaylem1  22481  nvss  24143  lediri  25112  lejdiri  25114  sshhococi  25121  mayetes3i  25305  disjxpin  26101  imadifxp  26110  sxbrsigalem5  26867  eulerpartlemmf  26922  kur14lem6  27263  cvmlift2lem12  27367  bpoly4  28366  mblfinlem4  28599  areaquad  29760  relopabVD  31989  bj-rrhatsscchat  32917  lclkrs2  35543