| Description:
The following gives conventions used in the Metamath Proof Explorer
(MPE, set.mm) regarding labels.
For other conventions, see conventions 30660 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 3081"rgen.1 $e |- ( x e. A -> ph ) $."
or letters corresponding to the (main) class variable used in the
hypothesis, e.g., for mdet0 22724: "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 2692 and stirling 46661.
- 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 1862, and the restricted quantifier version of Theorem 21 from
Section 19 of [Margaris] p. 90 is labeled r19.21 3260.
- 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... 15925. 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 3910, and thus its syntax label fragment is "dif". Similarly, the
subclass relation 𝐴 ⊆ 𝐵 has syntax label fragment "ss"
because it is defined in df-ss 3924. 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 4092. There are many other syntax label fragments, e.g.,
singleton construct {𝐴} has syntax label fragment "sn" (because it
is defined in df-sn 4586), and the pair construct {𝐴, 𝐵} has
fragment "pr" ( from df-pr 4588). 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 4749. 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 11094) and "re" represents real numbers ℝ (Definition df-r 11098).
The empty set ∅ often uses fragment 0, even though it is defined
in df-nul 4289. The syntax construct (𝐴 + 𝐵) usually uses the
fragment "add" (which is consistent with df-add 11099), 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 12366.
- 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 16196 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 16114) we have value cosval 16169 and
closure coscl 16173.
- 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 30663 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 1962 versus 19.21 2245. This
often permits to prove the result using fewer axioms, and/or to
eliminate a nonfreeness hypothesis (such as Ⅎ𝑥𝜑 in 19.21 2245).
If no constraint is put on axiom use, then the v-version can be proved
from the original theorem using nfv 1937. If two (resp. three) such
disjoint variable conditions are added, then the suffix "vv" (resp.
"vvv") is used, e.g., exlimivv 1955.
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 2606 derived from eu6 2604. 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 5421.
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 2443 (cbval 2432 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 3529.
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 3158 |
| abl | Abelian group | df-abl 19844 |
Abel | Yes | ablgrp 19846, zringabl 21561 |
| abs | absorption | | | No |
ressabs 17298 |
| abs | absolute value (of a complex number) |
df-abs 15277 | (abs‘𝐴) | Yes |
absval 15279, absneg 15318, abs1 15338 |
| ad | adding | |
| No | adantr 485, ad2antlr 739 |
| add | add (see "p") | df-add 11099 |
(𝐴 + 𝐵) | Yes |
addcl 11170, addcom 11384, addass 11175 |
| al | "for all" | |
∀𝑥𝜑 | No | alim 1833, alex 1849 |
| ALT | alternative/less preferred (suffix) | |
| No | idALT 24 |
| an | and | df-an 401 |
(𝜑 ∧ 𝜓) | Yes |
anor 998, iman 406, imnan 404 |
| ant | antecedent | |
| No | adantr 485 |
| ass | associative | |
| No | biass 388, orass 934, mulass 11176 |
| asym | asymmetric, antisymmetric | |
| No | intasym 6106, asymref 6107, posasymb 18365 |
| ax | axiom | |
| No | ax6dgen 2165, ax1cn 11122 |
| bas, base |
base (set of an extensible structure) | df-base 17260 |
(Base‘𝑆) | Yes |
baseval 17261, ressbas 17286, cnfldbas 21486 |
| b, bi | biconditional ("iff", "if and only if")
| df-bi 210 | (𝜑 ↔ 𝜓) | Yes |
impbid 215, sspwb 5421 |
| br | binary relation | df-br 5106 |
𝐴𝑅𝐵 | Yes | brab1 5153, brun 5156 |
| c | commutes, commuted (suffix) | | |
No | biimpac 483 |
| c | contraction (suffix) | | |
No | sylc 66, syl2anc 595 |
| cbv | change bound variable | | |
No | cbvalivw 2030, cbvrex 3353 |
| cdm | codomain | |
| No | ffvelcdm 7066, focdmex 7941 |
| cl | closure | | | No |
ifclda 4519, ovrcl 7441, zaddcl 12625 |
| cn | complex numbers | df-c 11094 |
ℂ | Yes | nnsscn 12229, nncn 12232 |
| cnfld | field of complex numbers | df-cnfld 21483 |
ℂfld | Yes | cnfldbas 21486, cnfldinv 21513 |
| cntz | centralizer | df-cntz 19378 |
(Cntz‘𝑀) | Yes |
cntzfval 19381, dprdfcntz 20078 |
| cnv | converse | df-cnv 5660 |
◡𝐴 | Yes | opelcnvg 5857, f1ocnv 6823 |
| co | composition | df-co 5661 |
(𝐴 ∘ 𝐵) | Yes | cnvco 5866, fmptco 7115 |
| com | commutative | |
| No | orcom 883, bicomi 227, eqcomi 2774 |
| con | contradiction, contraposition | |
| No | condan 829, con2d 135 |
| csb | class substitution | df-csb 3856 |
⦋𝐴 / 𝑥⦌𝐵 | Yes |
csbid 3868, csbie2g 3895 |
| cyg | cyclic group | df-cyg 19939 |
CycGrp | Yes |
iscyg 19940, zringcyg 21579 |
| d | deduction form (suffix) | |
| No | idd 25, impbid 215 |
| df | (alternate) definition (prefix) | |
| No | dfrel2 6179, dffn2 6697 |
| di, distr | distributive | |
| No |
andi 1023, imdi 393, ordi 1021, difindi 4247, ndmovdistr 7589 |
| dif | class difference | df-dif 3910 |
(𝐴 ∖ 𝐵) | Yes |
difss 4092, difindi 4247 |
| div | division | df-div 11860 |
(𝐴 / 𝐵) | Yes |
divcl 11866, divval 11862, divmul 11863 |
| dm | domain | df-dm 5662 |
dom 𝐴 | Yes | dmmpt 6231, iswrddm0 14565 |
| e, eq, equ | equals (equ for setvars, eq for
classes) | df-cleq 2757 |
𝐴 = 𝐵 | Yes |
2p2e4 12366, uneqri 4112, equtr 2044 |
| edg | edge | df-edg 29307 |
(Edg‘𝐺) | Yes |
edgopval 29310, usgredgppr 29455 |
| el | element of | |
𝐴 ∈ 𝐵 | Yes |
eldif 3917, eldifsn 4749, elssuni 4900 |
| en | equinumerous | df-en |
𝐴 ≈ 𝐵 | Yes | domen 8946, enfi 9159 |
| eu | "there exists exactly one" | eu6 2604 |
∃!𝑥𝜑 | Yes | euex 2607, euabsn 4688 |
| ex | exists (i.e. is a set) | |
∈ V | No | brrelex1 5705, 0ex 5262 |
| ex, e | "there exists (at least one)" |
df-ex 1803 |
∃𝑥𝜑 | Yes | exim 1857, alex 1849 |
| exp | export | |
| No | expt 178, expcom 418 |
| f | "not free in" (suffix) | |
| No | equs45f 2493, sbf 2308 |
| f | function | df-f 6529 |
𝐹:𝐴⟶𝐵 | Yes | fssxp 6723, opelf 6729 |
| fal | false | df-fal 1576 |
⊥ | Yes | bifal 1579, falantru 1598 |
| fi | finite intersection | df-fi 9359 |
(fi‘𝐵) | Yes | fival 9360, inelfi 9366 |
| fi, fin | finite | df-fin 8935 |
Fin | Yes |
isfi 8960, snfi 9028, onfin 9187 |
| fld | field (Note: there is an alternative
definition Fld of a field, see df-fld 38503) | df-field 20807 |
Field | Yes | isfld 20815, fldidom 20844 |
| fn | function with domain | df-fn 6528 |
𝐴 Fn 𝐵 | Yes | ffn 6695, fndm 6628 |
| frgp | free group | df-frgp 19771 |
(freeGrp‘𝐼) | Yes |
frgpval 19819, frgpadd 19824 |
| fsupp | finitely supported function |
df-fsupp 9310 | 𝑅 finSupp 𝑍 | Yes |
isfsupp 9313, fdmfisuppfi 9322, fsuppco 9350 |
| fun | function | df-fun 6527 |
Fun 𝐹 | Yes | funrel 6542, ffun 6698 |
| fv | function value | df-fv 6533 |
(𝐹‘𝐴) | Yes | fvres 6890, swrdfv 14676 |
| fz | finite set of sequential integers |
df-fz 13527 |
(𝑀...𝑁) | Yes | fzval 13528, eluzfz 13538 |
| fz0 | finite set of sequential nonnegative integers |
|
(0...𝑁) | Yes | nn0fz0 13644, fz0tp 13647 |
| fzo | half-open integer range | df-fzo 13674 |
(𝑀..^𝑁) | Yes |
elfzo 13680, elfzofz 13695 |
| g | more general (suffix); eliminates "is a set"
hypotheses | |
| No | uniexg 7727 |
| gr | graph | |
| No | uhgrf 29321, isumgr 29354, usgrres1 29574 |
| grp | group | df-grp 18993 |
Grp | Yes | isgrp 18996, tgpgrp 24196 |
| gsum | group sum | df-gsum 17485 |
(𝐺 Σg 𝐹) | Yes |
gsumval 18725, gsumwrev 19427 |
| hash | size (of a set) | df-hash 14358 |
(♯‘𝐴) | Yes |
hashgval 14360, hashfz1 14373, hashcl 14383 |
| hb | hypothesis builder (prefix) | |
| No | hbxfrbi 1848, hbald 2205, hbequid 39545 |
| hm | (monoid, group, ring, ...) homomorphism |
| | No |
ismhm 18833, isghm 19277, isrhm 20551 |
| i | inference (suffix) | |
| No | eleq1i 2856, tcsni 9698 |
| i | implication (suffix) | |
| No | brwdomi 9518, infeq5i 9593 |
| id | identity | |
| No | biid 264 |
| iedg | indexed edge | df-iedg 29258 |
(iEdg‘𝐺) | Yes |
iedgval0 29299, edgiedgb 29313 |
| idm | idempotent | |
| No | anidm 574, tpidm13 4718 |
| im, imp | implication (label often omitted) |
df-im 15142 | (𝐴 → 𝐵) | Yes |
iman 406, imnan 404, impbidd 213 |
| im | (group, ring, ...) isomorphism | |
| No | isgim 19323, rimrcl 20554 |
| ima | image | df-ima 5665 |
(𝐴 “ 𝐵) | Yes | resima 6005, imaundi 6138 |
| imp | import | |
| No | biimpa 481, impcom 412 |
| in | intersection | df-in 3914 |
(𝐴 ∩ 𝐵) | Yes | elin 3923, incom 4164 |
| inf | infimum | df-inf 9391 |
inf(ℝ+, ℝ*, < ) | Yes |
fiinfcl 9451, infiso 9458 |
| is... | is (something a) ...? | |
| No | isring 20310 |
| j | joining, disjoining | |
| No | jc 162, jaoi 870 |
| l | left | |
| No | olcd 887, simpl 487 |
| map | mapping operation or set exponentiation |
df-map 8814 | (𝐴 ↑m 𝐵) | Yes |
mapvalg 8821, elmapex 8833 |
| mat | matrix | df-mat 22526 |
(𝑁 Mat 𝑅) | Yes |
matval 22529, matring 22561 |
| mdet | determinant (of a square matrix) |
df-mdet 22703 | (𝑁 maDet 𝑅) | Yes |
mdetleib 22705, mdetrlin 22720 |
| mgm | magma | df-mgm 18688 |
Magma | Yes |
mgmidmo 18708, mgmlrid 18715, ismgm 18689 |
| mgp | multiplicative group | df-mgp 20208 |
(mulGrp‘𝑅) | Yes |
mgpress 20217, ringmgp 20312 |
| mnd | monoid | df-mnd 18783 |
Mnd | Yes | mndass 18791, mndodcong 19603 |
| mo | "there exists at most one" | df-mo 2569 |
∃*𝑥𝜑 | Yes | eumo 2608, moim 2574 |
| mp | modus ponens | ax-mp 5 |
| No | mpd 16, mpi 21 |
| mpo | maps-to notation for an operation |
df-mpo 7405 | (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) | Yes |
mpompt 7514, resmpo 7520 |
| mpt | modus ponendo tollens | |
| No | mptnan 1791, mptxor 1792 |
| mpt | maps-to notation for a function |
df-mpt 5187 | (𝑥 ∈ 𝐴 ↦ 𝐵) | Yes |
fconstmpt 5714, resmpt 6030 |
| mul | multiplication (see "t") | df-mul 11100 |
(𝐴 · 𝐵) | Yes |
mulcl 11172, divmul 11863, mulcom 11174, mulass 11176 |
| n, not | not | |
¬ 𝜑 | Yes |
nan 842, notnotr 131 |
| ne | not equal | df-ne | 𝐴 ≠ 𝐵 |
Yes | exmidne 2970, neeqtrd 3029 |
| nel | not element of | df-nel | 𝐴 ∉ 𝐵
|
Yes | neli 3066, nnel 3074 |
| ne0 | not equal to zero (see n0) | |
≠ 0 | No |
negne0d 11555, ine0 11637, gt0ne0 11667 |
| nf | "not free in" (prefix) | df-nf 1807 |
Ⅎ𝑥𝜑 | Yes | nfnd 1881 |
| ngp | normed group | df-ngp 24701 |
NrmGrp | Yes | isngp 24714, ngptps 24720 |
| nm | norm (on a group or ring) | df-nm 24700 |
(norm‘𝑊) | Yes |
nmval 24707, subgnm 24751 |
| nn | positive integers | df-nn 12225 |
ℕ | Yes | nnsscn 12229, nncn 12232 |
| nn0 | nonnegative integers | df-n0 12496 |
ℕ0 | Yes | nnnn0 12502, nn0cn 12505 |
| n0 | not the empty set (see ne0) | |
≠ ∅ | No | n0i 4295, vn0 4300, ssn0 4361 |
| OLD | old, obsolete (to be removed soon) | |
| No | 19.43OLD 1906 |
| on | ordinal number | df-on 6354 |
𝐴 ∈ On | Yes |
elon 6359, 1on 8454 onelon 6375 |
| op | ordered pair | df-op 4592 |
⟨𝐴, 𝐵⟩ | Yes | dfopif 4831, opth 5449 |
| or | or | df-or 861 |
(𝜑 ∨ 𝜓) | Yes |
orcom 883, anor 998 |
| ot | ordered triple | df-ot 4594 |
⟨𝐴, 𝐵, 𝐶⟩ | Yes |
euotd 5487, fnotovb 7452 |
| ov | operation value | df-ov 7403 |
(𝐴𝐹𝐵) | Yes
| fnotovb 7452, fnovrn 7575 |
| p | plus (see "add"), for all-constant
theorems | df-add 11099 |
(3 + 2) = 5 | Yes |
3p2e5 12382 |
| pfx | prefix | df-pfx 14699 |
(𝑊 prefix 𝐿) | Yes |
pfxlen 14711, ccatpfx 14728 |
| pm | Principia Mathematica | |
| No | pm2.27 43 |
| pm | partial mapping (operation) | df-pm 8815 |
(𝐴 ↑pm 𝐵) | Yes | elpmi 8831, pmsspw 8863 |
| pr | pair | df-pr 4588 |
{𝐴, 𝐵} | Yes |
elpr 4610, prcom 4694, prid1g 4722, prnz 4739 |
| prm, prime | prime (number) | df-prm 16720 |
ℙ | Yes | 1nprm 16727, dvdsprime 16735 |
| pss | proper subset | df-pss 3927 |
𝐴 ⊊ 𝐵 | Yes | pssss 4054, sspsstri 4062 |
| q | rational numbers ("quotients") | df-q 12964 |
ℚ | Yes | elq 12965 |
| r | reversed (suffix) | |
| No | pm4.71r 567, caovdir 7634 |
| r | right | |
| No | orcd 886, simprl 782 |
| rab | restricted class abstraction |
df-rab 3418 | {𝑥 ∈ 𝐴 ∣ 𝜑} | Yes |
rabswap 3426, df-oprab 7404 |
| ral | restricted universal quantification |
df-ral 3080 | ∀𝑥 ∈ 𝐴𝜑 | Yes |
ralnex 3091, ralrnmpo 7539 |
| rcl | reverse closure | |
| No | ndmfvrcl 6904, nnarcl 8590 |
| re | real numbers | df-r 11098 |
ℝ | Yes | recn 11178, 0re 11198 |
| rel | relation | df-rel 5659 | Rel 𝐴 |
Yes | brrelex1 5705, relmpoopab 8077 |
| res | restriction | df-res 5664 |
(𝐴 ↾ 𝐵) | Yes |
opelres 5975, f1ores 6825 |
| reu | restricted existential uniqueness |
df-reu 3371 | ∃!𝑥 ∈ 𝐴𝜑 | Yes |
nfreud 3414, reurex 3374 |
| rex | restricted existential quantification |
df-rex 3090 | ∃𝑥 ∈ 𝐴𝜑 | Yes |
rexnal 3117, rexrnmpo 7540 |
| rmo | restricted "at most one" |
df-rmo 3370 | ∃*𝑥 ∈ 𝐴𝜑 | Yes |
nfrmod 3413, nrexrmo 3389 |
| rn | range | df-rn 5663 | ran 𝐴 |
Yes | elrng 5872, rncnvcnv 5915 |
| ring | (unital) ring | df-ring 20308 |
Ring | Yes |
ringidval 20256, isring 20310, ringgrp 20311 |
| rng | non-unital ring | df-rng 20222 |
Rng | Yes |
isrng 20223, rngabl 20224, rnglz 20234 |
| rot | rotation | |
| No | 3anrot 1115, 3orrot 1106 |
| s | eliminates need for syllogism (suffix) |
| | No | ancoms 463 |
| sb | (proper) substitution (of a set) |
df-sb 2094 | [𝑦 / 𝑥]𝜑 | Yes |
spsbe 2118, sbimi 2110 |
| sbc | (proper) substitution of a class |
df-sbc 3748 | [𝐴 / 𝑥]𝜑 | Yes |
sbc2or 3756, sbcth 3762 |
| sca | scalar | df-sca 17316 |
(Scalar‘𝐻) | Yes |
resssca 17386, mgpsca 20213 |
| simp | simple, simplification | |
| No | simpl 487, simp3r3 1300 |
| sn | singleton | df-sn 4586 |
{𝐴} | Yes | eldifsn 4749 |
| sp | specialization | |
| No | spsbe 2118, spei 2428 |
| ss | subset | df-ss 3924 |
𝐴 ⊆ 𝐵 | Yes | difss 4092 |
| struct | structure | df-struct 17197 |
Struct | Yes | brstruct 17198, structfn 17206 |
| sub | subtract | df-sub 11431 |
(𝐴 − 𝐵) | Yes |
subval 11436, subaddi 11533 |
| sup | supremum | df-sup 9390 |
sup(𝐴, 𝐵, < ) | Yes |
fisupcl 9418, supmo 9400 |
| supp | support (of a function) | df-supp 8145 |
(𝐹 supp 𝑍) | Yes |
ressuppfi 9343, mptsuppd 8171 |
| swap | swap (two parts within a theorem) |
| | No | rabswap 3426, 2reuswap 3712 |
| syl | syllogism | syl 18 |
| No | 3syl 19 |
| sym | symmetric | |
| No | df-symdif 4208, cnvsym 6105 |
| symg | symmetric group | df-symg 19431 |
(SymGrp‘𝐴) | Yes |
symghash 19439, pgrpsubgsymg 19470 |
| t |
times (see "mul"), for all-constant theorems |
df-mul 11100 |
(3 · 2) = 6 | Yes |
3t2e6 12397 |
| th, t |
theorem |
|
|
No |
nfth 1824, sbcth 3762, weth 10467, ancomst 469 |
| tp | triple | df-tp 4590 |
{𝐴, 𝐵, 𝐶} | Yes |
eltpi 4650, tpeq1 4704 |
| tr | transitive | |
| No | bitrd 282, biantr 817 |
| tru, t |
true, truth |
df-tru 1566 |
⊤ |
Yes |
bitru 1572, truanfal 1597, biimt 363 |
| un | union | df-un 3912 |
(𝐴 ∪ 𝐵) | Yes |
uneqri 4112, uncom 4114 |
| unit | unit (in a ring) |
df-unit 20431 | (Unit‘𝑅) | Yes |
isunit 20446, nzrunit 20599 |
| v |
setvar (especially for specializations of
theorems when a class is replaced by a setvar variable) |
|
x |
Yes |
cv 1562, vex 3461, velpw 4563, vtoclf 3533 |
| v |
disjoint variable condition used in place of nonfreeness
hypothesis (suffix) |
|
|
No |
spimv 2424 |
| vtx |
vertex |
df-vtx 29257 |
(Vtx‘𝐺) |
Yes |
vtxval0 29298, opvtxov 29264 |
| vv |
two disjoint variable conditions used in place of nonfreeness
hypotheses (suffix) |
|
|
No |
19.23vv 1966 |
| w | weak (version of a theorem) (suffix) | |
| No | ax11w 2167, spnfw 2002 |
| wrd | word |
df-word 14541 | Word 𝑆 | Yes |
iswrdb 14547, wrdfn 14555, ffz0iswrd 14568 |
| xp | cross product (Cartesian product) |
df-xp 5658 | (𝐴 × 𝐵) | Yes |
elxp 5675, opelxpi 5689, xpundi 5721 |
| xr | eXtended reals | df-xr 11235 |
ℝ* | Yes | ressxr 11241, rexr 11243, 0xr 11244 |
| z | integers (from German "Zahlen") |
df-z 12583 | ℤ | Yes |
elz 12584, zcn 12587 |
| zn | ring of integers mod 𝑁 | df-zn 21616 |
(ℤ/nℤ‘𝑁) | Yes |
znval 21645, zncrng 21654, znhash 21668 |
| zring | ring of integers | df-zring 21557 |
ℤring | Yes | zringbas 21563, zringcrng 21558
|
| 0, z |
slashed zero (empty set) | df-nul 4289 |
∅ | Yes |
n0i 4295, vn0 4300; snnz 4738, prnz 4739 |
(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.) |
