Metamath Proof Explorer


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 𝑥 𝑥 𝑥

Proof

Step Hyp Ref Expression
1 omex ω ∈ V
2 infeq5i ( ω ∈ V → ∃ 𝑥 𝑥 𝑥 )
3 1 2 ax-mp 𝑥 𝑥 𝑥