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 e. X_ x e. A B -> F Fn A )

Proof

Step Hyp Ref Expression
1 fneq1 
 |-  ( f = F -> ( f Fn A <-> F Fn A ) )
2 elixp2 
 |-  ( f e. X_ x e. A B <-> ( f e. _V /\ f Fn A /\ A. x e. A ( f ` x ) e. B ) )
3 2 simp2bi 
 |-  ( f e. X_ x e. A B -> f Fn A )
4 1 3 vtoclga 
 |-  ( F e. X_ x e. A B -> F Fn A )