Theorem 3sstr4 2096

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 2083	. 2 |- (C (_ D <-> A (_ B)
5	1, 4	mpbir 190	1 |- C (_ D

Syntax hints:   = wceq 954   (_ wss 2043

This theorem is referenced by:  dmcoss 3355  rncoss 3356  imassrn 3407  rnin 3450  ssoprab2i 3999  rankval4 4682  npex 5071  axresscn 5248  cncnplem1 7724  bcthlem12 7960  ipasslem7 8440  ledir 9398  lejdir 9400  sshhococ 9407  0alg 10569

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-in 2047  df-ss 2049

Copyright terms: Public domain