Definition df-tp 3615

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 3609	. 2 class {𝐴, 𝐵, 𝐶}
5	1, 2	cpr 3608	. . 3 class {𝐴, 𝐵}
6	3	csn 3607	. . 3 class {𝐶}
7	5, 6	cun 3142	. 2 class ({𝐴, 𝐵} ∪ {𝐶})
8	4, 7	wceq 1364	1 wff {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})

This definition is referenced by:  eltpg  3652  raltpg  3660  rextpg  3661  tpeq1  3693  tpeq2  3694  tpeq3  3695  tpcoma  3701  tpass  3703  qdass  3704  tpidm12  3706  diftpsn3  3748  snsstp1  3757  snsstp2  3758  snsstp3  3759  prsstp12  3760  tpss  3773  tpssi  3774  ord3ex  4205  tpexg  4459  dmtpop  5119  funtpg  5283  funtp  5285  fntpg  5288  ftpg  5717  fvtp1g  5741  tpfidisj  6946  fztp  10098  sumtp  11442  strle3g  12593  lsptpcl  13678  bdctp  15028