Theorem inf5

Description: The statement "there exists a set that is a proper subset of its union" is equivalent to the Axiom of Infinity (see Theorem infeq5 ). This provides us with a very compact way to express the Axiom of Infinity using only elementary symbols. (Contributed by NM, 3-Jun-2005)

	Ref	Expression
Assertion	inf5	$$⊢\exists xx\subset \bigcup x$$

Proof

Step	Hyp	Ref	Expression
1		omex	$$⊢\mathrm{\omega }\in \mathrm{V}$$
2		infeq5i	$$⊢\mathrm{\omega }\in \mathrm{V}\to \exists xx\subset \bigcup x$$
3	1 2	ax-mp	$$⊢\exists xx\subset \bigcup x$$