Theorem fsnd

Description: A singleton of an ordered pair is a function. (Contributed by AV, 17-Apr-2021)

	Ref	Expression
Hypotheses	fsnd.a	|- ( ph -> A e. V )
	fsnd.b	|- ( ph -> B e. W )
Assertion	fsnd	|- ( ph -> { <. A , B >. } : { A } --> W )

Proof

Step	Hyp	Ref	Expression
1		fsnd.a	|- ( ph -> A e. V )
2		fsnd.b	|- ( ph -> B e. W )
3	1 2	jca	|- ( ph -> ( A e. V /\ B e. W ) )
4		f1sng	|- ( ( A e. V /\ B e. W ) -> { <. A , B >. } : { A } -1-1-> W )
5		f1f	|- ( { <. A , B >. } : { A } -1-1-> W -> { <. A , B >. } : { A } --> W )
6	3 4 5	3syl	|- ( ph -> { <. A , B >. } : { A } --> W )