![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > df-tp | Unicode version |
Description: Define unordered triple of classes. Definition of [Enderton] p. 19. (Contributed by NM, 9-Apr-1994.) |
Ref | Expression |
---|---|
df-tp |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA |
. . 3
![]() ![]() | |
2 | cB |
. . 3
![]() ![]() | |
3 | cC |
. . 3
![]() ![]() | |
4 | 1, 2, 3 | ctp 3776 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 2 | cpr 3775 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() |
6 | 3 | csn 3774 |
. . 3
![]() ![]() ![]() ![]() |
7 | 5, 6 | cun 3278 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | 4, 7 | wceq 1649 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: eltpg 3811 raltpg 3819 rextpg 3820 tpeq1 3852 tpeq2 3853 tpeq3 3854 tpcoma 3860 tpass 3862 qdass 3863 tpidm12 3865 diftpsn3 3897 tpprceq3 3898 tppreqb 3899 snsstp1 3909 snsstp2 3910 snsstp3 3911 sstp 3923 tpss 3924 tpssi 3925 ord3ex 4349 tpex 4667 fr3nr 4719 dmtpop 5305 funtpg 5460 funtp 5462 fntpg 5465 ftpg 5875 fvtp1 5898 fvtp1g 5901 tpfi 7341 fztp 11058 hashtplei 11645 hashtpg 11646 strlemor3 13513 strle3 13517 lsptpcl 16010 perfectlem2 20967 constr2spthlem1 21547 ex-un 21685 ex-ss 21688 ex-pw 21690 sltsolem1 25536 bpoly3 26008 dvh4dimlem 31926 dvhdimlem 31927 dvh4dimN 31930 |
Copyright terms: Public domain | W3C validator |