Metamath Proof Explorer

Theorem fsng

Description: A function maps a singleton to a singleton iff it is the singleton of an ordered pair. (Contributed by NM, 26-Oct-2012)

Ref Expression
Assertion fsng 
|- ( ( A e. C /\ B e. D ) -> ( F : { A } --> { B } <-> F = { <. A , B >. } ) )

Proof

Step Hyp Ref Expression
1 sneq 
 |-  ( a = A -> { a } = { A } )
2 1 feq2d 
 |-  ( a = A -> ( F : { a } --> { b } <-> F : { A } --> { b } ) )
3 opeq1 
 |-  ( a = A -> <. a , b >. = <. A , b >. )
4 3 sneqd 
 |-  ( a = A -> { <. a , b >. } = { <. A , b >. } )
5 4 eqeq2d 
 |-  ( a = A -> ( F = { <. a , b >. } <-> F = { <. A , b >. } ) )
6 2 5 bibi12d 
 |-  ( a = A -> ( ( F : { a } --> { b } <-> F = { <. a , b >. } ) <-> ( F : { A } --> { b } <-> F = { <. A , b >. } ) ) )
7 sneq 
 |-  ( b = B -> { b } = { B } )
8 7 feq3d 
 |-  ( b = B -> ( F : { A } --> { b } <-> F : { A } --> { B } ) )
9 opeq2 
 |-  ( b = B -> <. A , b >. = <. A , B >. )
10 9 sneqd 
 |-  ( b = B -> { <. A , b >. } = { <. A , B >. } )
11 10 eqeq2d 
 |-  ( b = B -> ( F = { <. A , b >. } <-> F = { <. A , B >. } ) )
12 8 11 bibi12d 
 |-  ( b = B -> ( ( F : { A } --> { b } <-> F = { <. A , b >. } ) <-> ( F : { A } --> { B } <-> F = { <. A , B >. } ) ) )
13 vex 
 |-  a e. _V
14 vex 
 |-  b e. _V
15 13 14 fsn 
 |-  ( F : { a } --> { b } <-> F = { <. a , b >. } )
16 6 12 15 vtocl2g 
 |-  ( ( A e. C /\ B e. D ) -> ( F : { A } --> { B } <-> F = { <. A , B >. } ) )