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