Definition df-tp 3583

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 3577	. 2 class { A , B , C }
5	1, 2	cpr 3576	. . 3 class { A , B }
6	3	csn 3575	. . 3 class { C }
7	5, 6	cun 3113	. 2 class ( { A , B } u. { C } )
8	4, 7	wceq 1343	1 wff { A , B , C } = ( { A , B } u. { C } )

This definition is referenced by:  eltpg  3620  raltpg  3628  rextpg  3629  tpeq1  3661  tpeq2  3662  tpeq3  3663  tpcoma  3669  tpass  3671  qdass  3672  tpidm12  3674  diftpsn3  3713  snsstp1  3722  snsstp2  3723  snsstp3  3724  prsstp12  3725  tpss  3737  tpssi  3738  ord3ex  4168  tpexg  4421  dmtpop  5078  funtpg  5238  funtp  5240  fntpg  5243  ftpg  5668  fvtp1g  5692  tpfidisj  6889  fztp  10009  sumtp  11351  strle3g  12482  bdctp  13714