Definition df-tp 3678

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 3672	. 2 class {𝐴, 𝐵, 𝐶}
5	1, 2	cpr 3671	. . 3 class {𝐴, 𝐵}
6	3	csn 3670	. . 3 class {𝐶}
7	5, 6	cun 3197	. 2 class ({𝐴, 𝐵} ∪ {𝐶})
8	4, 7	wceq 1397	1 wff {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})

This definition is referenced by:  eltpg  3715  raltpg  3723  rextpg  3724  tpeq1  3758  tpeq2  3759  tpeq3  3760  tpcoma  3766  tpass  3768  qdass  3769  tpidm12  3771  diftpsn3  3815  snsstp1  3824  snsstp2  3825  snsstp3  3826  prsstp12  3827  tpss  3842  tpssi  3843  ord3ex  4282  tpexg  4543  dmtpop  5214  funtpg  5383  funtp  5385  fntpg  5388  ftpg  5841  fvtp1g  5865  tpfidisj  7126  tpfidceq  7127  fztp  10318  hashtpgim  11115  sumtp  11998  strle3g  13214  lsptpcl  14432  perfectlem2  15753  bdctp  16527