Definition df-ixp 7471

Description: Definition of infinite Cartesian product of [Enderton] p. 54. Enderton uses a bold "X" with x e. A written underneath or as a subscript, as does Stoll p. 47. Some books use a capital pi, but we will reserve that notation for products of numbers. Usually B represents a class expression containing x free and thus can be thought of as B ( x ). Normally, x is not free in A, although this is not a requirement of the definition. (Contributed by NM, 28-Sep-2006.)

Assertion

Ref	Expression
df-ixp	|- X_ x e. A B = { f | ( f Fn { x | x e. A } /\ A. x e. A ( f ` x ) e. B ) }

Distinct variable groups:   x, f   A, f   B, f

Allowed substitution hints:   A( x)   B( x)

Detailed syntax breakdown of Definition df-ixp

Step	Hyp	Ref	Expression
1		vx	. . 3 setvar x
2		cA	. . 3 class A
3		cB	. . 3 class B
4	1, 2, 3	cixp 7470	. 2 class X_ x e. A B
5		vf	. . . . . 6 setvar f
6	5	cv 1436	. . . . 5 class f
7	1	cv 1436	. . . . . . 7 class x
8	7, 2	wcel 1872	. . . . . 6 wff x e. A
9	8, 1	cab 2408	. . . . 5 class { x | x e. A }
10	6, 9	wfn 5532	. . . 4 wff f Fn { x | x e. A }
11	7, 6	cfv 5537	. . . . . 6 class ( f ` x )
12	11, 3	wcel 1872	. . . . 5 wff ( f ` x ) e. B
13	12, 1, 2	wral 2708	. . . 4 wff A. x e. A ( f ` x ) e. B
14	10, 13	wa 370	. . 3 wff ( f Fn { x | x e. A } /\ A. x e. A ( f ` x ) e. B )
15	14, 5	cab 2408	. 2 class { f | ( f Fn { x | x e. A } /\ A. x e. A ( f ` x ) e. B ) }
16	4, 15	wceq 1437	1 wff X_ x e. A B = { f | ( f Fn { x | x e. A } /\ A. x e. A ( f ` x ) e. B ) }

This definition is referenced by:  dfixp  7472  ss2ixp  7483  nfixp  7489  nfixp1  7490  ixpn0  7502