Metamath Proof Explorer

Theorem f10d

Description: The empty set maps one-to-one into any class, deduction version. (Contributed by AV, 25-Nov-2020)

Ref Expression
Hypothesis f10d.f 
|- ( ph -> F = (/) )
Assertion f10d 
|- ( ph -> F : dom F -1-1-> A )

Proof

Step Hyp Ref Expression
1 f10d.f 
 |-  ( ph -> F = (/) )
2 f10 
 |-  (/) : (/) -1-1-> A
3 dm0 
 |-  dom (/) = (/)
4 f1eq2 
 |-  ( dom (/) = (/) -> ( (/) : dom (/) -1-1-> A <-> (/) : (/) -1-1-> A ) )
5 3 4 ax-mp 
 |-  ( (/) : dom (/) -1-1-> A <-> (/) : (/) -1-1-> A )
6 2 5 mpbir 
 |-  (/) : dom (/) -1-1-> A
7 1 dmeqd 
 |-  ( ph -> dom F = dom (/) )
8 eqidd 
 |-  ( ph -> A = A )
9 1 7 8 f1eq123d 
 |-  ( ph -> ( F : dom F -1-1-> A <-> (/) : dom (/) -1-1-> A ) )
10 6 9 mpbiri 
 |-  ( ph -> F : dom F -1-1-> A )