Description: The empty function. (Contributed by NM, 14-Aug-1999)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | f0 | |- (/) : (/) --> A |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eqid | |- (/) = (/) |
|
| 2 | fn0 | |- ( (/) Fn (/) <-> (/) = (/) ) |
|
| 3 | 1 2 | mpbir | |- (/) Fn (/) |
| 4 | rn0 | |- ran (/) = (/) |
|
| 5 | 0ss | |- (/) C_ A |
|
| 6 | 4 5 | eqsstri | |- ran (/) C_ A |
| 7 | df-f | |- ( (/) : (/) --> A <-> ( (/) Fn (/) /\ ran (/) C_ A ) ) |
|
| 8 | 3 6 7 | mpbir2an | |- (/) : (/) --> A |