Definition df-tp 3675

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

This definition is referenced by:  eltpg  3712  raltpg  3720  rextpg  3721  tpeq1  3755  tpeq2  3756  tpeq3  3757  tpcoma  3763  tpass  3765  qdass  3766  tpidm12  3768  diftpsn3  3812  snsstp1  3821  snsstp2  3822  snsstp3  3823  prsstp12  3824  tpss  3839  tpssi  3840  ord3ex  4278  tpexg  4539  dmtpop  5210  funtpg  5378  funtp  5380  fntpg  5383  ftpg  5833  fvtp1g  5857  tpfidisj  7116  tpfidceq  7117  fztp  10306  sumtp  11968  strle3g  13184  lsptpcl  14401  perfectlem2  15717  bdctp  16417