Definition df-tp 3597

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 3591	. 2 class {𝐴, 𝐵, 𝐶}
5	1, 2	cpr 3590	. . 3 class {𝐴, 𝐵}
6	3	csn 3589	. . 3 class {𝐶}
7	5, 6	cun 3125	. 2 class ({𝐴, 𝐵} ∪ {𝐶})
8	4, 7	wceq 1353	1 wff {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})

This definition is referenced by:  eltpg  3634  raltpg  3642  rextpg  3643  tpeq1  3675  tpeq2  3676  tpeq3  3677  tpcoma  3683  tpass  3685  qdass  3686  tpidm12  3688  diftpsn3  3730  snsstp1  3739  snsstp2  3740  snsstp3  3741  prsstp12  3742  tpss  3754  tpssi  3755  ord3ex  4185  tpexg  4438  dmtpop  5096  funtpg  5259  funtp  5261  fntpg  5264  ftpg  5692  fvtp1g  5716  tpfidisj  6917  fztp  10046  sumtp  11388  strle3g  12521  bdctp  14164