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

Proof

Step	Hyp	Ref	Expression
1		eleq1	⊢ ( 𝑦 = 𝐴 → ( 𝑦 ∈ 𝑥 ↔ 𝐴 ∈ 𝑥 ) )
2		dftr3	⊢ ( Tr 𝑥 ↔ ∀ 𝑧 ∈ 𝑥 𝑧 ⊆ 𝑥 )
3		df-ss	⊢ ( 𝑧 ⊆ 𝑥 ↔ ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) )
4	3	ralbii	⊢ ( ∀ 𝑧 ∈ 𝑥 𝑧 ⊆ 𝑥 ↔ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) )
5		df-ral	⊢ ( ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) ↔ ∀ 𝑧 ( 𝑧 ∈ 𝑥 → ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) ) )
6	2 4 5	3bitrri	⊢ ( ∀ 𝑧 ( 𝑧 ∈ 𝑥 → ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) ) ↔ Tr 𝑥 )
7	6	a1i	⊢ ( 𝑦 = 𝐴 → ( ∀ 𝑧 ( 𝑧 ∈ 𝑥 → ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) ) ↔ Tr 𝑥 ) )
8	1 7	anbi12d	⊢ ( 𝑦 = 𝐴 → ( ( 𝑦 ∈ 𝑥 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑥 → ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) ) ) ↔ ( 𝐴 ∈ 𝑥 ∧ Tr 𝑥 ) ) )
9	8	exbidv	⊢ ( 𝑦 = 𝐴 → ( ∃ 𝑥 ( 𝑦 ∈ 𝑥 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑥 → ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) ) ) ↔ ∃ 𝑥 ( 𝐴 ∈ 𝑥 ∧ Tr 𝑥 ) ) )
10		axtco1	⊢ ∃ 𝑥 ( 𝑦 ∈ 𝑥 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑥 → ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) ) )
11	9 10	vtoclg	⊢ ( 𝐴 ∈ 𝑉 → ∃ 𝑥 ( 𝐴 ∈ 𝑥 ∧ Tr 𝑥 ) )