Definition df-tp 3677

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

This definition is referenced by:  eltpg  3714  raltpg  3722  rextpg  3723  tpeq1  3757  tpeq2  3758  tpeq3  3759  tpcoma  3765  tpass  3767  qdass  3768  tpidm12  3770  diftpsn3  3814  snsstp1  3823  snsstp2  3824  snsstp3  3825  prsstp12  3826  tpss  3841  tpssi  3842  ord3ex  4280  tpexg  4541  dmtpop  5212  funtpg  5381  funtp  5383  fntpg  5386  ftpg  5838  fvtp1g  5862  tpfidisj  7121  tpfidceq  7122  fztp  10313  sumtp  11977  strle3g  13193  lsptpcl  14411  perfectlem2  15727  bdctp  16488