Theorem 3sstr4i 3503

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

Syntax hints:   = wceq 1437   C_ wss 3436

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401

This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-in 3443  df-ss 3450

This theorem is referenced by:  brab2a  4903  rncoss  5114  imassrn  5198  rnin  5264  inimass  5271  ssoprab2i  6400  omopthlem2  7369  rankval4  8347  cardf2  8386  r0weon  8452  dcomex  8885  axdc2lem  8886  fpwwe2lem1  9064  canthwe  9084  recmulnq  9397  npex  9419  axresscn  9580  trclublem  13060  bpoly4  14112  2strop1  15235  odlem1  17181  odlem1OLD  17184  gexlem1  17228  gexlem1OLD  17230  psrbagsn  18718  bwth  20424  2ndcctbss  20469  uniioombllem4  22543  uniioombllem5  22544  eff1olem  23496  birthdaylem1  23876  nvss  26211  lediri  27189  lejdiri  27191  sshhococi  27198  mayetes3i  27381  disjxpin  28201  imadifxp  28215  sxbrsigalem5  29119  eulerpartlemmf  29217  kur14lem6  29943  cvmlift2lem12  30046  bj-rrhatsscchat  31643  mblfinlem4  31945  lclkrs2  35078  areaquad  36072  corclrcl  36270  corcltrcl  36302  relopabVD  37272