Definition df-tp 3623

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 3617	. 2 class { A , B , C }
5	1, 2	cpr 3616	. . 3 class { A , B }
6	3	csn 3615	. . 3 class { C }
7	5, 6	cun 3125	. 2 class ( { A , B } u. { C } )
8	4, 7	wceq 1619	1 wff { A , B , C } = ( { A , B } u. { C } )

This definition is referenced by:  eltpg  3651  raltpg  3659  rextpg  3660  tpeq1  3690  tpeq2  3691  tpeq3  3692  tpcoma  3698  tpass  3700  qdass  3701  tpidm12  3703  snsstp1  3741  snsstp2  3742  snsstp3  3743  sstp  3753  tpss  3754  ord3ex  4173  tpex  4492  fr3nr  4544  dmtpop  5121  funtp  5242  fvtp1  5659  tpfi  7101  fztp  10809  hashtplei  11347  strlemor3  13201  strle3  13205  lsptpcl  15700  perfectlem2  20433  ex-un  20756  ex-ss  20759  ex-pw  20761  axsltsolem1  23692  bpoly3  24170  ftp  26262  dvh4dimlem  30892  dvhdimlem  30893  dvh4dimN  30896