Metamath Proof Explorer

Theorem trel3

Description: In a transitive class, the membership relation is transitive. (Contributed by NM, 19-Apr-1994)

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

Proof

Step Hyp Ref Expression
1 3anass ⊢B∈C∧C∈D∧D∈A↔B∈C∧C∈D∧D∈A
2 trel ⊢Tr⁡A→C∈D∧D∈A→C∈A
3 2 anim2d ⊢Tr⁡A→B∈C∧C∈D∧D∈A→B∈C∧C∈A
4 1 3 biimtrid ⊢Tr⁡A→B∈C∧C∈D∧D∈A→B∈C∧C∈A
5 trel ⊢Tr⁡A→B∈C∧C∈A→B∈A
6 4 5 syld ⊢Tr⁡A→B∈C∧C∈D∧D∈A→B∈A