Definition df-tp 3696

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 3690	. 2 class {𝐴, 𝐵, 𝐶}
5	1, 2	cpr 3689	. . 3 class {𝐴, 𝐵}
6	3	csn 3688	. . 3 class {𝐶}
7	5, 6	cun 3208	. 2 class ({𝐴, 𝐵} ∪ {𝐶})
8	4, 7	wceq 1398	1 wff {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})

This definition is referenced by:  eltpg  3733  raltpg  3741  rextpg  3742  tpeq1  3776  tpeq2  3777  tpeq3  3778  tpcoma  3784  tpass  3786  qdass  3787  tpidm12  3789  diftpsn3  3834  snsstp1  3843  snsstp2  3844  snsstp3  3845  prsstp12  3846  tpss  3861  tpssi  3862  ord3ex  4302  tpexg  4564  dmtpop  5237  funtpg  5406  funtp  5408  fntpg  5411  ftpg  5867  fvtp1g  5891  tpfidisj  7188  tpfidceq  7189  fztp  10408  hashtpgim  11210  sumtp  12093  strle3g  13310  lsptpcl  14529  perfectlem2  15855  bdctp  16629