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

Theorem trel 5145
 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 5140 . 2 (Tr 𝐴 ↔ ∀𝑦𝑥((𝑦𝑥𝑥𝐴) → 𝑦𝐴))
2 eleq12 2841 . . . . . 6 ((𝑦 = 𝐵𝑥 = 𝐶) → (𝑦𝑥𝐵𝐶))
3 eleq1 2839 . . . . . . 7 (𝑥 = 𝐶 → (𝑥𝐴𝐶𝐴))
43adantl 485 . . . . . 6 ((𝑦 = 𝐵𝑥 = 𝐶) → (𝑥𝐴𝐶𝐴))
52, 4anbi12d 633 . . . . 5 ((𝑦 = 𝐵𝑥 = 𝐶) → ((𝑦𝑥𝑥𝐴) ↔ (𝐵𝐶𝐶𝐴)))
6 eleq1 2839 . . . . . 6 (𝑦 = 𝐵 → (𝑦𝐴𝐵𝐴))
76adantr 484 . . . . 5 ((𝑦 = 𝐵𝑥 = 𝐶) → (𝑦𝐴𝐵𝐴))
85, 7imbi12d 348 . . . 4 ((𝑦 = 𝐵𝑥 = 𝐶) → (((𝑦𝑥𝑥𝐴) → 𝑦𝐴) ↔ ((𝐵𝐶𝐶𝐴) → 𝐵𝐴)))
98spc2gv 3519 . . 3 ((𝐵𝐶𝐶𝐴) → (∀𝑦𝑥((𝑦𝑥𝑥𝐴) → 𝑦𝐴) → ((𝐵𝐶𝐶𝐴) → 𝐵𝐴)))
109pm2.43b 55 . 2 (∀𝑦𝑥((𝑦𝑥𝑥𝐴) → 𝑦𝐴) → ((𝐵𝐶𝐶𝐴) → 𝐵𝐴))
111, 10sylbi 220 1 (Tr 𝐴 → ((𝐵𝐶𝐶𝐴) → 𝐵𝐴))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399  ∀wal 1536   = wceq 1538   ∈ wcel 2111  Tr wtr 5138 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729 This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-v 3411  df-in 3865  df-ss 3875  df-uni 4799  df-tr 5139 This theorem is referenced by:  trel3  5146  ordn2lp  6189  ordelord  6191  tz7.7  6195  ordtr1  6212  suctr  6252  trsuc  6253  ordom  7588  elnn  7589  epfrs  9206  tcrank  9346  dfon2lem6  33280  tratrb  41615  truniALT  41620  onfrALTlem2  41625  trelded  41644  pwtrrVD  41904  suctrALT  41905  suctrALT2VD  41915  suctrALT2  41916  tratrbVD  41940  truniALTVD  41957  trintALTVD  41959  trintALT  41960  onfrALTlem2VD  41968  suctrALTcf  42001  suctrALTcfVD  42002
 Copyright terms: Public domain W3C validator