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 φF=
Assertion f10d φF:domF1-1A

Proof

Step Hyp Ref Expression
1 f10d.f φF=
2 f10 :1-1A
3 dm0 dom=
4 f1eq2 dom=:dom1-1A:1-1A
5 3 4 ax-mp :dom1-1A:1-1A
6 2 5 mpbir :dom1-1A
7 1 dmeqd φdomF=dom
8 eqidd φA=A
9 1 7 8 f1eq123d φF:domF1-1A:dom1-1A
10 6 9 mpbiri φF:domF1-1A