| Description:
The following gives conventions used in the Metamath Proof Explorer
(MPE, set.mm) regarding labels.
For other conventions, see conventions 30375 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 3049"rgen.1 $e |- ( x e. A -> ph ) $."
or letters corresponding to the (main) class variable used in the
hypothesis, e.g., for mdet0 22519: "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 2658 and stirling 46126.
- 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 1840, and the restricted quantifier version of Theorem 21 from
Section 19 of [Margaris] p. 90 is labeled r19.21 3227.
- 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... 15785. 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 3905, and thus its syntax label fragment is "dif". Similarly, the
subclass relation 𝐴 ⊆ 𝐵 has syntax label fragment "ss"
because it is defined in df-ss 3919. 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 4086. There are many other syntax label fragments, e.g.,
singleton construct {𝐴} has syntax label fragment "sn" (because it
is defined in df-sn 4577), and the pair construct {𝐴, 𝐵} has
fragment "pr" ( from df-pr 4579). 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 4738. An "n" is often used for negation (¬), e.g.,
nan 829.
- 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 11009) and "re" represents real numbers ℝ (Definition df-r 11013).
The empty set ∅ often uses fragment 0, even though it is defined
in df-nul 4284. The syntax construct (𝐴 + 𝐵) usually uses the
fragment "add" (which is consistent with df-add 11014), 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 12252.
- 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 16056 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 15974) we have value cosval 16029 and
closure coscl 16033.
- 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 30378 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 1940 versus 19.21 2210. This
often permits to prove the result using fewer axioms, and/or to
eliminate a nonfreeness hypothesis (such as Ⅎ𝑥𝜑 in 19.21 2210).
If no constraint is put on axiom use, then the v-version can be proved
from the original theorem using nfv 1915. If two (resp. three) such
disjoint variable conditions are added, then the suffix "vv" (resp.
"vvv") is used, e.g., exlimivv 1933.
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 2571 derived from eu6 2569. 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 5390.
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 2409 (cbval 2398 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 3515.
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 584), commutes
(e.g., biimpac 478)
- 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 476, rexlimiva 3125 |
| abl | Abelian group | df-abl 19693 |
Abel | Yes | ablgrp 19695, zringabl 21386 |
| abs | absorption | | | No |
ressabs 17156 |
| abs | absolute value (of a complex number) |
df-abs 15140 | (abs‘𝐴) | Yes |
absval 15142, absneg 15181, abs1 15201 |
| ad | adding | |
| No | adantr 480, ad2antlr 727 |
| add | add (see "p") | df-add 11014 |
(𝐴 + 𝐵) | Yes |
addcl 11085, addcom 11296, addass 11090 |
| al | "for all" | |
∀𝑥𝜑 | No | alim 1811, alex 1827 |
| ALT | alternative/less preferred (suffix) | |
| No | idALT 23 |
| an | and | df-an 396 |
(𝜑 ∧ 𝜓) | Yes |
anor 984, iman 401, imnan 399 |
| ant | antecedent | |
| No | adantr 480 |
| ass | associative | |
| No | biass 384, orass 921, mulass 11091 |
| asym | asymmetric, antisymmetric | |
| No | intasym 6062, asymref 6063, posasymb 18222 |
| ax | axiom | |
| No | ax6dgen 2131, ax1cn 11037 |
| bas, base |
base (set of an extensible structure) | df-base 17118 |
(Base‘𝑆) | Yes |
baseval 17119, ressbas 17144, cnfldbas 21293 |
| b, bi | biconditional ("iff", "if and only if")
| df-bi 207 | (𝜑 ↔ 𝜓) | Yes |
impbid 212, sspwb 5390 |
| br | binary relation | df-br 5092 |
𝐴𝑅𝐵 | Yes | brab1 5139, brun 5142 |
| c | commutes, commuted (suffix) | | |
No | biimpac 478 |
| c | contraction (suffix) | | |
No | sylc 65, syl2anc 584 |
| cbv | change bound variable | | |
No | cbvalivw 2008, cbvrex 3329 |
| cdm | codomain | |
| No | ffvelcdm 7014, focdmex 7888 |
| cl | closure | | | No |
ifclda 4511, ovrcl 7387, zaddcl 12509 |
| cn | complex numbers | df-c 11009 |
ℂ | Yes | nnsscn 12127, nncn 12130 |
| cnfld | field of complex numbers | df-cnfld 21290 |
ℂfld | Yes | cnfldbas 21293, cnfldinv 21337 |
| cntz | centralizer | df-cntz 19227 |
(Cntz‘𝑀) | Yes |
cntzfval 19230, dprdfcntz 19927 |
| cnv | converse | df-cnv 5624 |
◡𝐴 | Yes | opelcnvg 5820, f1ocnv 6775 |
| co | composition | df-co 5625 |
(𝐴 ∘ 𝐵) | Yes | cnvco 5825, fmptco 7062 |
| com | commutative | |
| No | orcom 870, bicomi 224, eqcomi 2740 |
| con | contradiction, contraposition | |
| No | condan 817, con2d 134 |
| csb | class substitution | df-csb 3851 |
⦋𝐴 / 𝑥⦌𝐵 | Yes |
csbid 3863, csbie2g 3890 |
| cyg | cyclic group | df-cyg 19788 |
CycGrp | Yes |
iscyg 19789, zringcyg 21404 |
| d | deduction form (suffix) | |
| No | idd 24, impbid 212 |
| df | (alternate) definition (prefix) | |
| No | dfrel2 6136, dffn2 6653 |
| di, distr | distributive | |
| No |
andi 1009, imdi 389, ordi 1007, difindi 4242, ndmovdistr 7535 |
| dif | class difference | df-dif 3905 |
(𝐴 ∖ 𝐵) | Yes |
difss 4086, difindi 4242 |
| div | division | df-div 11772 |
(𝐴 / 𝐵) | Yes |
divcl 11779, divval 11775, divmul 11776 |
| dm | domain | df-dm 5626 |
dom 𝐴 | Yes | dmmpt 6187, iswrddm0 14442 |
| e, eq, equ | equals (equ for setvars, eq for
classes) | df-cleq 2723 |
𝐴 = 𝐵 | Yes |
2p2e4 12252, uneqri 4106, equtr 2022 |
| edg | edge | df-edg 29024 |
(Edg‘𝐺) | Yes |
edgopval 29027, usgredgppr 29172 |
| el | element of | |
𝐴 ∈ 𝐵 | Yes |
eldif 3912, eldifsn 4738, elssuni 4889 |
| en | equinumerous | df-en |
𝐴 ≈ 𝐵 | Yes | domen 8884, enfi 9096 |
| eu | "there exists exactly one" | eu6 2569 |
∃!𝑥𝜑 | Yes | euex 2572, euabsn 4679 |
| ex | exists (i.e. is a set) | |
∈ V | No | brrelex1 5669, 0ex 5245 |
| ex, e | "there exists (at least one)" |
df-ex 1781 |
∃𝑥𝜑 | Yes | exim 1835, alex 1827 |
| exp | export | |
| No | expt 177, expcom 413 |
| f | "not free in" (suffix) | |
| No | equs45f 2459, sbf 2273 |
| f | function | df-f 6485 |
𝐹:𝐴⟶𝐵 | Yes | fssxp 6678, opelf 6684 |
| fal | false | df-fal 1554 |
⊥ | Yes | bifal 1557, falantru 1576 |
| fi | finite intersection | df-fi 9295 |
(fi‘𝐵) | Yes | fival 9296, inelfi 9302 |
| fi, fin | finite | df-fin 8873 |
Fin | Yes |
isfi 8898, snfi 8965, onfin 9124 |
| fld | field (Note: there is an alternative
definition Fld of a field, see df-fld 38031) | df-field 20645 |
Field | Yes | isfld 20653, fldidom 20684 |
| fn | function with domain | df-fn 6484 |
𝐴 Fn 𝐵 | Yes | ffn 6651, fndm 6584 |
| frgp | free group | df-frgp 19620 |
(freeGrp‘𝐼) | Yes |
frgpval 19668, frgpadd 19673 |
| fsupp | finitely supported function |
df-fsupp 9246 | 𝑅 finSupp 𝑍 | Yes |
isfsupp 9249, fdmfisuppfi 9258, fsuppco 9286 |
| fun | function | df-fun 6483 |
Fun 𝐹 | Yes | funrel 6498, ffun 6654 |
| fv | function value | df-fv 6489 |
(𝐹‘𝐴) | Yes | fvres 6841, swrdfv 14553 |
| fz | finite set of sequential integers |
df-fz 13405 |
(𝑀...𝑁) | Yes | fzval 13406, eluzfz 13416 |
| fz0 | finite set of sequential nonnegative integers |
|
(0...𝑁) | Yes | nn0fz0 13522, fz0tp 13525 |
| fzo | half-open integer range | df-fzo 13552 |
(𝑀..^𝑁) | Yes |
elfzo 13558, elfzofz 13572 |
| g | more general (suffix); eliminates "is a set"
hypotheses | |
| No | uniexg 7673 |
| gr | graph | |
| No | uhgrf 29038, isumgr 29071, usgrres1 29291 |
| grp | group | df-grp 18846 |
Grp | Yes | isgrp 18849, tgpgrp 23991 |
| gsum | group sum | df-gsum 17343 |
(𝐺 Σg 𝐹) | Yes |
gsumval 18582, gsumwrev 19276 |
| hash | size (of a set) | df-hash 14235 |
(♯‘𝐴) | Yes |
hashgval 14237, hashfz1 14250, hashcl 14260 |
| hb | hypothesis builder (prefix) | |
| No | hbxfrbi 1826, hbald 2171, hbequid 38947 |
| hm | (monoid, group, ring, ...) homomorphism |
| | No |
ismhm 18690, isghm 19125, isrhm 20394 |
| i | inference (suffix) | |
| No | eleq1i 2822, tcsni 9633 |
| i | implication (suffix) | |
| No | brwdomi 9454, infeq5i 9526 |
| id | identity | |
| No | biid 261 |
| iedg | indexed edge | df-iedg 28975 |
(iEdg‘𝐺) | Yes |
iedgval0 29016, edgiedgb 29030 |
| idm | idempotent | |
| No | anidm 564, tpidm13 4709 |
| im, imp | implication (label often omitted) |
df-im 15005 | (𝐴 → 𝐵) | Yes |
iman 401, imnan 399, impbidd 210 |
| im | (group, ring, ...) isomorphism | |
| No | isgim 19172, rimrcl 20397 |
| ima | image | df-ima 5629 |
(𝐴 “ 𝐵) | Yes | resima 5964, imaundi 6096 |
| imp | import | |
| No | biimpa 476, impcom 407 |
| in | intersection | df-in 3909 |
(𝐴 ∩ 𝐵) | Yes | elin 3918, incom 4159 |
| inf | infimum | df-inf 9327 |
inf(ℝ+, ℝ*, < ) | Yes |
fiinfcl 9387, infiso 9394 |
| is... | is (something a) ...? | |
| No | isring 20153 |
| j | joining, disjoining | |
| No | jc 161, jaoi 857 |
| l | left | |
| No | olcd 874, simpl 482 |
| map | mapping operation or set exponentiation |
df-map 8752 | (𝐴 ↑m 𝐵) | Yes |
mapvalg 8760, elmapex 8772 |
| mat | matrix | df-mat 22321 |
(𝑁 Mat 𝑅) | Yes |
matval 22324, matring 22356 |
| mdet | determinant (of a square matrix) |
df-mdet 22498 | (𝑁 maDet 𝑅) | Yes |
mdetleib 22500, mdetrlin 22515 |
| mgm | magma | df-mgm 18545 |
Magma | Yes |
mgmidmo 18565, mgmlrid 18572, ismgm 18546 |
| mgp | multiplicative group | df-mgp 20057 |
(mulGrp‘𝑅) | Yes |
mgpress 20066, ringmgp 20155 |
| mnd | monoid | df-mnd 18640 |
Mnd | Yes | mndass 18648, mndodcong 19452 |
| mo | "there exists at most one" | df-mo 2535 |
∃*𝑥𝜑 | Yes | eumo 2573, moim 2539 |
| mp | modus ponens | ax-mp 5 |
| No | mpd 15, mpi 20 |
| mpo | maps-to notation for an operation |
df-mpo 7351 | (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) | Yes |
mpompt 7460, resmpo 7466 |
| mpt | modus ponendo tollens | |
| No | mptnan 1769, mptxor 1770 |
| mpt | maps-to notation for a function |
df-mpt 5173 | (𝑥 ∈ 𝐴 ↦ 𝐵) | Yes |
fconstmpt 5678, resmpt 5986 |
| mul | multiplication (see "t") | df-mul 11015 |
(𝐴 · 𝐵) | Yes |
mulcl 11087, divmul 11776, mulcom 11089, mulass 11091 |
| n, not | not | |
¬ 𝜑 | Yes |
nan 829, notnotr 130 |
| ne | not equal | df-ne | 𝐴 ≠ 𝐵 |
Yes | exmidne 2938, neeqtrd 2997 |
| nel | not element of | df-nel | 𝐴 ∉ 𝐵
|
Yes | neli 3034, nnel 3042 |
| ne0 | not equal to zero (see n0) | |
≠ 0 | No |
negne0d 11467, ine0 11549, gt0ne0 11579 |
| nf | "not free in" (prefix) | df-nf 1785 |
Ⅎ𝑥𝜑 | Yes | nfnd 1859 |
| ngp | normed group | df-ngp 24496 |
NrmGrp | Yes | isngp 24509, ngptps 24515 |
| nm | norm (on a group or ring) | df-nm 24495 |
(norm‘𝑊) | Yes |
nmval 24502, subgnm 24546 |
| nn | positive integers | df-nn 12123 |
ℕ | Yes | nnsscn 12127, nncn 12130 |
| nn0 | nonnegative integers | df-n0 12379 |
ℕ0 | Yes | nnnn0 12385, nn0cn 12388 |
| n0 | not the empty set (see ne0) | |
≠ ∅ | No | n0i 4290, vn0 4295, ssn0 4354 |
| OLD | old, obsolete (to be removed soon) | |
| No | 19.43OLD 1884 |
| on | ordinal number | df-on 6310 |
𝐴 ∈ On | Yes |
elon 6315, 1on 8397 onelon 6331 |
| op | ordered pair | df-op 4583 |
⟨𝐴, 𝐵⟩ | Yes | dfopif 4822, opth 5416 |
| or | or | df-or 848 |
(𝜑 ∨ 𝜓) | Yes |
orcom 870, anor 984 |
| ot | ordered triple | df-ot 4585 |
⟨𝐴, 𝐵, 𝐶⟩ | Yes |
euotd 5453, fnotovb 7398 |
| ov | operation value | df-ov 7349 |
(𝐴𝐹𝐵) | Yes
| fnotovb 7398, fnovrn 7521 |
| p | plus (see "add"), for all-constant
theorems | df-add 11014 |
(3 + 2) = 5 | Yes |
3p2e5 12268 |
| pfx | prefix | df-pfx 14576 |
(𝑊 prefix 𝐿) | Yes |
pfxlen 14588, ccatpfx 14605 |
| pm | Principia Mathematica | |
| No | pm2.27 42 |
| pm | partial mapping (operation) | df-pm 8753 |
(𝐴 ↑pm 𝐵) | Yes | elpmi 8770, pmsspw 8801 |
| pr | pair | df-pr 4579 |
{𝐴, 𝐵} | Yes |
elpr 4601, prcom 4685, prid1g 4713, prnz 4730 |
| prm, prime | prime (number) | df-prm 16580 |
ℙ | Yes | 1nprm 16587, dvdsprime 16595 |
| pss | proper subset | df-pss 3922 |
𝐴 ⊊ 𝐵 | Yes | pssss 4048, sspsstri 4055 |
| q | rational numbers ("quotients") | df-q 12844 |
ℚ | Yes | elq 12845 |
| r | reversed (suffix) | |
| No | pm4.71r 558, caovdir 7580 |
| r | right | |
| No | orcd 873, simprl 770 |
| rab | restricted class abstraction |
df-rab 3396 | {𝑥 ∈ 𝐴 ∣ 𝜑} | Yes |
rabswap 3404, df-oprab 7350 |
| ral | restricted universal quantification |
df-ral 3048 | ∀𝑥 ∈ 𝐴𝜑 | Yes |
ralnex 3058, ralrnmpo 7485 |
| rcl | reverse closure | |
| No | ndmfvrcl 6855, nnarcl 8531 |
| re | real numbers | df-r 11013 |
ℝ | Yes | recn 11093, 0re 11111 |
| rel | relation | df-rel 5623 | Rel 𝐴 |
Yes | brrelex1 5669, relmpoopab 8024 |
| res | restriction | df-res 5628 |
(𝐴 ↾ 𝐵) | Yes |
opelres 5934, f1ores 6777 |
| reu | restricted existential uniqueness |
df-reu 3347 | ∃!𝑥 ∈ 𝐴𝜑 | Yes |
nfreud 3392, reurex 3350 |
| rex | restricted existential quantification |
df-rex 3057 | ∃𝑥 ∈ 𝐴𝜑 | Yes |
rexnal 3084, rexrnmpo 7486 |
| rmo | restricted "at most one" |
df-rmo 3346 | ∃*𝑥 ∈ 𝐴𝜑 | Yes |
nfrmod 3391, nrexrmo 3365 |
| rn | range | df-rn 5627 | ran 𝐴 |
Yes | elrng 5831, rncnvcnv 5874 |
| ring | (unital) ring | df-ring 20151 |
Ring | Yes |
ringidval 20099, isring 20153, ringgrp 20154 |
| rng | non-unital ring | df-rng 20069 |
Rng | Yes |
isrng 20070, rngabl 20071, rnglz 20081 |
| rot | rotation | |
| No | 3anrot 1099, 3orrot 1091 |
| s | eliminates need for syllogism (suffix) |
| | No | ancoms 458 |
| sb | (proper) substitution (of a set) |
df-sb 2068 | [𝑦 / 𝑥]𝜑 | Yes |
spsbe 2085, sbimi 2077 |
| sbc | (proper) substitution of a class |
df-sbc 3742 | [𝐴 / 𝑥]𝜑 | Yes |
sbc2or 3750, sbcth 3756 |
| sca | scalar | df-sca 17174 |
(Scalar‘𝐻) | Yes |
resssca 17244, mgpsca 20062 |
| simp | simple, simplification | |
| No | simpl 482, simp3r3 1284 |
| sn | singleton | df-sn 4577 |
{𝐴} | Yes | eldifsn 4738 |
| sp | specialization | |
| No | spsbe 2085, spei 2394 |
| ss | subset | df-ss 3919 |
𝐴 ⊆ 𝐵 | Yes | difss 4086 |
| struct | structure | df-struct 17055 |
Struct | Yes | brstruct 17056, structfn 17064 |
| sub | subtract | df-sub 11343 |
(𝐴 − 𝐵) | Yes |
subval 11348, subaddi 11445 |
| sup | supremum | df-sup 9326 |
sup(𝐴, 𝐵, < ) | Yes |
fisupcl 9354, supmo 9336 |
| supp | support (of a function) | df-supp 8091 |
(𝐹 supp 𝑍) | Yes |
ressuppfi 9279, mptsuppd 8117 |
| swap | swap (two parts within a theorem) |
| | No | rabswap 3404, 2reuswap 3705 |
| syl | syllogism | syl 17 |
| No | 3syl 18 |
| sym | symmetric | |
| No | df-symdif 4203, cnvsym 6061 |
| symg | symmetric group | df-symg 19280 |
(SymGrp‘𝐴) | Yes |
symghash 19288, pgrpsubgsymg 19319 |
| t |
times (see "mul"), for all-constant theorems |
df-mul 11015 |
(3 · 2) = 6 | Yes |
3t2e6 12283 |
| th, t |
theorem |
|
|
No |
nfth 1802, sbcth 3756, weth 10383, ancomst 464 |
| tp | triple | df-tp 4581 |
{𝐴, 𝐵, 𝐶} | Yes |
eltpi 4641, tpeq1 4695 |
| tr | transitive | |
| No | bitrd 279, biantr 805 |
| tru, t |
true, truth |
df-tru 1544 |
⊤ |
Yes |
bitru 1550, truanfal 1575, biimt 360 |
| un | union | df-un 3907 |
(𝐴 ∪ 𝐵) | Yes |
uneqri 4106, uncom 4108 |
| unit | unit (in a ring) |
df-unit 20274 | (Unit‘𝑅) | Yes |
isunit 20289, nzrunit 20437 |
| v |
setvar (especially for specializations of
theorems when a class is replaced by a setvar variable) |
|
x |
Yes |
cv 1540, vex 3440, velpw 4555, vtoclf 3519 |
| v |
disjoint variable condition used in place of nonfreeness
hypothesis (suffix) |
|
|
No |
spimv 2390 |
| vtx |
vertex |
df-vtx 28974 |
(Vtx‘𝐺) |
Yes |
vtxval0 29015, opvtxov 28981 |
| vv |
two disjoint variable conditions used in place of nonfreeness
hypotheses (suffix) |
|
|
No |
19.23vv 1944 |
| w | weak (version of a theorem) (suffix) | |
| No | ax11w 2133, spnfw 1980 |
| wrd | word |
df-word 14418 | Word 𝑆 | Yes |
iswrdb 14424, wrdfn 14432, ffz0iswrd 14445 |
| xp | cross product (Cartesian product) |
df-xp 5622 | (𝐴 × 𝐵) | Yes |
elxp 5639, opelxpi 5653, xpundi 5685 |
| xr | eXtended reals | df-xr 11147 |
ℝ* | Yes | ressxr 11153, rexr 11155, 0xr 11156 |
| z | integers (from German "Zahlen") |
df-z 12466 | ℤ | Yes |
elz 12467, zcn 12470 |
| zn | ring of integers mod 𝑁 | df-zn 21441 |
(ℤ/nℤ‘𝑁) | Yes |
znval 21470, zncrng 21479, znhash 21493 |
| zring | ring of integers | df-zring 21382 |
ℤring | Yes | zringbas 21388, zringcrng 21383
|
| 0, z |
slashed zero (empty set) | df-nul 4284 |
∅ | Yes |
n0i 4290, vn0 4295; snnz 4729, prnz 4730 |
(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.) |
