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

Metamath Proof Explorer

Theorem f10d

Description: The empty set maps one-to-one into any class, deduction version. (Contributed by AV, 25-Nov-2020)

Ref Expression
Hypothesis f10d.f ⊢ φ → F = ∅
Assertion f10d ⊢ φ → F : dom ⁡ F ⟶ 1-1 A

Proof

Step Hyp Ref Expression
1 f10d.f ⊢ φ → F = ∅
2 f10 ⊢ ∅ : ∅ ⟶ 1-1 A
3 dm0 ⊢ dom ⁡ ∅ = ∅
4 f1eq2 ⊢ dom ⁡ ∅ = ∅ → ∅ : dom ⁡ ∅ ⟶ 1-1 A ↔ ∅ : ∅ ⟶ 1-1 A
5 3 4 ax-mp ⊢ ∅ : dom ⁡ ∅ ⟶ 1-1 A ↔ ∅ : ∅ ⟶ 1-1 A
6 2 5 mpbir ⊢ ∅ : dom ⁡ ∅ ⟶ 1-1 A
7 1 dmeqd ⊢ φ → dom ⁡ F = dom ⁡ ∅
8 eqidd ⊢ φ → A = A
9 1 7 8 f1eq123d ⊢ φ → F : dom ⁡ F ⟶ 1-1 A ↔ ∅ : dom ⁡ ∅ ⟶ 1-1 A
10 6 9 mpbiri ⊢ φ → F : dom ⁡ F ⟶ 1-1 A