Definition df-tp 3501

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 3495	. 2 class { A , B , C }
5	1, 2	cpr 3494	. . 3 class { A , B }
6	3	csn 3493	. . 3 class { C }
7	5, 6	cun 3035	. 2 class ( { A , B } u. { C } )
8	4, 7	wceq 1314	1 wff { A , B , C } = ( { A , B } u. { C } )

This definition is referenced by:  eltpg  3535  raltpg  3542  rextpg  3543  tpeq1  3575  tpeq2  3576  tpeq3  3577  tpcoma  3583  tpass  3585  qdass  3586  tpidm12  3588  diftpsn3  3627  snsstp1  3636  snsstp2  3637  snsstp3  3638  prsstp12  3639  tpss  3651  tpssi  3652  ord3ex  4074  tpexg  4325  dmtpop  4972  funtpg  5132  funtp  5134  fntpg  5137  ftpg  5558  fvtp1g  5582  tpfidisj  6769  fztp  9751  sumtp  11075  strle3g  11894  bdctp  12762