Definition df-tp 3717

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 3711	. 2 class {𝐴, 𝐵, 𝐶}
5	1, 2	cpr 3710	. . 3 class {𝐴, 𝐵}
6	3	csn 3709	. . 3 class {𝐶}
7	5, 6	cun 3218	. 2 class ({𝐴, 𝐵} ∪ {𝐶})
8	4, 7	wceq 1402	1 wff {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})

This definition is used by:  eltpg  3754  raltpg  3762  rextpg  3763  tpeq1  3797  tpeq2  3798  tpeq3  3799  tpcoma  3805  tpass  3807  qdass  3808  tpidm12  3810  diftpsn3  3856  snsstp1  3865  snsstp2  3866  snsstp3  3867  prsstp12  3868  tpss  3883  tpssi  3884  ord3ex  4329  tpexg  4592  dmtpop  5266  funtpg  5435  funtp  5437  fntpg  5440  ftpg  5902  fvtp1g  5926  tpfidisj  7241  tpfidceq  7242  fztp  10503  hashtpgim  11320  sumtp  12207  strle3g  13522  lsptpcl  14841  perfectlem2  16312  bdctp  17115