Definition df-tp 3589

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 3583	. 2 class { A , B , C }
5	1, 2	cpr 3582	. . 3 class { A , B }
6	3	csn 3581	. . 3 class { C }
7	5, 6	cun 3092	. 2 class ( { A , B } u. { C } )
8	4, 7	wceq 1619	1 wff { A , B , C } = ( { A , B } u. { C } )

This definition is referenced by:  eltpg  3617  raltpg  3625  rextpg  3626  tpeq1  3656  tpeq2  3657  tpeq3  3658  tpcoma  3664  tpass  3666  qdass  3667  tpidm12  3669  snsstp1  3707  snsstp2  3708  snsstp3  3709  sstp  3719  tpss  3720  ord3ex  4138  tpex  4456  fr3nr  4508  dmtpop  5101  funtp  5206  fvtp1  5623  tpfi  7065  fztp  10772  hashtplei  11310  strlemor3  13164  strle3  13168  lsptpcl  15663  perfectlem2  20396  ex-un  20719  ex-ss  20722  ex-pw  20724  axsltsolem1  23655  bpoly3  24133  ftp  26225  dvh4dimlem  30763  dvhdimlem  30764  dvh4dimN  30767