Definition df-tp 3608

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 3602	. 2 class { A , B , C }
5	1, 2	cpr 3601	. . 3 class { A , B }
6	3	csn 3600	. . 3 class { C }
7	5, 6	cun 3111	. 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  3636  raltpg  3644  rextpg  3645  tpeq1  3675  tpeq2  3676  tpeq3  3677  tpcoma  3683  tpass  3685  qdass  3686  tpidm12  3688  snsstp1  3726  snsstp2  3727  snsstp3  3728  sstp  3738  tpss  3739  ord3ex  4158  tpex  4477  fr3nr  4529  dmtpop  5122  funtp  5227  fvtp1  5644  tpfi  7086  fztp  10793  hashtplei  11331  strlemor3  13185  strle3  13189  lsptpcl  15684  perfectlem2  20417  ex-un  20740  ex-ss  20743  ex-pw  20745  axsltsolem1  23676  bpoly3  24154  ftp  26246  dvh4dimlem  30784  dvhdimlem  30785  dvh4dimN  30788