Metamath Proof Explorer


Theorem fnmptd

Description: The maps-to notation defines a function with domain. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses fnmptd.1 x φ
fnmptd.2 φ x A B V
fnmptd.3 F = x A B
Assertion fnmptd φ F Fn A

Proof

Step Hyp Ref Expression
1 fnmptd.1 x φ
2 fnmptd.2 φ x A B V
3 fnmptd.3 F = x A B
4 2 ex φ x A B V
5 1 4 ralrimi φ x A B V
6 3 fnmpt x A B V F Fn A
7 5 6 syl φ F Fn A