Definition df-tp 3568

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 3562	. 2 class { A , B , C }
5	1, 2	cpr 3561	. . 3 class { A , B }
6	3	csn 3560	. . 3 class { C }
7	5, 6	cun 3100	. 2 class ( { A , B } u. { C } )
8	4, 7	wceq 1335	1 wff { A , B , C } = ( { A , B } u. { C } )

This definition is referenced by:  eltpg  3604  raltpg  3612  rextpg  3613  tpeq1  3645  tpeq2  3646  tpeq3  3647  tpcoma  3653  tpass  3655  qdass  3656  tpidm12  3658  diftpsn3  3697  snsstp1  3706  snsstp2  3707  snsstp3  3708  prsstp12  3709  tpss  3721  tpssi  3722  ord3ex  4150  tpexg  4402  dmtpop  5058  funtpg  5218  funtp  5220  fntpg  5223  ftpg  5648  fvtp1g  5672  tpfidisj  6865  fztp  9962  sumtp  11293  strle3g  12242  bdctp  13406