Theorem elixp2

Description: Membership in an infinite Cartesian product. See df-ixp for discussion of the notation. (Contributed by NM, 28-Sep-2006)

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

Proof

Step	Hyp	Ref	Expression
1		fneq1	|- ( f = F -> ( f Fn A <-> F Fn A ) )
2		fveq1	|- ( f = F -> ( f ` x ) = ( F ` x ) )
3	2	eleq1d	|- ( f = F -> ( ( f ` x ) e. B <-> ( F ` x ) e. B ) )
4	3	ralbidv	|- ( f = F -> ( A. x e. A ( f ` x ) e. B <-> A. x e. A ( F ` x ) e. B ) )
5	1 4	anbi12d	|- ( f = F -> ( ( f Fn A /\ A. x e. A ( f ` x ) e. B ) <-> ( F Fn A /\ A. x e. A ( F ` x ) e. B ) ) )
6		dfixp	|- X_ x e. A B = { f | ( f Fn A /\ A. x e. A ( f ` x ) e. B ) }
7	5 6	elab2g	|- ( F e. _V -> ( F e. X_ x e. A B <-> ( F Fn A /\ A. x e. A ( F ` x ) e. B ) ) )
8	7	pm5.32i	|- ( ( F e. _V /\ F e. X_ x e. A B ) <-> ( F e. _V /\ ( F Fn A /\ A. x e. A ( F ` x ) e. B ) ) )
9		elex	|- ( F e. X_ x e. A B -> F e. _V )
10	9	pm4.71ri	|- ( F e. X_ x e. A B <-> ( F e. _V /\ F e. X_ x e. A B ) )
11		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 ) ) )
12	8 10 11	3bitr4i	|- ( F e. X_ x e. A B <-> ( F e. _V /\ F Fn A /\ A. x e. A ( F ` x ) e. B ) )