Theorem axtco1

Description: Strong form of the Axiom of Transitive Containment. See ax-tco for more information. In particular, this theorem generalizes the statement of ax-tco , allowing it to be written with only three variables, since x need not be distinct from both z and w . (Contributed by Matthew House, 7-Apr-2026)

	Ref	Expression
Assertion	axtco1	|- E. y ( x e. y /\ A. z ( z e. y -> A. w ( w e. z -> w e. y ) ) )

Proof

Step	Hyp	Ref	Expression
1		elequ1	|- ( v = x -> ( v e. y <-> x e. y ) )
2	1	anbi1d	|- ( v = x -> ( ( v e. y /\ A. z ( z e. y -> A. w ( w e. z -> w e. y ) ) ) <-> ( x e. y /\ A. z ( z e. y -> A. w ( w e. z -> w e. y ) ) ) ) )
3	2	exbidv	|- ( v = x -> ( E. y ( v e. y /\ A. z ( z e. y -> A. w ( w e. z -> w e. y ) ) ) <-> E. y ( x e. y /\ A. z ( z e. y -> A. w ( w e. z -> w e. y ) ) ) ) )
4		ax-tco	|- E. y ( v e. y /\ A. z ( z e. y -> A. w ( w e. z -> w e. y ) ) )
5	3 4	chvarvv	|- E. y ( x e. y /\ A. z ( z e. y -> A. w ( w e. z -> w e. y ) ) )