Metamath Proof Explorer

Theorem trel

Description: In a transitive class, the membership relation is transitive. (Contributed by NM, 19-Apr-1994) (Proof shortened by Andrew Salmon, 9-Jul-2011)

Ref Expression
Assertion trel ⊢ Tr ⁡ A → B ∈ C ∧ C ∈ A → B ∈ A

Proof

Step Hyp Ref Expression
1 dftr2 ⊢ Tr ⁡ A ↔ ∀ y ∀ x y ∈ x ∧ x ∈ A → y ∈ A
2 eleq12 ⊢ y = B ∧ x = C → y ∈ x ↔ B ∈ C
3 eleq1 ⊢ x = C → x ∈ A ↔ C ∈ A
4 3 adantl ⊢ y = B ∧ x = C → x ∈ A ↔ C ∈ A
5 2 4 anbi12d ⊢ y = B ∧ x = C → y ∈ x ∧ x ∈ A ↔ B ∈ C ∧ C ∈ A
6 eleq1 ⊢ y = B → y ∈ A ↔ B ∈ A
7 6 adantr ⊢ y = B ∧ x = C → y ∈ A ↔ B ∈ A
8 5 7 imbi12d ⊢ y = B ∧ x = C → y ∈ x ∧ x ∈ A → y ∈ A ↔ B ∈ C ∧ C ∈ A → B ∈ A
9 8 spc2gv ⊢ B ∈ C ∧ C ∈ A → ∀ y ∀ x y ∈ x ∧ x ∈ A → y ∈ A → B ∈ C ∧ C ∈ A → B ∈ A
10 9 pm2.43b ⊢ ∀ y ∀ x y ∈ x ∧ x ∈ A → y ∈ A → B ∈ C ∧ C ∈ A → B ∈ A
11 1 10 sylbi ⊢ Tr ⁡ A → B ∈ C ∧ C ∈ A → B ∈ A