Theorem axtco2

Description: Weak form of the Axiom of Transitive Containment. See ax-tco for more information. In particular, this theorem shows the derivation of the weak form from the strong form. (Contributed by Matthew House, 6-Apr-2026)

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

Proof

Step	Hyp	Ref	Expression
1		axtco1	|- E. y ( x e. y /\ A. z ( z e. y -> A. w ( w e. z -> w e. y ) ) )
2		elequ1	|- ( z = x -> ( z e. y <-> x e. y ) )
3	2	biimprcd	|- ( x e. y -> ( z = x -> z e. y ) )
4	3	imim1d	|- ( x e. y -> ( ( z e. y -> A. w ( w e. z -> w e. y ) ) -> ( z = x -> A. w ( w e. z -> w e. y ) ) ) )
5	4	alimdv	|- ( x e. y -> ( A. z ( z e. y -> A. w ( w e. z -> w e. y ) ) -> A. z ( z = x -> A. w ( w e. z -> w e. y ) ) ) )
6		jao	|- ( ( z = x -> A. w ( w e. z -> w e. y ) ) -> ( ( z e. y -> A. w ( w e. z -> w e. y ) ) -> ( ( z = x \/ z e. y ) -> A. w ( w e. z -> w e. y ) ) ) )
7	6	al2imi	|- ( A. z ( z = x -> A. w ( w e. z -> w e. y ) ) -> ( A. z ( z e. y -> A. w ( w e. z -> w e. y ) ) -> A. z ( ( z = x \/ z e. y ) -> A. w ( w e. z -> w e. y ) ) ) )
8	5 7	syli	|- ( x e. y -> ( A. z ( z e. y -> A. w ( w e. z -> w e. y ) ) -> A. z ( ( z = x \/ z e. y ) -> A. w ( w e. z -> w e. y ) ) ) )
9	8	imp	|- ( ( x e. y /\ A. z ( z e. y -> A. w ( w e. z -> w e. y ) ) ) -> A. z ( ( z = x \/ z e. y ) -> A. w ( w e. z -> w e. y ) ) )
10	1 9	eximii	|- E. y A. z ( ( z = x \/ z e. y ) -> A. w ( w e. z -> w e. y ) )