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

Theorem trel 4411
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 4406 . 2  |-  ( Tr  A  <->  A. y A. x
( ( y  e.  x  /\  x  e.  A )  ->  y  e.  A ) )
2 eleq12 2505 . . . . . 6  |-  ( ( y  =  B  /\  x  =  C )  ->  ( y  e.  x  <->  B  e.  C ) )
3 eleq1 2503 . . . . . . 7  |-  ( x  =  C  ->  (
x  e.  A  <->  C  e.  A ) )
43adantl 466 . . . . . 6  |-  ( ( y  =  B  /\  x  =  C )  ->  ( x  e.  A  <->  C  e.  A ) )
52, 4anbi12d 710 . . . . 5  |-  ( ( y  =  B  /\  x  =  C )  ->  ( ( y  e.  x  /\  x  e.  A )  <->  ( B  e.  C  /\  C  e.  A ) ) )
6 eleq1 2503 . . . . . 6  |-  ( y  =  B  ->  (
y  e.  A  <->  B  e.  A ) )
76adantr 465 . . . . 5  |-  ( ( y  =  B  /\  x  =  C )  ->  ( y  e.  A  <->  B  e.  A ) )
85, 7imbi12d 320 . . . 4  |-  ( ( y  =  B  /\  x  =  C )  ->  ( ( ( y  e.  x  /\  x  e.  A )  ->  y  e.  A )  <->  ( ( B  e.  C  /\  C  e.  A )  ->  B  e.  A ) ) )
98spc2gv 3079 . . 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 50 . 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 195 1  |-  ( Tr  A  ->  ( ( B  e.  C  /\  C  e.  A )  ->  B  e.  A ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369   A.wal 1367    = wceq 1369    e. wcel 1756   Tr wtr 4404
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-v 2993  df-in 3354  df-ss 3361  df-uni 4111  df-tr 4405
This theorem is referenced by:  trel3  4412  trintss  4420  ordn2lp  4758  ordelord  4760  tz7.7  4764  ordtr1  4781  suctr  4821  trsuc  4822  ordom  6504  elnn  6505  epfrs  7970  tcrank  8110  dfon2lem6  27620  tratrb  31265  truniALT  31271  onfrALTlem2  31277  trelded  31297  pwtrrVD  31584  suctrALT  31585  suctrALT2VD  31595  suctrALT2  31596  tratrbVD  31620  truniALTVD  31637  trintALTVD  31639  trintALT  31640  onfrALTlem2VD  31648  suctrALTcf  31681  suctrALTcfVD  31682
  Copyright terms: Public domain W3C validator