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

Metamath Proof Explorer

Theorem mofmo

Description: There is at most one function into a class containing at most one element. (Contributed by Zhi Wang, 19-Sep-2024)

Ref Expression
Assertion mofmo ⊢ ∃* x x ∈ B → ∃* f f : A ⟶ B

Proof

Step Hyp Ref Expression
1 mo0sn ⊢ ∃* x x ∈ B ↔ B = ∅ ∨ ∃ y B = y
2 mof02 ⊢ B = ∅ → ∃* f f : A ⟶ B
3 mofsn2 ⊢ B = y → ∃* f f : A ⟶ B
4 3 exlimiv ⊢ ∃ y B = y → ∃* f f : A ⟶ B
5 2 4 jaoi ⊢ B = ∅ ∨ ∃ y B = y → ∃* f f : A ⟶ B
6 1 5 sylbi ⊢ ∃* x x ∈ B → ∃* f f : A ⟶ B