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	$$⊢\exists yx\in y$$

Proof

Step	Hyp	Ref	Expression
1		ax-tco	$$⊢\exists y\left(x\in y\wedge \forall z\left(z\in y\to \forall w\left(w\in z\to w\in y\right)\right)\right)$$
2		simpl	$$⊢\left(x\in y\wedge \forall z\left(z\in y\to \forall w\left(w\in z\to w\in y\right)\right)\right)\to x\in y$$
3	1 2	eximii	$$⊢\exists yx\in y$$