This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem f0

Description: The empty function. (Contributed by NM, 14-Aug-1999)

Ref Expression
Assertion f0 ⊢ ∅ : ∅ ⟶ A

Proof

Step Hyp Ref Expression
1 eqid ⊢ ∅ = ∅
2 fn0 ⊢ ∅ Fn ∅ ↔ ∅ = ∅
3 1 2 mpbir ⊢ ∅ Fn ∅
4 rn0 ⊢ ran ⁡ ∅ = ∅
5 0ss ⊢ ∅ ⊆ A
6 4 5 eqsstri ⊢ ran ⁡ ∅ ⊆ A
7 df-f ⊢ ∅ : ∅ ⟶ A ↔ ∅ Fn ∅ ∧ ran ⁡ ∅ ⊆ A
8 3 6 7 mpbir2an ⊢ ∅ : ∅ ⟶ A