Theorem 3sstr4i 3457

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

Syntax hints:   = wceq 1452   C_ wss 3390

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451

This theorem depends on definitions:  df-bi 190  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-in 3397  df-ss 3404

This theorem is referenced by:  brab2a  4889  rncoss  5101  imassrn  5185  rnin  5251  inimass  5258  ssoprab2i  6404  omopthlem2  7375  rankval4  8356  cardf2  8395  r0weon  8461  dcomex  8895  axdc2lem  8896  fpwwe2lem1  9074  canthwe  9094  recmulnq  9407  npex  9429  axresscn  9590  trclublem  13134  bpoly4  14189  2strop1  15313  odlem1  17259  odlem1OLD  17262  gexlem1  17306  gexlem1OLD  17308  psrbagsn  18795  bwth  20502  2ndcctbss  20547  uniioombllem4  22623  uniioombllem5  22624  eff1olem  23576  birthdaylem1  23956  nvss  26293  lediri  27271  lejdiri  27273  sshhococi  27280  mayetes3i  27463  disjxpin  28275  imadifxp  28288  sxbrsigalem5  29183  eulerpartlemmf  29281  kur14lem6  30006  cvmlift2lem12  30109  bj-rrhatsscchat  31748  mblfinlem4  32044  lclkrs2  35179  areaquad  36172  corclrcl  36370  corcltrcl  36402  relopabVD  37361