Definition df-tp 3535

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 3529	. 2 class { A , B , C }
5	1, 2	cpr 3528	. . 3 class { A , B }
6	3	csn 3527	. . 3 class { C }
7	5, 6	cun 3069	. 2 class ( { A , B } u. { C } )
8	4, 7	wceq 1331	1 wff { A , B , C } = ( { A , B } u. { C } )

This definition is referenced by:  eltpg  3569  raltpg  3576  rextpg  3577  tpeq1  3609  tpeq2  3610  tpeq3  3611  tpcoma  3617  tpass  3619  qdass  3620  tpidm12  3622  diftpsn3  3661  snsstp1  3670  snsstp2  3671  snsstp3  3672  prsstp12  3673  tpss  3685  tpssi  3686  ord3ex  4114  tpexg  4365  dmtpop  5014  funtpg  5174  funtp  5176  fntpg  5179  ftpg  5604  fvtp1g  5628  tpfidisj  6816  fztp  9858  sumtp  11183  strle3g  12051  bdctp  13070