Definition df-tp 3383

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 3377	. 2 class { A , B , C }
5	1, 2	cpr 3376	. . 3 class { A , B }
6	3	csn 3375	. . 3 class { C }
7	5, 6	cun 2915	. 2 class ( { A , B } u. { C } )
8	4, 7	wceq 1243	1 wff { A , B , C } = ( { A , B } u. { C } )

This definition is referenced by:  eltpg  3416  raltpg  3423  rextpg  3424  tpeq1  3456  tpeq2  3457  tpeq3  3458  tpcoma  3464  tpass  3466  qdass  3467  tpidm12  3469  diftpsn3  3505  snsstp1  3514  snsstp2  3515  snsstp3  3516  prsstp12  3517  tpss  3529  tpssi  3530  ord3ex  3941  tpexg  4179  dmtpop  4796  funtpg  4950  funtp  4952  fntpg  4955  ftpg  5347  fvtp1g  5369  fztp  8940  bdctp  9992