Theorem elALTtco

Description: Derivation of el from ax-tco . Use el instead. (Contributed by Matthew House, 7-Apr-2026) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	elALTtco	⊢ ∃ 𝑦 𝑥 ∈ 𝑦

Proof

Step	Hyp	Ref	Expression
1		ax-tco	⊢ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) ) )
2		simpl	⊢ ( ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) ) ) → 𝑥 ∈ 𝑦 )
3	1 2	eximii	⊢ ∃ 𝑦 𝑥 ∈ 𝑦