Definition df-tp 3782

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 3776	. 2 class { A , B , C }
5	1, 2	cpr 3775	. . 3 class { A , B }
6	3	csn 3774	. . 3 class { C }
7	5, 6	cun 3278	. 2 class ( { A , B } u. { C } )
8	4, 7	wceq 1649	1 wff { A , B , C } = ( { A , B } u. { C } )

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