Definition df-tp 3716

Description: Define unordered triple of classes. Definition of [Enderton] p. 19. (Contributed by NM, 9-Apr-1994.)

Assertion

Ref	Expression
df-tp	⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})

Detailed syntax breakdown of Definition df-tp

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cB	. . 3 class 𝐵
3		cC	. . 3 class 𝐶
4	1, 2, 3	ctp 3710	. 2 class {𝐴, 𝐵, 𝐶}
5	1, 2	cpr 3709	. . 3 class {𝐴, 𝐵}
6	3	csn 3708	. . 3 class {𝐶}
7	5, 6	cun 3218	. 2 class ({𝐴, 𝐵} ∪ {𝐶})
8	4, 7	wceq 1402	1 wff {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})

This definition is referenced by:  eltpg  3753  raltpg  3761  rextpg  3762  tpeq1  3796  tpeq2  3797  tpeq3  3798  tpcoma  3804  tpass  3806  qdass  3807  tpidm12  3809  diftpsn3  3854  snsstp1  3863  snsstp2  3864  snsstp3  3865  prsstp12  3866  tpss  3881  tpssi  3882  ord3ex  4325  tpexg  4588  dmtpop  5261  funtpg  5430  funtp  5432  fntpg  5435  ftpg  5893  fvtp1g  5917  tpfidisj  7230  tpfidceq  7231  fztp  10468  hashtpgim  11280  sumtp  12164  strle3g  13445  lsptpcl  14714  perfectlem2  16097  bdctp  16881