Theorem 3sstr4i 3543

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

Syntax hints:   = wceq 1379   C_ wss 3476

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-in 3483  df-ss 3490

This theorem is referenced by:  brab2a  5048  rncoss  5261  imassrn  5346  rnin  5413  inimass  5420  ssoprab2i  6373  omopthlem2  7302  rankval4  8281  cardf2  8320  r0weon  8386  dcomex  8823  axdc2lem  8824  fpwwe2lem1  9005  canthwe  9025  recmulnq  9338  npex  9360  axresscn  9521  odlem1  16352  gexlem1  16392  psrbagsn  17928  bwth  19673  2ndcctbss  19719  uniioombllem4  21727  uniioombllem5  21728  eff1olem  22665  birthdaylem1  23006  nvss  25159  lediri  26128  lejdiri  26130  sshhococi  26137  mayetes3i  26321  disjxpin  27117  imadifxp  27128  sxbrsigalem5  27896  eulerpartlemmf  27951  kur14lem6  28292  cvmlift2lem12  28396  bpoly4  29395  mblfinlem4  29629  areaquad  30789  relopabVD  32781  bj-rrhatsscchat  33711  lclkrs2  36337  trclubg  36795