Metamath Proof Explorer

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 ⊢ A ∈ V → ∃ x A ∈ x ∧ Tr ⁡ x

Proof

Step Hyp Ref Expression
1 eleq1 ⊢ y = A → y ∈ x ↔ A ∈ x
2 dftr3 ⊢ Tr ⁡ x ↔ ∀ z ∈ x z ⊆ x
3 df-ss ⊢ z ⊆ x ↔ ∀ w w ∈ z → w ∈ x
4 3 ralbii ⊢ ∀ z ∈ x z ⊆ x ↔ ∀ z ∈ x ∀ w w ∈ z → w ∈ x
5 df-ral ⊢ ∀ z ∈ x ∀ w w ∈ z → w ∈ x ↔ ∀ z z ∈ x → ∀ w w ∈ z → w ∈ x
6 2 4 5 3bitrri ⊢ ∀ z z ∈ x → ∀ w w ∈ z → w ∈ x ↔ Tr ⁡ x
7 6 a1i ⊢ y = A → ∀ z z ∈ x → ∀ w w ∈ z → w ∈ x ↔ Tr ⁡ x
8 1 7 anbi12d ⊢ y = A → y ∈ x ∧ ∀ z z ∈ x → ∀ w w ∈ z → w ∈ x ↔ A ∈ x ∧ Tr ⁡ x
9 8 exbidv ⊢ y = A → ∃ x y ∈ x ∧ ∀ z z ∈ x → ∀ w w ∈ z → w ∈ x ↔ ∃ x A ∈ x ∧ Tr ⁡ x
10 axtco1 ⊢ ∃ x y ∈ x ∧ ∀ z z ∈ x → ∀ w w ∈ z → w ∈ x
11 9 10 vtoclg ⊢ A ∈ V → ∃ x A ∈ x ∧ Tr ⁡ x