Metamath Proof Explorer

Theorem eldmne0

Description: A function of nonempty domain is not empty. (Contributed by Thierry Arnoux, 20-Nov-2023)

Ref Expression
Assertion eldmne0 
|- ( X e. dom F -> F =/= (/) )

Proof

Step Hyp Ref Expression
1 ne0i 
 |-  ( X e. dom F -> dom F =/= (/) )
2 dmeq 
 |-  ( F = (/) -> dom F = dom (/) )
3 dm0 
 |-  dom (/) = (/)
4 2 3 eqtrdi 
 |-  ( F = (/) -> dom F = (/) )
5 4 necon3i 
 |-  ( dom F =/= (/) -> F =/= (/) )
6 1 5 syl 
 |-  ( X e. dom F -> F =/= (/) )