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

Theorem trel 4552
 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

Proof of Theorem trel
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dftr2 4547 . 2
2 eleq12 2533 . . . . . 6
3 eleq1 2529 . . . . . . 7
43adantl 466 . . . . . 6
52, 4anbi12d 710 . . . . 5
6 eleq1 2529 . . . . . 6
76adantr 465 . . . . 5
85, 7imbi12d 320 . . . 4
98spc2gv 3197 . . 3
109pm2.43b 50 . 2
111, 10sylbi 195 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  <->wb 184  /\wa 369  A.wal 1393  =wceq 1395  e.wcel 1818  Trwtr 4545 This theorem is referenced by:  trel3  4553  trintss  4561  ordn2lp  4903  ordelord  4905  tz7.7  4909  ordtr1  4926  suctr  4966  trsuc  4967  ordom  6709  elnn  6710  epfrs  8183  tcrank  8323  dfon2lem6  29220  tratrb  33307  truniALT  33312  onfrALTlem2  33318  trelded  33338  pwtrrVD  33625  suctrALT  33626  suctrALT2VD  33636  suctrALT2  33637  tratrbVD  33661  truniALTVD  33678  trintALTVD  33680  trintALT  33681  onfrALTlem2VD  33689  suctrALTcf  33722  suctrALTcfVD  33723 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435 This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-in 3482  df-ss 3489  df-uni 4250  df-tr 4546
 Copyright terms: Public domain W3C validator