Definition df-tp 3578

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 3572	. 2 class {𝐴, 𝐵, 𝐶}
5	1, 2	cpr 3571	. . 3 class {𝐴, 𝐵}
6	3	csn 3570	. . 3 class {𝐶}
7	5, 6	cun 3109	. 2 class ({𝐴, 𝐵} ∪ {𝐶})
8	4, 7	wceq 1342	1 wff {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})

This definition is referenced by:  eltpg  3615  raltpg  3623  rextpg  3624  tpeq1  3656  tpeq2  3657  tpeq3  3658  tpcoma  3664  tpass  3666  qdass  3667  tpidm12  3669  diftpsn3  3708  snsstp1  3717  snsstp2  3718  snsstp3  3719  prsstp12  3720  tpss  3732  tpssi  3733  ord3ex  4163  tpexg  4416  dmtpop  5073  funtpg  5233  funtp  5235  fntpg  5238  ftpg  5663  fvtp1g  5687  tpfidisj  6884  fztp  10003  sumtp  11341  strle3g  12423  bdctp  13589