# Metamath Proof Explorer

## Definition df-ixp

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)

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

### Detailed syntax breakdown

Step Hyp Ref Expression
0 vx 𝑥
1 cA 𝐴
2 cB 𝐵
3 0 1 2 cixp X 𝑥𝐴 𝐵
4 vf 𝑓
5 4 cv 𝑓
6 0 cv 𝑥
7 6 1 wcel 𝑥𝐴
8 7 0 cab { 𝑥𝑥𝐴 }
9 5 8 wfn 𝑓 Fn { 𝑥𝑥𝐴 }
10 6 5 cfv ( 𝑓𝑥 )
11 10 2 wcel ( 𝑓𝑥 ) ∈ 𝐵
12 11 0 1 wral 𝑥𝐴 ( 𝑓𝑥 ) ∈ 𝐵
13 9 12 wa ( 𝑓 Fn { 𝑥𝑥𝐴 } ∧ ∀ 𝑥𝐴 ( 𝑓𝑥 ) ∈ 𝐵 )
14 13 4 cab { 𝑓 ∣ ( 𝑓 Fn { 𝑥𝑥𝐴 } ∧ ∀ 𝑥𝐴 ( 𝑓𝑥 ) ∈ 𝐵 ) }
15 3 14 wceq X 𝑥𝐴 𝐵 = { 𝑓 ∣ ( 𝑓 Fn { 𝑥𝑥𝐴 } ∧ ∀ 𝑥𝐴 ( 𝑓𝑥 ) ∈ 𝐵 ) }