Theorem ixp0x

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

	Ref	Expression
Assertion	ixp0x	$$⊢\underset{x\in \varnothing }{⨉}A=\left\{\varnothing \right\}$$

Proof

Step	Hyp	Ref	Expression
1		dfixp	$$⊢\underset{x\in \varnothing }{⨉}A=\left\{f|\left(fFn\varnothing \wedge \forall x\in \varnothing f\left(x\right)\in A\right)\right\}$$
2		velsn	$$⊢f\in \left\{\varnothing \right\}\leftrightarrow f=\varnothing$$
3		fn0	$$⊢fFn\varnothing \leftrightarrow f=\varnothing$$
4		ral0	$$⊢\forall x\in \varnothing f\left(x\right)\in A$$
5	4	biantru	$$⊢fFn\varnothing \leftrightarrow \left(fFn\varnothing \wedge \forall x\in \varnothing f\left(x\right)\in A\right)$$
6	2 3 5	3bitr2i	$$⊢f\in \left\{\varnothing \right\}\leftrightarrow \left(fFn\varnothing \wedge \forall x\in \varnothing f\left(x\right)\in A\right)$$
7	6	eqabi	$$⊢\left\{\varnothing \right\}=\left\{f|\left(fFn\varnothing \wedge \forall x\in \varnothing f\left(x\right)\in A\right)\right\}$$
8	1 7	eqtr4i	$$⊢\underset{x\in \varnothing }{⨉}A=\left\{\varnothing \right\}$$