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	⊢ ( 𝐴 ∈ 𝑉 → ∃ 𝑥 ( 𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		axtco1g	⊢ ( 𝐴 ∈ 𝑉 → ∃ 𝑥 ( 𝐴 ∈ 𝑥 ∧ Tr 𝑥 ) )
2		trss	⊢ ( Tr 𝑥 → ( 𝐴 ∈ 𝑥 → 𝐴 ⊆ 𝑥 ) )
3	2	imdistanri	⊢ ( ( 𝐴 ∈ 𝑥 ∧ Tr 𝑥 ) → ( 𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ) )
4	3	eximi	⊢ ( ∃ 𝑥 ( 𝐴 ∈ 𝑥 ∧ Tr 𝑥 ) → ∃ 𝑥 ( 𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ) )
5	1 4	syl	⊢ ( 𝐴 ∈ 𝑉 → ∃ 𝑥 ( 𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ) )