Theorem mptfng

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

	Ref	Expression
Hypothesis	mptfng.1	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
Assertion	mptfng	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ V ↔ 𝐹 Fn 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		mptfng.1	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
2		eueq	⊢ ( 𝐵 ∈ V ↔ ∃! 𝑦 𝑦 = 𝐵 )
3	2	ralbii	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ V ↔ ∀ 𝑥 ∈ 𝐴 ∃! 𝑦 𝑦 = 𝐵 )
4		df-mpt	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) }
5	1 4	eqtri	⊢ 𝐹 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) }
6	5	fnopabg	⊢ ( ∀ 𝑥 ∈ 𝐴 ∃! 𝑦 𝑦 = 𝐵 ↔ 𝐹 Fn 𝐴 )
7	3 6	bitri	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ V ↔ 𝐹 Fn 𝐴 )