Definition df-tp 3699

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 3693	. 2 class {𝐴, 𝐵, 𝐶}
5	1, 2	cpr 3692	. . 3 class {𝐴, 𝐵}
6	3	csn 3691	. . 3 class {𝐶}
7	5, 6	cun 3211	. 2 class ({𝐴, 𝐵} ∪ {𝐶})
8	4, 7	wceq 1398	1 wff {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})

This definition is referenced by:  eltpg  3736  raltpg  3744  rextpg  3745  tpeq1  3779  tpeq2  3780  tpeq3  3781  tpcoma  3787  tpass  3789  qdass  3790  tpidm12  3792  diftpsn3  3837  snsstp1  3846  snsstp2  3847  snsstp3  3848  prsstp12  3849  tpss  3864  tpssi  3865  ord3ex  4305  tpexg  4567  dmtpop  5240  funtpg  5409  funtp  5411  fntpg  5414  ftpg  5870  fvtp1g  5894  tpfidisj  7191  tpfidceq  7192  fztp  10419  hashtpgim  11225  sumtp  12108  strle3g  13342  lsptpcl  14591  perfectlem2  15917  bdctp  16691