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\in V\to \exists x\left(A\subseteq x\wedge \mathrm{Tr}x\right)$$

Proof

Step	Hyp	Ref	Expression
1		axtco1g	$$⊢A\in V\to \exists x\left(A\in x\wedge \mathrm{Tr}x\right)$$
2		trss	$$⊢\mathrm{Tr}x\to \left(A\in x\to A\subseteq x\right)$$
3	2	imdistanri	$$⊢\left(A\in x\wedge \mathrm{Tr}x\right)\to \left(A\subseteq x\wedge \mathrm{Tr}x\right)$$
4	3	eximi	$$⊢\exists x\left(A\in x\wedge \mathrm{Tr}x\right)\to \exists x\left(A\subseteq x\wedge \mathrm{Tr}x\right)$$
5	1 4	syl	$$⊢A\in V\to \exists x\left(A\subseteq x\wedge \mathrm{Tr}x\right)$$