Metamath Proof Explorer


Theorem mptfnd

Description: The maps-to notation defines a function with domain. (Contributed by NM, 9-Apr-2013) (Revised by Thierry Arnoux, 10-May-2017)

Ref Expression
Hypotheses mptfnd.1 𝑥 𝐴
mptfnd.2 𝑥 𝜑
mptfnd.3 ( ( 𝜑𝑥𝐴 ) → 𝐵𝑉 )
Assertion mptfnd ( 𝜑 → ( 𝑥𝐴𝐵 ) Fn 𝐴 )

Proof

Step Hyp Ref Expression
1 mptfnd.1 𝑥 𝐴
2 mptfnd.2 𝑥 𝜑
3 mptfnd.3 ( ( 𝜑𝑥𝐴 ) → 𝐵𝑉 )
4 3 ex ( 𝜑 → ( 𝑥𝐴𝐵𝑉 ) )
5 elex ( 𝐵𝑉𝐵 ∈ V )
6 4 5 syl6 ( 𝜑 → ( 𝑥𝐴𝐵 ∈ V ) )
7 2 6 ralrimi ( 𝜑 → ∀ 𝑥𝐴 𝐵 ∈ V )
8 1 mptfnf ( ∀ 𝑥𝐴 𝐵 ∈ V ↔ ( 𝑥𝐴𝐵 ) Fn 𝐴 )
9 7 8 sylib ( 𝜑 → ( 𝑥𝐴𝐵 ) Fn 𝐴 )