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)

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 fnsnr ⊢ F Fn A → x ∈ F → x = A F ⁡ A
3 df-fn ⊢ F Fn A ↔ Fun ⁡ F ∧ dom ⁡ F = A
4 1 snid ⊢ A ∈ A
5 eleq2 ⊢ dom ⁡ F = A → A ∈ dom ⁡ F ↔ A ∈ A
6 4 5 mpbiri ⊢ dom ⁡ F = A → A ∈ dom ⁡ F
7 6 anim2i ⊢ Fun ⁡ F ∧ dom ⁡ F = A → Fun ⁡ F ∧ A ∈ dom ⁡ F
8 3 7 sylbi ⊢ F Fn A → Fun ⁡ F ∧ A ∈ dom ⁡ F
9 funfvop ⊢ Fun ⁡ F ∧ A ∈ dom ⁡ F → A F ⁡ A ∈ F
10 8 9 syl ⊢ F Fn A → A F ⁡ A ∈ F
11 eleq1 ⊢ x = A F ⁡ A → x ∈ F ↔ A F ⁡ A ∈ F
12 10 11 syl5ibrcom ⊢ F Fn A → x = A F ⁡ A → x ∈ F
13 2 12 impbid ⊢ F Fn A → x ∈ F ↔ x = A F ⁡ A
14 velsn ⊢ x ∈ A F ⁡ A ↔ x = A F ⁡ A
15 13 14 bitr4di ⊢ F Fn A → x ∈ F ↔ x ∈ A F ⁡ A
16 15 eqrdv ⊢ F Fn A → F = A F ⁡ A
17 fvex ⊢ F ⁡ A ∈ V
18 1 17 fnsn ⊢ A F ⁡ A Fn A
19 fneq1 ⊢ F = A F ⁡ A → F Fn A ↔ A F ⁡ A Fn A
20 18 19 mpbiri ⊢ F = A F ⁡ A → F Fn A
21 16 20 impbii ⊢ F Fn A ↔ F = A F ⁡ A