Definition df-tp 3406

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 3400	. 2 class {𝐴, 𝐵, 𝐶}
5	1, 2	cpr 3399	. . 3 class {𝐴, 𝐵}
6	3	csn 3398	. . 3 class {𝐶}
7	5, 6	cun 2971	. 2 class ({𝐴, 𝐵} ∪ {𝐶})
8	4, 7	wceq 1284	1 wff {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})

This definition is referenced by:  eltpg  3438  raltpg  3445  rextpg  3446  tpeq1  3478  tpeq2  3479  tpeq3  3480  tpcoma  3486  tpass  3488  qdass  3489  tpidm12  3491  diftpsn3  3527  snsstp1  3535  snsstp2  3536  snsstp3  3537  prsstp12  3538  tpss  3550  tpssi  3551  ord3ex  3961  tpexg  4197  dmtpop  4816  funtpg  4970  funtp  4972  fntpg  4975  ftpg  5368  fvtp1g  5390  fztp  9095  bdctp  10663