This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem zfinf

Description: Axiom of Infinity expressed with the fewest number of different variables. (New usage is discouraged.) (Contributed by NM, 14-Aug-2003)

Ref Expression
Assertion zfinf ∃ 𝑥 ( 𝑦 ∈ 𝑥 ∧ ∀ 𝑦 ( 𝑦 ∈ 𝑥 → ∃ 𝑧 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 ax-inf ⊢ ∃ 𝑥 ( 𝑦 ∈ 𝑥 ∧ ∀ 𝑤 ( 𝑤 ∈ 𝑥 → ∃ 𝑧 ( 𝑤 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥 ) ) )
2 elequ1 ⊢ ( 𝑤 = 𝑦 → ( 𝑤 ∈ 𝑥 ↔ 𝑦 ∈ 𝑥 ) )
3 elequ1 ⊢ ( 𝑤 = 𝑦 → ( 𝑤 ∈ 𝑧 ↔ 𝑦 ∈ 𝑧 ) )
4 3 anbi1d ⊢ ( 𝑤 = 𝑦 → ( ( 𝑤 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥 ) ↔ ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥 ) ) )
5 4 exbidv ⊢ ( 𝑤 = 𝑦 → ( ∃ 𝑧 ( 𝑤 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥 ) ↔ ∃ 𝑧 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥 ) ) )
6 2 5 imbi12d ⊢ ( 𝑤 = 𝑦 → ( ( 𝑤 ∈ 𝑥 → ∃ 𝑧 ( 𝑤 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥 ) ) ↔ ( 𝑦 ∈ 𝑥 → ∃ 𝑧 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥 ) ) ) )
7 6 cbvalvw ⊢ ( ∀ 𝑤 ( 𝑤 ∈ 𝑥 → ∃ 𝑧 ( 𝑤 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥 ) ) ↔ ∀ 𝑦 ( 𝑦 ∈ 𝑥 → ∃ 𝑧 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥 ) ) )
8 7 anbi2i ⊢ ( ( 𝑦 ∈ 𝑥 ∧ ∀ 𝑤 ( 𝑤 ∈ 𝑥 → ∃ 𝑧 ( 𝑤 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥 ) ) ) ↔ ( 𝑦 ∈ 𝑥 ∧ ∀ 𝑦 ( 𝑦 ∈ 𝑥 → ∃ 𝑧 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥 ) ) ) )
9 8 exbii ⊢ ( ∃ 𝑥 ( 𝑦 ∈ 𝑥 ∧ ∀ 𝑤 ( 𝑤 ∈ 𝑥 → ∃ 𝑧 ( 𝑤 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥 ) ) ) ↔ ∃ 𝑥 ( 𝑦 ∈ 𝑥 ∧ ∀ 𝑦 ( 𝑦 ∈ 𝑥 → ∃ 𝑧 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥 ) ) ) )
10 1 9 mpbi ⊢ ∃ 𝑥 ( 𝑦 ∈ 𝑥 ∧ ∀ 𝑦 ( 𝑦 ∈ 𝑥 → ∃ 𝑧 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥 ) ) )