Definition df-tp 3439

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 3433	. 2 class {𝐴, 𝐵, 𝐶}
5	1, 2	cpr 3432	. . 3 class {𝐴, 𝐵}
6	3	csn 3431	. . 3 class {𝐶}
7	5, 6	cun 2986	. 2 class ({𝐴, 𝐵} ∪ {𝐶})
8	4, 7	wceq 1287	1 wff {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})

This definition is referenced by:  eltpg  3473  raltpg  3480  rextpg  3481  tpeq1  3513  tpeq2  3514  tpeq3  3515  tpcoma  3521  tpass  3523  qdass  3524  tpidm12  3526  diftpsn3  3563  snsstp1  3572  snsstp2  3573  snsstp3  3574  prsstp12  3575  tpss  3587  tpssi  3588  ord3ex  4001  tpexg  4245  dmtpop  4874  funtpg  5032  funtp  5034  fntpg  5037  ftpg  5446  fvtp1g  5468  tpfidisj  6592  fztp  9425  sumtp  10695  bdctp  11232