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	|- E. y x e. y

Proof

Step	Hyp	Ref	Expression
1		ax-tco	|- E. y ( x e. y /\ A. z ( z e. y -> A. w ( w e. z -> w e. y ) ) )
2		simpl	|- ( ( x e. y /\ A. z ( z e. y -> A. w ( w e. z -> w e. y ) ) ) -> x e. y )
3	1 2	eximii	|- E. y x e. y