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

Metamath Proof Explorer

Theorem fnsnb

Description: A function whose domain is a singleton can be represented as a singleton of an ordered pair. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) Revised to add reverse implication. (Revised by NM, 29-Dec-2018) (Proof shortened by Zhi Wang, 21-Oct-2025)

Ref Expression
Hypothesis fnsnb.1 ⊢ A ∈ V
Assertion fnsnb ⊢ F Fn A ↔ F = A F ⁡ A

Proof

Step Hyp Ref Expression
1 fnsnb.1 ⊢ A ∈ V
2 fnsnbg ⊢ A ∈ V → F Fn A ↔ F = A F ⁡ A
3 1 2 ax-mp ⊢ F Fn A ↔ F = A F ⁡ A