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

Theorem trel 4309
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 4304 . 2  |-  ( Tr  A  <->  A. y A. x
( ( y  e.  x  /\  x  e.  A )  ->  y  e.  A ) )
2 eleq12 2498 . . . . . 6  |-  ( ( y  =  B  /\  x  =  C )  ->  ( y  e.  x  <->  B  e.  C ) )
3 eleq1 2496 . . . . . . 7  |-  ( x  =  C  ->  (
x  e.  A  <->  C  e.  A ) )
43adantl 453 . . . . . 6  |-  ( ( y  =  B  /\  x  =  C )  ->  ( x  e.  A  <->  C  e.  A ) )
52, 4anbi12d 692 . . . . 5  |-  ( ( y  =  B  /\  x  =  C )  ->  ( ( y  e.  x  /\  x  e.  A )  <->  ( B  e.  C  /\  C  e.  A ) ) )
6 eleq1 2496 . . . . . 6  |-  ( y  =  B  ->  (
y  e.  A  <->  B  e.  A ) )
76adantr 452 . . . . 5  |-  ( ( y  =  B  /\  x  =  C )  ->  ( y  e.  A  <->  B  e.  A ) )
85, 7imbi12d 312 . . . 4  |-  ( ( y  =  B  /\  x  =  C )  ->  ( ( ( y  e.  x  /\  x  e.  A )  ->  y  e.  A )  <->  ( ( B  e.  C  /\  C  e.  A )  ->  B  e.  A ) ) )
98spc2gv 3039 . . 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 48 . 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 188 1  |-  ( Tr  A  ->  ( ( B  e.  C  /\  C  e.  A )  ->  B  e.  A ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359   A.wal 1549    = wceq 1652    e. wcel 1725   Tr wtr 4302
This theorem is referenced by:  trel3  4310  trintss  4318  ordn2lp  4601  ordelord  4603  tz7.7  4607  ordtr1  4624  suctrALT  4664  suctr  4665  trsuc  4666  ordom  4854  elnn  4855  epfrs  7667  tcrank  7808  dfon2lem6  25415  tratrb  28620  truniALT  28626  onfrALTlem2  28632  trelded  28652  pwtrrVD  28938  suctrALT2VD  28948  suctrALT2  28949  tratrbVD  28973  truniALTVD  28990  trintALTVD  28992  trintALT  28993  onfrALTlem2VD  29001  suctrALTcf  29034  suctrALTcfVD  29035
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-v 2958  df-in 3327  df-ss 3334  df-uni 4016  df-tr 4303
  Copyright terms: Public domain W3C validator