Theorem 3sstr4 2090

Description: Substitution of equality in both sides of a subclass relationship. (The proof was shortened by Eric Schmidt, 26-Jan-2007.)

Hypotheses

Ref	Expression
3sstr4.1	|- A (_ B
3sstr4.2	|- C = A
3sstr4.3	|- D = B

Assertion

Ref	Expression
3sstr4	|- C (_ D

Proof of Theorem 3sstr4

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

Syntax hints:   = wceq 953   (_ wss 2037

This theorem is referenced by:  dmcoss 3347  rncoss 3348  imassrn 3399  rnin 3444  ssoprab2i 3993  rankval4 4674  npex 5063  axresscn 5240  cncnplem1 7713  bcthlem12 7944  ipasslem7 8427  ledir 9375  lejdir 9377  sshhococ 9384  0alg 10533

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-12 965  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978  df-sb 1168  df-clab 1457  df-cleq 1462  df-clel 1465  df-in 2041  df-ss 2043

Copyright terms: Public domain