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

Theorem trel 4157
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 4152 . 2  |-  ( Tr  A  <->  A. y A. x
( ( y  e.  x  /\  x  e.  A )  ->  y  e.  A ) )
2 eleq12 2378 . . . . . 6  |-  ( ( y  =  B  /\  x  =  C )  ->  ( y  e.  x  <->  B  e.  C ) )
3 eleq1 2376 . . . . . . 7  |-  ( x  =  C  ->  (
x  e.  A  <->  C  e.  A ) )
43adantl 452 . . . . . 6  |-  ( ( y  =  B  /\  x  =  C )  ->  ( x  e.  A  <->  C  e.  A ) )
52, 4anbi12d 691 . . . . 5  |-  ( ( y  =  B  /\  x  =  C )  ->  ( ( y  e.  x  /\  x  e.  A )  <->  ( B  e.  C  /\  C  e.  A ) ) )
6 eleq1 2376 . . . . . 6  |-  ( y  =  B  ->  (
y  e.  A  <->  B  e.  A ) )
76adantr 451 . . . . 5  |-  ( ( y  =  B  /\  x  =  C )  ->  ( y  e.  A  <->  B  e.  A ) )
85, 7imbi12d 311 . . . 4  |-  ( ( y  =  B  /\  x  =  C )  ->  ( ( ( y  e.  x  /\  x  e.  A )  ->  y  e.  A )  <->  ( ( B  e.  C  /\  C  e.  A )  ->  B  e.  A ) ) )
98spc2gv 2905 . . 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 46 . 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 187 1  |-  ( Tr  A  ->  ( ( B  e.  C  /\  C  e.  A )  ->  B  e.  A ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358   A.wal 1531    = wceq 1633    e. wcel 1701   Tr wtr 4150
This theorem is referenced by:  trel3  4158  trintss  4166  ordn2lp  4449  ordelord  4451  tz7.7  4455  ordtr1  4472  suctr  4512  trsuc  4513  trsuc2OLD  4514  ordom  4702  elnn  4703  epfrs  7458  tcrank  7599  dfon2lem6  24529  tratrb  27793  truniALT  27799  onfrALTlem2  27805  trelded  27825  pwtrrVD  28111  pwtrrOLD  28112  suctrALT2VD  28123  suctrALT2  28124  tratrbVD  28148  truniALTVD  28165  trintALTVD  28167  trintALT  28168  onfrALTlem2VD  28176  suctrALTcf  28209  suctrALTcfVD  28210  suctrALT4  28215
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-v 2824  df-in 3193  df-ss 3200  df-uni 3865  df-tr 4151
  Copyright terms: Public domain W3C validator