Theorem axtco

Description: Axiom of Transitive Containment, derived as a theorem from ax-ext , ax-rep , and ax-inf2 . Use ax-tco instead. (Contributed by Matthew House, 6-Apr-2026) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		vsnex	|- { x } e. _V
2	1	tz9.1	|- E. y ( { x } C_ y /\ Tr y /\ A. z ( ( { x } C_ z /\ Tr z ) -> y C_ z ) )
3		vex	|- x e. _V
4	3	snss	|- ( x e. y <-> { x } C_ y )
5		dftr3	|- ( Tr y <-> A. z e. y z C_ y )
6		df-ss	|- ( z C_ y <-> A. w ( w e. z -> w e. y ) )
7	6	ralbii	|- ( A. z e. y z C_ y <-> A. z e. y A. w ( w e. z -> w e. y ) )
8		df-ral	|- ( A. z e. y A. w ( w e. z -> w e. y ) <-> A. z ( z e. y -> A. w ( w e. z -> w e. y ) ) )
9	5 7 8	3bitrri	|- ( A. z ( z e. y -> A. w ( w e. z -> w e. y ) ) <-> Tr y )
10	4 9	anbi12i	|- ( ( x e. y /\ A. z ( z e. y -> A. w ( w e. z -> w e. y ) ) ) <-> ( { x } C_ y /\ Tr y ) )
11	10	biimpri	|- ( ( { x } C_ y /\ Tr y ) -> ( x e. y /\ A. z ( z e. y -> A. w ( w e. z -> w e. y ) ) ) )
12	11	3adant3	|- ( ( { x } C_ y /\ Tr y /\ A. z ( ( { x } C_ z /\ Tr z ) -> y C_ z ) ) -> ( x e. y /\ A. z ( z e. y -> A. w ( w e. z -> w e. y ) ) ) )
13	2 12	eximii	|- E. y ( x e. y /\ A. z ( z e. y -> A. w ( w e. z -> w e. y ) ) )