Definition df-tp 3649

Description: Define unordered triple of classes. Definition of [Enderton] p. 19. (Contributed by NM, 9-Apr-1994.)

Assertion

Ref	Expression
df-tp	|- { A , B , C } = ( { A , B } u. { C } )

Detailed syntax breakdown of Definition df-tp

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3		cC	. . 3 class C
4	1, 2, 3	ctp 3643	. 2 class { A , B , C }
5	1, 2	cpr 3642	. . 3 class { A , B }
6	3	csn 3641	. . 3 class { C }
7	5, 6	cun 3151	. 2 class ( { A , B } u. { C } )
8	4, 7	wceq 1623	1 wff { A , B , C } = ( { A , B } u. { C } )

This definition is referenced by:  eltpg  3677  raltpg  3685  rextpg  3686  tpeq1  3716  tpeq2  3717  tpeq3  3718  tpcoma  3724  tpass  3726  qdass  3727  tpidm12  3729  snsstp1  3767  snsstp2  3768  snsstp3  3769  sstp  3779  tpss  3780  ord3ex  4199  tpex  4518  fr3nr  4570  dmtpop  5147  funtp  5269  fvtp1  5686  tpfi  7128  fztp  10837  hashtplei  11376  strlemor3  13233  strle3  13237  lsptpcl  15732  perfectlem2  20465  ex-un  20788  ex-ss  20791  ex-pw  20793  axsltsolem1  23725  bpoly3  24203  ftp  26304  dvh4dimlem  30912  dvhdimlem  30913  dvh4dimN  30916