conventions-labels

Description:

The following gives conventions used in the Metamath Proof Explorer (MPE, set.mm) regarding labels. For other conventions, see conventions and links therein.

Every statement has a unique identifying label, which serves the same purpose as an equation number in a book. We use various label naming conventions to provide easy-to-remember hints about their contents. Labels are not a 1-to-1 mapping, because that would create long names that would be difficult to remember and tedious to type. Instead, label names are relatively short while suggesting their purpose. Names are occasionally changed to make them more consistent or as we find better ways to name them. Here are a few of the label naming conventions:

Axioms, definitions, and wff syntax. As noted earlier, axioms are named "ax-NAME", proofs of proven axioms are named "axNAME", and definitions are named "df-NAME". Wff syntax declarations have labels beginning with "w" followed by short fragment suggesting its purpose.

Hypotheses. Hypotheses have the name of the final axiom or theorem, followed by ".", followed by a unique id (these ids are usually consecutive integers starting with 1, e.g. for rgen "rgen.1 $e |- ( x e. A -> ph ) $." or letters corresponding to the (main) class variable used in the hypothesis, e.g. for mdet0 : "mdet0.d $e |- D = ( N maDet R ) $.").

Common names. If a theorem has a well-known name, that name (or a short version of it) is sometimes used directly. Examples include barbara and stirling .

Principia Mathematica. Proofs of theorems from Principia Mathematica often use a special naming convention: "pm" followed by its identifier. For example, Theorem *2.27 of WhiteheadRussell p. 104 is named pm2.27 .

19.x series of theorems. Similar to the conventions for the theorems from Principia Mathematica, theorems from Section 19 of Margaris p. 90 often use a special naming convention: "19." resp. "r19." (for corresponding restricted quantifier versions) followed by its identifier. For example, Theorem 38 from Section 19 of Margaris p. 90 is labeled 19.38 , and the restricted quantifier version of Theorem 21 from Section 19 of Margaris p. 90 is labeled r19.21 .

Characters to be used for labels. Although the specification of Metamath allows for dots/periods "." in any label, it is usually used only in labels for hypotheses (see above). Exceptions are the labels of theorems from Principia Mathematica and the 19.x series of theorems from Section 19 of Margaris p. 90 (see above) and 0.999... . Furthermore, the underscore "_" should not be used. Finally, only lower case characters should be used (except the special suffixes OLD, ALT, and ALTV mentioned in bullet point "Suffixes"), at least in main set.mm (exceptions are tolerated in mathboxes).

Syntax label fragments. Most theorems are named using a concatenation of syntax label fragments (omitting variables) that represent the important part of the theorem's main conclusion. Almost every syntactic construct has a definition labeled "df-NAME", and normally NAME is the syntax label fragment. For example, the class difference construct ( A \ B ) is defined in df-dif , and thus its syntax label fragment is "dif". Similarly, the subclass relation A C_ B has syntax label fragment "ss" because it is defined in df-ss . Most theorem names follow from these fragments, for example, the theorem proving ( A \ B ) C_ A involves a class difference ("dif") of a subset ("ss"), and thus is labeled difss . There are many other syntax label fragments, e.g., singleton construct { A } has syntax label fragment "sn" (because it is defined in df-sn ), and the pair construct { A , B } has fragment "pr" ( from df-pr ). Digits are used to represent themselves. Suffixes (e.g., with numbers) are sometimes used to distinguish multiple theorems that would otherwise produce the same label.

Phantom definitions. In some cases there are common label fragments for something that could be in a definition, but for technical reasons is not. The is-element-of (is member of) construct A e. B does not have a df-NAME definition; in this case its syntax label fragment is "el". Thus, because the theorem beginning with ( A e. ( B \ { C } ) uses is-element-of ("el") of a class difference ("dif") of a singleton ("sn"), it is labeled eldifsn . An "n" is often used for negation ( -. ), e.g., nan .

Exceptions. Sometimes there is a definition df-NAME but the label fragment is not the NAME part. The definition should note this exception as part of its definition. In addition, the table below attempts to list all such cases and marks them in bold. For example, the label fragment "cn" represents complex numbers CC (even though its definition is in df-c ) and "re" represents real numbers RR (Definition df-r ). The empty set (/) often uses fragment 0, even though it is defined in df-nul . The syntax construct ( A + B ) usually uses the fragment "add" (which is consistent with df-add ), but "p" is used as the fragment for constant theorems. Equality ( A = B ) often uses "e" as the fragment. As a result, "two plus two equals four" is labeled 2p2e4 .

Other markings. In labels we sometimes use "com" for "commutative", "ass" for "associative", "rot" for "rotation", and "di" for "distributive".

Focus on the important part of the conclusion. Typically the conclusion is the part the user is most interested in. So, a rough guideline is that a label typically provides a hint about only the conclusion; a label rarely says anything about the hypotheses or antecedents. If there are multiple theorems with the same conclusion but different hypotheses/antecedents, then the labels will need to differ; those label differences should emphasize what is different. There is no need to always fully describe the conclusion; just identify the important part. For example, cos0 is the theorem that provides the value for the cosine of 0; we would need to look at the theorem itself to see what that value is. The label "cos0" is concise and we use it instead of "cos0eq1". There is no need to add the "eq1", because there will never be a case where we have to disambiguate between different values produced by the cosine of zero, and we generally prefer shorter labels if they are unambiguous.

Closures and values. As noted above, if a function df-NAME is defined, there is typically a proof of its value labeled "NAMEval" and of its closure labeled "NAMEcl". E.g., for cosine ( df-cos ) we have value cosval and closure coscl .

Special cases. Sometimes, syntax and related markings are insufficient to distinguish different theorems. For example, there are over a hundred different implication-only theorems. They are grouped in a more ad-hoc way that attempts to make their distinctions clearer. These often use abbreviations such as "mp" for "modus ponens", "syl" for syllogism, and "id" for "identity". It is especially hard to give good names in the propositional calculus section because there are so few primitives. However, in most cases this is not a serious problem. There are a few very common theorems like ax-mp and syl that you will have no trouble remembering, a few theorem series like syl*anc and simp* that you can use parametrically, and a few other useful glue things for destructuring 'and's and 'or's (see natded for a list), and that is about all you need for most things. As for the rest, you can just assume that if it involves at most three connectives, then it is probably already proved in set.mm, and searching for it will give you the label.

Suffixes. Suffixes are used to indicate the form of a theorem (inference, deduction, or closed form, see above). Additionally, we sometimes suffix with "v" the label of a theorem adding a disjoint variable condition, as in 19.21v versus 19.21 . This often permits to prove the result using fewer axioms, and/or to eliminate a nonfreeness hypothesis (such as F/ x ph in 19.21 ). If no constraint is put on axiom use, then the v-version can be proved from the original theorem using nfv . If two (resp. three) such disjoint variable conditions are added, then the suffix "vv" (resp. "vvv") is used, e.g., exlimivv . Conversely, we sometimes suffix with "f" the label of a theorem introducing such a hypothesis to eliminate the need for the disjoint variable condition; e.g. euf derived from eu6 . The "f" stands for "not free in" which is less restrictive than "does not occur in." The suffix "b" often means "biconditional" ( <-> , "iff" , "if and only if"), e.g., sspwb . We sometimes suffix with "s" the label of an inference that manipulates an antecedent, leaving the consequent unchanged. The "s" means that the inference eliminates the need for a syllogism ( syl ) -type inference in a proof. A theorem label is suffixed with "ALT" if it provides an alternate less-preferred proof of a theorem (e.g., the proof is clearer but uses more axioms than the preferred version). The "ALT" may be further suffixed with a number if there is more than one alternate theorem. Furthermore, a theorem label is suffixed with "OLD" if there is a new version of it and the OLD version is obsolete (and will be removed within one year).

Finally, it should be mentioned that suffixes can be combined, for example in cbvaldva ( cbval in deduction form "d" with a not free variable replaced by a disjoint variable condition "v" with a conjunction as antecedent "a"). As a general rule, the suffixes for the theorem forms ("i", "d" or "g") should be the first of multiple suffixes, as for example in vtocldf .

Here is a non-exhaustive list of common suffixes:

a : theorem having a conjunction as antecedent
b : theorem expressing a logical equivalence
c : contraction (e.g., sylc , syl2anc ), commutes (e.g., biimpac )
d : theorem in deduction form
f : theorem with a hypothesis such as F/ x ph
g : theorem in closed form having an "is a set" antecedent
i : theorem in inference form
l : theorem concerning something at the left
r : theorem concerning something at the right
r : theorem with something reversed (e.g., a biconditional)
s : inference that manipulates an antecedent ("s" refers to an application of syl that is eliminated)
t : theorem in closed form (not having an "is a set" antecedent)
v : theorem with one (main) disjoint variable condition
vv : theorem with two (main) disjoint variable conditions
w : weak(er) form of a theorem
ALT : alternate proof of a theorem
ALTV : alternate version of a theorem or definition (mathbox only)
OLD : old/obsolete version of a theorem (or proof) or definition

Reuse. When creating a new theorem or axiom, try to reuse abbreviations used elsewhere. A comment should explain the first use of an abbreviation.

The following table shows some commonly used abbreviations in labels, in alphabetical order. For each abbreviation we provide a mnenomic, the source theorem or the assumption defining it, an expression showing what it looks like, whether or not it is a "syntax fragment" (an abbreviation that indicates a particular kind of syntax), and hyperlinks to label examples that use the abbreviation. The abbreviation is bolded if there is a df-NAME definition but the label fragment is not NAME. This is not a complete list of abbreviations, though we do want this to eventually be a complete list of exceptions.

Abbreviation	Mnenomic	Source	Expression	Syntax?	Example(s)
a	and (suffix)			No	biimpa , rexlimiva
abl	Abelian group	df-abl	Abel	Yes	ablgrp , zringabl
abs	absorption			No	ressabs
abs	absolute value (of a complex number)	df-abs	( absA )	Yes	absval , absneg , abs1
ad	adding			No	adantr , ad2antlr
add	add (see "p")	df-add	( A + B )	Yes	addcl , addcom , addass
al	"for all"		A. x ph	No	alim , alex
ALT	alternative/less preferred (suffix)			No	idALT
an	and	df-an	( ph /\ ps )	Yes	anor , iman , imnan
ant	antecedent			No	adantr
ass	associative			No	biass , orass , mulass
asym	asymmetric, antisymmetric			No	intasym , asymref , posasymb
ax	axiom			No	ax6dgen , ax1cn
bas, base	base (set of an extensible structure)	df-base	( BaseS )	Yes	baseval , ressbas , cnfldbas
b, bi	biconditional ("iff", "if and only if")	df-bi	( ph <-> ps )	Yes	impbid , sspwb
br	binary relation	df-br	A R B	Yes	brab1 , brun
cbv	change bound variable			No	cbvalivw , cbvrex
cl	closure			No	ifclda , ovrcl , zaddcl
cn	complex numbers	df-c	CC	Yes	nnsscn , nncn
cnfld	field of complex numbers	df-cnfld	CCfld	Yes	cnfldbas , cnfldinv
cntz	centralizer	df-cntz	( CntzM )	Yes	cntzfval , dprdfcntz
cnv	converse	df-cnv	` ``' A	Yes	opelcnvg , f1ocnv
co	composition	df-co	( A o. B )	Yes	cnvco , fmptco
com	commutative			No	orcom , bicomi , eqcomi
con	contradiction, contraposition			No	condan , con2d
csb	class substitution	df-csb	[_ A / x ]_ B	Yes	csbid , csbie2g
cyg	cyclic group	df-cyg	CycGrp	Yes	iscyg , zringcyg
d	deduction form (suffix)			No	idd , impbid
df	(alternate) definition (prefix)			No	dfrel2 , dffn2
di, distr	distributive			No	andi , imdi , ordi , difindi , ndmovdistr
dif	class difference	df-dif	( A \ B )	Yes	difss , difindi
div	division	df-div	( A / B )	Yes	divcl , divval , divmul
dm	domain	df-dm	dom A	Yes	dmmpt , iswrddm0
e, eq, equ	equals (equ for setvars, eq for classes)	df-cleq	A = B	Yes	2p2e4 , uneqri , equtr
edg	edge	df-edg	( Edg `G )	Yes	edgopval , usgredgppr
el	element of		A e. B	Yes	eldif , eldifsn , elssuni
en	equinumerous	df-en	A ~B	Yes	domen , enfi
eu	"there exists exactly one"	eu6	E! x ph	Yes	euex , euabsn
ex	exists (i.e. is a set)		e.V	No	brrelex1 , 0ex
ex, e	"there exists (at least one)"	df-ex	E. x ph	Yes	exim , alex
exp	export			No	expt , expcom
f	"not free in" (suffix)			No	equs45f , sbf
f	function	df-f	F : A --> B	Yes	fssxp , opelf
fal	false	df-fal	F.	Yes	bifal , falantru
fi	finite intersection	df-fi	( fiB )	Yes	fival , inelfi
fi, fin	finite	df-fin	Fin	Yes	isfi , snfi , onfin
fld	field (Note: there is an alternative definition Fld of a field, see df-fld )	df-field	Field	Yes	isfld , fldidom
fn	function with domain	df-fn	A Fn B	Yes	ffn , fndm
frgp	free group	df-frgp	( freeGrpI )	Yes	frgpval , frgpadd
fsupp	finitely supported function	df-fsupp	R finSupp Z	Yes	isfsupp , fdmfisuppfi , fsuppco
fun	function	df-fun	Fun F	Yes	funrel , ffun
fv	function value	df-fv	( FA )	Yes	fvres , swrdfv
fz	finite set of sequential integers	df-fz	( M ... N )	Yes	fzval , eluzfz
fz0	finite set of sequential nonnegative integers		( 0 ... N )	Yes	nn0fz0 , fz0tp
fzo	half-open integer range	df-fzo	( M ..^ N )	Yes	elfzo , elfzofz
g	more general (suffix); eliminates "is a set" hypotheses			No	uniexg
gr	graph			No	uhgrf , isumgr , usgrres1
grp	group	df-grp	Grp	Yes	isgrp , tgpgrp
gsum	group sum	df-gsum	( G gsum F )	Yes	gsumval , gsumwrev
hash	size (of a set)	df-hash	( #A )	Yes	hashgval , hashfz1 , hashcl
hb	hypothesis builder (prefix)			No	hbxfrbi , hbald , hbequid
hm	(monoid, group, ring) homomorphism			No	ismhm , isghm , isrhm
i	inference (suffix)			No	eleq1i , tcsni
i	implication (suffix)			No	brwdomi , infeq5i
id	identity			No	biid
iedg	indexed edge	df-iedg	( iEdgG )	Yes	iedgval0 , edgiedgb
idm	idempotent			No	anidm , tpidm13
im, imp	implication (label often omitted)	df-im	( A -> B )	Yes	iman , imnan , impbidd
ima	image	df-ima	( A " B )	Yes	resima , imaundi
imp	import			No	biimpa , impcom
in	intersection	df-in	( A i^i B )	Yes	elin , incom
inf	infimum	df-inf	inf ( RR+ , RR* , < )	Yes	fiinfcl , infiso
is...	is (something a) ...?			No	isring
j	joining, disjoining			No	jc , jaoi
l	left			No	olcd , simpl
map	mapping operation or set exponentiation	df-map	( A ^m B )	Yes	mapvalg , elmapex
mat	matrix	df-mat	( N Mat R )	Yes	matval , matring
mdet	determinant (of a square matrix)	df-mdet	( N maDet R )	Yes	mdetleib , mdetrlin
mgm	magma	df-mgm	Magma	Yes	mgmidmo , mgmlrid , ismgm
mgp	multiplicative group	df-mgp	( mulGrpR )	Yes	mgpress , ringmgp
mnd	monoid	df-mnd	Mnd	Yes	mndass , mndodcong
mo	"there exists at most one"	df-mo	E* x ph	Yes	eumo , moim
mp	modus ponens	ax-mp		No	mpd , mpi
mpo	maps-to notation for an operation	df-mpo	( x e. A , y e. B \|-> C )	Yes	mpompt , resmpo
mpt	modus ponendo tollens			No	mptnan , mptxor
mpt	maps-to notation for a function	df-mpt	( x e. A \|-> B )	Yes	fconstmpt , resmpt
mpt2	maps-to notation for an operation (deprecated). We are in the process of replacing mpt2 with mpo in labels.	df-mpo	( x e. A , y e. B \|-> C )	Yes	mpompt , resmpo
mul	multiplication (see "t")	df-mul	( A x. B )	Yes	mulcl , divmul , mulcom , mulass
n, not	not		-. ph	Yes	nan , notnotr
ne	not equal	df-ne	A =/= B	Yes	exmidne , neeqtrd
nel	not element of	df-nel	A e/ B	Yes	neli , nnel
ne0	not equal to zero (see n0)		=/= 0	No	negne0d , ine0 , gt0ne0
nf	"not free in" (prefix)			No	nfnd
ngp	normed group	df-ngp	NrmGrp	Yes	isngp , ngptps
nm	norm (on a group or ring)	df-nm	( normW )	Yes	nmval , subgnm
nn	positive integers	df-nn	NN	Yes	nnsscn , nncn
nn0	nonnegative integers	df-n0	NN0	Yes	nnnn0 , nn0cn
n0	not the empty set (see ne0)		=/= (/)	No	n0i , vn0 , ssn0
OLD	old, obsolete (to be removed soon)			No	19.43OLD
on	ordinal number	df-on	A e. On	Yes	elon , 1on onelon
op	ordered pair	df-op	<. A , B >.	Yes	dfopif , opth
or	or	df-or	( ph \/ ps )	Yes	orcom , anor
ot	ordered triple	df-ot	<. A , B , C >.	Yes	euotd , fnotovb
ov	operation value	df-ov	( A F B )	Yes	fnotovb , fnovrn
p	plus (see "add"), for all-constant theorems	df-add	( 3 + 2 ) = 5	Yes	3p2e5
pfx	prefix	df-pfx	( W prefix L )	Yes	pfxlen , ccatpfx
pm	Principia Mathematica			No	pm2.27
pm	partial mapping (operation)	df-pm	( A ^pm B )	Yes	elpmi , pmsspw
pr	pair	df-pr	{ A , B }	Yes	elpr , prcom , prid1g , prnz
prm, prime	prime (number)	df-prm	Prime	Yes	1nprm , dvdsprime
pss	proper subset	df-pss	A C. B	Yes	pssss , sspsstri
q	rational numbers ("quotients")	df-q	QQ	Yes	elq
r	right			No	orcd , simprl
rab	restricted class abstraction	df-rab	{ x e. A \| ph }	Yes	rabswap , df-oprab
ral	restricted universal quantification	df-ral	A. x e. A ph	Yes	ralnex , ralrnmpo
rcl	reverse closure			No	ndmfvrcl , nnarcl
re	real numbers	df-r	RR	Yes	recn , 0re
rel	relation	df-rel	Rel A	Yes	brrelex1 , relmpoopab
res	restriction	df-res	` ( A \|`B )	Yes	opelres , f1ores
reu	restricted existential uniqueness	df-reu	E! x e. A ph	Yes	nfreud , reurex
rex	restricted existential quantification	df-rex	E. x e. A ph	Yes	rexnal , rexrnmpo
rmo	restricted "at most one"	df-rmo	E* x e. A ph	Yes	nfrmod , nrexrmo
rn	range	df-rn	ran A	Yes	elrng , rncnvcnv
rng	(unital) ring	df-ring	Ring	Yes	ringidval , isring , ringgrp
rot	rotation			No	3anrot , 3orrot
s	eliminates need for syllogism (suffix)			No	ancoms
sb	(proper) substitution (of a set)	df-sb	[ y / x ] ph	Yes	spsbe , sbimi
sbc	(proper) substitution of a class	df-sbc	[. A / x ]. ph	Yes	sbc2or , sbcth
sca	scalar	df-sca	( ScalarH )	Yes	resssca , mgpsca
simp	simple, simplification			No	simpl , simp3r3
sn	singleton	df-sn	{ A }	Yes	eldifsn
sp	specialization			No	spsbe , spei
ss	subset	df-ss	A C B	Yes	difss
struct	structure	df-struct	Struct	Yes	brstruct , structfn
sub	subtract	df-sub	( A - B )	Yes	subval , subaddi
sup	supremum	df-sup	sup ( A , B , < )	Yes	fisupcl , supmo
supp	support (of a function)	df-supp	( F supp Z )	Yes	ressuppfi , mptsuppd
swap	swap (two parts within a theorem)			No	rabswap , 2reuswap
syl	syllogism	syl		No	3syl
sym	symmetric			No	df-symdif , cnvsym
symg	symmetric group	df-symg	( SymGrpA )	Yes	symghash , pgrpsubgsymg
t	times (see "mul"), for all-constant theorems	df-mul	( 3 x. 2 ) = 6	Yes	3t2e6
th, t	theorem			No	nfth , sbcth , weth , ancomst
tp	triple	df-tp	{ A , B , C }	Yes	eltpi , tpeq1
tr	transitive			No	bitrd , biantr
tru, t	true, truth	df-tru	T.	Yes	bitru , truanfal , biimt
un	union	df-un	( A u. B )	Yes	uneqri , uncom
unit	unit (in a ring)	df-unit	( UnitR )	Yes	isunit , nzrunit
v	setvar (especially for specializations of theorems when a class is replaced by a setvar variable)		x	Yes	cv , vex , velpw , vtoclf
v	disjoint variable condition used in place of nonfreeness hypothesis (suffix)			No	spimv
vtx	vertex	df-vtx	( VtxG )	Yes	vtxval0 , opvtxov
vv	two disjoint variable conditions used in place of nonfreeness hypotheses (suffix)			No	19.23vv
w	weak (version of a theorem) (suffix)			No	ax11w , spnfw
wrd	word	df-word	Word S	Yes	iswrdb , wrdfn , ffz0iswrd
xp	cross product (Cartesian product)	df-xp	( A X. B )	Yes	elxp , opelxpi , xpundi
xr	eXtended reals	df-xr	RR*	Yes	ressxr , rexr , 0xr
z	integers (from German "Zahlen")	df-z	ZZ	Yes	elz , zcn
zn	ring of integers mod N	df-zn	( Z/nZN )	Yes	znval , zncrng , znhash
zring	ring of integers	df-zring	ZZring	Yes	zringbas , zringcrng
0, z	slashed zero (empty set)	df-nul	(/)	Yes	n0i , vn0 ; snnz , prnz

Abbreviation

Mnenomic

Source

Expression

Syntax?

Example(s)

and (suffix)

biimpa , rexlimiva

abl

Abelian group

df-abl

Abel

Yes

ablgrp , zringabl

abs

absorption

ressabs

abs

absolute value (of a complex number)

df-abs

( absA )

Yes

absval , absneg , abs1

adding

adantr , ad2antlr

add

add (see "p")

df-add

( A + B )

Yes

addcl , addcom , addass

"for all"

A. x ph

alim , alex

ALT

alternative/less preferred (suffix)

idALT

and

df-an

( ph /\ ps )

Yes

anor , iman , imnan

ant

antecedent

adantr

ass

associative

biass , orass , mulass

asym

asymmetric, antisymmetric

intasym , asymref , posasymb

axiom

ax6dgen , ax1cn

bas, base

base (set of an extensible structure)

df-base

( BaseS )

Yes

baseval , ressbas , cnfldbas

b, bi

biconditional ("iff", "if and only if")

df-bi

( ph <-> ps )

Yes

impbid , sspwb

binary relation

df-br

A R B

Yes

brab1 , brun

cbv

change bound variable

cbvalivw , cbvrex

closure

ifclda , ovrcl , zaddcl

complex numbers

df-c

Yes

nnsscn , nncn

cnfld

field of complex numbers

df-cnfld

CCfld

Yes

cnfldbas , cnfldinv

cntz

centralizer

df-cntz

( CntzM )

Yes

cntzfval , dprdfcntz

cnv

converse

df-cnv

` ``' A

Yes

opelcnvg , f1ocnv

composition

df-co

( A o. B )

Yes

cnvco , fmptco

com

commutative

orcom , bicomi , eqcomi

con

contradiction, contraposition

condan , con2d

csb

class substitution

df-csb

[_ A / x ]_ B

Yes

csbid , csbie2g

cyg

cyclic group

df-cyg

CycGrp

Yes

iscyg , zringcyg

deduction form (suffix)

idd , impbid

(alternate) definition (prefix)

dfrel2 , dffn2

di, distr

distributive

andi , imdi , ordi , difindi , ndmovdistr

dif

class difference

df-dif

( A \ B )

Yes

difss , difindi

div

division

df-div

( A / B )

Yes

divcl , divval , divmul

domain

df-dm

dom A

Yes

dmmpt , iswrddm0

e, eq, equ

equals (equ for setvars, eq for classes)

df-cleq

A = B

Yes

2p2e4 , uneqri , equtr

edg

edge

df-edg

( Edg `G )

Yes

edgopval , usgredgppr

element of

A e. B

Yes

eldif , eldifsn , elssuni

equinumerous

df-en

A ~B

Yes

domen , enfi

"there exists exactly one"

eu6

E! x ph

Yes

euex , euabsn

exists (i.e. is a set)

e.V

brrelex1 , 0ex

ex, e

"there exists (at least one)"

df-ex

E. x ph

Yes

exim , alex

exp

export

expt , expcom

"not free in" (suffix)

equs45f , sbf

function

df-f

F : A --> B

Yes

fssxp , opelf

fal

false

df-fal

Yes

bifal , falantru

finite intersection

df-fi

( fiB )

Yes

fival , inelfi

fi, fin

finite

df-fin

Fin

Yes

isfi , snfi , onfin

fld

field (Note: there is an alternative definition Fld of a field, see df-fld )

df-field

Field

Yes

isfld , fldidom

function with domain

df-fn

A Fn B

Yes

ffn , fndm

frgp

free group

df-frgp

( freeGrpI )

Yes

frgpval , frgpadd

fsupp

finitely supported function

df-fsupp

R finSupp Z

Yes

isfsupp , fdmfisuppfi , fsuppco

fun

function

df-fun

Fun F

Yes

funrel , ffun

function value

df-fv

( FA )

Yes

fvres , swrdfv

finite set of sequential integers

df-fz

( M ... N )

Yes

fzval , eluzfz

fz0

finite set of sequential nonnegative integers

( 0 ... N )

Yes

nn0fz0 , fz0tp

fzo

half-open integer range

df-fzo

( M ..^ N )

Yes

elfzo , elfzofz

more general (suffix); eliminates "is a set" hypotheses

uniexg

graph

uhgrf , isumgr , usgrres1

grp

group

df-grp

Grp

Yes

isgrp , tgpgrp

gsum

group sum

df-gsum

( G gsum F )

Yes

gsumval , gsumwrev

hash

size (of a set)

df-hash

( #A )

Yes

hashgval , hashfz1 , hashcl

hypothesis builder (prefix)

hbxfrbi , hbald , hbequid

(monoid, group, ring) homomorphism

ismhm , isghm , isrhm

inference (suffix)

eleq1i , tcsni

implication (suffix)

brwdomi , infeq5i

identity

biid

iedg

indexed edge

df-iedg

( iEdgG )

Yes

iedgval0 , edgiedgb

idm

idempotent

anidm , tpidm13

im, imp

implication (label often omitted)

df-im

( A -> B )

Yes

iman , imnan , impbidd

ima

image

df-ima

( A " B )

Yes

resima , imaundi

imp

import

biimpa , impcom

intersection

df-in

( A i^i B )

Yes

elin , incom

inf

infimum

df-inf

inf ( RR+ , RR* , < )

Yes

fiinfcl , infiso

is...

is (something a) ...?

isring

joining, disjoining

jc , jaoi

left

olcd , simpl

map

mapping operation or set exponentiation

df-map

( A ^m B )

Yes

mapvalg , elmapex

mat

matrix

df-mat

( N Mat R )

Yes

matval , matring

mdet

determinant (of a square matrix)

df-mdet

( N maDet R )

Yes

mdetleib , mdetrlin

mgm

magma

df-mgm

Magma

Yes

mgmidmo , mgmlrid , ismgm

mgp

multiplicative group

df-mgp

( mulGrpR )

Yes

mgpress , ringmgp

mnd

monoid

df-mnd

Mnd

Yes

mndass , mndodcong

"there exists at most one"

df-mo

E* x ph

Yes

eumo , moim

modus ponens

ax-mp

mpd , mpi

mpo

maps-to notation for an operation

df-mpo

( x e. A , y e. B |-> C )

Yes

mpompt , resmpo

mpt

modus ponendo tollens

mptnan , mptxor

mpt

maps-to notation for a function

df-mpt

( x e. A |-> B )

Yes

fconstmpt , resmpt

mpt2

maps-to notation for an operation (deprecated). We are in the process of replacing mpt2 with mpo in labels.

df-mpo

( x e. A , y e. B |-> C )

Yes

mpompt , resmpo

mul

multiplication (see "t")

df-mul

( A x. B )

Yes

mulcl , divmul , mulcom , mulass

n, not

not

-. ph

Yes

nan , notnotr

not equal

df-ne

A =/= B

Yes

exmidne , neeqtrd

nel

not element of

df-nel

A e/ B

Yes

neli , nnel

ne0

not equal to zero (see n0)

=/= 0

negne0d , ine0 , gt0ne0

"not free in" (prefix)

nfnd

ngp

normed group

df-ngp

NrmGrp

Yes

isngp , ngptps

norm (on a group or ring)

df-nm

( normW )

Yes

nmval , subgnm

positive integers

df-nn

Yes

nnsscn , nncn

nn0

nonnegative integers

df-n0

NN0

Yes

nnnn0 , nn0cn

not the empty set (see ne0)

=/= (/)

n0i , vn0 , ssn0

OLD

old, obsolete (to be removed soon)

19.43OLD

ordinal number

df-on

A e. On

Yes

elon , 1on onelon

ordered pair

df-op

<. A , B >.

Yes

dfopif , opth

df-or

( ph \/ ps )

Yes

orcom , anor

ordered triple

df-ot

<. A , B , C >.

Yes

euotd , fnotovb

operation value

df-ov

( A F B )

Yes

fnotovb , fnovrn

plus (see "add"), for all-constant theorems

df-add

( 3 + 2 ) = 5

Yes

3p2e5

pfx

prefix

df-pfx

( W prefix L )

Yes

pfxlen , ccatpfx

Principia Mathematica

pm2.27

partial mapping (operation)

df-pm

( A ^pm B )

Yes

elpmi , pmsspw

pair

df-pr

{ A , B }

Yes

elpr , prcom , prid1g , prnz

prm, prime

prime (number)

df-prm

Prime

Yes

1nprm , dvdsprime

pss

proper subset

df-pss

A C. B

Yes

pssss , sspsstri

rational numbers ("quotients")

df-q

Yes

elq

right

orcd , simprl

rab

restricted class abstraction

df-rab

{ x e. A | ph }

Yes

rabswap , df-oprab

ral

restricted universal quantification

df-ral

A. x e. A ph

Yes

ralnex , ralrnmpo

rcl

reverse closure

ndmfvrcl , nnarcl

real numbers

df-r

Yes

recn , 0re

rel

relation

df-rel

Rel A

Yes

brrelex1 , relmpoopab

res

restriction

df-res

` ( A |`B )

Yes

opelres , f1ores

reu

restricted existential uniqueness

df-reu

E! x e. A ph

Yes

nfreud , reurex

rex

restricted existential quantification

df-rex

E. x e. A ph

Yes

rexnal , rexrnmpo

rmo

restricted "at most one"

df-rmo

E* x e. A ph

Yes

nfrmod , nrexrmo

range

df-rn

ran A

Yes

elrng , rncnvcnv

rng

(unital) ring

df-ring

Ring

Yes

ringidval , isring , ringgrp

rot

rotation

3anrot , 3orrot

eliminates need for syllogism (suffix)

ancoms

(proper) substitution (of a set)

df-sb

[ y / x ] ph

Yes

spsbe , sbimi

sbc

(proper) substitution of a class

df-sbc

[. A / x ]. ph

Yes

sbc2or , sbcth

sca

scalar

df-sca

( ScalarH )

Yes

resssca , mgpsca

simp

simple, simplification

simpl , simp3r3

singleton

df-sn

{ A }

Yes

eldifsn

specialization

spsbe , spei

subset

df-ss

A C B

Yes

difss

struct

structure

df-struct

Struct

Yes

brstruct , structfn

sub

subtract

df-sub

( A - B )

Yes

subval , subaddi

sup

supremum

df-sup

sup ( A , B , < )

Yes

fisupcl , supmo

supp

support (of a function)

df-supp

( F supp Z )

Yes

ressuppfi , mptsuppd

swap

swap (two parts within a theorem)

rabswap , 2reuswap

syl

syllogism

syl

3syl

sym

symmetric

df-symdif , cnvsym

symg

symmetric group

df-symg

( SymGrpA )

Yes

symghash , pgrpsubgsymg

times (see "mul"), for all-constant theorems

df-mul

( 3 x. 2 ) = 6

Yes

3t2e6

th, t

theorem

nfth , sbcth , weth , ancomst

triple

df-tp

{ A , B , C }

Yes

eltpi , tpeq1

transitive

bitrd , biantr

tru, t

true, truth

df-tru

Yes

bitru , truanfal , biimt

union

df-un

( A u. B )

Yes

uneqri , uncom

unit

unit (in a ring)

df-unit

( UnitR )

Yes

isunit , nzrunit

setvar (especially for specializations of theorems when a class is replaced by a setvar variable)

Yes

cv , vex , velpw , vtoclf

disjoint variable condition used in place of nonfreeness hypothesis (suffix)

spimv

vtx

vertex

df-vtx

( VtxG )

Yes

vtxval0 , opvtxov

two disjoint variable conditions used in place of nonfreeness hypotheses (suffix)

19.23vv

weak (version of a theorem) (suffix)

ax11w , spnfw

wrd

word

df-word

Word S

Yes

iswrdb , wrdfn , ffz0iswrd

cross product (Cartesian product)

df-xp

( A X. B )

Yes

elxp , opelxpi , xpundi

eXtended reals

df-xr

RR*

Yes

ressxr , rexr , 0xr

integers (from German "Zahlen")

df-z

Yes

elz , zcn

ring of integers mod N

df-zn

( Z/nZN )

Yes

znval , zncrng , znhash

zring

ring of integers

df-zring

ZZring

Yes

zringbas , zringcrng

0, z

slashed zero (empty set)

df-nul

(/)

Yes

n0i , vn0 ; snnz , prnz

(Contributed by the Metamath team, 27-Dec-2016) Date of last revision. (Revised by the Metamath team, 22-Sep-2022) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Hypothesis	conventions-labels.1	\|- ph
	Assertion	conventions-labels	\|- ph

Proof

Step	Hyp	Ref	Expression
1		conventions-labels.1	\|- ph

Metamath Proof Explorer

Theorem conventions-labels

Proof