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 ⊢ ∃ x y ∈ x ∧ ∀ y y ∈ x → ∃ z y ∈ z ∧ z ∈ x

Proof

Step Hyp Ref Expression
1 ax-inf ⊢ ∃ x y ∈ x ∧ ∀ w w ∈ x → ∃ z w ∈ z ∧ z ∈ x
2 elequ1 ⊢ w = y → w ∈ x ↔ y ∈ x
3 elequ1 ⊢ w = y → w ∈ z ↔ y ∈ z
4 3 anbi1d ⊢ w = y → w ∈ z ∧ z ∈ x ↔ y ∈ z ∧ z ∈ x
5 4 exbidv ⊢ w = y → ∃ z w ∈ z ∧ z ∈ x ↔ ∃ z y ∈ z ∧ z ∈ x
6 2 5 imbi12d ⊢ w = y → w ∈ x → ∃ z w ∈ z ∧ z ∈ x ↔ y ∈ x → ∃ z y ∈ z ∧ z ∈ x
7 6 cbvalvw ⊢ ∀ w w ∈ x → ∃ z w ∈ z ∧ z ∈ x ↔ ∀ y y ∈ x → ∃ z y ∈ z ∧ z ∈ x
8 7 anbi2i ⊢ y ∈ x ∧ ∀ w w ∈ x → ∃ z w ∈ z ∧ z ∈ x ↔ y ∈ x ∧ ∀ y y ∈ x → ∃ z y ∈ z ∧ z ∈ x
9 8 exbii ⊢ ∃ x y ∈ x ∧ ∀ w w ∈ x → ∃ z w ∈ z ∧ z ∈ x ↔ ∃ x y ∈ x ∧ ∀ y y ∈ x → ∃ z y ∈ z ∧ z ∈ x
10 1 9 mpbi ⊢ ∃ x y ∈ x ∧ ∀ y y ∈ x → ∃ z y ∈ z ∧ z ∈ x