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

Theorem trel 4468
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  A  ->  ( ( B  e.  C  /\  C  e.  A )  ->  B  e.  A ) )

Proof of Theorem trel
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dftr2 4463 . 2  |-  ( Tr  A  <->  A. y A. x
( ( y  e.  x  /\  x  e.  A )  ->  y  e.  A ) )
2 eleq12 2496 . . . . . 6  |-  ( ( y  =  B  /\  x  =  C )  ->  ( y  e.  x  <->  B  e.  C ) )
3 eleq1 2494 . . . . . . 7  |-  ( x  =  C  ->  (
x  e.  A  <->  C  e.  A ) )
43adantl 467 . . . . . 6  |-  ( ( y  =  B  /\  x  =  C )  ->  ( x  e.  A  <->  C  e.  A ) )
52, 4anbi12d 715 . . . . 5  |-  ( ( y  =  B  /\  x  =  C )  ->  ( ( y  e.  x  /\  x  e.  A )  <->  ( B  e.  C  /\  C  e.  A ) ) )
6 eleq1 2494 . . . . . 6  |-  ( y  =  B  ->  (
y  e.  A  <->  B  e.  A ) )
76adantr 466 . . . . 5  |-  ( ( y  =  B  /\  x  =  C )  ->  ( y  e.  A  <->  B  e.  A ) )
85, 7imbi12d 321 . . . 4  |-  ( ( y  =  B  /\  x  =  C )  ->  ( ( ( y  e.  x  /\  x  e.  A )  ->  y  e.  A )  <->  ( ( B  e.  C  /\  C  e.  A )  ->  B  e.  A ) ) )
98spc2gv 3112 . . 3  |-  ( ( B  e.  C  /\  C  e.  A )  ->  ( A. y A. x ( ( y  e.  x  /\  x  e.  A )  ->  y  e.  A )  ->  (
( B  e.  C  /\  C  e.  A
)  ->  B  e.  A ) ) )
109pm2.43b 52 . 2  |-  ( A. y A. x ( ( y  e.  x  /\  x  e.  A )  ->  y  e.  A )  ->  ( ( B  e.  C  /\  C  e.  A )  ->  B  e.  A ) )
111, 10sylbi 198 1  |-  ( Tr  A  ->  ( ( B  e.  C  /\  C  e.  A )  ->  B  e.  A ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    /\ wa 370   A.wal 1435    = wceq 1437    e. wcel 1872   Tr wtr 4461
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-v 3024  df-in 3386  df-ss 3393  df-uni 4163  df-tr 4462
This theorem is referenced by:  trel3  4469  trintss  4477  ordn2lp  5405  ordelord  5407  tz7.7  5411  ordtr1  5428  suctr  5468  trsuc  5469  ordom  6659  elnn  6660  epfrs  8167  tcrank  8307  dfon2lem6  30385  tratrb  36810  truniALT  36815  onfrALTlem2  36825  trelded  36845  pwtrrVD  37137  suctrALT  37138  suctrALT2VD  37148  suctrALT2  37149  tratrbVD  37174  truniALTVD  37191  trintALTVD  37193  trintALT  37194  onfrALTlem2VD  37202  suctrALTcf  37235  suctrALTcfVD  37236
  Copyright terms: Public domain W3C validator