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.

Step	Hyp	Ref	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 ) )
4	3	adantl 466	. . . . . 6 |- ( ( y = B /\ x = C ) -> ( x e. A <-> C e. A ) )
5	2, 4	anbi12d 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 ) )
7	6	adantr 465	. . . . 5 |- ( ( y = B /\ x = C ) -> ( y e. A <-> B e. A ) )
8	5, 7	imbi12d 320	. . . 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 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 ) ) )
10	9	pm2.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 ) )
11	1, 10	sylbi 195	1 |- ( Tr A -> ( ( B e. C /\ C e. A ) -> B e. A ) )

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