Metamath Proof Explorer


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 AV
f1osn.2 BV
Assertion f1osn AB:A1-1 ontoB

Proof

Step Hyp Ref Expression
1 f1osn.1 AV
2 f1osn.2 BV
3 1 2 fnsn ABFnA
4 2 1 fnsn BAFnB
5 1 2 cnvsn AB-1=BA
6 5 fneq1i AB-1FnBBAFnB
7 4 6 mpbir AB-1FnB
8 dff1o4 AB:A1-1 ontoBABFnAAB-1FnB
9 3 7 8 mpbir2an AB:A1-1 ontoB