Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  trel Structured version   Visualization version   GIF version

Theorem trel 4757
 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.
StepHypRef Expression
1 dftr2 4752 . 2 (Tr 𝐴 ↔ ∀𝑦𝑥((𝑦𝑥𝑥𝐴) → 𝑦𝐴))
2 eleq12 2690 . . . . . 6 ((𝑦 = 𝐵𝑥 = 𝐶) → (𝑦𝑥𝐵𝐶))
3 eleq1 2688 . . . . . . 7 (𝑥 = 𝐶 → (𝑥𝐴𝐶𝐴))
43adantl 482 . . . . . 6 ((𝑦 = 𝐵𝑥 = 𝐶) → (𝑥𝐴𝐶𝐴))
52, 4anbi12d 747 . . . . 5 ((𝑦 = 𝐵𝑥 = 𝐶) → ((𝑦𝑥𝑥𝐴) ↔ (𝐵𝐶𝐶𝐴)))
6 eleq1 2688 . . . . . 6 (𝑦 = 𝐵 → (𝑦𝐴𝐵𝐴))
76adantr 481 . . . . 5 ((𝑦 = 𝐵𝑥 = 𝐶) → (𝑦𝐴𝐵𝐴))
85, 7imbi12d 334 . . . 4 ((𝑦 = 𝐵𝑥 = 𝐶) → (((𝑦𝑥𝑥𝐴) → 𝑦𝐴) ↔ ((𝐵𝐶𝐶𝐴) → 𝐵𝐴)))
98spc2gv 3294 . . 3 ((𝐵𝐶𝐶𝐴) → (∀𝑦𝑥((𝑦𝑥𝑥𝐴) → 𝑦𝐴) → ((𝐵𝐶𝐶𝐴) → 𝐵𝐴)))
109pm2.43b 55 . 2 (∀𝑦𝑥((𝑦𝑥𝑥𝐴) → 𝑦𝐴) → ((𝐵𝐶𝐶𝐴) → 𝐵𝐴))
111, 10sylbi 207 1 (Tr 𝐴 → ((𝐵𝐶𝐶𝐴) → 𝐵𝐴))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384  ∀wal 1480   = wceq 1482   ∈ wcel 1989  Tr wtr 4750 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1485  df-ex 1704  df-nf 1709  df-sb 1880  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-v 3200  df-in 3579  df-ss 3586  df-uni 4435  df-tr 4751 This theorem is referenced by:  trel3  4758  trintssOLD  4768  ordn2lp  5741  ordelord  5743  tz7.7  5747  ordtr1  5765  suctr  5806  suctrOLD  5807  trsuc  5808  ordom  7071  elnn  7072  epfrs  8604  tcrank  8744  dfon2lem6  31677  tratrb  38572  truniALT  38577  onfrALTlem2  38587  trelded  38607  pwtrrVD  38886  suctrALT  38887  suctrALT2VD  38897  suctrALT2  38898  tratrbVD  38923  truniALTVD  38940  trintALTVD  38942  trintALT  38943  onfrALTlem2VD  38951  suctrALTcf  38984  suctrALTcfVD  38985
 Copyright terms: Public domain W3C validator