Definition df-tp 3824

Description: Define unordered triple of classes. Definition of [Enderton] p. 19. (Contributed by NM, 9-Apr-1994.)

Assertion

Ref	Expression
df-tp	|- { A , B , C } = ( { A , B } u. { C } )

Detailed syntax breakdown of Definition df-tp

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3		cC	. . 3 class C
4	1, 2, 3	ctp 3818	. 2 class { A , B , C }
5	1, 2	cpr 3817	. . 3 class { A , B }
6	3	csn 3816	. . 3 class { C }
7	5, 6	cun 3320	. 2 class ( { A , B } u. { C } )
8	4, 7	wceq 1653	1 wff { A , B , C } = ( { A , B } u. { C } )

This definition is referenced by:  eltpg  3853  raltpg  3861  rextpg  3862  tpeq1  3894  tpeq2  3895  tpeq3  3896  tpcoma  3902  tpass  3904  qdass  3905  tpidm12  3907  diftpsn3  3939  tpprceq3  3940  tppreqb  3941  snsstp1  3951  snsstp2  3952  snsstp3  3953  sstp  3965  tpss  3966  tpssi  3967  ord3ex  4392  tpex  4711  fr3nr  4763  dmtpop  5349  funtpg  5504  funtp  5506  fntpg  5509  ftpg  5919  fvtp1  5942  fvtp1g  5945  tpfi  7385  fztp  11107  hashtplei  11695  hashtpg  11696  strlemor3  13563  strle3  13567  lsptpcl  16060  perfectlem2  21019  constr2spthlem1  21599  ex-un  21737  ex-ss  21740  ex-pw  21742  sltsolem1  25628  bpoly3  26109  dvh4dimlem  32315  dvhdimlem  32316  dvh4dimN  32319