Theorem trel 4517

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.

Step	Hyp	Ref	Expression
1		dftr2 4512	. 2 |- ( Tr A <-> A. y A. x ( ( y e. x /\ x e. A ) -> y e. A ) )
2		eleq12 2529	. . . . . 6 |- ( ( y = B /\ x = C ) -> ( y e. x <-> B e. C ) )
3		eleq1 2527	. . . . . . 7 |- ( x = C -> ( x e. A <-> C e. A ) )
4	3	adantl 472	. . . . . 6 |- ( ( y = B /\ x = C ) -> ( x e. A <-> C e. A ) )
5	2, 4	anbi12d 722	. . . . 5 |- ( ( y = B /\ x = C ) -> ( ( y e. x /\ x e. A ) <-> ( B e. C /\ C e. A ) ) )
6		eleq1 2527	. . . . . 6 |- ( y = B -> ( y e. A <-> B e. A ) )
7	6	adantr 471	. . . . 5 |- ( ( y = B /\ x = C ) -> ( y e. A <-> B e. A ) )
8	5, 7	imbi12d 326	. . . 4 |- ( ( y = B /\ x = C ) -> ( ( ( y e. x /\ x e. A ) -> y e. A ) <-> ( ( B e. C /\ C e. A ) -> B e. A ) ) )
9	8	spc2gv 3148	. . 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 ) ) )
10	9	pm2.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 ) )
11	1, 10	sylbi 200	1 |- ( Tr A -> ( ( B e. C /\ C e. A ) -> B e. A ) )

Syntax hints:   -> wi 4   <-> wb 189   /\ wa 375   A.wal 1452   = wceq 1454   e. wcel 1897   Tr wtr 4510

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441

This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-v 3058  df-in 3422  df-ss 3429  df-uni 4212  df-tr 4511

This theorem is referenced by:  trel3  4518  trintss  4526  ordn2lp  5461  ordelord  5463  tz7.7  5467  ordtr1  5484  suctr  5524  trsuc  5525  ordom  6727  elnn  6728  epfrs  8240  tcrank  8380  dfon2lem6  30482  tratrb  36940  truniALT  36945  onfrALTlem2  36955  trelded  36975  pwtrrVD  37260  suctrALT  37261  suctrALT2VD  37271  suctrALT2  37272  tratrbVD  37297  truniALTVD  37314  trintALTVD  37316  trintALT  37317  onfrALTlem2VD  37325  suctrALTcf  37358  suctrALTcfVD  37359