Theorem axtco1g

Description: Strong form of the Axiom of Transitive Containment using class variables and abbreviations. See ax-tco for more information. (Contributed by Matthew House, 6-Apr-2026)

	Ref	Expression
Assertion	axtco1g	|- ( A e. V -> E. x ( A e. x /\ Tr x ) )

Proof

Step	Hyp	Ref	Expression
1		eleq1	|- ( y = A -> ( y e. x <-> A e. x ) )
2		dftr3	|- ( Tr x <-> A. z e. x z C_ x )
3		df-ss	|- ( z C_ x <-> A. w ( w e. z -> w e. x ) )
4	3	ralbii	|- ( A. z e. x z C_ x <-> A. z e. x A. w ( w e. z -> w e. x ) )
5		df-ral	|- ( A. z e. x A. w ( w e. z -> w e. x ) <-> A. z ( z e. x -> A. w ( w e. z -> w e. x ) ) )
6	2 4 5	3bitrri	|- ( A. z ( z e. x -> A. w ( w e. z -> w e. x ) ) <-> Tr x )
7	6	a1i	|- ( y = A -> ( A. z ( z e. x -> A. w ( w e. z -> w e. x ) ) <-> Tr x ) )
8	1 7	anbi12d	|- ( y = A -> ( ( y e. x /\ A. z ( z e. x -> A. w ( w e. z -> w e. x ) ) ) <-> ( A e. x /\ Tr x ) ) )
9	8	exbidv	|- ( y = A -> ( E. x ( y e. x /\ A. z ( z e. x -> A. w ( w e. z -> w e. x ) ) ) <-> E. x ( A e. x /\ Tr x ) ) )
10		axtco1	|- E. x ( y e. x /\ A. z ( z e. x -> A. w ( w e. z -> w e. x ) ) )
11	9 10	vtoclg	|- ( A e. V -> E. x ( A e. x /\ Tr x ) )