Theorem trel 5226

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

Assertion

Ref	Expression
trel	⊢ (Tr 𝐴 → ((𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) → 𝐵 ∈ 𝐴))

Proof of Theorem trel

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		dftr2 5219	. 2 ⊢ (Tr 𝐴 ↔ ∀𝑦∀𝑥((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐴))
2		eleq12 2819	. . . . . 6 ⊢ ((𝑦 = 𝐵 ∧ 𝑥 = 𝐶) → (𝑦 ∈ 𝑥 ↔ 𝐵 ∈ 𝐶))
3		eleq1 2817	. . . . . . 7 ⊢ (𝑥 = 𝐶 → (𝑥 ∈ 𝐴 ↔ 𝐶 ∈ 𝐴))
4	3	adantl 481	. . . . . 6 ⊢ ((𝑦 = 𝐵 ∧ 𝑥 = 𝐶) → (𝑥 ∈ 𝐴 ↔ 𝐶 ∈ 𝐴))
5	2, 4	anbi12d 632	. . . . 5 ⊢ ((𝑦 = 𝐵 ∧ 𝑥 = 𝐶) → ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) ↔ (𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴)))
6		eleq1 2817	. . . . . 6 ⊢ (𝑦 = 𝐵 → (𝑦 ∈ 𝐴 ↔ 𝐵 ∈ 𝐴))
7	6	adantr 480	. . . . 5 ⊢ ((𝑦 = 𝐵 ∧ 𝑥 = 𝐶) → (𝑦 ∈ 𝐴 ↔ 𝐵 ∈ 𝐴))
8	5, 7	imbi12d 344	. . . 4 ⊢ ((𝑦 = 𝐵 ∧ 𝑥 = 𝐶) → (((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐴) ↔ ((𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) → 𝐵 ∈ 𝐴)))
9	8	spc2gv 3569	. . 3 ⊢ ((𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) → (∀𝑦∀𝑥((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐴) → ((𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) → 𝐵 ∈ 𝐴)))
10	9	pm2.43b 55	. 2 ⊢ (∀𝑦∀𝑥((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐴) → ((𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) → 𝐵 ∈ 𝐴))
11	1, 10	sylbi 217	1 ⊢ (Tr 𝐴 → ((𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) → 𝐵 ∈ 𝐴))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1538   = wceq 1540   ∈ wcel 2109  Tr wtr 5217

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-ss 3934  df-uni 4875  df-tr 5218

This theorem is referenced by:  trel3  5227  ordn2lp  6355  ordelord  6357  tz7.7  6361  ordtr1  6379  suctr  6423  trsuc  6424  trom  7854  elnn  7856  epfrs  9691  tcrank  9844  dfon2lem6  35783  tratrb  44533  truniALT  44538  onfrALTlem2  44543  trelded  44562  pwtrrVD  44821  suctrALT  44822  suctrALT2VD  44832  suctrALT2  44833  tratrbVD  44857  truniALTVD  44874  trintALTVD  44876  trintALT  44877  onfrALTlem2VD  44885  suctrALTcf  44918  suctrALTcfVD  44919  traxext  44974  modelac8prim  44989