![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > trel | Unicode version |
Description: In a transitive class, the membership relation is transitive. (Contributed by NM, 19-Apr-1994.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) |
Ref | Expression |
---|---|
trel |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dftr2 4547 | . 2 | |
2 | eleq12 2533 | . . . . . 6 | |
3 | eleq1 2529 | . . . . . . 7 | |
4 | 3 | adantl 466 | . . . . . 6 |
5 | 2, 4 | anbi12d 710 | . . . . 5 |
6 | eleq1 2529 | . . . . . 6 | |
7 | 6 | adantr 465 | . . . . 5 |
8 | 5, 7 | imbi12d 320 | . . . 4 |
9 | 8 | spc2gv 3197 | . . 3 |
10 | 9 | pm2.43b 50 | . 2 |
11 | 1, 10 | sylbi 195 | 1 |
Colors of variables: wff setvar class |
Syntax hints: -> wi 4 <-> wb 184
/\ wa 369 A. wal 1393 = wceq 1395
e. wcel 1818 Tr wtr 4545 |
This theorem is referenced by: trel3 4553 trintss 4561 ordn2lp 4903 ordelord 4905 tz7.7 4909 ordtr1 4926 suctr 4966 trsuc 4967 ordom 6709 elnn 6710 epfrs 8183 tcrank 8323 dfon2lem6 29220 tratrb 33307 truniALT 33312 onfrALTlem2 33318 trelded 33338 pwtrrVD 33625 suctrALT 33626 suctrALT2VD 33636 suctrALT2 33637 tratrbVD 33661 truniALTVD 33678 trintALTVD 33680 trintALT 33681 onfrALTlem2VD 33689 suctrALTcf 33722 suctrALTcfVD 33723 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1618 ax-4 1631 ax-5 1704 ax-6 1747 ax-7 1790 ax-10 1837 ax-11 1842 ax-12 1854 ax-13 1999 ax-ext 2435 |
This theorem depends on definitions: df-bi 185 df-an 371 df-tru 1398 df-ex 1613 df-nf 1617 df-sb 1740 df-clab 2443 df-cleq 2449 df-clel 2452 df-nfc 2607 df-v 3111 df-in 3482 df-ss 3489 df-uni 4250 df-tr 4546 |
Copyright terms: Public domain | W3C validator |