Definition df-tp 3674

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 3668	. 2 class { A , B , C }
5	1, 2	cpr 3667	. . 3 class { A , B }
6	3	csn 3666	. . 3 class { C }
7	5, 6	cun 3195	. 2 class ( { A , B } u. { C } )
8	4, 7	wceq 1395	1 wff { A , B , C } = ( { A , B } u. { C } )

This definition is referenced by:  eltpg  3711  raltpg  3719  rextpg  3720  tpeq1  3752  tpeq2  3753  tpeq3  3754  tpcoma  3760  tpass  3762  qdass  3763  tpidm12  3765  diftpsn3  3809  snsstp1  3818  snsstp2  3819  snsstp3  3820  prsstp12  3821  tpss  3836  tpssi  3837  ord3ex  4274  tpexg  4535  dmtpop  5204  funtpg  5372  funtp  5374  fntpg  5377  ftpg  5827  fvtp1g  5851  tpfidisj  7099  tpfidceq  7100  fztp  10282  sumtp  11933  strle3g  13149  lsptpcl  14366  perfectlem2  15682  bdctp  16259