Theorem axtco

Description: Axiom of Transitive Containment, derived as a theorem from ax-ext , ax-rep , and ax-inf2 . Use ax-tco instead. (Contributed by Matthew House, 6-Apr-2026) (New usage is discouraged.)

	Ref	Expression
Assertion	axtco	⊢ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) ) )

Proof

Step	Hyp	Ref	Expression
1		vsnex	⊢ { 𝑥 } ∈ V
2	1	tz9.1	⊢ ∃ 𝑦 ( { 𝑥 } ⊆ 𝑦 ∧ Tr 𝑦 ∧ ∀ 𝑧 ( ( { 𝑥 } ⊆ 𝑧 ∧ Tr 𝑧 ) → 𝑦 ⊆ 𝑧 ) )
3		vex	⊢ 𝑥 ∈ V
4	3	snss	⊢ ( 𝑥 ∈ 𝑦 ↔ { 𝑥 } ⊆ 𝑦 )
5		dftr3	⊢ ( Tr 𝑦 ↔ ∀ 𝑧 ∈ 𝑦 𝑧 ⊆ 𝑦 )
6		df-ss	⊢ ( 𝑧 ⊆ 𝑦 ↔ ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) )
7	6	ralbii	⊢ ( ∀ 𝑧 ∈ 𝑦 𝑧 ⊆ 𝑦 ↔ ∀ 𝑧 ∈ 𝑦 ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) )
8		df-ral	⊢ ( ∀ 𝑧 ∈ 𝑦 ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) ↔ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) ) )
9	5 7 8	3bitrri	⊢ ( ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) ) ↔ Tr 𝑦 )
10	4 9	anbi12i	⊢ ( ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) ) ) ↔ ( { 𝑥 } ⊆ 𝑦 ∧ Tr 𝑦 ) )
11	10	biimpri	⊢ ( ( { 𝑥 } ⊆ 𝑦 ∧ Tr 𝑦 ) → ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) ) ) )
12	11	3adant3	⊢ ( ( { 𝑥 } ⊆ 𝑦 ∧ Tr 𝑦 ∧ ∀ 𝑧 ( ( { 𝑥 } ⊆ 𝑧 ∧ Tr 𝑧 ) → 𝑦 ⊆ 𝑧 ) ) → ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) ) ) )
13	2 12	eximii	⊢ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) ) )