Metamath Proof Explorer


Theorem elfvne0

Description: If a function value has a member, then the function is not an empty set (An artifact of our function value definition.) (Contributed by Zhi Wang, 16-Sep-2024)

Ref Expression
Assertion elfvne0 A F B F

Proof

Step Hyp Ref Expression
1 ne0i A F B F B
2 fveq1 F = F B = B
3 0fv B =
4 2 3 eqtrdi F = F B =
5 4 necon3i F B F
6 1 5 syl A F B F