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

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.
StepHypRef Expression
1 dftr2 4904 . 2 (Tr 𝐴 ↔ ∀𝑦𝑥((𝑦𝑥𝑥𝐴) → 𝑦𝐴))
2 eleq12 2827 . . . . . 6 ((𝑦 = 𝐵𝑥 = 𝐶) → (𝑦𝑥𝐵𝐶))
3 eleq1 2825 . . . . . . 7 (𝑥 = 𝐶 → (𝑥𝐴𝐶𝐴))
43adantl 473 . . . . . 6 ((𝑦 = 𝐵𝑥 = 𝐶) → (𝑥𝐴𝐶𝐴))
52, 4anbi12d 749 . . . . 5 ((𝑦 = 𝐵𝑥 = 𝐶) → ((𝑦𝑥𝑥𝐴) ↔ (𝐵𝐶𝐶𝐴)))
6 eleq1 2825 . . . . . 6 (𝑦 = 𝐵 → (𝑦𝐴𝐵𝐴))
76adantr 472 . . . . 5 ((𝑦 = 𝐵𝑥 = 𝐶) → (𝑦𝐴𝐵𝐴))
85, 7imbi12d 333 . . . 4 ((𝑦 = 𝐵𝑥 = 𝐶) → (((𝑦𝑥𝑥𝐴) → 𝑦𝐴) ↔ ((𝐵𝐶𝐶𝐴) → 𝐵𝐴)))
98spc2gv 3434 . . 3 ((𝐵𝐶𝐶𝐴) → (∀𝑦𝑥((𝑦𝑥𝑥𝐴) → 𝑦𝐴) → ((𝐵𝐶𝐶𝐴) → 𝐵𝐴)))
109pm2.43b 55 . 2 (∀𝑦𝑥((𝑦𝑥𝑥𝐴) → 𝑦𝐴) → ((𝐵𝐶𝐶𝐴) → 𝐵𝐴))
111, 10sylbi 207 1 (Tr 𝐴 → ((𝐵𝐶𝐶𝐴) → 𝐵𝐴))
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator