This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 𝐴 → ( ( 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 ) → 𝐵 ∈ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 dftr2 ⊢ ( Tr 𝐴 ↔ ∀ 𝑦 ∀ 𝑥 ( ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴 ) → 𝑦 ∈ 𝐴 ) )
2 eleq12 ⊢ ( ( 𝑦 = 𝐵 ∧ 𝑥 = 𝐶 ) → ( 𝑦 ∈ 𝑥 ↔ 𝐵 ∈ 𝐶 ) )
3 eleq1 ⊢ ( 𝑥 = 𝐶 → ( 𝑥 ∈ 𝐴 ↔ 𝐶 ∈ 𝐴 ) )
4 3 adantl ⊢ ( ( 𝑦 = 𝐵 ∧ 𝑥 = 𝐶 ) → ( 𝑥 ∈ 𝐴 ↔ 𝐶 ∈ 𝐴 ) )
5 2 4 anbi12d ⊢ ( ( 𝑦 = 𝐵 ∧ 𝑥 = 𝐶 ) → ( ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴 ) ↔ ( 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 ) ) )
6 eleq1 ⊢ ( 𝑦 = 𝐵 → ( 𝑦 ∈ 𝐴 ↔ 𝐵 ∈ 𝐴 ) )
7 6 adantr ⊢ ( ( 𝑦 = 𝐵 ∧ 𝑥 = 𝐶 ) → ( 𝑦 ∈ 𝐴 ↔ 𝐵 ∈ 𝐴 ) )
8 5 7 imbi12d ⊢ ( ( 𝑦 = 𝐵 ∧ 𝑥 = 𝐶 ) → ( ( ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴 ) → 𝑦 ∈ 𝐴 ) ↔ ( ( 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 ) → 𝐵 ∈ 𝐴 ) ) )
9 8 spc2gv ⊢ ( ( 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 ) → ( ∀ 𝑦 ∀ 𝑥 ( ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴 ) → 𝑦 ∈ 𝐴 ) → ( ( 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 ) → 𝐵 ∈ 𝐴 ) ) )
10 9 pm2.43b ⊢ ( ∀ 𝑦 ∀ 𝑥 ( ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴 ) → 𝑦 ∈ 𝐴 ) → ( ( 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 ) → 𝐵 ∈ 𝐴 ) )
11 1 10 sylbi ⊢ ( Tr 𝐴 → ( ( 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 ) → 𝐵 ∈ 𝐴 ) )