Metamath Proof Explorer

Theorem f10

Description: The empty set maps one-to-one into any class. (Contributed by NM, 7-Apr-1998)

Ref Expression
Assertion f10 
|- (/) : (/) -1-1-> A

Proof

Step Hyp Ref Expression
1 f0 
 |-  (/) : (/) --> A
2 funcnv0 
 |-  Fun `' (/)
3 df-f1 
 |-  ( (/) : (/) -1-1-> A <-> ( (/) : (/) --> A /\ Fun `' (/) ) )
4 1 2 3 mpbir2an 
 |-  (/) : (/) -1-1-> A