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

Theorem trel 5170
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 5165 . 2 (Tr 𝐴 ↔ ∀𝑦𝑥((𝑦𝑥𝑥𝐴) → 𝑦𝐴))
2 eleq12 2899 . . . . . 6 ((𝑦 = 𝐵𝑥 = 𝐶) → (𝑦𝑥𝐵𝐶))
3 eleq1 2897 . . . . . . 7 (𝑥 = 𝐶 → (𝑥𝐴𝐶𝐴))
43adantl 482 . . . . . 6 ((𝑦 = 𝐵𝑥 = 𝐶) → (𝑥𝐴𝐶𝐴))
52, 4anbi12d 630 . . . . 5 ((𝑦 = 𝐵𝑥 = 𝐶) → ((𝑦𝑥𝑥𝐴) ↔ (𝐵𝐶𝐶𝐴)))
6 eleq1 2897 . . . . . 6 (𝑦 = 𝐵 → (𝑦𝐴𝐵𝐴))
76adantr 481 . . . . 5 ((𝑦 = 𝐵𝑥 = 𝐶) → (𝑦𝐴𝐵𝐴))
85, 7imbi12d 346 . . . 4 ((𝑦 = 𝐵𝑥 = 𝐶) → (((𝑦𝑥𝑥𝐴) → 𝑦𝐴) ↔ ((𝐵𝐶𝐶𝐴) → 𝐵𝐴)))
98spc2gv 3598 . . 3 ((𝐵𝐶𝐶𝐴) → (∀𝑦𝑥((𝑦𝑥𝑥𝐴) → 𝑦𝐴) → ((𝐵𝐶𝐶𝐴) → 𝐵𝐴)))
109pm2.43b 55 . 2 (∀𝑦𝑥((𝑦𝑥𝑥𝐴) → 𝑦𝐴) → ((𝐵𝐶𝐶𝐴) → 𝐵𝐴))
111, 10sylbi 218 1 (Tr 𝐴 → ((𝐵𝐶𝐶𝐴) → 𝐵𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396  wal 1526   = wceq 1528  wcel 2105  Tr wtr 5163
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-v 3494  df-in 3940  df-ss 3949  df-uni 4831  df-tr 5164
This theorem is referenced by:  trel3  5171  ordn2lp  6204  ordelord  6206  tz7.7  6210  ordtr1  6227  suctr  6267  trsuc  6268  ordom  7578  elnn  7579  epfrs  9161  tcrank  9301  dfon2lem6  32930  tratrb  40747  truniALT  40752  onfrALTlem2  40757  trelded  40776  pwtrrVD  41036  suctrALT  41037  suctrALT2VD  41047  suctrALT2  41048  tratrbVD  41072  truniALTVD  41089  trintALTVD  41091  trintALT  41092  onfrALTlem2VD  41100  suctrALTcf  41133  suctrALTcfVD  41134
  Copyright terms: Public domain W3C validator