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

Theorem trel 5267
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 5260 . 2 (Tr 𝐴 ↔ ∀𝑦𝑥((𝑦𝑥𝑥𝐴) → 𝑦𝐴))
2 eleq12 2830 . . . . . 6 ((𝑦 = 𝐵𝑥 = 𝐶) → (𝑦𝑥𝐵𝐶))
3 eleq1 2828 . . . . . . 7 (𝑥 = 𝐶 → (𝑥𝐴𝐶𝐴))
43adantl 481 . . . . . 6 ((𝑦 = 𝐵𝑥 = 𝐶) → (𝑥𝐴𝐶𝐴))
52, 4anbi12d 632 . . . . 5 ((𝑦 = 𝐵𝑥 = 𝐶) → ((𝑦𝑥𝑥𝐴) ↔ (𝐵𝐶𝐶𝐴)))
6 eleq1 2828 . . . . . 6 (𝑦 = 𝐵 → (𝑦𝐴𝐵𝐴))
76adantr 480 . . . . 5 ((𝑦 = 𝐵𝑥 = 𝐶) → (𝑦𝐴𝐵𝐴))
85, 7imbi12d 344 . . . 4 ((𝑦 = 𝐵𝑥 = 𝐶) → (((𝑦𝑥𝑥𝐴) → 𝑦𝐴) ↔ ((𝐵𝐶𝐶𝐴) → 𝐵𝐴)))
98spc2gv 3599 . . 3 ((𝐵𝐶𝐶𝐴) → (∀𝑦𝑥((𝑦𝑥𝑥𝐴) → 𝑦𝐴) → ((𝐵𝐶𝐶𝐴) → 𝐵𝐴)))
109pm2.43b 55 . 2 (∀𝑦𝑥((𝑦𝑥𝑥𝐴) → 𝑦𝐴) → ((𝐵𝐶𝐶𝐴) → 𝐵𝐴))
111, 10sylbi 217 1 (Tr 𝐴 → ((𝐵𝐶𝐶𝐴) → 𝐵𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  wal 1537   = wceq 1539  wcel 2107  Tr wtr 5258
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-v 3481  df-ss 3967  df-uni 4907  df-tr 5259
This theorem is referenced by:  trel3  5268  ordn2lp  6403  ordelord  6405  tz7.7  6409  ordtr1  6426  suctr  6469  trsuc  6470  trom  7897  elnn  7899  epfrs  9772  tcrank  9925  dfon2lem6  35790  tratrb  44561  truniALT  44566  onfrALTlem2  44571  trelded  44590  pwtrrVD  44850  suctrALT  44851  suctrALT2VD  44861  suctrALT2  44862  tratrbVD  44886  truniALTVD  44903  trintALTVD  44905  trintALT  44906  onfrALTlem2VD  44914  suctrALTcf  44947  suctrALTcfVD  44948  traxext  44999  modelac8prim  45014
  Copyright terms: Public domain W3C validator