Theorem axtco2g

Description: Weak 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	axtco2g	|- ( A e. V -> E. x ( A C_ x /\ Tr x ) )

Proof

Step	Hyp	Ref	Expression
1		axtco1g	|- ( A e. V -> E. x ( A e. x /\ Tr x ) )
2		trss	|- ( Tr x -> ( A e. x -> A C_ x ) )
3	2	imdistanri	|- ( ( A e. x /\ Tr x ) -> ( A C_ x /\ Tr x ) )
4	3	eximi	|- ( E. x ( A e. x /\ Tr x ) -> E. x ( A C_ x /\ Tr x ) )
5	1 4	syl	|- ( A e. V -> E. x ( A C_ x /\ Tr x ) )