Theorem trel 4468

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 4463	. 2 |- ( Tr A <-> A. y A. x ( ( y e. x /\ x e. A ) -> y e. A ) )
2		eleq12 2496	. . . . . 6 |- ( ( y = B /\ x = C ) -> ( y e. x <-> B e. C ) )
3		eleq1 2494	. . . . . . 7 |- ( x = C -> ( x e. A <-> C e. A ) )
4	3	adantl 467	. . . . . 6 |- ( ( y = B /\ x = C ) -> ( x e. A <-> C e. A ) )
5	2, 4	anbi12d 715	. . . . 5 |- ( ( y = B /\ x = C ) -> ( ( y e. x /\ x e. A ) <-> ( B e. C /\ C e. A ) ) )
6		eleq1 2494	. . . . . 6 |- ( y = B -> ( y e. A <-> B e. A ) )
7	6	adantr 466	. . . . 5 |- ( ( y = B /\ x = C ) -> ( y e. A <-> B e. A ) )
8	5, 7	imbi12d 321	. . . 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 3112	. . 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 198	1 |- ( Tr A -> ( ( B e. C /\ C e. A ) -> B e. A ) )

Syntax hints:   -> wi 4   <-> wb 187   /\ wa 370   A.wal 1435   = wceq 1437   e. wcel 1872   Tr wtr 4461

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408

This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-v 3024  df-in 3386  df-ss 3393  df-uni 4163  df-tr 4462

This theorem is referenced by:  trel3  4469  trintss  4477  ordn2lp  5405  ordelord  5407  tz7.7  5411  ordtr1  5428  suctr  5468  trsuc  5469  ordom  6659  elnn  6660  epfrs  8167  tcrank  8307  dfon2lem6  30385  tratrb  36810  truniALT  36815  onfrALTlem2  36825  trelded  36845  pwtrrVD  37137  suctrALT  37138  suctrALT2VD  37148  suctrALT2  37149  tratrbVD  37174  truniALTVD  37191  trintALTVD  37193  trintALT  37194  onfrALTlem2VD  37202  suctrALTcf  37235  suctrALTcfVD  37236