Metamath Proof Explorer

Theorem iswrddm0

Description: A function with empty domain is a word. (Contributed by AV, 13-Oct-2018)

Ref Expression
Assertion iswrddm0 
|- ( W : (/) --> S -> W e. Word S )

Proof

Step Hyp Ref Expression
1 fzo0 
 |-  ( 0 ..^ 0 ) = (/)
2 1 feq2i 
 |-  ( W : ( 0 ..^ 0 ) --> S <-> W : (/) --> S )
3 iswrdi 
 |-  ( W : ( 0 ..^ 0 ) --> S -> W e. Word S )
4 2 3 sylbir 
 |-  ( W : (/) --> S -> W e. Word S )