Theorem f1osn

Description: A singleton of an ordered pair is one-to-one onto function. (Contributed by NM, 18-May-1998) (Proof shortened by Andrew Salmon, 22-Oct-2011)

	Ref	Expression
Hypotheses	f1osn.1	|- A e. _V
	f1osn.2	|- B e. _V
Assertion	f1osn	|- { <. A , B >. } : { A } -1-1-onto-> { B }

Proof

Step	Hyp	Ref	Expression
1		f1osn.1	|- A e. _V
2		f1osn.2	|- B e. _V
3	1 2	fnsn	|- { <. A , B >. } Fn { A }
4	2 1	fnsn	|- { <. B , A >. } Fn { B }
5	1 2	cnvsn	|- `' { <. A , B >. } = { <. B , A >. }
6	5	fneq1i	|- ( `' { <. A , B >. } Fn { B } <-> { <. B , A >. } Fn { B } )
7	4 6	mpbir	|- `' { <. A , B >. } Fn { B }
8		dff1o4	|- ( { <. A , B >. } : { A } -1-1-onto-> { B } <-> ( { <. A , B >. } Fn { A } /\ `' { <. A , B >. } Fn { B } ) )
9	3 7 8	mpbir2an	|- { <. A , B >. } : { A } -1-1-onto-> { B }