Theorem elixpconst

Description: Membership in an infinite Cartesian product of a constant B . (Contributed by NM, 12-Apr-2008)

	Ref	Expression
Hypothesis	elixp.1	|- F e. _V
Assertion	elixpconst	|- ( F e. X_ x e. A B <-> F : A --> B )

Proof

Step	Hyp	Ref	Expression
1		elixp.1	|- F e. _V
2	1	elixp	|- ( F e. X_ x e. A B <-> ( F Fn A /\ A. x e. A ( F ` x ) e. B ) )
3		ffnfv	|- ( F : A --> B <-> ( F Fn A /\ A. x e. A ( F ` x ) e. B ) )
4	2 3	bitr4i	|- ( F e. X_ x e. A B <-> F : A --> B )