Theorem 0elixp

Description: Membership of the empty set in an infinite Cartesian product. (Contributed by Steve Rodriguez, 29-Sep-2006)

	Ref	Expression
Assertion	0elixp	$$⊢\varnothing \in \underset{x\in \varnothing }{⨉}A$$

Proof

Step	Hyp	Ref	Expression
1		0ex	$$⊢\varnothing \in \mathrm{V}$$
2	1	snid	$$⊢\varnothing \in \left\{\varnothing \right\}$$
3		ixp0x	$$⊢\underset{x\in \varnothing }{⨉}A=\left\{\varnothing \right\}$$
4	2 3	eleqtrri	$$⊢\varnothing \in \underset{x\in \varnothing }{⨉}A$$