Definition df-ixp 6758

Description: Definition of infinite Cartesian product of [Enderton] p. 54. Enderton uses a bold "X" with 𝑥 ∈ 𝐴 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 𝐵 represents a class expression containing 𝑥 free and thus can be thought of as 𝐵(𝑥). Normally, 𝑥 is not free in 𝐴, although this is not a requirement of the definition. (Contributed by NM, 28-Sep-2006.)

Assertion

Ref	Expression
df-ixp	⊢ X𝑥 ∈ 𝐴 𝐵 = {𝑓 ∣ (𝑓 Fn {𝑥 ∣ 𝑥 ∈ 𝐴} ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐵)}

Distinct variable groups:   𝑥,𝑓   𝐴,𝑓   𝐵,𝑓

Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥)

Detailed syntax breakdown of Definition df-ixp

Step	Hyp	Ref	Expression
1		vx	. . 3 setvar 𝑥
2		cA	. . 3 class 𝐴
3		cB	. . 3 class 𝐵
4	1, 2, 3	cixp 6757	. 2 class X𝑥 ∈ 𝐴 𝐵
5		vf	. . . . . 6 setvar 𝑓
6	5	cv 1363	. . . . 5 class 𝑓
7	1	cv 1363	. . . . . . 7 class 𝑥
8	7, 2	wcel 2167	. . . . . 6 wff 𝑥 ∈ 𝐴
9	8, 1	cab 2182	. . . . 5 class {𝑥 ∣ 𝑥 ∈ 𝐴}
10	6, 9	wfn 5253	. . . 4 wff 𝑓 Fn {𝑥 ∣ 𝑥 ∈ 𝐴}
11	7, 6	cfv 5258	. . . . . 6 class (𝑓‘𝑥)
12	11, 3	wcel 2167	. . . . 5 wff (𝑓‘𝑥) ∈ 𝐵
13	12, 1, 2	wral 2475	. . . 4 wff ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐵
14	10, 13	wa 104	. . 3 wff (𝑓 Fn {𝑥 ∣ 𝑥 ∈ 𝐴} ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐵)
15	14, 5	cab 2182	. 2 class {𝑓 ∣ (𝑓 Fn {𝑥 ∣ 𝑥 ∈ 𝐴} ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐵)}
16	4, 15	wceq 1364	1 wff X𝑥 ∈ 𝐴 𝐵 = {𝑓 ∣ (𝑓 Fn {𝑥 ∣ 𝑥 ∈ 𝐴} ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐵)}

This definition is referenced by:  dfixp  6759  ss2ixp  6770  nfixpxy  6776  nfixp1  6777  ixpm  6789