Metamath Proof Explorer


Theorem fvmptndm

Description: Value of a function given by the maps-to notation, outside of its domain. (Contributed by AV, 31-Dec-2020)

Ref Expression
Hypothesis fvmptndm.1 F = x A B
Assertion fvmptndm ¬ X A F X =

Proof

Step Hyp Ref Expression
1 fvmptndm.1 F = x A B
2 df-mpt x A B = x y | x A y = B
3 1 2 eqtri F = x y | x A y = B
4 3 fvopab4ndm ¬ X A F X =