Metamath Proof Explorer

Theorem dftr5OLD

Description: Obsolete version of dftr5 as of 28-Dec-2024. (Contributed by NM, 20-Mar-2004) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion dftr5OLD ⊢ 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