Definition df-tp 3703

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

This definition is referenced by:  eltpg  3740  raltpg  3748  rextpg  3749  tpeq1  3783  tpeq2  3784  tpeq3  3785  tpcoma  3791  tpass  3793  qdass  3794  tpidm12  3796  diftpsn3  3841  snsstp1  3850  snsstp2  3851  snsstp3  3852  prsstp12  3853  tpss  3868  tpssi  3869  ord3ex  4309  tpexg  4572  dmtpop  5245  funtpg  5414  funtp  5416  fntpg  5419  ftpg  5875  fvtp1g  5899  tpfidisj  7204  tpfidceq  7205  fztp  10439  hashtpgim  11247  sumtp  12131  strle3g  13411  lsptpcl  14675  perfectlem2  15999  bdctp  16783