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  4327  tpexg  4590  dmtpop  5263  funtpg  5432  funtp  5434  fntpg  5437  ftpg  5899  fvtp1g  5923  tpfidisj  7236  tpfidceq  7237  fztp  10487  hashtpgim  11299  sumtp  12183  strle3g  13464  lsptpcl  14733  perfectlem2  16120  bdctp  16910