Description: The value of a prefix operation for out-of-domain arguments. (This is due to our definition of function values for out-of-domain arguments, see ndmfv ). (Contributed by AV, 3-Dec-2022) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | pfxnndmnd | |- ( -. ( S e. _V /\ L e. NN0 ) -> ( S prefix L ) = (/) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-pfx | |- prefix = ( s e. _V , l e. NN0 |-> ( s substr <. 0 , l >. ) ) |
|
| 2 | 1 | mpondm0 | |- ( -. ( S e. _V /\ L e. NN0 ) -> ( S prefix L ) = (/) ) |