Definition df-tp 3530

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 3524	. 2 class {𝐴, 𝐵, 𝐶}
5	1, 2	cpr 3523	. . 3 class {𝐴, 𝐵}
6	3	csn 3522	. . 3 class {𝐶}
7	5, 6	cun 3064	. 2 class ({𝐴, 𝐵} ∪ {𝐶})
8	4, 7	wceq 1331	1 wff {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})

This definition is referenced by:  eltpg  3564  raltpg  3571  rextpg  3572  tpeq1  3604  tpeq2  3605  tpeq3  3606  tpcoma  3612  tpass  3614  qdass  3615  tpidm12  3617  diftpsn3  3656  snsstp1  3665  snsstp2  3666  snsstp3  3667  prsstp12  3668  tpss  3680  tpssi  3681  ord3ex  4109  tpexg  4360  dmtpop  5009  funtpg  5169  funtp  5171  fntpg  5174  ftpg  5597  fvtp1g  5621  tpfidisj  6809  fztp  9851  sumtp  11176  strle3g  12040  bdctp  13059