Theorem trel3 2701

Description: In a transitive class, the membership relation is transitive.

Assertion

Ref	Expression
trel3	⊢ (Tr A → ((B ∈ C ⋀ C ∈ D ⋀ D ∈ A) → B ∈ A))

Proof of Theorem trel3

Step	Hyp	Ref	Expression
1		trel 2700	. . . 4 ⊢ (Tr A → ((C ∈ D ⋀ D ∈ A) → C ∈ A))
2	1	anim2d 564	. . 3 ⊢ (Tr A → ((B ∈ C ⋀ (C ∈ D ⋀ D ∈ A)) → (B ∈ C ⋀ C ∈ A)))
3		3anass 783	. . 3 ⊢ ((B ∈ C ⋀ C ∈ D ⋀ D ∈ A) ↔ (B ∈ C ⋀ (C ∈ D ⋀ D ∈ A)))
4	2, 3	syl5ib 206	. 2 ⊢ (Tr A → ((B ∈ C ⋀ C ∈ D ⋀ D ∈ A) → (B ∈ C ⋀ C ∈ A)))
5		trel 2700	. 2 ⊢ (Tr A → ((B ∈ C ⋀ C ∈ A) → B ∈ A))
6	4, 5	syld 27	1 ⊢ (Tr A → ((B ∈ C ⋀ C ∈ D ⋀ D ∈ A) → B ∈ A))

Syntax hints:   → wi 3   ⋀ wa 223   ⋀ w3a 779   ∈ wcel 962  Tr wtr 2693

This theorem is referenced by:  ordelord 2984

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 966  ax-gen 967  ax-8 968  ax-10 970  ax-12 972  ax-17 975  ax-4 977  ax-5o 979  ax-6o 982  ax-9o 1129  ax-10o 1146  ax-16 1216  ax-11o 1224  ax-ext 1466

This theorem depends on definitions:  df-bi 147  df-an 225  df-3an 781  df-ex 985  df-sb 1178  df-clab 1471  df-cleq 1476  df-clel 1479  df-v 1819  df-in 2060  df-ss 2062  df-uni 2516  df-tr 2694

Copyright terms: Public domain