Definition df-tp 4483

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 4482	. 2 class {𝐴, 𝐵, 𝐶}
5	1, 2	cpr 4480	. . 3 class {𝐴, 𝐵}
6	3	csn 4478	. . 3 class {𝐶}
7	5, 6	cun 3863	. 2 class ({𝐴, 𝐵} ∪ {𝐶})
8	4, 7	wceq 1525	1 wff {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})

This definition is referenced by:  eltpg  4536  raltpg  4547  rextpg  4548  disjtpsn  4564  disjtp2  4565  tpeq1  4591  tpeq2  4592  tpeq3  4593  tpcoma  4599  tpass  4601  qdass  4602  tpidm12  4604  diftpsn3  4648  tpprceq3  4650  tppreqb  4651  snsstp1  4662  snsstp2  4663  snsstp3  4664  sstp  4680  tpss  4681  tpssi  4682  ord3ex  5185  dmtpop  5957  funtpg  6286  funtp  6288  fntpg  6291  funcnvtp  6294  ftpg  6788  fvtp1  6831  fvtp1g  6834  tpex  7334  fr3nr  7357  tpfi  8647  fztp  12817  hashtplei  13692  hashtpg  13693  s3tpop  14111  sumtp  14941  bpoly3  15249  strle3  16427  estrreslem2  17221  estrres  17222  lsptpcl  19445  perfectlem2  25492  ex-un  27891  ex-ss  27894  ex-pw  27896  ex-hash  27920  fnimatp  30109  prodtp  30223  sltsolem1  32791  dvh4dimlem  38131  dvhdimlem  38132  dvh4dimN  38135  tr3dom  39400  df3o2  39880  df3o3  39881  perfectALTVlem2  43391