Metamath Proof Explorer


Theorem ixp0x

Description: An infinite Cartesian product with an empty index set. (Contributed by NM, 21-Sep-2007)

Ref Expression
Assertion ixp0x
|- X_ x e. (/) A = { (/) }

Proof

Step Hyp Ref Expression
1 dfixp
 |-  X_ x e. (/) A = { f | ( f Fn (/) /\ A. x e. (/) ( f ` x ) e. A ) }
2 velsn
 |-  ( f e. { (/) } <-> f = (/) )
3 fn0
 |-  ( f Fn (/) <-> f = (/) )
4 ral0
 |-  A. x e. (/) ( f ` x ) e. A
5 4 biantru
 |-  ( f Fn (/) <-> ( f Fn (/) /\ A. x e. (/) ( f ` x ) e. A ) )
6 2 3 5 3bitr2i
 |-  ( f e. { (/) } <-> ( f Fn (/) /\ A. x e. (/) ( f ` x ) e. A ) )
7 6 abbi2i
 |-  { (/) } = { f | ( f Fn (/) /\ A. x e. (/) ( f ` x ) e. A ) }
8 1 7 eqtr4i
 |-  X_ x e. (/) A = { (/) }