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	⊢ ∃ 𝑥 ( 𝑦 ∈ 𝑥 ∧ ∀ 𝑦 ( 𝑦 ∈ 𝑥 → ∃ 𝑧 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥 ) ) )