**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 𝐴 ) |