Theorem elixp

Description: Membership in an infinite Cartesian product. (Contributed by NM, 28-Sep-2006)

	Ref	Expression
Hypothesis	elixp.1	|- F e. _V
Assertion	elixp	|- ( F e. X_ x e. A B <-> ( F Fn A /\ A. x e. A ( F ` x ) e. B ) )

Proof

Step	Hyp	Ref	Expression
1		elixp.1	|- F e. _V
2		elixp2	|- ( F e. X_ x e. A B <-> ( F e. _V /\ F Fn A /\ A. x e. A ( F ` x ) e. B ) )
3		3anass	|- ( ( F e. _V /\ F Fn A /\ A. x e. A ( F ` x ) e. B ) <-> ( F e. _V /\ ( F Fn A /\ A. x e. A ( F ` x ) e. B ) ) )
4	1 3	mpbiran	|- ( ( F e. _V /\ F Fn A /\ A. x e. A ( F ` x ) e. B ) <-> ( F Fn A /\ A. x e. A ( F ` x ) e. B ) )
5	2 4	bitri	|- ( F e. X_ x e. A B <-> ( F Fn A /\ A. x e. A ( F ` x ) e. B ) )