Metamath Proof Explorer


Theorem 1fv

Description: A function on a singleton. (Contributed by Alexander van der Vekens, 3-Dec-2017) (Proof shortened by AV, 18-Apr-2021)

Ref Expression
Assertion 1fv NVP=0NP:00VP0=N

Proof

Step Hyp Ref Expression
1 0z 0
2 1 a1i NV0
3 id NVNV
4 2 3 fsnd NV0N:0V
5 fvsng 0NV0N0=N
6 1 5 mpan NV0N0=N
7 4 6 jca NV0N:0V0N0=N
8 7 adantr NVP=0N0N:0V0N0=N
9 id P=0NP=0N
10 fz0sn 00=0
11 10 a1i P=0N00=0
12 9 11 feq12d P=0NP:00V0N:0V
13 fveq1 P=0NP0=0N0
14 13 eqeq1d P=0NP0=N0N0=N
15 12 14 anbi12d P=0NP:00VP0=N0N:0V0N0=N
16 15 adantl NVP=0NP:00VP0=N0N:0V0N0=N
17 8 16 mpbird NVP=0NP:00VP0=N