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