Description: A set of two pairs is a function if their first members are different. (Contributed by FL, 26-Jun-2011) (Proof shortened by JJ, 14-Jul-2021)
Ref | Expression | ||
---|---|---|---|
Assertion | funprg | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | funsng | |
|
2 | funsng | |
|
3 | 1 2 | anim12i | |
4 | 3 | an4s | |
5 | 4 | 3adant3 | |
6 | dmsnopg | |
|
7 | dmsnopg | |
|
8 | 6 7 | ineqan12d | |
9 | disjsn2 | |
|
10 | 8 9 | sylan9eq | |
11 | 10 | 3adant1 | |
12 | funun | |
|
13 | 5 11 12 | syl2anc | |
14 | df-pr | |
|
15 | 14 | funeqi | |
16 | 13 15 | sylibr | |