Theorem trel 4909

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 4904	. 2 ⊢ (Tr 𝐴 ↔ ∀𝑦∀𝑥((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐴))
2		eleq12 2827	. . . . . 6 ⊢ ((𝑦 = 𝐵 ∧ 𝑥 = 𝐶) → (𝑦 ∈ 𝑥 ↔ 𝐵 ∈ 𝐶))
3		eleq1 2825	. . . . . . 7 ⊢ (𝑥 = 𝐶 → (𝑥 ∈ 𝐴 ↔ 𝐶 ∈ 𝐴))
4	3	adantl 473	. . . . . 6 ⊢ ((𝑦 = 𝐵 ∧ 𝑥 = 𝐶) → (𝑥 ∈ 𝐴 ↔ 𝐶 ∈ 𝐴))
5	2, 4	anbi12d 749	. . . . 5 ⊢ ((𝑦 = 𝐵 ∧ 𝑥 = 𝐶) → ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) ↔ (𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴)))
6		eleq1 2825	. . . . . 6 ⊢ (𝑦 = 𝐵 → (𝑦 ∈ 𝐴 ↔ 𝐵 ∈ 𝐴))
7	6	adantr 472	. . . . 5 ⊢ ((𝑦 = 𝐵 ∧ 𝑥 = 𝐶) → (𝑦 ∈ 𝐴 ↔ 𝐵 ∈ 𝐴))
8	5, 7	imbi12d 333	. . . 4 ⊢ ((𝑦 = 𝐵 ∧ 𝑥 = 𝐶) → (((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐴) ↔ ((𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) → 𝐵 ∈ 𝐴)))
9	8	spc2gv 3434	. . 3 ⊢ ((𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) → (∀𝑦∀𝑥((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐴) → ((𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) → 𝐵 ∈ 𝐴)))
10	9	pm2.43b 55	. 2 ⊢ (∀𝑦∀𝑥((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐴) → ((𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) → 𝐵 ∈ 𝐴))
11	1, 10	sylbi 207	1 ⊢ (Tr 𝐴 → ((𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) → 𝐵 ∈ 𝐴))

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383  ∀wal 1628   = wceq 1630   ∈ wcel 2137  Tr wtr 4902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1986  ax-6 2052  ax-7 2088  ax-9 2146  ax-10 2166  ax-11 2181  ax-12 2194  ax-13 2389  ax-ext 2738

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2045  df-clab 2745  df-cleq 2751  df-clel 2754  df-nfc 2889  df-v 3340  df-in 3720  df-ss 3727  df-uni 4587  df-tr 4903

This theorem is referenced by:  trel3  4910  trintssOLD  4920  ordn2lp  5902  ordelord  5904  tz7.7  5908  ordtr1  5926  suctr  5967  suctrOLD  5968  trsuc  5969  ordom  7237  elnn  7238  epfrs  8778  tcrank  8918  dfon2lem6  31996  tratrb  39246  truniALT  39251  onfrALTlem2  39261  trelded  39281  pwtrrVD  39557  suctrALT  39558  suctrALT2VD  39568  suctrALT2  39569  tratrbVD  39594  truniALTVD  39611  trintALTVD  39613  trintALT  39614  onfrALTlem2VD  39622  suctrALTcf  39655  suctrALTcfVD  39656