Theorem ixpfn

Description: A nuple is a function. (Contributed by FL, 6-Jun-2011) (Revised by Mario Carneiro, 31-May-2014)

	Ref	Expression
Assertion	ixpfn	⊢ ( 𝐹 ∈ X 𝑥 ∈ 𝐴 𝐵 → 𝐹 Fn 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		fneq1	⊢ ( 𝑓 = 𝐹 → ( 𝑓 Fn 𝐴 ↔ 𝐹 Fn 𝐴 ) )
2		elixp2	⊢ ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 ↔ ( 𝑓 ∈ V ∧ 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ) )
3	2	simp2bi	⊢ ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 → 𝑓 Fn 𝐴 )
4	1 3	vtoclga	⊢ ( 𝐹 ∈ X 𝑥 ∈ 𝐴 𝐵 → 𝐹 Fn 𝐴 )