Theorem tz9.1ctco

Description: Version of tz9.1c derived from ax-tco . (Contributed by Matthew House, 6-Apr-2026)

	Ref	Expression
Hypothesis	tz9.1ctco.1	|- A e. _V
Assertion	tz9.1ctco	|- |^| { x | ( A C_ x /\ Tr x ) } e. _V

Proof

Step	Hyp	Ref	Expression
1		tz9.1ctco.1	|- A e. _V
2		axtco2g	|- ( A e. _V -> E. x ( A C_ x /\ Tr x ) )
3	1 2	ax-mp	|- E. x ( A C_ x /\ Tr x )
4		intexab	|- ( E. x ( A C_ x /\ Tr x ) <-> |^| { x | ( A C_ x /\ Tr x ) } e. _V )
5	3 4	mpbi	|- |^| { x | ( A C_ x /\ Tr x ) } e. _V