Theorem fvsng

Description: The value of a singleton of an ordered pair is the second member. (Contributed by NM, 26-Oct-2012) (Proof shortened by BJ, 25-Feb-2023)

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

Proof

Step	Hyp	Ref	Expression
1		funsng	|- ( ( A e. V /\ B e. W ) -> Fun { <. A , B >. } )
2		opex	|- <. A , B >. e. _V
3	2	snid	|- <. A , B >. e. { <. A , B >. }
4		funopfv	|- ( Fun { <. A , B >. } -> ( <. A , B >. e. { <. A , B >. } -> ( { <. A , B >. } ` A ) = B ) )
5	1 3 4	mpisyl	|- ( ( A e. V /\ B e. W ) -> ( { <. A , B >. } ` A ) = B )