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

Theorem trel 4120
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 4115 . 2  |-  ( Tr  A  <->  A. y A. x
( ( y  e.  x  /\  x  e.  A )  ->  y  e.  A ) )
2 eleq12 2345 . . . . . 6  |-  ( ( y  =  B  /\  x  =  C )  ->  ( y  e.  x  <->  B  e.  C ) )
3 eleq1 2343 . . . . . . 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 2343 . . . . . 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 2871 . . 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 1527    = wceq 1623    e. wcel 1684   Tr wtr 4113
This theorem is referenced by:  trel3  4121  trintss  4129  ordn2lp  4412  ordelord  4414  tz7.7  4418  ordtr1  4435  suctr  4475  trsuc  4476  trsuc2OLD  4477  ordom  4665  elnn  4666  epfrs  7413  tcrank  7554  dfon2lem6  24144  fnctartar  25907  tratrb  28299  truniALT  28305  onfrALTlem2  28311  trelded  28331  pwtrrVD  28600  pwtrrOLD  28601  suctrALT2VD  28612  suctrALT2  28613  tratrbVD  28637  truniALTVD  28654  trintALTVD  28656  trintALT  28657  onfrALTlem2VD  28665  suctrALTcf  28698  suctrALTcfVD  28699  suctrALT4  28704
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-in 3159  df-ss 3166  df-uni 3828  df-tr 4114
  Copyright terms: Public domain W3C validator