Description: The singleton relationship is a function over the universe. (Contributed by Scott Fenton, 4-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | fnsingle | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | difss | |
|
2 | df-rel | |
|
3 | 1 2 | mpbir | |
4 | df-singleton | |
|
5 | 4 | releqi | |
6 | 3 5 | mpbir | |
7 | vex | |
|
8 | vex | |
|
9 | 7 8 | brsingle | |
10 | vex | |
|
11 | 7 10 | brsingle | |
12 | eqtr3 | |
|
13 | 9 11 12 | syl2anb | |
14 | 13 | ax-gen | |
15 | 14 | gen2 | |
16 | dffun2 | |
|
17 | 6 15 16 | mpbir2an | |
18 | eqv | |
|
19 | eqid | |
|
20 | snex | |
|
21 | 7 20 | brsingle | |
22 | 19 21 | mpbir | |
23 | breq2 | |
|
24 | 20 23 | spcev | |
25 | 22 24 | ax-mp | |
26 | 7 | eldm | |
27 | 25 26 | mpbir | |
28 | 18 27 | mpgbir | |
29 | df-fn | |
|
30 | 17 28 29 | mpbir2an | |