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 ) >. } ) ) )