theorem funcss3 (A B C F: set): $ B C_ C -> func F A B -> func F A C $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sstr | Ran F C_ B -> B C_ C -> Ran F C_ C |
|
2 | 1 | com12 | B C_ C -> Ran F C_ B -> Ran F C_ C |
3 | 2 | anim2d | B C_ C -> isfun F /\ Dom F == A /\ Ran F C_ B -> isfun F /\ Dom F == A /\ Ran F C_ C |
4 | 3 | conv func | B C_ C -> func F A B -> func F A C |