Metamath Proof Explorer

Theorem dftr5

Description: An alternate way of defining a transitive class. (Contributed by NM, 20-Mar-2004)

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

Proof

Step Hyp Ref Expression
1 dftr2 ⊢ Tr ⁡ A ↔ ∀ y ∀ x y ∈ x ∧ x ∈ A → y ∈ A
2 alcom ⊢ ∀ y ∀ x y ∈ x ∧ x ∈ A → y ∈ A ↔ ∀ x ∀ y y ∈ x ∧ x ∈ A → y ∈ A
3 impexp ⊢ y ∈ x ∧ x ∈ A → y ∈ A ↔ y ∈ x → x ∈ A → y ∈ A
4 3 albii ⊢ ∀ y y ∈ x ∧ x ∈ A → y ∈ A ↔ ∀ y y ∈ x → x ∈ A → y ∈ A
5 df-ral ⊢ ∀ y ∈ x x ∈ A → y ∈ A ↔ ∀ y y ∈ x → x ∈ A → y ∈ A
6 4 5 bitr4i ⊢ ∀ y y ∈ x ∧ x ∈ A → y ∈ A ↔ ∀ y ∈ x x ∈ A → y ∈ A
7 r19.21v ⊢ ∀ y ∈ x x ∈ A → y ∈ A ↔ x ∈ A → ∀ y ∈ x y ∈ A
8 6 7 bitri ⊢ ∀ y y ∈ x ∧ x ∈ A → y ∈ A ↔ x ∈ A → ∀ y ∈ x y ∈ A
9 8 albii ⊢ ∀ x ∀ y y ∈ x ∧ x ∈ A → y ∈ A ↔ ∀ x x ∈ A → ∀ y ∈ x y ∈ A
10 df-ral ⊢ ∀ x ∈ A ∀ y ∈ x y ∈ A ↔ ∀ x x ∈ A → ∀ y ∈ x y ∈ A
11 9 10 bitr4i ⊢ ∀ x ∀ y y ∈ x ∧ x ∈ A → y ∈ A ↔ ∀ x ∈ A ∀ y ∈ x y ∈ A
12 2 11 bitri ⊢ ∀ y ∀ x y ∈ x ∧ x ∈ A → y ∈ A ↔ ∀ x ∈ A ∀ y ∈ x y ∈ A
13 1 12 bitri ⊢ Tr ⁡ A ↔ ∀ x ∈ A ∀ y ∈ x y ∈ A