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 ( 𝐹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 𝐴 )