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

Metamath Proof Explorer

Theorem fsn2g

Description: A function that maps a singleton to a class is the singleton of an ordered pair. (Contributed by Thierry Arnoux, 11-Jul-2020)

Ref Expression
Assertion fsn2g 
|- ( A e. V -> ( F : { A } --> B <-> ( ( F ` A ) e. B /\ F = { <. A , ( F ` A ) >. } ) ) )

Proof

Step Hyp Ref Expression
1 sneq 
 |-  ( a = A -> { a } = { A } )
2 1 feq2d 
 |-  ( a = A -> ( F : { a } --> B <-> F : { A } --> B ) )
3 fveq2 
 |-  ( a = A -> ( F ` a ) = ( F ` A ) )
4 3 eleq1d 
 |-  ( a = A -> ( ( F ` a ) e. B <-> ( F ` A ) e. B ) )
5 id 
 |-  ( a = A -> a = A )
6 5 3 opeq12d 
 |-  ( a = A -> <. a , ( F ` a ) >. = <. A , ( F ` A ) >. )
7 6 sneqd 
 |-  ( a = A -> { <. a , ( F ` a ) >. } = { <. A , ( F ` A ) >. } )
8 7 eqeq2d 
 |-  ( a = A -> ( F = { <. a , ( F ` a ) >. } <-> F = { <. A , ( F ` A ) >. } ) )
9 4 8 anbi12d 
 |-  ( a = A -> ( ( ( F ` a ) e. B /\ F = { <. a , ( F ` a ) >. } ) <-> ( ( F ` A ) e. B /\ F = { <. A , ( F ` A ) >. } ) ) )
10 vex 
 |-  a e. _V
11 10 fsn2 
 |-  ( F : { a } --> B <-> ( ( F ` a ) e. B /\ F = { <. a , ( F ` a ) >. } ) )
12 2 9 11 vtoclbg 
 |-  ( A e. V -> ( F : { A } --> B <-> ( ( F ` A ) e. B /\ F = { <. A , ( F ` A ) >. } ) ) )