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	eqabi	|- { (/) } = { f | ( f Fn (/) /\ A. x e. (/) ( f ` x ) e. A ) }
8	1 7	eqtr4i	|- X_ x e. (/) A = { (/) }