Theorem f1sng

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

	Ref	Expression
Assertion	f1sng	|- ( ( A e. V /\ B e. W ) -> { <. A , B >. } : { A } -1-1-> W )

Proof

Step	Hyp	Ref	Expression
1		f1osng	|- ( ( A e. V /\ B e. W ) -> { <. A , B >. } : { A } -1-1-onto-> { B } )
2		f1of1	|- ( { <. A , B >. } : { A } -1-1-onto-> { B } -> { <. A , B >. } : { A } -1-1-> { B } )
3	1 2	syl	|- ( ( A e. V /\ B e. W ) -> { <. A , B >. } : { A } -1-1-> { B } )
4		snssi	|- ( B e. W -> { B } C_ W )
5	4	adantl	|- ( ( A e. V /\ B e. W ) -> { B } C_ W )
6		f1ss	|- ( ( { <. A , B >. } : { A } -1-1-> { B } /\ { B } C_ W ) -> { <. A , B >. } : { A } -1-1-> W )
7	3 5 6	syl2anc	|- ( ( A e. V /\ B e. W ) -> { <. A , B >. } : { A } -1-1-> W )