| Description:
The following gives conventions used in the Metamath Proof Explorer
(MPE, set.mm) regarding labels.
For other conventions, see conventions 30762 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 3080"rgen.1 $e |- ( x e. A -> ph ) $."
or letters corresponding to the (main) class variable used in the
hypothesis, e.g., for mdet0 22774: "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 2689 and stirling 46831.
- 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 43.
- 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 1868, and the restricted quantifier version of Theorem 21 from
Section 19 of [Margaris] p. 90 is labeled r19.21 3259.
- 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... 15942. 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 3907, and thus its syntax label fragment is "dif". Similarly, the
subclass relation 𝐴 ⊆ 𝐵 has syntax label fragment "ss"
because it is defined in df-ss 3921. 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 4089. There are many other syntax label fragments, e.g.,
singleton construct {𝐴} has syntax label fragment "sn" (because it
is defined in df-sn 4589), and the pair construct {𝐴, 𝐵} has
fragment "pr" ( from df-pr 4591). 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 4752. An "n" is often used for negation (¬), e.g.,
nan 842.
- 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 11112) and "re" represents real numbers ℝ (Definition df-r 11116).
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 11117), 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 12381.
- 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 16212 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 16130) we have value cosval 16185 and
closure coscl 16189.
- 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 18 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 30765 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 1968 versus 19.21 2242. This
often permits to prove the result using fewer axioms, and/or to
eliminate a nonfreeness hypothesis (such as Ⅎ𝑥𝜑 in 19.21 2242).
If no constraint is put on axiom use, then the v-version can be proved
from the original theorem using nfv 1943. If two (resp. three) such
disjoint variable conditions are added, then the suffix "vv" (resp.
"vvv") is used, e.g., exlimivv 1961.
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 2603 derived from eu6 2601. 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 5429.
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 18) -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 2440 (cbval 2429 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 3525.
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 66, syl2anc 595), commutes
(e.g., biimpac 483)
- 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 18 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 481, rexlimiva 3157 |
| abl | Abelian group | df-abl 19859 |
Abel | Yes | ablgrp 19861, zringabl 21612 |
| abs | absorption | | | No |
ressabs 17314 |
| abs | absolute value (of a complex number) |
df-abs 15294 | (abs‘𝐴) | Yes |
absval 15296, absneg 15335, abs1 15355 |
| ad | adding | |
| No | adantr 485, ad2antlr 739 |
| add | add (see "p") | df-add 11117 |
(𝐴 + 𝐵) | Yes |
addcl 11188, addcom 11402, addass 11193 |
| al | "for all" | |
∀𝑥𝜑 | No | alim 1839, alex 1855 |
| ALT | alternative/less preferred (suffix) | |
| No | idALT 24 |
| an | and | df-an 401 |
(𝜑 ∧ 𝜓) | Yes |
anor 997, iman 406, imnan 404 |
| ant | antecedent | |
| No | adantr 485 |
| ass | associative | |
| No | biass 388, orass 934, mulass 11194 |
| asym | asymmetric, antisymmetric | |
| No | intasym 6114, asymref 6115, posasymb 18381 |
| ax | axiom | |
| No | ax6dgen 2162, ax1cn 11140 |
| bas, base |
base (set of an extensible structure) | df-base 17276 |
(Base‘𝑆) | Yes |
baseval 17277, ressbas 17302, cnfldbas 21537 |
| b, bi | biconditional ("iff", "if and only if")
| df-bi 210 | (𝜑 ↔ 𝜓) | Yes |
impbid 215, sspwb 5429 |
| br | binary relation | df-br 5109 |
𝐴𝑅𝐵 | Yes | brab1 5158, brun 5161 |
| c | commutes, commuted (suffix) | | |
No | biimpac 483 |
| c | contraction (suffix) | | |
No | sylc 66, syl2anc 595 |
| cbv | change bound variable | | |
No | cbvalivw 2036, cbvrex 3351 |
| cdm | codomain | |
| No | ffvelcdm 7076, focdmex 7951 |
| cl | closure | | | No |
ifclda 4522, ovrcl 7453, zaddcl 12640 |
| cn | complex numbers | df-c 11112 |
ℂ | Yes | nnsscn 12244, nncn 12247 |
| cnfld | field of complex numbers | df-cnfld 21534 |
ℂfld | Yes | cnfldbas 21537, cnfldinv 21564 |
| cntz | centralizer | df-cntz 19393 |
(Cntz‘𝑀) | Yes |
cntzfval 19396, dprdfcntz 20093 |
| cnv | converse | df-cnv 5668 |
◡𝐴 | Yes | opelcnvg 5865, f1ocnv 6833 |
| co | composition | df-co 5669 |
(𝐴 ∘ 𝐵) | Yes | cnvco 5874, fmptco 7125 |
| com | commutative | |
| No | orcom 883, bicomi 227, eqcomi 2771 |
| con | contradiction, contraposition | |
| No | condan 829, con2d 135 |
| csb | class substitution | df-csb 3853 |
⦋𝐴 / 𝑥⦌𝐵 | Yes |
csbid 3865, csbie2g 3892 |
| cyg | cyclic group | df-cyg 19954 |
CycGrp | Yes |
iscyg 19955, zringcyg 21630 |
| d | deduction form (suffix) | |
| No | idd 25, impbid 215 |
| df | (alternate) definition (prefix) | |
| No | dfrel2 6186, dffn2 6707 |
| di, distr | distributive | |
| No |
andi 1024, imdi 393, ordi 1022, difindi 4244, ndmovdistr 7601 |
| dif | class difference | df-dif 3907 |
(𝐴 ∖ 𝐵) | Yes |
difss 4089, difindi 4244 |
| div | division | df-div 11878 |
(𝐴 / 𝐵) | Yes |
divcl 11884, divval 11880, divmul 11881 |
| dm | domain | df-dm 5670 |
dom 𝐴 | Yes | dmmpt 6240, iswrddm0 14582 |
| e, eq, equ | equals (equ for setvars, eq for
classes) | df-cleq 2754 |
𝐴 = 𝐵 | Yes |
2p2e4 12381, uneqri 4109, equtr 2050 |
| edg | edge | df-edg 29409 |
(Edg‘𝐺) | Yes |
edgopval 29412, usgredgppr 29557 |
| el | element of | |
𝐴 ∈ 𝐵 | Yes |
eldif 3914, eldifsn 4752, elssuni 4903 |
| en | equinumerous | df-en |
𝐴 ≈ 𝐵 | Yes | domen 8956, enfi 9169 |
| eu | "there exists exactly one" | eu6 2601 |
∃!𝑥𝜑 | Yes | euex 2604, euabsn 4691 |
| ex | exists (i.e. is a set) | |
∈ V | No | brrelex1 5713, 0ex 5269 |
| ex, e | "there exists (at least one)" |
df-ex 1809 |
∃𝑥𝜑 | Yes | exim 1863, alex 1855 |
| exp | export | |
| No | expt 178, expcom 418 |
| f | "not free in" (suffix) | |
| No | equs45f 2490, sbf 2305 |
| f | function | df-f 6540 |
𝐹:𝐴⟶𝐵 | Yes | fssxp 6733, opelf 6739 |
| fal | false | df-fal 1582 |
⊥ | Yes | bifal 1585, falantru 1604 |
| fi | finite intersection | df-fi 9369 |
(fi‘𝐵) | Yes | fival 9370, inelfi 9376 |
| fi, fin | finite | df-fin 8945 |
Fin | Yes |
isfi 8970, snfi 9038, onfin 9197 |
| fld | field (Note: there is an alternative
definition Fld of a field, see df-fld 38671) | df-field 20841 |
Field | Yes | isfld 20851, fldidom 20886 |
| fn | function with domain | df-fn 6539 |
𝐴 Fn 𝐵 | Yes | ffn 6705, fndm 6638 |
| frgp | free group | df-frgp 19786 |
(freeGrp‘𝐼) | Yes |
frgpval 19834, frgpadd 19839 |
| fsupp | finitely supported function |
df-fsupp 9320 | 𝑅 finSupp 𝑍 | Yes |
isfsupp 9323, fdmfisuppfi 9332, fsuppco 9360 |
| fun | function | df-fun 6538 |
Fun 𝐹 | Yes | funrel 6553, ffun 6708 |
| fv | function value | df-fv 6544 |
(𝐹‘𝐴) | Yes | fvres 6900, swrdfv 14693 |
| fz | finite set of sequential integers |
df-fz 13542 |
(𝑀...𝑁) | Yes | fzval 13543, eluzfz 13553 |
| fz0 | finite set of sequential nonnegative integers |
|
(0...𝑁) | Yes | nn0fz0 13660, fz0tp 13663 |
| fzo | half-open integer range | df-fzo 13690 |
(𝑀..^𝑁) | Yes |
elfzo 13696, elfzofz 13711 |
| g | more general (suffix); eliminates "is a set"
hypotheses | |
| No | uniexg 7740 |
| gr | graph | |
| No | uhgrf 29423, isumgr 29456, usgrres1 29676 |
| grp | group | df-grp 19009 |
Grp | Yes | isgrp 19012, tgpgrp 24246 |
| gsum | group sum | df-gsum 17501 |
(𝐺 Σg 𝐹) | Yes |
gsumval 18741, gsumwrev 19442 |
| hash | size (of a set) | df-hash 14374 |
(♯‘𝐴) | Yes |
hashgval 14376, hashfz1 14389, hashcl 14399 |
| hb | hypothesis builder (prefix) | |
| No | hbxfrbi 1854, hbald 2202, hbequid 39711 |
| hm | (monoid, group, ring, ...) homomorphism |
| | No |
ismhm 18849, isghm 19292, isrhm 20568 |
| i | inference (suffix) | |
| No | eleq1i 2853, tcsni 9708 |
| i | implication (suffix) | |
| No | brwdomi 9528, infeq5i 9603 |
| id | identity | |
| No | biid 264 |
| iedg | indexed edge | df-iedg 29360 |
(iEdg‘𝐺) | Yes |
iedgval0 29401, edgiedgb 29415 |
| idm | idempotent | |
| No | anidm 574, tpidm13 4721 |
| im, imp | implication (label often omitted) |
df-im 15159 | (𝐴 → 𝐵) | Yes |
iman 406, imnan 404, impbidd 213 |
| im | (group, ring, ...) isomorphism | |
| No | isgim 19338, rimrcl 20571 |
| ima | image | df-ima 5673 |
(𝐴 “ 𝐵) | Yes | resima 6013, imaundi 6146 |
| imp | import | |
| No | biimpa 481, impcom 412 |
| in | intersection | df-in 3911 |
(𝐴 ∩ 𝐵) | Yes | elin 3920, incom 4161 |
| inf | infimum | df-inf 9401 |
inf(ℝ+, ℝ*, < ) | Yes |
fiinfcl 9461, infiso 9468 |
| is... | is (something a) ...? | |
| No | isring 20325 |
| j | joining, disjoining | |
| No | jc 162, jaoi 870 |
| l | left | |
| No | olcd 887, simpl 487 |
| map | mapping operation or set exponentiation |
df-map 8824 | (𝐴 ↑m 𝐵) | Yes |
mapvalg 8831, elmapex 8843 |
| mat | matrix | df-mat 22576 |
(𝑁 Mat 𝑅) | Yes |
matval 22579, matring 22611 |
| mdet | determinant (of a square matrix) |
df-mdet 22753 | (𝑁 maDet 𝑅) | Yes |
mdetleib 22755, mdetrlin 22770 |
| mgm | magma | df-mgm 18704 |
Magma | Yes |
mgmidmo 18724, mgmlrid 18731, ismgm 18705 |
| mgp | multiplicative group | df-mgp 20223 |
(mulGrp‘𝑅) | Yes |
mgpress 20232, ringmgp 20327 |
| mnd | monoid | df-mnd 18799 |
Mnd | Yes | mndass 18807, mndodcong 19618 |
| mo | "there exists at most one" | df-mo 2566 |
∃*𝑥𝜑 | Yes | eumo 2605, moim 2571 |
| mp | modus ponens | ax-mp 5 |
| No | mpd 16, mpi 21 |
| mpo | maps-to notation for an operation |
df-mpo 7417 | (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) | Yes |
mpompt 7526, resmpo 7532 |
| mpt | modus ponendo tollens | |
| No | mptnan 1797, mptxor 1798 |
| mpt | maps-to notation for a function |
df-mpt 5192 | (𝑥 ∈ 𝐴 ↦ 𝐵) | Yes |
fconstmpt 5722, resmpt 6038 |
| mul | multiplication (see "t") | df-mul 11118 |
(𝐴 · 𝐵) | Yes |
mulcl 11190, divmul 11881, mulcom 11192, mulass 11194 |
| n, not | not | |
¬ 𝜑 | Yes |
nan 842, notnotr 131 |
| ne | not equal | df-ne | 𝐴 ≠ 𝐵 |
Yes | exmidne 2967, neeqtrd 3026 |
| nel | not element of | df-nel | 𝐴 ∉ 𝐵
|
Yes | neli 3065, nnel 3073 |
| ne0 | not equal to zero (see n0) | |
≠ 0 | No |
negne0d 11573, ine0 11655, gt0ne0 11685 |
| nf | "not free in" (prefix) | df-nf 1813 |
Ⅎ𝑥𝜑 | Yes | nfnd 1887 |
| ngp | normed group | df-ngp 24751 |
NrmGrp | Yes | isngp 24764, ngptps 24770 |
| nm | norm (on a group or ring) | df-nm 24750 |
(norm‘𝑊) | Yes |
nmval 24757, subgnm 24801 |
| nn | positive integers | df-nn 12240 |
ℕ | Yes | nnsscn 12244, nncn 12247 |
| nn0 | nonnegative integers | df-n0 12511 |
ℕ0 | Yes | nnnn0 12517, nn0cn 12520 |
| n0 | not the empty set (see ne0) | |
≠ ∅ | No | n0i 4292, vn0 4297, ssn0 4361 |
| OLD | old, obsolete (to be removed soon) | |
| No | 19.43OLD 1912 |
| on | ordinal number | df-on 6364 |
𝐴 ∈ On | Yes |
elon 6369, 1on 8464 onelon 6385 |
| op | ordered pair | df-op 4595 |
⟨𝐴, 𝐵⟩ | Yes | dfopif 4834, opth 5457 |
| or | or | df-or 861 |
(𝜑 ∨ 𝜓) | Yes |
orcom 883, anor 997 |
| ot | ordered triple | df-ot 4597 |
⟨𝐴, 𝐵, 𝐶⟩ | Yes |
euotd 5495, fnotovb 7464 |
| ov | operation value | df-ov 7415 |
(𝐴𝐹𝐵) | Yes
| fnotovb 7464, fnovrn 7587 |
| p | plus (see "add"), for all-constant
theorems | df-add 11117 |
(3 + 2) = 5 | Yes |
3p2e5 12397 |
| pfx | prefix | df-pfx 14716 |
(𝑊 prefix 𝐿) | Yes |
pfxlen 14728, ccatpfx 14745 |
| pm | Principia Mathematica | |
| No | pm2.27 43 |
| pm | partial mapping (operation) | df-pm 8825 |
(𝐴 ↑pm 𝐵) | Yes | elpmi 8841, pmsspw 8873 |
| pr | pair | df-pr 4591 |
{𝐴, 𝐵} | Yes |
elpr 4613, prcom 4697, prid1g 4725, prnz 4742 |
| prm, prime | prime (number) | df-prm 16736 |
ℙ | Yes | 1nprm 16743, dvdsprime 16751 |
| pss | proper subset | df-pss 3924 |
𝐴 ⊊ 𝐵 | Yes | pssss 4051, sspsstri 4059 |
| q | rational numbers ("quotients") | df-q 12979 |
ℚ | Yes | elq 12980 |
| r | reversed (suffix) | |
| No | pm4.71r 567, caovdir 7646 |
| r | right | |
| No | orcd 886, simprl 782 |
| rab | restricted class abstraction |
df-rab 3416 | {𝑥 ∈ 𝐴 ∣ 𝜑} | Yes |
rabswap 3424, df-oprab 7416 |
| ral | restricted universal quantification |
df-ral 3079 | ∀𝑥 ∈ 𝐴𝜑 | Yes |
ralnex 3090, ralrnmpo 7551 |
| rcl | reverse closure | |
| No | ndmfvrcl 6914, nnarcl 8600 |
| re | real numbers | df-r 11116 |
ℝ | Yes | recn 11196, 0re 11216 |
| rel | relation | df-rel 5667 | Rel 𝐴 |
Yes | brrelex1 5713, relmpoopab 8087 |
| res | restriction | df-res 5672 |
(𝐴 ↾ 𝐵) | Yes |
opelres 5983, f1ores 6835 |
| reu | restricted existential uniqueness |
df-reu 3369 | ∃!𝑥 ∈ 𝐴𝜑 | Yes |
nfreud 3412, reurex 3372 |
| rex | restricted existential quantification |
df-rex 3089 | ∃𝑥 ∈ 𝐴𝜑 | Yes |
rexnal 3116, rexrnmpo 7552 |
| rmo | restricted "at most one" |
df-rmo 3368 | ∃*𝑥 ∈ 𝐴𝜑 | Yes |
nfrmod 3411, nrexrmo 3387 |
| rn | range | df-rn 5671 | ran 𝐴 |
Yes | elrng 5880, rncnvcnv 5923 |
| ring | (unital) ring | df-ring 20323 |
Ring | Yes |
ringidval 20271, isring 20325, ringgrp 20326 |
| rng | non-unital ring | df-rng 20237 |
Rng | Yes |
isrng 20238, rngabl 20239, rnglz 20249 |
| rot | rotation | |
| No | 3anrot 1116, 3orrot 1107 |
| s | eliminates need for syllogism (suffix) |
| | No | ancoms 463 |
| sb | (proper) substitution (of a set) |
df-sb 2096 | [𝑦 / 𝑥]𝜑 | Yes |
spsbe 2115, sbimi 2107 |
| sbc | (proper) substitution of a class |
df-sbc 3744 | [𝐴 / 𝑥]𝜑 | Yes |
sbc2or 3752, sbcth 3758 |
| sca | scalar | df-sca 17332 |
(Scalar‘𝐻) | Yes |
resssca 17402, mgpsca 20228 |
| simp | simple, simplification | |
| No | simpl 487, simp3r3 1301 |
| sn | singleton | df-sn 4589 |
{𝐴} | Yes | eldifsn 4752 |
| sp | specialization | |
| No | spsbe 2115, spei 2425 |
| ss | subset | df-ss 3921 |
𝐴 ⊆ 𝐵 | Yes | difss 4089 |
| struct | structure | df-struct 17213 |
Struct | Yes | brstruct 17214, structfn 17222 |
| sub | subtract | df-sub 11449 |
(𝐴 − 𝐵) | Yes |
subval 11454, subaddi 11551 |
| sup | supremum | df-sup 9400 |
sup(𝐴, 𝐵, < ) | Yes |
fisupcl 9428, supmo 9410 |
| supp | support (of a function) | df-supp 8155 |
(𝐹 supp 𝑍) | Yes |
ressuppfi 9353, mptsuppd 8181 |
| swap | swap (two parts within a theorem) |
| | No | rabswap 3424, 2reuswap 3708 |
| syl | syllogism | syl 18 |
| No | 3syl 19 |
| sym | symmetric | |
| No | df-symdif 4205, cnvsym 6113 |
| symg | symmetric group | df-symg 19446 |
(SymGrp‘𝐴) | Yes |
symghash 19454, pgrpsubgsymg 19485 |
| t |
times (see "mul"), for all-constant theorems |
df-mul 11118 |
(3 · 2) = 6 | Yes |
3t2e6 12412 |
| th, t |
theorem |
|
|
No |
nfth 1830, sbcth 3758, weth 10485, ancomst 469 |
| tp | triple | df-tp 4593 |
{𝐴, 𝐵, 𝐶} | Yes |
eltpi 4653, tpeq1 4707 |
| tr | transitive | |
| No | bitrd 282, biantr 817 |
| tru, t |
true, truth |
df-tru 1572 |
⊤ |
Yes |
bitru 1578, truanfal 1603, biimt 363 |
| un | union | df-un 3909 |
(𝐴 ∪ 𝐵) | Yes |
uneqri 4109, uncom 4111 |
| unit | unit (in a ring) |
df-unit 20447 | (Unit‘𝑅) | Yes |
isunit 20462, nzrunit 20633 |
| v |
setvar (especially for specializations of
theorems when a class is replaced by a setvar variable) |
|
x |
Yes |
cv 1568, vex 3458, velpw 4566, vtoclf 3529 |
| v |
disjoint variable condition used in place of nonfreeness
hypothesis (suffix) |
|
|
No |
spimv 2421 |
| vtx |
vertex |
df-vtx 29359 |
(Vtx‘𝐺) |
Yes |
vtxval0 29400, opvtxov 29366 |
| vv |
two disjoint variable conditions used in place of nonfreeness
hypotheses (suffix) |
|
|
No |
19.23vv 1972 |
| w | weak (version of a theorem) (suffix) | |
| No | ax11w 2164, spnfw 2008 |
| wrd | word |
df-word 14558 | Word 𝑆 | Yes |
iswrdb 14564, wrdfn 14572, ffz0iswrd 14585 |
| xp | cross product (Cartesian product) |
df-xp 5666 | (𝐴 × 𝐵) | Yes |
elxp 5683, opelxpi 5697, xpundi 5729 |
| xr | eXtended reals | df-xr 11253 |
ℝ* | Yes | ressxr 11259, rexr 11261, 0xr 11262 |
| z | integers (from German "Zahlen") |
df-z 12598 | ℤ | Yes |
elz 12599, zcn 12602 |
| zn | ring of integers mod 𝑁 | df-zn 21667 |
(ℤ/nℤ‘𝑁) | Yes |
znval 21696, zncrng 21705, znhash 21719 |
| zring | ring of integers | df-zring 21608 |
ℤring | Yes | zringbas 21614, zringcrng 21609
|
| 0, z |
slashed zero (empty set) | df-nul 4286 |
∅ | Yes |
n0i 4292, vn0 4297; snnz 4741, prnz 4742 |
(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.) |
