Definition df-tp 3702

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

This definition is referenced by:  eltpg  3739  raltpg  3747  rextpg  3748  tpeq1  3782  tpeq2  3783  tpeq3  3784  tpcoma  3790  tpass  3792  qdass  3793  tpidm12  3795  diftpsn3  3840  snsstp1  3849  snsstp2  3850  snsstp3  3851  prsstp12  3852  tpss  3867  tpssi  3868  ord3ex  4308  tpexg  4570  dmtpop  5243  funtpg  5412  funtp  5414  fntpg  5417  ftpg  5873  fvtp1g  5897  tpfidisj  7202  tpfidceq  7203  fztp  10437  hashtpgim  11245  sumtp  12128  strle3g  13408  lsptpcl  14671  perfectlem2  15997  bdctp  16781