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

Metamath Proof Explorer

Theorem fnsnbOLD

Description: Obsolete version of fnsnb as of 21-Oct-2025. 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 modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis fnsnb.1 
|- A e. _V
Assertion fnsnbOLD 
|- ( F Fn { A } <-> F = { <. A , ( F ` A ) >. } )

Proof

Step Hyp Ref Expression
1 fnsnb.1 
 |-  A e. _V
2 fnsnr 
 |-  ( F Fn { A } -> ( x e. F -> x = <. A , ( F ` A ) >. ) )
3 df-fn 
 |-  ( F Fn { A } <-> ( Fun F /\ dom F = { A } ) )
4 1 snid 
 |-  A e. { A }
5 eleq2 
 |-  ( dom F = { A } -> ( A e. dom F <-> A e. { A } ) )
6 4 5 mpbiri 
 |-  ( dom F = { A } -> A e. dom F )
7 6 anim2i 
 |-  ( ( Fun F /\ dom F = { A } ) -> ( Fun F /\ A e. dom F ) )
8 3 7 sylbi 
 |-  ( F Fn { A } -> ( Fun F /\ A e. dom F ) )
9 funfvop 
 |-  ( ( Fun F /\ A e. dom F ) -> <. A , ( F ` A ) >. e. F )
10 8 9 syl 
 |-  ( F Fn { A } -> <. A , ( F ` A ) >. e. F )
11 eleq1 
 |-  ( x = <. A , ( F ` A ) >. -> ( x e. F <-> <. A , ( F ` A ) >. e. F ) )
12 10 11 syl5ibrcom 
 |-  ( F Fn { A } -> ( x = <. A , ( F ` A ) >. -> x e. F ) )
13 2 12 impbid 
 |-  ( F Fn { A } -> ( x e. F <-> x = <. A , ( F ` A ) >. ) )
14 velsn 
 |-  ( x e. { <. A , ( F ` A ) >. } <-> x = <. A , ( F ` A ) >. )
15 13 14 bitr4di 
 |-  ( F Fn { A } -> ( x e. F <-> x e. { <. A , ( F ` A ) >. } ) )
16 15 eqrdv 
 |-  ( F Fn { A } -> F = { <. A , ( F ` A ) >. } )
17 fvex 
 |-  ( F ` A ) e. _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 ) >. } )