Description: A singleton of an ordered pair is one-to-one onto function. (Contributed by NM, 18-May-1998) (Proof shortened by Andrew Salmon, 22-Oct-2011)
Ref | Expression | ||
---|---|---|---|
Hypotheses | f1osn.1 | |
|
f1osn.2 | |
||
Assertion | f1osn | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | f1osn.1 | |
|
2 | f1osn.2 | |
|
3 | 1 2 | fnsn | |
4 | 2 1 | fnsn | |
5 | 1 2 | cnvsn | |
6 | 5 | fneq1i | |
7 | 4 6 | mpbir | |
8 | dff1o4 | |
|
9 | 3 7 8 | mpbir2an | |