Definition df-tp 3674

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 3668	. 2 class {𝐴, 𝐵, 𝐶}
5	1, 2	cpr 3667	. . 3 class {𝐴, 𝐵}
6	3	csn 3666	. . 3 class {𝐶}
7	5, 6	cun 3195	. 2 class ({𝐴, 𝐵} ∪ {𝐶})
8	4, 7	wceq 1395	1 wff {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})

This definition is referenced by:  eltpg  3711  raltpg  3719  rextpg  3720  tpeq1  3752  tpeq2  3753  tpeq3  3754  tpcoma  3760  tpass  3762  qdass  3763  tpidm12  3765  diftpsn3  3809  snsstp1  3818  snsstp2  3819  snsstp3  3820  prsstp12  3821  tpss  3836  tpssi  3837  ord3ex  4275  tpexg  4536  dmtpop  5207  funtpg  5375  funtp  5377  fntpg  5380  ftpg  5830  fvtp1g  5854  tpfidisj  7107  tpfidceq  7108  fztp  10291  sumtp  11946  strle3g  13162  lsptpcl  14379  perfectlem2  15695  bdctp  16344