| Description:
The following gives conventions used in the Metamath Proof Explorer
(MPE, set.mm) regarding labels.
For other conventions, see conventions 30475 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 22550: "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 2663 and stirling 46329.
- 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 3231.
- 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... 15804. 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 3904, and thus its syntax label fragment is "dif". Similarly, the
subclass relation 𝐴 ⊆ 𝐵 has syntax label fragment "ss"
because it is defined in df-ss 3918. 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 4088. There are many other syntax label fragments, e.g.,
singleton construct {𝐴} has syntax label fragment "sn" (because it
is defined in df-sn 4581), and the pair construct {𝐴, 𝐵} has
fragment "pr" ( from df-pr 4583). 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 4742. 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 11032) and "re" represents real numbers ℝ (Definition df-r 11036).
The empty set ∅ often uses fragment 0, even though it is defined
in df-nul 4286. The syntax construct (𝐴 + 𝐵) usually uses the
fragment "add" (which is consistent with df-add 11037), 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 12275.
- 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 16075 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 15993) we have value cosval 16048 and
closure coscl 16052.
- 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 30478 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 2214. This
often permits to prove the result using fewer axioms, and/or to
eliminate a nonfreeness hypothesis (such as Ⅎ𝑥𝜑 in 19.21 2214).
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 2576 derived from eu6 2574. 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 5397.
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 2413 (cbval 2402 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 3517.
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 3129 |
| abl | Abelian group | df-abl 19712 |
Abel | Yes | ablgrp 19714, zringabl 21406 |
| abs | absorption | | | No |
ressabs 17175 |
| abs | absolute value (of a complex number) |
df-abs 15159 | (abs‘𝐴) | Yes |
absval 15161, absneg 15200, abs1 15220 |
| ad | adding | |
| No | adantr 480, ad2antlr 727 |
| add | add (see "p") | df-add 11037 |
(𝐴 + 𝐵) | Yes |
addcl 11108, addcom 11319, addass 11113 |
| 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 11114 |
| asym | asymmetric, antisymmetric | |
| No | intasym 6072, asymref 6073, posasymb 18242 |
| ax | axiom | |
| No | ax6dgen 2133, ax1cn 11060 |
| bas, base |
base (set of an extensible structure) | df-base 17137 |
(Base‘𝑆) | Yes |
baseval 17138, ressbas 17163, cnfldbas 21313 |
| b, bi | biconditional ("iff", "if and only if")
| df-bi 207 | (𝜑 ↔ 𝜓) | Yes |
impbid 212, sspwb 5397 |
| br | binary relation | df-br 5099 |
𝐴𝑅𝐵 | Yes | brab1 5146, brun 5149 |
| c | commutes, commuted (suffix) | | |
No | biimpac 478 |
| c | contraction (suffix) | | |
No | sylc 65, syl2anc 584 |
| cbv | change bound variable | | |
No | cbvalivw 2008, cbvrex 3333 |
| cdm | codomain | |
| No | ffvelcdm 7026, focdmex 7900 |
| cl | closure | | | No |
ifclda 4515, ovrcl 7399, zaddcl 12531 |
| cn | complex numbers | df-c 11032 |
ℂ | Yes | nnsscn 12150, nncn 12153 |
| cnfld | field of complex numbers | df-cnfld 21310 |
ℂfld | Yes | cnfldbas 21313, cnfldinv 21357 |
| cntz | centralizer | df-cntz 19246 |
(Cntz‘𝑀) | Yes |
cntzfval 19249, dprdfcntz 19946 |
| cnv | converse | df-cnv 5632 |
◡𝐴 | Yes | opelcnvg 5829, f1ocnv 6786 |
| co | composition | df-co 5633 |
(𝐴 ∘ 𝐵) | Yes | cnvco 5834, fmptco 7074 |
| com | commutative | |
| No | orcom 870, bicomi 224, eqcomi 2745 |
| con | contradiction, contraposition | |
| No | condan 817, con2d 134 |
| csb | class substitution | df-csb 3850 |
⦋𝐴 / 𝑥⦌𝐵 | Yes |
csbid 3862, csbie2g 3889 |
| cyg | cyclic group | df-cyg 19807 |
CycGrp | Yes |
iscyg 19808, zringcyg 21424 |
| d | deduction form (suffix) | |
| No | idd 24, impbid 212 |
| df | (alternate) definition (prefix) | |
| No | dfrel2 6147, dffn2 6664 |
| di, distr | distributive | |
| No |
andi 1009, imdi 389, ordi 1007, difindi 4244, ndmovdistr 7547 |
| dif | class difference | df-dif 3904 |
(𝐴 ∖ 𝐵) | Yes |
difss 4088, difindi 4244 |
| div | division | df-div 11795 |
(𝐴 / 𝐵) | Yes |
divcl 11802, divval 11798, divmul 11799 |
| dm | domain | df-dm 5634 |
dom 𝐴 | Yes | dmmpt 6198, iswrddm0 14461 |
| e, eq, equ | equals (equ for setvars, eq for
classes) | df-cleq 2728 |
𝐴 = 𝐵 | Yes |
2p2e4 12275, uneqri 4108, equtr 2022 |
| edg | edge | df-edg 29121 |
(Edg‘𝐺) | Yes |
edgopval 29124, usgredgppr 29269 |
| el | element of | |
𝐴 ∈ 𝐵 | Yes |
eldif 3911, eldifsn 4742, elssuni 4894 |
| en | equinumerous | df-en |
𝐴 ≈ 𝐵 | Yes | domen 8898, enfi 9111 |
| eu | "there exists exactly one" | eu6 2574 |
∃!𝑥𝜑 | Yes | euex 2577, euabsn 4683 |
| ex | exists (i.e. is a set) | |
∈ V | No | brrelex1 5677, 0ex 5252 |
| 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 2463, sbf 2277 |
| f | function | df-f 6496 |
𝐹:𝐴⟶𝐵 | Yes | fssxp 6689, opelf 6695 |
| fal | false | df-fal 1554 |
⊥ | Yes | bifal 1557, falantru 1576 |
| fi | finite intersection | df-fi 9314 |
(fi‘𝐵) | Yes | fival 9315, inelfi 9321 |
| fi, fin | finite | df-fin 8887 |
Fin | Yes |
isfi 8912, snfi 8980, onfin 9139 |
| fld | field (Note: there is an alternative
definition Fld of a field, see df-fld 38189) | df-field 20665 |
Field | Yes | isfld 20673, fldidom 20704 |
| fn | function with domain | df-fn 6495 |
𝐴 Fn 𝐵 | Yes | ffn 6662, fndm 6595 |
| frgp | free group | df-frgp 19639 |
(freeGrp‘𝐼) | Yes |
frgpval 19687, frgpadd 19692 |
| fsupp | finitely supported function |
df-fsupp 9265 | 𝑅 finSupp 𝑍 | Yes |
isfsupp 9268, fdmfisuppfi 9277, fsuppco 9305 |
| fun | function | df-fun 6494 |
Fun 𝐹 | Yes | funrel 6509, ffun 6665 |
| fv | function value | df-fv 6500 |
(𝐹‘𝐴) | Yes | fvres 6853, swrdfv 14572 |
| fz | finite set of sequential integers |
df-fz 13424 |
(𝑀...𝑁) | Yes | fzval 13425, eluzfz 13435 |
| fz0 | finite set of sequential nonnegative integers |
|
(0...𝑁) | Yes | nn0fz0 13541, fz0tp 13544 |
| fzo | half-open integer range | df-fzo 13571 |
(𝑀..^𝑁) | Yes |
elfzo 13577, elfzofz 13591 |
| g | more general (suffix); eliminates "is a set"
hypotheses | |
| No | uniexg 7685 |
| gr | graph | |
| No | uhgrf 29135, isumgr 29168, usgrres1 29388 |
| grp | group | df-grp 18866 |
Grp | Yes | isgrp 18869, tgpgrp 24022 |
| gsum | group sum | df-gsum 17362 |
(𝐺 Σg 𝐹) | Yes |
gsumval 18602, gsumwrev 19295 |
| hash | size (of a set) | df-hash 14254 |
(♯‘𝐴) | Yes |
hashgval 14256, hashfz1 14269, hashcl 14279 |
| hb | hypothesis builder (prefix) | |
| No | hbxfrbi 1826, hbald 2173, hbequid 39165 |
| hm | (monoid, group, ring, ...) homomorphism |
| | No |
ismhm 18710, isghm 19144, isrhm 20414 |
| i | inference (suffix) | |
| No | eleq1i 2827, tcsni 9650 |
| i | implication (suffix) | |
| No | brwdomi 9473, infeq5i 9545 |
| id | identity | |
| No | biid 261 |
| iedg | indexed edge | df-iedg 29072 |
(iEdg‘𝐺) | Yes |
iedgval0 29113, edgiedgb 29127 |
| idm | idempotent | |
| No | anidm 564, tpidm13 4713 |
| im, imp | implication (label often omitted) |
df-im 15024 | (𝐴 → 𝐵) | Yes |
iman 401, imnan 399, impbidd 210 |
| im | (group, ring, ...) isomorphism | |
| No | isgim 19191, rimrcl 20417 |
| ima | image | df-ima 5637 |
(𝐴 “ 𝐵) | Yes | resima 5974, imaundi 6107 |
| imp | import | |
| No | biimpa 476, impcom 407 |
| in | intersection | df-in 3908 |
(𝐴 ∩ 𝐵) | Yes | elin 3917, incom 4161 |
| inf | infimum | df-inf 9346 |
inf(ℝ+, ℝ*, < ) | Yes |
fiinfcl 9406, infiso 9413 |
| is... | is (something a) ...? | |
| No | isring 20172 |
| j | joining, disjoining | |
| No | jc 161, jaoi 857 |
| l | left | |
| No | olcd 874, simpl 482 |
| map | mapping operation or set exponentiation |
df-map 8765 | (𝐴 ↑m 𝐵) | Yes |
mapvalg 8773, elmapex 8785 |
| mat | matrix | df-mat 22352 |
(𝑁 Mat 𝑅) | Yes |
matval 22355, matring 22387 |
| mdet | determinant (of a square matrix) |
df-mdet 22529 | (𝑁 maDet 𝑅) | Yes |
mdetleib 22531, mdetrlin 22546 |
| mgm | magma | df-mgm 18565 |
Magma | Yes |
mgmidmo 18585, mgmlrid 18592, ismgm 18566 |
| mgp | multiplicative group | df-mgp 20076 |
(mulGrp‘𝑅) | Yes |
mgpress 20085, ringmgp 20174 |
| mnd | monoid | df-mnd 18660 |
Mnd | Yes | mndass 18668, mndodcong 19471 |
| mo | "there exists at most one" | df-mo 2539 |
∃*𝑥𝜑 | Yes | eumo 2578, moim 2544 |
| mp | modus ponens | ax-mp 5 |
| No | mpd 15, mpi 20 |
| mpo | maps-to notation for an operation |
df-mpo 7363 | (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) | Yes |
mpompt 7472, resmpo 7478 |
| mpt | modus ponendo tollens | |
| No | mptnan 1769, mptxor 1770 |
| mpt | maps-to notation for a function |
df-mpt 5180 | (𝑥 ∈ 𝐴 ↦ 𝐵) | Yes |
fconstmpt 5686, resmpt 5996 |
| mul | multiplication (see "t") | df-mul 11038 |
(𝐴 · 𝐵) | Yes |
mulcl 11110, divmul 11799, mulcom 11112, mulass 11114 |
| n, not | not | |
¬ 𝜑 | Yes |
nan 829, notnotr 130 |
| ne | not equal | df-ne | 𝐴 ≠ 𝐵 |
Yes | exmidne 2942, neeqtrd 3001 |
| nel | not element of | df-nel | 𝐴 ∉ 𝐵
|
Yes | neli 3038, nnel 3046 |
| ne0 | not equal to zero (see n0) | |
≠ 0 | No |
negne0d 11490, ine0 11572, gt0ne0 11602 |
| nf | "not free in" (prefix) | df-nf 1785 |
Ⅎ𝑥𝜑 | Yes | nfnd 1859 |
| ngp | normed group | df-ngp 24527 |
NrmGrp | Yes | isngp 24540, ngptps 24546 |
| nm | norm (on a group or ring) | df-nm 24526 |
(norm‘𝑊) | Yes |
nmval 24533, subgnm 24577 |
| nn | positive integers | df-nn 12146 |
ℕ | Yes | nnsscn 12150, nncn 12153 |
| nn0 | nonnegative integers | df-n0 12402 |
ℕ0 | Yes | nnnn0 12408, nn0cn 12411 |
| n0 | not the empty set (see ne0) | |
≠ ∅ | No | n0i 4292, vn0 4297, ssn0 4356 |
| OLD | old, obsolete (to be removed soon) | |
| No | 19.43OLD 1884 |
| on | ordinal number | df-on 6321 |
𝐴 ∈ On | Yes |
elon 6326, 1on 8409 onelon 6342 |
| op | ordered pair | df-op 4587 |
⟨𝐴, 𝐵⟩ | Yes | dfopif 4826, opth 5424 |
| or | or | df-or 848 |
(𝜑 ∨ 𝜓) | Yes |
orcom 870, anor 984 |
| ot | ordered triple | df-ot 4589 |
⟨𝐴, 𝐵, 𝐶⟩ | Yes |
euotd 5461, fnotovb 7410 |
| ov | operation value | df-ov 7361 |
(𝐴𝐹𝐵) | Yes
| fnotovb 7410, fnovrn 7533 |
| p | plus (see "add"), for all-constant
theorems | df-add 11037 |
(3 + 2) = 5 | Yes |
3p2e5 12291 |
| pfx | prefix | df-pfx 14595 |
(𝑊 prefix 𝐿) | Yes |
pfxlen 14607, ccatpfx 14624 |
| pm | Principia Mathematica | |
| No | pm2.27 42 |
| pm | partial mapping (operation) | df-pm 8766 |
(𝐴 ↑pm 𝐵) | Yes | elpmi 8783, pmsspw 8815 |
| pr | pair | df-pr 4583 |
{𝐴, 𝐵} | Yes |
elpr 4605, prcom 4689, prid1g 4717, prnz 4734 |
| prm, prime | prime (number) | df-prm 16599 |
ℙ | Yes | 1nprm 16606, dvdsprime 16614 |
| pss | proper subset | df-pss 3921 |
𝐴 ⊊ 𝐵 | Yes | pssss 4050, sspsstri 4057 |
| q | rational numbers ("quotients") | df-q 12862 |
ℚ | Yes | elq 12863 |
| r | reversed (suffix) | |
| No | pm4.71r 558, caovdir 7592 |
| r | right | |
| No | orcd 873, simprl 770 |
| rab | restricted class abstraction |
df-rab 3400 | {𝑥 ∈ 𝐴 ∣ 𝜑} | Yes |
rabswap 3408, df-oprab 7362 |
| ral | restricted universal quantification |
df-ral 3052 | ∀𝑥 ∈ 𝐴𝜑 | Yes |
ralnex 3062, ralrnmpo 7497 |
| rcl | reverse closure | |
| No | ndmfvrcl 6867, nnarcl 8544 |
| re | real numbers | df-r 11036 |
ℝ | Yes | recn 11116, 0re 11134 |
| rel | relation | df-rel 5631 | Rel 𝐴 |
Yes | brrelex1 5677, relmpoopab 8036 |
| res | restriction | df-res 5636 |
(𝐴 ↾ 𝐵) | Yes |
opelres 5944, f1ores 6788 |
| reu | restricted existential uniqueness |
df-reu 3351 | ∃!𝑥 ∈ 𝐴𝜑 | Yes |
nfreud 3396, reurex 3354 |
| rex | restricted existential quantification |
df-rex 3061 | ∃𝑥 ∈ 𝐴𝜑 | Yes |
rexnal 3088, rexrnmpo 7498 |
| rmo | restricted "at most one" |
df-rmo 3350 | ∃*𝑥 ∈ 𝐴𝜑 | Yes |
nfrmod 3395, nrexrmo 3369 |
| rn | range | df-rn 5635 | ran 𝐴 |
Yes | elrng 5840, rncnvcnv 5883 |
| ring | (unital) ring | df-ring 20170 |
Ring | Yes |
ringidval 20118, isring 20172, ringgrp 20173 |
| rng | non-unital ring | df-rng 20088 |
Rng | Yes |
isrng 20089, rngabl 20090, rnglz 20100 |
| 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 2087, sbimi 2079 |
| sbc | (proper) substitution of a class |
df-sbc 3741 | [𝐴 / 𝑥]𝜑 | Yes |
sbc2or 3749, sbcth 3755 |
| sca | scalar | df-sca 17193 |
(Scalar‘𝐻) | Yes |
resssca 17263, mgpsca 20081 |
| simp | simple, simplification | |
| No | simpl 482, simp3r3 1284 |
| sn | singleton | df-sn 4581 |
{𝐴} | Yes | eldifsn 4742 |
| sp | specialization | |
| No | spsbe 2087, spei 2398 |
| ss | subset | df-ss 3918 |
𝐴 ⊆ 𝐵 | Yes | difss 4088 |
| struct | structure | df-struct 17074 |
Struct | Yes | brstruct 17075, structfn 17083 |
| sub | subtract | df-sub 11366 |
(𝐴 − 𝐵) | Yes |
subval 11371, subaddi 11468 |
| sup | supremum | df-sup 9345 |
sup(𝐴, 𝐵, < ) | Yes |
fisupcl 9373, supmo 9355 |
| supp | support (of a function) | df-supp 8103 |
(𝐹 supp 𝑍) | Yes |
ressuppfi 9298, mptsuppd 8129 |
| swap | swap (two parts within a theorem) |
| | No | rabswap 3408, 2reuswap 3704 |
| syl | syllogism | syl 17 |
| No | 3syl 18 |
| sym | symmetric | |
| No | df-symdif 4205, cnvsym 6071 |
| symg | symmetric group | df-symg 19299 |
(SymGrp‘𝐴) | Yes |
symghash 19307, pgrpsubgsymg 19338 |
| t |
times (see "mul"), for all-constant theorems |
df-mul 11038 |
(3 · 2) = 6 | Yes |
3t2e6 12306 |
| th, t |
theorem |
|
|
No |
nfth 1802, sbcth 3755, weth 10405, ancomst 464 |
| tp | triple | df-tp 4585 |
{𝐴, 𝐵, 𝐶} | Yes |
eltpi 4645, tpeq1 4699 |
| 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 3906 |
(𝐴 ∪ 𝐵) | Yes |
uneqri 4108, uncom 4110 |
| unit | unit (in a ring) |
df-unit 20294 | (Unit‘𝑅) | Yes |
isunit 20309, nzrunit 20457 |
| v |
setvar (especially for specializations of
theorems when a class is replaced by a setvar variable) |
|
x |
Yes |
cv 1540, vex 3444, velpw 4559, vtoclf 3521 |
| v |
disjoint variable condition used in place of nonfreeness
hypothesis (suffix) |
|
|
No |
spimv 2394 |
| vtx |
vertex |
df-vtx 29071 |
(Vtx‘𝐺) |
Yes |
vtxval0 29112, opvtxov 29078 |
| 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 2135, spnfw 1980 |
| wrd | word |
df-word 14437 | Word 𝑆 | Yes |
iswrdb 14443, wrdfn 14451, ffz0iswrd 14464 |
| xp | cross product (Cartesian product) |
df-xp 5630 | (𝐴 × 𝐵) | Yes |
elxp 5647, opelxpi 5661, xpundi 5693 |
| xr | eXtended reals | df-xr 11170 |
ℝ* | Yes | ressxr 11176, rexr 11178, 0xr 11179 |
| z | integers (from German "Zahlen") |
df-z 12489 | ℤ | Yes |
elz 12490, zcn 12493 |
| zn | ring of integers mod 𝑁 | df-zn 21461 |
(ℤ/nℤ‘𝑁) | Yes |
znval 21490, zncrng 21499, znhash 21513 |
| zring | ring of integers | df-zring 21402 |
ℤring | Yes | zringbas 21408, zringcrng 21403
|
| 0, z |
slashed zero (empty set) | df-nul 4286 |
∅ | Yes |
n0i 4292, vn0 4297; snnz 4733, prnz 4734 |
(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.) |
