Metamath Proof Explorer


Theorem mptfng

Description: The maps-to notation defines a function with domain. (Contributed by Scott Fenton, 21-Mar-2011)

Ref Expression
Hypothesis mptfng.1 F = x A B
Assertion mptfng x A B V F Fn A

Proof

Step Hyp Ref Expression
1 mptfng.1 F = x A B
2 eueq B V ∃! y y = B
3 2 ralbii x A B V x A ∃! y y = B
4 df-mpt x A B = x y | x A y = B
5 1 4 eqtri F = x y | x A y = B
6 5 fnopabg x A ∃! y y = B F Fn A
7 3 6 bitri x A B V F Fn A