Description: Substitution of equality into both sides of a subclass relationship. (Contributed by NM, 30-Nov-1995) (Proof shortened by Eric Schmidt, 26-Jan-2007)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | 3sstr4d.1 | |- ( ph -> A C_ B ) |
|
| 3sstr4d.2 | |- ( ph -> C = A ) |
||
| 3sstr4d.3 | |- ( ph -> D = B ) |
||
| Assertion | 3sstr4d | |- ( ph -> C C_ D ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 3sstr4d.1 | |- ( ph -> A C_ B ) |
|
| 2 | 3sstr4d.2 | |- ( ph -> C = A ) |
|
| 3 | 3sstr4d.3 | |- ( ph -> D = B ) |
|
| 4 | 2 3 | sseq12d | |- ( ph -> ( C C_ D <-> A C_ B ) ) |
| 5 | 1 4 | mpbird | |- ( ph -> C C_ D ) |