Metamath Proof Explorer

Theorem dftr5

Description: An alternate way of defining a transitive class. Definition 1.1 of Schloeder p. 1. (Contributed by NM, 20-Mar-2004) Avoid ax-11 . (Revised by BTernaryTau, 28-Dec-2024)

Ref Expression
Assertion dftr5 ⊢ Tr ⁡ A ↔ ∀ x ∈ A ∀ y ∈ x y ∈ A

Proof

Step Hyp Ref Expression
1 impexp ⊢ y ∈ x ∧ x ∈ A → y ∈ A ↔ y ∈ x → x ∈ A → y ∈ A
2 1 albii ⊢ ∀ y y ∈ x ∧ x ∈ A → y ∈ A ↔ ∀ y y ∈ x → x ∈ A → y ∈ A
3 df-ral ⊢ ∀ y ∈ x x ∈ A → y ∈ A ↔ ∀ y y ∈ x → x ∈ A → y ∈ A
4 r19.21v ⊢ ∀ y ∈ x x ∈ A → y ∈ A ↔ x ∈ A → ∀ y ∈ x y ∈ A
5 2 3 4 3bitr2i ⊢ ∀ y y ∈ x ∧ x ∈ A → y ∈ A ↔ x ∈ A → ∀ y ∈ x y ∈ A
6 5 albii ⊢ ∀ x ∀ y y ∈ x ∧ x ∈ A → y ∈ A ↔ ∀ x x ∈ A → ∀ y ∈ x y ∈ A
7 dftr2c ⊢ Tr ⁡ A ↔ ∀ x ∀ y y ∈ x ∧ x ∈ A → y ∈ A
8 df-ral ⊢ ∀ x ∈ A ∀ y ∈ x y ∈ A ↔ ∀ x x ∈ A → ∀ y ∈ x y ∈ A
9 6 7 8 3bitr4i ⊢ Tr ⁡ A ↔ ∀ x ∈ A ∀ y ∈ x y ∈ A