Definition df-bj-1upl 34305

Description: Definition of the Morse monuple (1-tuple). This is not useful per se, but is used as a step towards the definition of couples (2-tuples, or ordered pairs). The reason for "tagging" the set is so that an m-tuple and an n-tuple be equal only when m = n. Note that with this definition, the 0-tuple is the empty set. New usage is discouraged because the precise definition is generally unimportant compared to the characteristic properties bj-2upleq 34319, bj-2uplth 34328, bj-2uplex 34329, and the properties of the projections (see df-bj-pr1 34308 and df-bj-pr2 34322). (Contributed by BJ, 6-Apr-2019.) (New usage is discouraged.)

Assertion

Ref	Expression
df-bj-1upl	⊢ ⦅𝐴⦆ = ({∅} × tag 𝐴)

Detailed syntax breakdown of Definition df-bj-1upl

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2	1	bj-c1upl 34304	. 2 class ⦅𝐴⦆
3		c0 4290	. . . 4 class ∅
4	3	csn 4560	. . 3 class {∅}
5	1	bj-ctag 34281	. . 3 class tag 𝐴
6	4, 5	cxp 5547	. 2 class ({∅} × tag 𝐴)
7	2, 6	wceq 1533	1 wff ⦅𝐴⦆ = ({∅} × tag 𝐴)

This definition is referenced by:  bj-1upleq  34306  bj-pr11val  34312  bj-1uplex  34315  bj-1upln0  34316  bj-pr22val  34326  bj-2upln1upl  34331