Theorem conventions-labels 30267

Description:

The following gives conventions used in the Metamath Proof Explorer (MPE, set.mm) regarding labels. For other conventions, see conventions 30266 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 3053"rgen.1 $e |- ( x e. A -> ph ) $." or letters corresponding to the (main) class variable used in the hypothesis, e.g., for mdet0 22538: "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 2651 and stirling 45540.
• 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 42.
• 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 1833, and the restricted quantifier version of Theorem 21 from Section 19 of [Margaris] p. 90 is labeled r19.21 3242.
• 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... 15859. 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 (𝐴 ∖ 𝐵) is defined in df-dif 3948, and thus its syntax label fragment is "dif". Similarly, the subclass relation 𝐴 ⊆ 𝐵 has syntax label fragment "ss" because it is defined in df-ss 3962. Most theorem names follow from these fragments, for example, the theorem proving (𝐴 ∖ 𝐵) ⊆ 𝐴 involves a class difference ("dif") of a subset ("ss"), and thus is labeled difss 4129. There are many other syntax label fragments, e.g., singleton construct {𝐴} has syntax label fragment "sn" (because it is defined in df-sn 4630), and the pair construct {𝐴, 𝐵} has fragment "pr" ( from df-pr 4632). 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 𝐴 ∈ 𝐵 does not have a df-NAME definition; in this case its syntax label fragment is "el". Thus, because the theorem beginning with (𝐴 ∈ (𝐵 ∖ {𝐶}) uses is-element-of ("el") of a class difference ("dif") of a singleton ("sn"), it is labeled eldifsn 4791. An "n" is often used for negation (¬), e.g., nan 828.
• 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 ℂ (even though its definition is in df-c 11144) and "re" represents real numbers ℝ (Definition df-r 11148). The empty set ∅ often uses fragment 0, even though it is defined in df-nul 4324. The syntax construct (𝐴 + 𝐵) usually uses the fragment "add" (which is consistent with df-add 11149), but "p" is used as the fragment for constant theorems. Equality (𝐴 = 𝐵) often uses "e" as the fragment. As a result, "two plus two equals four" is labeled 2p2e4 12377.
• 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 16126 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 16046) we have value cosval 16099 and closure coscl 16103.
• 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 5 and syl 17 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 30269 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 1934 versus 19.21 2195. This often permits to prove the result using fewer axioms, and/or to eliminate a nonfreeness hypothesis (such as Ⅎ𝑥𝜑 in 19.21 2195). If no constraint is put on axiom use, then the v-version can be proved from the original theorem using nfv 1909. If two (resp. three) such disjoint variable conditions are added, then the suffix "vv" (resp. "vvv") is used, e.g., exlimivv 1927. 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 2564 derived from eu6 2562. 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 5450. 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 17) -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 2402 (cbval 2391 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 3538. 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 65, syl2anc 582), commutes (e.g., biimpac 477)
  • d : theorem in deduction form
  • f : theorem with a hypothesis such as Ⅎ𝑥𝜑
  • 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 17 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 475, rexlimiva 3137
abl	Abelian group	df-abl 19742	Abel	Yes	ablgrp 19744, zringabl 21381
abs	absorption			No	ressabs 17229
abs	absolute value (of a complex number)	df-abs 15215	(abs‘𝐴)	Yes	absval 15217, absneg 15256, abs1 15276
ad	adding			No	adantr 479, ad2antlr 725
add	add (see "p")	df-add 11149	(𝐴 + 𝐵)	Yes	addcl 11220, addcom 11430, addass 11225
al	"for all"		∀𝑥𝜑	No	alim 1804, alex 1820
ALT	alternative/less preferred (suffix)			No	idALT 23
an	and	df-an 395	(𝜑 ∧ 𝜓)	Yes	anor 980, iman 400, imnan 398
ant	antecedent			No	adantr 479
ass	associative			No	biass 383, orass 919, mulass 11226
asym	asymmetric, antisymmetric			No	intasym 6121, asymref 6122, posasymb 18310
ax	axiom			No	ax6dgen 2116, ax1cn 11172
bas, base	base (set of an extensible structure)	df-base 17180	(Base‘𝑆)	Yes	baseval 17181, ressbas 17214, cnfldbas 21287
b, bi	biconditional ("iff", "if and only if")	df-bi 206	(𝜑 ↔ 𝜓)	Yes	impbid 211, sspwb 5450
br	binary relation	df-br 5149	𝐴𝑅𝐵	Yes	brab1 5196, brun 5199
c	commutes, commuted (suffix)			No	biimpac 477
c	contraction (suffix)			No	sylc 65, syl2anc 582
cbv	change bound variable			No	cbvalivw 2002, cbvrex 3347
cdm	codomain			No	ffvelcdm 7088, focdmex 7958
cl	closure			No	ifclda 4564, ovrcl 7458, zaddcl 12632
cn	complex numbers	df-c 11144	ℂ	Yes	nnsscn 12247, nncn 12250
cnfld	field of complex numbers	df-cnfld 21284	ℂfld	Yes	cnfldbas 21287, cnfldinv 21334
cntz	centralizer	df-cntz 19272	(Cntz‘𝑀)	Yes	cntzfval 19275, dprdfcntz 19976
cnv	converse	df-cnv 5685	◡𝐴	Yes	opelcnvg 5882, f1ocnv 6848
co	composition	df-co 5686	(𝐴 ∘ 𝐵)	Yes	cnvco 5887, fmptco 7136
com	commutative			No	orcom 868, bicomi 223, eqcomi 2734
con	contradiction, contraposition			No	condan 816, con2d 134
csb	class substitution	df-csb 3891	⦋𝐴 / 𝑥⦌𝐵	Yes	csbid 3903, csbie2g 3933
cyg	cyclic group	df-cyg 19837	CycGrp	Yes	iscyg 19838, zringcyg 21399
d	deduction form (suffix)			No	idd 24, impbid 211
df	(alternate) definition (prefix)			No	dfrel2 6193, dffn2 6723
di, distr	distributive			No	andi 1005, imdi 388, ordi 1003, difindi 4281, ndmovdistr 7608
dif	class difference	df-dif 3948	(𝐴 ∖ 𝐵)	Yes	difss 4129, difindi 4281
div	division	df-div 11902	(𝐴 / 𝐵)	Yes	divcl 11908, divval 11904, divmul 11905
dm	domain	df-dm 5687	dom 𝐴	Yes	dmmpt 6244, iswrddm0 14520
e, eq, equ	equals (equ for setvars, eq for classes)	df-cleq 2717	𝐴 = 𝐵	Yes	2p2e4 12377, uneqri 4149, equtr 2016
edg	edge	df-edg 28917	(Edg‘𝐺)	Yes	edgopval 28920, usgredgppr 29065
el	element of		𝐴 ∈ 𝐵	Yes	eldif 3955, eldifsn 4791, elssuni 4940
en	equinumerous	df-en	𝐴 ≈ 𝐵	Yes	domen 8980, enfi 9213
eu	"there exists exactly one"	eu6 2562	∃!𝑥𝜑	Yes	euex 2565, euabsn 4731
ex	exists (i.e. is a set)		∈ V	No	brrelex1 5730, 0ex 5307
ex, e	"there exists (at least one)"	df-ex 1774	∃𝑥𝜑	Yes	exim 1828, alex 1820
exp	export			No	expt 177, expcom 412
f	"not free in" (suffix)			No	equs45f 2452, sbf 2257
f	function	df-f 6551	𝐹:𝐴⟶𝐵	Yes	fssxp 6749, opelf 6756
fal	false	df-fal 1546	⊥	Yes	bifal 1549, falantru 1568
fi	finite intersection	df-fi 9434	(fi‘𝐵)	Yes	fival 9435, inelfi 9441
fi, fin	finite	df-fin 8966	Fin	Yes	isfi 8995, snfi 9067, onfin 9253
fld	field (Note: there is an alternative definition Fld of a field, see df-fld 37535)	df-field 20631	Field	Yes	isfld 20639, fldidom 21262
fn	function with domain	df-fn 6550	𝐴 Fn 𝐵	Yes	ffn 6721, fndm 6656
frgp	free group	df-frgp 19669	(freeGrp‘𝐼)	Yes	frgpval 19717, frgpadd 19722
fsupp	finitely supported function	df-fsupp 9386	𝑅 finSupp 𝑍	Yes	isfsupp 9389, fdmfisuppfi 9397, fsuppco 9425
fun	function	df-fun 6549	Fun 𝐹	Yes	funrel 6569, ffun 6724
fv	function value	df-fv 6555	(𝐹‘𝐴)	Yes	fvres 6913, swrdfv 14630
fz	finite set of sequential integers	df-fz 13517	(𝑀...𝑁)	Yes	fzval 13518, eluzfz 13528
fz0	finite set of sequential nonnegative integers		(0...𝑁)	Yes	nn0fz0 13631, fz0tp 13634
fzo	half-open integer range	df-fzo 13660	(𝑀..^𝑁)	Yes	elfzo 13666, elfzofz 13680
g	more general (suffix); eliminates "is a set" hypotheses			No	uniexg 7744
gr	graph			No	uhgrf 28931, isumgr 28964, usgrres1 29184
grp	group	df-grp 18897	Grp	Yes	isgrp 18900, tgpgrp 24012
gsum	group sum	df-gsum 17423	(𝐺 Σg 𝐹)	Yes	gsumval 18636, gsumwrev 19324
hash	size (of a set)	df-hash 14322	(♯‘𝐴)	Yes	hashgval 14324, hashfz1 14337, hashcl 14347
hb	hypothesis builder (prefix)			No	hbxfrbi 1819, hbald 2157, hbequid 38450
hm	(monoid, group, ring, ...) homomorphism			No	ismhm 18741, isghm 19174, isrhm 20421
i	inference (suffix)			No	eleq1i 2816, tcsni 9766
i	implication (suffix)			No	brwdomi 9591, infeq5i 9659
id	identity			No	biid 260
iedg	indexed edge	df-iedg 28868	(iEdg‘𝐺)	Yes	iedgval0 28909, edgiedgb 28923
idm	idempotent			No	anidm 563, tpidm13 4761
im, imp	implication (label often omitted)	df-im 15080	(𝐴 → 𝐵)	Yes	iman 400, imnan 398, impbidd 209
im	(group, ring, ...) isomorphism			No	isgim 19220, rimrcl 20425
ima	image	df-ima 5690	(𝐴 “ 𝐵)	Yes	resima 6019, imaundi 6154
imp	import			No	biimpa 475, impcom 406
in	intersection	df-in 3952	(𝐴 ∩ 𝐵)	Yes	elin 3961, incom 4200
inf	infimum	df-inf 9466	inf(ℝ+, ℝ*, < )	Yes	fiinfcl 9524, infiso 9531
is...	is (something a) ...?			No	isring 20181
j	joining, disjoining			No	jc 161, jaoi 855
l	left			No	olcd 872, simpl 481
map	mapping operation or set exponentiation	df-map 8845	(𝐴 ↑m 𝐵)	Yes	mapvalg 8853, elmapex 8865
mat	matrix	df-mat 22338	(𝑁 Mat 𝑅)	Yes	matval 22341, matring 22375
mdet	determinant (of a square matrix)	df-mdet 22517	(𝑁 maDet 𝑅)	Yes	mdetleib 22519, mdetrlin 22534
mgm	magma	df-mgm 18599	Magma	Yes	mgmidmo 18619, mgmlrid 18626, ismgm 18600
mgp	multiplicative group	df-mgp 20079	(mulGrp‘𝑅)	Yes	mgpress 20093, ringmgp 20183
mnd	monoid	df-mnd 18694	Mnd	Yes	mndass 18702, mndodcong 19501
mo	"there exists at most one"	df-mo 2528	∃*𝑥𝜑	Yes	eumo 2566, moim 2532
mp	modus ponens	ax-mp 5		No	mpd 15, mpi 20
mpo	maps-to notation for an operation	df-mpo 7422	(𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)	Yes	mpompt 7532, resmpo 7538
mpt	modus ponendo tollens			No	mptnan 1762, mptxor 1763
mpt	maps-to notation for a function	df-mpt 5232	(𝑥 ∈ 𝐴 ↦ 𝐵)	Yes	fconstmpt 5739, resmpt 6041
mpt2	maps-to notation for an operation (deprecated). We are in the process of replacing mpt2 with mpo in labels.	df-mpo 7422	(𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)	Yes	mpompt 7532, resmpo 7538
mul	multiplication (see "t")	df-mul 11150	(𝐴 · 𝐵)	Yes	mulcl 11222, divmul 11905, mulcom 11224, mulass 11226
n, not	not		¬ 𝜑	Yes	nan 828, notnotr 130
ne	not equal	df-ne	𝐴 ≠ 𝐵	Yes	exmidne 2940, neeqtrd 3000
nel	not element of	df-nel	𝐴 ∉ 𝐵	Yes	neli 3038, nnel 3046
ne0	not equal to zero (see n0)		≠ 0	No	negne0d 11599, ine0 11679, gt0ne0 11709
nf	"not free in" (prefix)	df-nf 1778	Ⅎ𝑥𝜑	Yes	nfnd 1853
ngp	normed group	df-ngp 24522	NrmGrp	Yes	isngp 24535, ngptps 24541
nm	norm (on a group or ring)	df-nm 24521	(norm‘𝑊)	Yes	nmval 24528, subgnm 24572
nn	positive integers	df-nn 12243	ℕ	Yes	nnsscn 12247, nncn 12250
nn0	nonnegative integers	df-n0 12503	ℕ0	Yes	nnnn0 12509, nn0cn 12512
n0	not the empty set (see ne0)		≠ ∅	No	n0i 4334, vn0 4339, ssn0 4401
OLD	old, obsolete (to be removed soon)			No	19.43OLD 1878
on	ordinal number	df-on 6373	𝐴 ∈ On	Yes	elon 6378, 1on 8497 onelon 6394
op	ordered pair	df-op 4636	⟨𝐴, 𝐵⟩	Yes	dfopif 4871, opth 5477
or	or	df-or 846	(𝜑 ∨ 𝜓)	Yes	orcom 868, anor 980
ot	ordered triple	df-ot 4638	⟨𝐴, 𝐵, 𝐶⟩	Yes	euotd 5514, fnotovb 7468
ov	operation value	df-ov 7420	(𝐴𝐹𝐵)	Yes	fnotovb 7468, fnovrn 7594
p	plus (see "add"), for all-constant theorems	df-add 11149	(3 + 2) = 5	Yes	3p2e5 12393
pfx	prefix	df-pfx 14653	(𝑊 prefix 𝐿)	Yes	pfxlen 14665, ccatpfx 14683
pm	Principia Mathematica			No	pm2.27 42
pm	partial mapping (operation)	df-pm 8846	(𝐴 ↑pm 𝐵)	Yes	elpmi 8863, pmsspw 8894
pr	pair	df-pr 4632	{𝐴, 𝐵}	Yes	elpr 4653, prcom 4737, prid1g 4765, prnz 4782
prm, prime	prime (number)	df-prm 16642	ℙ	Yes	1nprm 16649, dvdsprime 16657
pss	proper subset	df-pss 3965	𝐴 ⊊ 𝐵	Yes	pssss 4092, sspsstri 4099
q	rational numbers ("quotients")	df-q 12963	ℚ	Yes	elq 12964
r	reversed (suffix)			No	pm4.71r 557, caovdir 7653
r	right			No	orcd 871, simprl 769
rab	restricted class abstraction	df-rab 3420	{𝑥 ∈ 𝐴 ∣ 𝜑}	Yes	rabswap 3429, df-oprab 7421
ral	restricted universal quantification	df-ral 3052	∀𝑥 ∈ 𝐴𝜑	Yes	ralnex 3062, ralrnmpo 7558
rcl	reverse closure			No	ndmfvrcl 6930, nnarcl 8635
re	real numbers	df-r 11148	ℝ	Yes	recn 11228, 0re 11246
rel	relation	df-rel 5684	Rel 𝐴	Yes	brrelex1 5730, relmpoopab 8097
res	restriction	df-res 5689	(𝐴 ↾ 𝐵)	Yes	opelres 5990, f1ores 6850
reu	restricted existential uniqueness	df-reu 3365	∃!𝑥 ∈ 𝐴𝜑	Yes	nfreud 3416, reurex 3368
rex	restricted existential quantification	df-rex 3061	∃𝑥 ∈ 𝐴𝜑	Yes	rexnal 3090, rexrnmpo 7559
rmo	restricted "at most one"	df-rmo 3364	∃*𝑥 ∈ 𝐴𝜑	Yes	nfrmod 3415, nrexrmo 3385
rn	range	df-rn 5688	ran 𝐴	Yes	elrng 5893, rncnvcnv 5935
ring	(unital) ring	df-ring 20179	Ring	Yes	ringidval 20127, isring 20181, ringgrp 20182
rng	non-unital ring	df-rng 20097	Rng	Yes	isrng 20098, rngabl 20099, rnglz 20109
rot	rotation			No	3anrot 1097, 3orrot 1089
s	eliminates need for syllogism (suffix)			No	ancoms 457
sb	(proper) substitution (of a set)	df-sb 2060	[𝑦 / 𝑥]𝜑	Yes	spsbe 2077, sbimi 2069
sbc	(proper) substitution of a class	df-sbc 3775	[𝐴 / 𝑥]𝜑	Yes	sbc2or 3783, sbcth 3789
sca	scalar	df-sca 17248	(Scalar‘𝐻)	Yes	resssca 17323, mgpsca 20086
simp	simple, simplification			No	simpl 481, simp3r3 1280
sn	singleton	df-sn 4630	{𝐴}	Yes	eldifsn 4791
sp	specialization			No	spsbe 2077, spei 2387
ss	subset	df-ss 3962	𝐴 ⊆ 𝐵	Yes	difss 4129
struct	structure	df-struct 17115	Struct	Yes	brstruct 17116, structfn 17124
sub	subtract	df-sub 11476	(𝐴 − 𝐵)	Yes	subval 11481, subaddi 11577
sup	supremum	df-sup 9465	sup(𝐴, 𝐵, < )	Yes	fisupcl 9492, supmo 9475
supp	support (of a function)	df-supp 8164	(𝐹 supp 𝑍)	Yes	ressuppfi 9418, mptsuppd 8190
swap	swap (two parts within a theorem)			No	rabswap 3429, 2reuswap 3739
syl	syllogism	syl 17		No	3syl 18
sym	symmetric			No	df-symdif 4242, cnvsym 6118
symg	symmetric group	df-symg 19326	(SymGrp‘𝐴)	Yes	symghash 19336, pgrpsubgsymg 19368
t	times (see "mul"), for all-constant theorems	df-mul 11150	(3 · 2) = 6	Yes	3t2e6 12408
th, t	theorem			No	nfth 1795, sbcth 3789, weth 10518, ancomst 463
tp	triple	df-tp 4634	{𝐴, 𝐵, 𝐶}	Yes	eltpi 4692, tpeq1 4747
tr	transitive			No	bitrd 278, biantr 804
tru, t	true, truth	df-tru 1536	⊤	Yes	bitru 1542, truanfal 1567, biimt 359
un	union	df-un 3950	(𝐴 ∪ 𝐵)	Yes	uneqri 4149, uncom 4151
unit	unit (in a ring)	df-unit 20301	(Unit‘𝑅)	Yes	isunit 20316, nzrunit 20465
v	setvar (especially for specializations of theorems when a class is replaced by a setvar variable)		x	Yes	cv 1532, vex 3467, velpw 4608, vtoclf 3543
v	disjoint variable condition used in place of nonfreeness hypothesis (suffix)			No	spimv 2383
vtx	vertex	df-vtx 28867	(Vtx‘𝐺)	Yes	vtxval0 28908, opvtxov 28874
vv	two disjoint variable conditions used in place of nonfreeness hypotheses (suffix)			No	19.23vv 1938
w	weak (version of a theorem) (suffix)			No	ax11w 2118, spnfw 1975
wrd	word	df-word 14497	Word 𝑆	Yes	iswrdb 14502, wrdfn 14510, ffz0iswrd 14523
xp	cross product (Cartesian product)	df-xp 5683	(𝐴 × 𝐵)	Yes	elxp 5700, opelxpi 5714, xpundi 5745
xr	eXtended reals	df-xr 11282	ℝ*	Yes	ressxr 11288, rexr 11290, 0xr 11291
z	integers (from German "Zahlen")	df-z 12589	ℤ	Yes	elz 12590, zcn 12593
zn	ring of integers mod 𝑁	df-zn 21436	(ℤ/nℤ‘𝑁)	Yes	znval 21469, zncrng 21482, znhash 21496
zring	ring of integers	df-zring 21377	ℤring	Yes	zringbas 21383, zringcrng 21378
0, z	slashed zero (empty set)	df-nul 4324	∅	Yes	n0i 4334, vn0 4339; snnz 4781, prnz 4782

(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.)

Hypothesis

Ref	Expression
conventions-labels.1	⊢ 𝜑

Assertion

Ref	Expression
conventions-labels	⊢ 𝜑

Proof of Theorem conventions-labels

Step	Hyp	Ref	Expression
1		conventions-labels.1	1 ⊢ 𝜑

This theorem is referenced by: (None)