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 𝐴 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fneq1 | ⊢ ( 𝑓 = 𝐹 → ( 𝑓 Fn 𝐴 ↔ 𝐹 Fn 𝐴 ) ) | |
2 | elixp2 | ⊢ ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 ↔ ( 𝑓 ∈ V ∧ 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ) ) | |
3 | 2 | simp2bi | ⊢ ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 → 𝑓 Fn 𝐴 ) |
4 | 1 3 | vtoclga | ⊢ ( 𝐹 ∈ X 𝑥 ∈ 𝐴 𝐵 → 𝐹 Fn 𝐴 ) |