| Description:
The following gives conventions used in the Metamath Proof Explorer
(MPE, set.mm) regarding labels.
For other conventions, see conventions 30487 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 3054"rgen.1 $e |- ( x e. A -> ph ) $."
or letters corresponding to the (main) class variable used in the
hypothesis, e.g., for mdet0 22562: "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 2664 and stirling 46441.
- 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 1841, and the restricted quantifier version of Theorem 21 from
Section 19 of [Margaris] p. 90 is labeled r19.21 3233.
- 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... 15816. 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 3906, and thus its syntax label fragment is "dif". Similarly, the
subclass relation 𝐴 ⊆ 𝐵 has syntax label fragment "ss"
because it is defined in df-ss 3920. 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 4090. There are many other syntax label fragments, e.g.,
singleton construct {𝐴} has syntax label fragment "sn" (because it
is defined in df-sn 4583), and the pair construct {𝐴, 𝐵} has
fragment "pr" ( from df-pr 4585). 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 4744. An "n" is often used for negation (¬), e.g.,
nan 830.
- 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 11044) and "re" represents real numbers ℝ (Definition df-r 11048).
The empty set ∅ often uses fragment 0, even though it is defined
in df-nul 4288. The syntax construct (𝐴 + 𝐵) usually uses the
fragment "add" (which is consistent with df-add 11049), 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 12287.
- 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 16087 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 16005) we have value cosval 16060 and
closure coscl 16064.
- 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 30490 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 1941 versus 19.21 2215. This
often permits to prove the result using fewer axioms, and/or to
eliminate a nonfreeness hypothesis (such as Ⅎ𝑥𝜑 in 19.21 2215).
If no constraint is put on axiom use, then the v-version can be proved
from the original theorem using nfv 1916. If two (resp. three) such
disjoint variable conditions are added, then the suffix "vv" (resp.
"vvv") is used, e.g., exlimivv 1934.
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 2577 derived from eu6 2575. 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 5404.
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 2414 (cbval 2403 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 3519.
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 585), 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 3131 |
| abl | Abelian group | df-abl 19724 |
Abel | Yes | ablgrp 19726, zringabl 21418 |
| abs | absorption | | | No |
ressabs 17187 |
| abs | absolute value (of a complex number) |
df-abs 15171 | (abs‘𝐴) | Yes |
absval 15173, absneg 15212, abs1 15232 |
| ad | adding | |
| No | adantr 480, ad2antlr 728 |
| add | add (see "p") | df-add 11049 |
(𝐴 + 𝐵) | Yes |
addcl 11120, addcom 11331, addass 11125 |
| al | "for all" | |
∀𝑥𝜑 | No | alim 1812, alex 1828 |
| ALT | alternative/less preferred (suffix) | |
| No | idALT 23 |
| an | and | df-an 396 |
(𝜑 ∧ 𝜓) | Yes |
anor 985, iman 401, imnan 399 |
| ant | antecedent | |
| No | adantr 480 |
| ass | associative | |
| No | biass 384, orass 922, mulass 11126 |
| asym | asymmetric, antisymmetric | |
| No | intasym 6080, asymref 6081, posasymb 18254 |
| ax | axiom | |
| No | ax6dgen 2134, ax1cn 11072 |
| bas, base |
base (set of an extensible structure) | df-base 17149 |
(Base‘𝑆) | Yes |
baseval 17150, ressbas 17175, cnfldbas 21325 |
| b, bi | biconditional ("iff", "if and only if")
| df-bi 207 | (𝜑 ↔ 𝜓) | Yes |
impbid 212, sspwb 5404 |
| br | binary relation | df-br 5101 |
𝐴𝑅𝐵 | Yes | brab1 5148, brun 5151 |
| c | commutes, commuted (suffix) | | |
No | biimpac 478 |
| c | contraction (suffix) | | |
No | sylc 65, syl2anc 585 |
| cbv | change bound variable | | |
No | cbvalivw 2009, cbvrex 3335 |
| cdm | codomain | |
| No | ffvelcdm 7035, focdmex 7910 |
| cl | closure | | | No |
ifclda 4517, ovrcl 7409, zaddcl 12543 |
| cn | complex numbers | df-c 11044 |
ℂ | Yes | nnsscn 12162, nncn 12165 |
| cnfld | field of complex numbers | df-cnfld 21322 |
ℂfld | Yes | cnfldbas 21325, cnfldinv 21369 |
| cntz | centralizer | df-cntz 19258 |
(Cntz‘𝑀) | Yes |
cntzfval 19261, dprdfcntz 19958 |
| cnv | converse | df-cnv 5640 |
◡𝐴 | Yes | opelcnvg 5837, f1ocnv 6794 |
| co | composition | df-co 5641 |
(𝐴 ∘ 𝐵) | Yes | cnvco 5842, fmptco 7084 |
| com | commutative | |
| No | orcom 871, bicomi 224, eqcomi 2746 |
| con | contradiction, contraposition | |
| No | condan 818, con2d 134 |
| csb | class substitution | df-csb 3852 |
⦋𝐴 / 𝑥⦌𝐵 | Yes |
csbid 3864, csbie2g 3891 |
| cyg | cyclic group | df-cyg 19819 |
CycGrp | Yes |
iscyg 19820, zringcyg 21436 |
| d | deduction form (suffix) | |
| No | idd 24, impbid 212 |
| df | (alternate) definition (prefix) | |
| No | dfrel2 6155, dffn2 6672 |
| di, distr | distributive | |
| No |
andi 1010, imdi 389, ordi 1008, difindi 4246, ndmovdistr 7557 |
| dif | class difference | df-dif 3906 |
(𝐴 ∖ 𝐵) | Yes |
difss 4090, difindi 4246 |
| div | division | df-div 11807 |
(𝐴 / 𝐵) | Yes |
divcl 11814, divval 11810, divmul 11811 |
| dm | domain | df-dm 5642 |
dom 𝐴 | Yes | dmmpt 6206, iswrddm0 14473 |
| e, eq, equ | equals (equ for setvars, eq for
classes) | df-cleq 2729 |
𝐴 = 𝐵 | Yes |
2p2e4 12287, uneqri 4110, equtr 2023 |
| edg | edge | df-edg 29133 |
(Edg‘𝐺) | Yes |
edgopval 29136, usgredgppr 29281 |
| el | element of | |
𝐴 ∈ 𝐵 | Yes |
eldif 3913, eldifsn 4744, elssuni 4896 |
| en | equinumerous | df-en |
𝐴 ≈ 𝐵 | Yes | domen 8910, enfi 9123 |
| eu | "there exists exactly one" | eu6 2575 |
∃!𝑥𝜑 | Yes | euex 2578, euabsn 4685 |
| ex | exists (i.e. is a set) | |
∈ V | No | brrelex1 5685, 0ex 5254 |
| ex, e | "there exists (at least one)" |
df-ex 1782 |
∃𝑥𝜑 | Yes | exim 1836, alex 1828 |
| exp | export | |
| No | expt 177, expcom 413 |
| f | "not free in" (suffix) | |
| No | equs45f 2464, sbf 2278 |
| f | function | df-f 6504 |
𝐹:𝐴⟶𝐵 | Yes | fssxp 6697, opelf 6703 |
| fal | false | df-fal 1555 |
⊥ | Yes | bifal 1558, falantru 1577 |
| fi | finite intersection | df-fi 9326 |
(fi‘𝐵) | Yes | fival 9327, inelfi 9333 |
| fi, fin | finite | df-fin 8899 |
Fin | Yes |
isfi 8924, snfi 8992, onfin 9151 |
| fld | field (Note: there is an alternative
definition Fld of a field, see df-fld 38237) | df-field 20677 |
Field | Yes | isfld 20685, fldidom 20716 |
| fn | function with domain | df-fn 6503 |
𝐴 Fn 𝐵 | Yes | ffn 6670, fndm 6603 |
| frgp | free group | df-frgp 19651 |
(freeGrp‘𝐼) | Yes |
frgpval 19699, frgpadd 19704 |
| fsupp | finitely supported function |
df-fsupp 9277 | 𝑅 finSupp 𝑍 | Yes |
isfsupp 9280, fdmfisuppfi 9289, fsuppco 9317 |
| fun | function | df-fun 6502 |
Fun 𝐹 | Yes | funrel 6517, ffun 6673 |
| fv | function value | df-fv 6508 |
(𝐹‘𝐴) | Yes | fvres 6861, swrdfv 14584 |
| fz | finite set of sequential integers |
df-fz 13436 |
(𝑀...𝑁) | Yes | fzval 13437, eluzfz 13447 |
| fz0 | finite set of sequential nonnegative integers |
|
(0...𝑁) | Yes | nn0fz0 13553, fz0tp 13556 |
| fzo | half-open integer range | df-fzo 13583 |
(𝑀..^𝑁) | Yes |
elfzo 13589, elfzofz 13603 |
| g | more general (suffix); eliminates "is a set"
hypotheses | |
| No | uniexg 7695 |
| gr | graph | |
| No | uhgrf 29147, isumgr 29180, usgrres1 29400 |
| grp | group | df-grp 18878 |
Grp | Yes | isgrp 18881, tgpgrp 24034 |
| gsum | group sum | df-gsum 17374 |
(𝐺 Σg 𝐹) | Yes |
gsumval 18614, gsumwrev 19307 |
| hash | size (of a set) | df-hash 14266 |
(♯‘𝐴) | Yes |
hashgval 14268, hashfz1 14281, hashcl 14291 |
| hb | hypothesis builder (prefix) | |
| No | hbxfrbi 1827, hbald 2174, hbequid 39279 |
| hm | (monoid, group, ring, ...) homomorphism |
| | No |
ismhm 18722, isghm 19156, isrhm 20426 |
| i | inference (suffix) | |
| No | eleq1i 2828, tcsni 9662 |
| i | implication (suffix) | |
| No | brwdomi 9485, infeq5i 9557 |
| id | identity | |
| No | biid 261 |
| iedg | indexed edge | df-iedg 29084 |
(iEdg‘𝐺) | Yes |
iedgval0 29125, edgiedgb 29139 |
| idm | idempotent | |
| No | anidm 564, tpidm13 4715 |
| im, imp | implication (label often omitted) |
df-im 15036 | (𝐴 → 𝐵) | Yes |
iman 401, imnan 399, impbidd 210 |
| im | (group, ring, ...) isomorphism | |
| No | isgim 19203, rimrcl 20429 |
| ima | image | df-ima 5645 |
(𝐴 “ 𝐵) | Yes | resima 5982, imaundi 6115 |
| imp | import | |
| No | biimpa 476, impcom 407 |
| in | intersection | df-in 3910 |
(𝐴 ∩ 𝐵) | Yes | elin 3919, incom 4163 |
| inf | infimum | df-inf 9358 |
inf(ℝ+, ℝ*, < ) | Yes |
fiinfcl 9418, infiso 9425 |
| is... | is (something a) ...? | |
| No | isring 20184 |
| j | joining, disjoining | |
| No | jc 161, jaoi 858 |
| l | left | |
| No | olcd 875, simpl 482 |
| map | mapping operation or set exponentiation |
df-map 8777 | (𝐴 ↑m 𝐵) | Yes |
mapvalg 8785, elmapex 8797 |
| mat | matrix | df-mat 22364 |
(𝑁 Mat 𝑅) | Yes |
matval 22367, matring 22399 |
| mdet | determinant (of a square matrix) |
df-mdet 22541 | (𝑁 maDet 𝑅) | Yes |
mdetleib 22543, mdetrlin 22558 |
| mgm | magma | df-mgm 18577 |
Magma | Yes |
mgmidmo 18597, mgmlrid 18604, ismgm 18578 |
| mgp | multiplicative group | df-mgp 20088 |
(mulGrp‘𝑅) | Yes |
mgpress 20097, ringmgp 20186 |
| mnd | monoid | df-mnd 18672 |
Mnd | Yes | mndass 18680, mndodcong 19483 |
| mo | "there exists at most one" | df-mo 2540 |
∃*𝑥𝜑 | Yes | eumo 2579, moim 2545 |
| mp | modus ponens | ax-mp 5 |
| No | mpd 15, mpi 20 |
| mpo | maps-to notation for an operation |
df-mpo 7373 | (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) | Yes |
mpompt 7482, resmpo 7488 |
| mpt | modus ponendo tollens | |
| No | mptnan 1770, mptxor 1771 |
| mpt | maps-to notation for a function |
df-mpt 5182 | (𝑥 ∈ 𝐴 ↦ 𝐵) | Yes |
fconstmpt 5694, resmpt 6004 |
| mul | multiplication (see "t") | df-mul 11050 |
(𝐴 · 𝐵) | Yes |
mulcl 11122, divmul 11811, mulcom 11124, mulass 11126 |
| n, not | not | |
¬ 𝜑 | Yes |
nan 830, notnotr 130 |
| ne | not equal | df-ne | 𝐴 ≠ 𝐵 |
Yes | exmidne 2943, neeqtrd 3002 |
| nel | not element of | df-nel | 𝐴 ∉ 𝐵
|
Yes | neli 3039, nnel 3047 |
| ne0 | not equal to zero (see n0) | |
≠ 0 | No |
negne0d 11502, ine0 11584, gt0ne0 11614 |
| nf | "not free in" (prefix) | df-nf 1786 |
Ⅎ𝑥𝜑 | Yes | nfnd 1860 |
| ngp | normed group | df-ngp 24539 |
NrmGrp | Yes | isngp 24552, ngptps 24558 |
| nm | norm (on a group or ring) | df-nm 24538 |
(norm‘𝑊) | Yes |
nmval 24545, subgnm 24589 |
| nn | positive integers | df-nn 12158 |
ℕ | Yes | nnsscn 12162, nncn 12165 |
| nn0 | nonnegative integers | df-n0 12414 |
ℕ0 | Yes | nnnn0 12420, nn0cn 12423 |
| n0 | not the empty set (see ne0) | |
≠ ∅ | No | n0i 4294, vn0 4299, ssn0 4358 |
| OLD | old, obsolete (to be removed soon) | |
| No | 19.43OLD 1885 |
| on | ordinal number | df-on 6329 |
𝐴 ∈ On | Yes |
elon 6334, 1on 8419 onelon 6350 |
| op | ordered pair | df-op 4589 |
⟨𝐴, 𝐵⟩ | Yes | dfopif 4828, opth 5432 |
| or | or | df-or 849 |
(𝜑 ∨ 𝜓) | Yes |
orcom 871, anor 985 |
| ot | ordered triple | df-ot 4591 |
⟨𝐴, 𝐵, 𝐶⟩ | Yes |
euotd 5469, fnotovb 7420 |
| ov | operation value | df-ov 7371 |
(𝐴𝐹𝐵) | Yes
| fnotovb 7420, fnovrn 7543 |
| p | plus (see "add"), for all-constant
theorems | df-add 11049 |
(3 + 2) = 5 | Yes |
3p2e5 12303 |
| pfx | prefix | df-pfx 14607 |
(𝑊 prefix 𝐿) | Yes |
pfxlen 14619, ccatpfx 14636 |
| pm | Principia Mathematica | |
| No | pm2.27 42 |
| pm | partial mapping (operation) | df-pm 8778 |
(𝐴 ↑pm 𝐵) | Yes | elpmi 8795, pmsspw 8827 |
| pr | pair | df-pr 4585 |
{𝐴, 𝐵} | Yes |
elpr 4607, prcom 4691, prid1g 4719, prnz 4736 |
| prm, prime | prime (number) | df-prm 16611 |
ℙ | Yes | 1nprm 16618, dvdsprime 16626 |
| pss | proper subset | df-pss 3923 |
𝐴 ⊊ 𝐵 | Yes | pssss 4052, sspsstri 4059 |
| q | rational numbers ("quotients") | df-q 12874 |
ℚ | Yes | elq 12875 |
| r | reversed (suffix) | |
| No | pm4.71r 558, caovdir 7602 |
| r | right | |
| No | orcd 874, simprl 771 |
| rab | restricted class abstraction |
df-rab 3402 | {𝑥 ∈ 𝐴 ∣ 𝜑} | Yes |
rabswap 3410, df-oprab 7372 |
| ral | restricted universal quantification |
df-ral 3053 | ∀𝑥 ∈ 𝐴𝜑 | Yes |
ralnex 3064, ralrnmpo 7507 |
| rcl | reverse closure | |
| No | ndmfvrcl 6875, nnarcl 8554 |
| re | real numbers | df-r 11048 |
ℝ | Yes | recn 11128, 0re 11146 |
| rel | relation | df-rel 5639 | Rel 𝐴 |
Yes | brrelex1 5685, relmpoopab 8046 |
| res | restriction | df-res 5644 |
(𝐴 ↾ 𝐵) | Yes |
opelres 5952, f1ores 6796 |
| reu | restricted existential uniqueness |
df-reu 3353 | ∃!𝑥 ∈ 𝐴𝜑 | Yes |
nfreud 3398, reurex 3356 |
| rex | restricted existential quantification |
df-rex 3063 | ∃𝑥 ∈ 𝐴𝜑 | Yes |
rexnal 3090, rexrnmpo 7508 |
| rmo | restricted "at most one" |
df-rmo 3352 | ∃*𝑥 ∈ 𝐴𝜑 | Yes |
nfrmod 3397, nrexrmo 3371 |
| rn | range | df-rn 5643 | ran 𝐴 |
Yes | elrng 5848, rncnvcnv 5891 |
| ring | (unital) ring | df-ring 20182 |
Ring | Yes |
ringidval 20130, isring 20184, ringgrp 20185 |
| rng | non-unital ring | df-rng 20100 |
Rng | Yes |
isrng 20101, rngabl 20102, rnglz 20112 |
| rot | rotation | |
| No | 3anrot 1100, 3orrot 1092 |
| s | eliminates need for syllogism (suffix) |
| | No | ancoms 458 |
| sb | (proper) substitution (of a set) |
df-sb 2069 | [𝑦 / 𝑥]𝜑 | Yes |
spsbe 2088, sbimi 2080 |
| sbc | (proper) substitution of a class |
df-sbc 3743 | [𝐴 / 𝑥]𝜑 | Yes |
sbc2or 3751, sbcth 3757 |
| sca | scalar | df-sca 17205 |
(Scalar‘𝐻) | Yes |
resssca 17275, mgpsca 20093 |
| simp | simple, simplification | |
| No | simpl 482, simp3r3 1285 |
| sn | singleton | df-sn 4583 |
{𝐴} | Yes | eldifsn 4744 |
| sp | specialization | |
| No | spsbe 2088, spei 2399 |
| ss | subset | df-ss 3920 |
𝐴 ⊆ 𝐵 | Yes | difss 4090 |
| struct | structure | df-struct 17086 |
Struct | Yes | brstruct 17087, structfn 17095 |
| sub | subtract | df-sub 11378 |
(𝐴 − 𝐵) | Yes |
subval 11383, subaddi 11480 |
| sup | supremum | df-sup 9357 |
sup(𝐴, 𝐵, < ) | Yes |
fisupcl 9385, supmo 9367 |
| supp | support (of a function) | df-supp 8113 |
(𝐹 supp 𝑍) | Yes |
ressuppfi 9310, mptsuppd 8139 |
| swap | swap (two parts within a theorem) |
| | No | rabswap 3410, 2reuswap 3706 |
| syl | syllogism | syl 17 |
| No | 3syl 18 |
| sym | symmetric | |
| No | df-symdif 4207, cnvsym 6079 |
| symg | symmetric group | df-symg 19311 |
(SymGrp‘𝐴) | Yes |
symghash 19319, pgrpsubgsymg 19350 |
| t |
times (see "mul"), for all-constant theorems |
df-mul 11050 |
(3 · 2) = 6 | Yes |
3t2e6 12318 |
| th, t |
theorem |
|
|
No |
nfth 1803, sbcth 3757, weth 10417, ancomst 464 |
| tp | triple | df-tp 4587 |
{𝐴, 𝐵, 𝐶} | Yes |
eltpi 4647, tpeq1 4701 |
| tr | transitive | |
| No | bitrd 279, biantr 806 |
| tru, t |
true, truth |
df-tru 1545 |
⊤ |
Yes |
bitru 1551, truanfal 1576, biimt 360 |
| un | union | df-un 3908 |
(𝐴 ∪ 𝐵) | Yes |
uneqri 4110, uncom 4112 |
| unit | unit (in a ring) |
df-unit 20306 | (Unit‘𝑅) | Yes |
isunit 20321, nzrunit 20469 |
| v |
setvar (especially for specializations of
theorems when a class is replaced by a setvar variable) |
|
x |
Yes |
cv 1541, vex 3446, velpw 4561, vtoclf 3523 |
| v |
disjoint variable condition used in place of nonfreeness
hypothesis (suffix) |
|
|
No |
spimv 2395 |
| vtx |
vertex |
df-vtx 29083 |
(Vtx‘𝐺) |
Yes |
vtxval0 29124, opvtxov 29090 |
| vv |
two disjoint variable conditions used in place of nonfreeness
hypotheses (suffix) |
|
|
No |
19.23vv 1945 |
| w | weak (version of a theorem) (suffix) | |
| No | ax11w 2136, spnfw 1981 |
| wrd | word |
df-word 14449 | Word 𝑆 | Yes |
iswrdb 14455, wrdfn 14463, ffz0iswrd 14476 |
| xp | cross product (Cartesian product) |
df-xp 5638 | (𝐴 × 𝐵) | Yes |
elxp 5655, opelxpi 5669, xpundi 5701 |
| xr | eXtended reals | df-xr 11182 |
ℝ* | Yes | ressxr 11188, rexr 11190, 0xr 11191 |
| z | integers (from German "Zahlen") |
df-z 12501 | ℤ | Yes |
elz 12502, zcn 12505 |
| zn | ring of integers mod 𝑁 | df-zn 21473 |
(ℤ/nℤ‘𝑁) | Yes |
znval 21502, zncrng 21511, znhash 21525 |
| zring | ring of integers | df-zring 21414 |
ℤring | Yes | zringbas 21420, zringcrng 21415
|
| 0, z |
slashed zero (empty set) | df-nul 4288 |
∅ | Yes |
n0i 4294, vn0 4299; snnz 4735, prnz 4736 |
(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.) |
