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

Metamath Proof Explorer

Theorem fnsnr

Description: If a class belongs to a function on a singleton, then that class is the obvious ordered pair. Note that this theorem also holds when A is a proper class, but its meaning is then different. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (Proof shortened by Mario Carneiro, 22-Dec-2016)

Ref Expression
Assertion fnsnr 
|- ( F Fn { A } -> ( B e. F -> B = <. A , ( F ` A ) >. ) )

Proof

Step Hyp Ref Expression
1 fnresdm 
 |-  ( F Fn { A } -> ( F |` { A } ) = F )
2 fnfun 
 |-  ( F Fn { A } -> Fun F )
3 funressn 
 |-  ( Fun F -> ( F |` { A } ) C_ { <. A , ( F ` A ) >. } )
4 2 3 syl 
 |-  ( F Fn { A } -> ( F |` { A } ) C_ { <. A , ( F ` A ) >. } )
5 1 4 eqsstrrd 
 |-  ( F Fn { A } -> F C_ { <. A , ( F ` A ) >. } )
6 5 sseld 
 |-  ( F Fn { A } -> ( B e. F -> B e. { <. A , ( F ` A ) >. } ) )
7 elsni 
 |-  ( B e. { <. A , ( F ` A ) >. } -> B = <. A , ( F ` A ) >. )
8 6 7 syl6 
 |-  ( F Fn { A } -> ( B e. F -> B = <. A , ( F ` A ) >. ) )