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	$$⊢\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)$$

Proof

Step	Hyp	Ref	Expression
1		elequ1	$$⊢v=x\to \left(v\in y\leftrightarrow x\in y\right)$$
2	1	anbi1d	$$⊢v=x\to \left(\left(v\in y\wedge \forall z\left(z\in y\to \forall w\left(w\in z\to w\in y\right)\right)\right)\leftrightarrow \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)\right)$$
3	2	exbidv	$$⊢v=x\to \left(\exists y\left(v\in y\wedge \forall z\left(z\in y\to \forall w\left(w\in z\to w\in y\right)\right)\right)\leftrightarrow \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)\right)$$
4		ax-tco	$$⊢\exists y\left(v\in y\wedge \forall z\left(z\in y\to \forall w\left(w\in z\to w\in y\right)\right)\right)$$
5	3 4	chvarvv	$$⊢\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)$$