Definition df-tp 3591

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 3585	. 2 class {𝐴, 𝐵, 𝐶}
5	1, 2	cpr 3584	. . 3 class {𝐴, 𝐵}
6	3	csn 3583	. . 3 class {𝐶}
7	5, 6	cun 3119	. 2 class ({𝐴, 𝐵} ∪ {𝐶})
8	4, 7	wceq 1348	1 wff {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})

This definition is referenced by:  eltpg  3628  raltpg  3636  rextpg  3637  tpeq1  3669  tpeq2  3670  tpeq3  3671  tpcoma  3677  tpass  3679  qdass  3680  tpidm12  3682  diftpsn3  3721  snsstp1  3730  snsstp2  3731  snsstp3  3732  prsstp12  3733  tpss  3745  tpssi  3746  ord3ex  4176  tpexg  4429  dmtpop  5086  funtpg  5249  funtp  5251  fntpg  5254  ftpg  5680  fvtp1g  5704  tpfidisj  6905  fztp  10034  sumtp  11377  strle3g  12510  bdctp  13907