Definition df-tp 3414

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 3408	. 2 class { A , B , C }
5	1, 2	cpr 3407	. . 3 class { A , B }
6	3	csn 3406	. . 3 class { C }
7	5, 6	cun 2972	. 2 class ( { A , B } u. { C } )
8	4, 7	wceq 1285	1 wff { A , B , C } = ( { A , B } u. { C } )

This definition is referenced by:  eltpg  3446  raltpg  3453  rextpg  3454  tpeq1  3486  tpeq2  3487  tpeq3  3488  tpcoma  3494  tpass  3496  qdass  3497  tpidm12  3499  diftpsn3  3535  snsstp1  3543  snsstp2  3544  snsstp3  3545  prsstp12  3546  tpss  3558  tpssi  3559  ord3ex  3969  tpexg  4205  dmtpop  4826  funtpg  4981  funtp  4983  fntpg  4986  ftpg  5379  fvtp1g  5401  fztp  9171  bdctp  10821