Theorem trel 5274

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 5267	. 2 ⊢ (Tr 𝐴 ↔ ∀𝑦∀𝑥((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐴))
2		eleq12 2829	. . . . . 6 ⊢ ((𝑦 = 𝐵 ∧ 𝑥 = 𝐶) → (𝑦 ∈ 𝑥 ↔ 𝐵 ∈ 𝐶))
3		eleq1 2827	. . . . . . 7 ⊢ (𝑥 = 𝐶 → (𝑥 ∈ 𝐴 ↔ 𝐶 ∈ 𝐴))
4	3	adantl 481	. . . . . 6 ⊢ ((𝑦 = 𝐵 ∧ 𝑥 = 𝐶) → (𝑥 ∈ 𝐴 ↔ 𝐶 ∈ 𝐴))
5	2, 4	anbi12d 632	. . . . 5 ⊢ ((𝑦 = 𝐵 ∧ 𝑥 = 𝐶) → ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) ↔ (𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴)))
6		eleq1 2827	. . . . . 6 ⊢ (𝑦 = 𝐵 → (𝑦 ∈ 𝐴 ↔ 𝐵 ∈ 𝐴))
7	6	adantr 480	. . . . 5 ⊢ ((𝑦 = 𝐵 ∧ 𝑥 = 𝐶) → (𝑦 ∈ 𝐴 ↔ 𝐵 ∈ 𝐴))
8	5, 7	imbi12d 344	. . . 4 ⊢ ((𝑦 = 𝐵 ∧ 𝑥 = 𝐶) → (((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐴) ↔ ((𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) → 𝐵 ∈ 𝐴)))
9	8	spc2gv 3600	. . 3 ⊢ ((𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) → (∀𝑦∀𝑥((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐴) → ((𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) → 𝐵 ∈ 𝐴)))
10	9	pm2.43b 55	. 2 ⊢ (∀𝑦∀𝑥((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐴) → ((𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) → 𝐵 ∈ 𝐴))
11	1, 10	sylbi 217	1 ⊢ (Tr 𝐴 → ((𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) → 𝐵 ∈ 𝐴))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1535   = wceq 1537   ∈ wcel 2106  Tr wtr 5265

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-ss 3980  df-uni 4913  df-tr 5266

This theorem is referenced by:  trel3  5275  ordn2lp  6406  ordelord  6408  tz7.7  6412  ordtr1  6429  suctr  6472  trsuc  6473  trom  7896  elnn  7898  epfrs  9769  tcrank  9922  dfon2lem6  35770  tratrb  44534  truniALT  44539  onfrALTlem2  44544  trelded  44563  pwtrrVD  44823  suctrALT  44824  suctrALT2VD  44834  suctrALT2  44835  tratrbVD  44859  truniALTVD  44876  trintALTVD  44878  trintALT  44879  onfrALTlem2VD  44887  suctrALTcf  44920  suctrALTcfVD  44921  traxext  44938