Metamath Proof Explorer

Theorem f1o0

Description: One-to-one onto mapping of the empty set. (Contributed by NM, 10-Sep-2004)

Ref Expression
Assertion f1o0 
|- (/) : (/) -1-1-onto-> (/)

Proof

Step Hyp Ref Expression
1 eqid 
 |-  (/) = (/)
2 f1o00 
 |-  ( (/) : (/) -1-1-onto-> (/) <-> ( (/) = (/) /\ (/) = (/) ) )
3 1 1 2 mpbir2an 
 |-  (/) : (/) -1-1-onto-> (/)