Metamath Proof Explorer

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 ⊢ F ∈ ⨉ x ∈ A B → F Fn A

Proof

Step Hyp Ref Expression
1 fneq1 ⊢ f = F → f Fn A ↔ F Fn A
2 elixp2 ⊢ f ∈ ⨉ x ∈ A B ↔ f ∈ V ∧ f Fn A ∧ ∀ x ∈ A f ⁡ x ∈ B
3 2 simp2bi ⊢ f ∈ ⨉ x ∈ A B → f Fn A
4 1 3 vtoclga ⊢ F ∈ ⨉ x ∈ A B → F Fn A