Definition df-tp 3697

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 3691	. 2 class { A , B , C }
5	1, 2	cpr 3690	. . 3 class { A , B }
6	3	csn 3689	. . 3 class { C }
7	5, 6	cun 3209	. 2 class ( { A , B } u. { C } )
8	4, 7	wceq 1398	1 wff { A , B , C } = ( { A , B } u. { C } )

This definition is referenced by:  eltpg  3734  raltpg  3742  rextpg  3743  tpeq1  3777  tpeq2  3778  tpeq3  3779  tpcoma  3785  tpass  3787  qdass  3788  tpidm12  3790  diftpsn3  3835  snsstp1  3844  snsstp2  3845  snsstp3  3846  prsstp12  3847  tpss  3862  tpssi  3863  ord3ex  4303  tpexg  4565  dmtpop  5238  funtpg  5407  funtp  5409  fntpg  5412  ftpg  5868  fvtp1g  5892  tpfidisj  7189  tpfidceq  7190  fztp  10412  hashtpgim  11217  sumtp  12100  strle3g  13321  lsptpcl  14542  perfectlem2  15868  bdctp  16642