| Description:
The following gives conventions used in the Metamath Proof Explorer
(MPE, set.mm) regarding labels.
For other conventions, see conventions 28900 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 3064"rgen.1 $e |- ( x e. A -> ph ) $."
or letters corresponding to the (main) class variable used in the
hypothesis, e.g., for mdet0 21838: "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 43880.
- 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 3234.
- 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... 15672. 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 3900, and thus its syntax label fragment is "dif". Similarly, the
subclass relation 𝐴 ⊆ 𝐵 has syntax label fragment "ss"
because it is defined in df-ss 3914. 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 4077. There are many other syntax label fragments, e.g.,
singleton construct {𝐴} has syntax label fragment "sn" (because it
is defined in df-sn 4572), and the pair construct {𝐴, 𝐵} has
fragment "pr" ( from df-pr 4574). 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 4732. An "n" is often used for negation (¬), e.g.,
nan 827.
- 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 10957) and "re" represents real numbers ℝ (Definition df-r 10961).
The empty set ∅ often uses fragment 0, even though it is defined
in df-nul 4268. The syntax construct (𝐴 + 𝐵) usually uses the
fragment "add" (which is consistent with df-add 10962), 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 12188.
- 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 15938 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 15859) we have value cosval 15911 and
closure coscl 15915.
- 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 28903 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 2199. This
often permits to prove the result using fewer axioms, and/or to
eliminate a nonfreeness hypothesis (such as Ⅎ𝑥𝜑 in 19.21 2199).
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 2575 derived from eu6 2573. 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 5384.
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 2408 (cbval 2397 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 3502.
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 479)
- 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 477, rexlimiva 3141 |
| abl | Abelian group | df-abl 19464 |
Abel | Yes | ablgrp 19466, zringabl 20757 |
| abs | absorption | | | No |
ressabs 17036 |
| abs | absolute value (of a complex number) |
df-abs 15026 | (abs‘𝐴) | Yes |
absval 15028, absneg 15068, abs1 15088 |
| ad | adding | |
| No | adantr 481, ad2antlr 724 |
| add | add (see "p") | df-add 10962 |
(𝐴 + 𝐵) | Yes |
addcl 11033, addcom 11241, addass 11038 |
| al | "for all" | |
∀𝑥𝜑 | No | alim 1811, alex 1827 |
| ALT | alternative/less preferred (suffix) | |
| No | idALT 23 |
| an | and | df-an 397 |
(𝜑 ∧ 𝜓) | Yes |
anor 980, iman 402, imnan 400 |
| ant | antecedent | |
| No | adantr 481 |
| ass | associative | |
| No | biass 385, orass 919, mulass 11039 |
| asym | asymmetric, antisymmetric | |
| No | intasym 6043, asymref 6044, posasymb 18114 |
| ax | axiom | |
| No | ax6dgen 2123, ax1cn 10985 |
| bas, base |
base (set of an extensible structure) | df-base 16990 |
(Base‘𝑆) | Yes |
baseval 16991, ressbas 17024, cnfldbas 20684 |
| b, bi | biconditional ("iff", "if and only if")
| df-bi 206 | (𝜑 ↔ 𝜓) | Yes |
impbid 211, sspwb 5384 |
| br | binary relation | df-br 5088 |
𝐴𝑅𝐵 | Yes | brab1 5135, brun 5138 |
| cbv | change bound variable | | |
No | cbvalivw 2009, cbvrex 3333 |
| cdm | codomain | |
| No | ffvelcdm 6999, focdmex 7845 |
| cl | closure | | | No |
ifclda 4506, ovrcl 7358, zaddcl 12440 |
| cn | complex numbers | df-c 10957 |
ℂ | Yes | nnsscn 12058, nncn 12061 |
| cnfld | field of complex numbers | df-cnfld 20681 |
ℂfld | Yes | cnfldbas 20684, cnfldinv 20712 |
| cntz | centralizer | df-cntz 18999 |
(Cntz‘𝑀) | Yes |
cntzfval 19002, dprdfcntz 19693 |
| cnv | converse | df-cnv 5616 |
◡𝐴 | Yes | opelcnvg 5810, f1ocnv 6766 |
| co | composition | df-co 5617 |
(𝐴 ∘ 𝐵) | Yes | cnvco 5815, fmptco 7041 |
| com | commutative | |
| No | orcom 867, bicomi 223, eqcomi 2746 |
| con | contradiction, contraposition | |
| No | condan 815, con2d 134 |
| csb | class substitution | df-csb 3843 |
⦋𝐴 / 𝑥⦌𝐵 | Yes |
csbid 3855, csbie2g 3885 |
| cyg | cyclic group | df-cyg 19553 |
CycGrp | Yes |
iscyg 19554, zringcyg 20774 |
| d | deduction form (suffix) | |
| No | idd 24, impbid 211 |
| df | (alternate) definition (prefix) | |
| No | dfrel2 6115, dffn2 6640 |
| di, distr | distributive | |
| No |
andi 1005, imdi 390, ordi 1003, difindi 4226, ndmovdistr 7503 |
| dif | class difference | df-dif 3900 |
(𝐴 ∖ 𝐵) | Yes |
difss 4077, difindi 4226 |
| div | division | df-div 11713 |
(𝐴 / 𝐵) | Yes |
divcl 11719, divval 11715, divmul 11716 |
| dm | domain | df-dm 5618 |
dom 𝐴 | Yes | dmmpt 6166, iswrddm0 14320 |
| e, eq, equ | equals (equ for setvars, eq for
classes) | df-cleq 2729 |
𝐴 = 𝐵 | Yes |
2p2e4 12188, uneqri 4096, equtr 2023 |
| edg | edge | df-edg 27554 |
(Edg‘𝐺) | Yes |
edgopval 27557, usgredgppr 27699 |
| el | element of | |
𝐴 ∈ 𝐵 | Yes |
eldif 3907, eldifsn 4732, elssuni 4883 |
| en | equinumerous | df-en |
𝐴 ≈ 𝐵 | Yes | domen 8801, enfi 9034 |
| eu | "there exists exactly one" | eu6 2573 |
∃!𝑥𝜑 | Yes | euex 2576, euabsn 4672 |
| ex | exists (i.e. is a set) | |
∈ V | No | brrelex1 5659, 0ex 5246 |
| ex, e | "there exists (at least one)" |
df-ex 1781 |
∃𝑥𝜑 | Yes | exim 1835, alex 1827 |
| exp | export | |
| No | expt 177, expcom 414 |
| f | "not free in" (suffix) | |
| No | equs45f 2458, sbf 2262 |
| f | function | df-f 6470 |
𝐹:𝐴⟶𝐵 | Yes | fssxp 6666, opelf 6673 |
| fal | false | df-fal 1553 |
⊥ | Yes | bifal 1556, falantru 1575 |
| fi | finite intersection | df-fi 9247 |
(fi‘𝐵) | Yes | fival 9248, inelfi 9254 |
| fi, fin | finite | df-fin 8787 |
Fin | Yes |
isfi 8816, snfi 8888, onfin 9074 |
| fld | field (Note: there is an alternative
definition Fld of a field, see df-fld 36222) | df-field 20073 |
Field | Yes | isfld 20081, fldidom 20659 |
| fn | function with domain | df-fn 6469 |
𝐴 Fn 𝐵 | Yes | ffn 6638, fndm 6575 |
| frgp | free group | df-frgp 19391 |
(freeGrp‘𝐼) | Yes |
frgpval 19439, frgpadd 19444 |
| fsupp | finitely supported function |
df-fsupp 9206 | 𝑅 finSupp 𝑍 | Yes |
isfsupp 9209, fdmfisuppfi 9214, fsuppco 9238 |
| fun | function | df-fun 6468 |
Fun 𝐹 | Yes | funrel 6488, ffun 6641 |
| fv | function value | df-fv 6474 |
(𝐹‘𝐴) | Yes | fvres 6831, swrdfv 14440 |
| fz | finite set of sequential integers |
df-fz 13320 |
(𝑀...𝑁) | Yes | fzval 13321, eluzfz 13331 |
| fz0 | finite set of sequential nonnegative integers |
|
(0...𝑁) | Yes | nn0fz0 13434, fz0tp 13437 |
| fzo | half-open integer range | df-fzo 13463 |
(𝑀..^𝑁) | Yes |
elfzo 13469, elfzofz 13483 |
| g | more general (suffix); eliminates "is a set"
hypotheses | |
| No | uniexg 7635 |
| gr | graph | |
| No | uhgrf 27568, isumgr 27601, usgrres1 27818 |
| grp | group | df-grp 18656 |
Grp | Yes | isgrp 18659, tgpgrp 23312 |
| gsum | group sum | df-gsum 17230 |
(𝐺 Σg 𝐹) | Yes |
gsumval 18438, gsumwrev 19049 |
| hash | size (of a set) | df-hash 14125 |
(♯‘𝐴) | Yes |
hashgval 14127, hashfz1 14140, hashcl 14150 |
| hb | hypothesis builder (prefix) | |
| No | hbxfrbi 1826, hbald 2167, hbequid 37143 |
| hm | (monoid, group, ring) homomorphism | |
| No | ismhm 18509, isghm 18910, isrhm 20040 |
| i | inference (suffix) | |
| No | eleq1i 2828, tcsni 9579 |
| i | implication (suffix) | |
| No | brwdomi 9404, infeq5i 9472 |
| id | identity | |
| No | biid 260 |
| iedg | indexed edge | df-iedg 27505 |
(iEdg‘𝐺) | Yes |
iedgval0 27546, edgiedgb 27560 |
| idm | idempotent | |
| No | anidm 565, tpidm13 4702 |
| im, imp | implication (label often omitted) |
df-im 14891 | (𝐴 → 𝐵) | Yes |
iman 402, imnan 400, impbidd 209 |
| ima | image | df-ima 5621 |
(𝐴 “ 𝐵) | Yes | resima 5945, imaundi 6076 |
| imp | import | |
| No | biimpa 477, impcom 408 |
| in | intersection | df-in 3904 |
(𝐴 ∩ 𝐵) | Yes | elin 3913, incom 4146 |
| inf | infimum | df-inf 9279 |
inf(ℝ+, ℝ*, < ) | Yes |
fiinfcl 9337, infiso 9344 |
| is... | is (something a) ...? | |
| No | isring 19862 |
| j | joining, disjoining | |
| No | jc 161, jaoi 854 |
| l | left | |
| No | olcd 871, simpl 483 |
| map | mapping operation or set exponentiation |
df-map 8667 | (𝐴 ↑m 𝐵) | Yes |
mapvalg 8675, elmapex 8686 |
| mat | matrix | df-mat 21638 |
(𝑁 Mat 𝑅) | Yes |
matval 21641, matring 21675 |
| mdet | determinant (of a square matrix) |
df-mdet 21817 | (𝑁 maDet 𝑅) | Yes |
mdetleib 21819, mdetrlin 21834 |
| mgm | magma | df-mgm 18403 |
Magma | Yes |
mgmidmo 18421, mgmlrid 18428, ismgm 18404 |
| mgp | multiplicative group | df-mgp 19796 |
(mulGrp‘𝑅) | Yes |
mgpress 19810, ringmgp 19864 |
| mnd | monoid | df-mnd 18463 |
Mnd | Yes | mndass 18471, mndodcong 19226 |
| mo | "there exists at most one" | df-mo 2539 |
∃*𝑥𝜑 | Yes | eumo 2577, moim 2543 |
| mp | modus ponens | ax-mp 5 |
| No | mpd 15, mpi 20 |
| mpo | maps-to notation for an operation |
df-mpo 7322 | (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) | Yes |
mpompt 7430, resmpo 7436 |
| mpt | modus ponendo tollens | |
| No | mptnan 1769, mptxor 1770 |
| mpt | maps-to notation for a function |
df-mpt 5171 | (𝑥 ∈ 𝐴 ↦ 𝐵) | Yes |
fconstmpt 5668, resmpt 5965 |
| mpt2 | maps-to notation for an operation (deprecated).
We are in the process of replacing mpt2 with mpo in labels. |
df-mpo 7322 | (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) | Yes |
mpompt 7430, resmpo 7436 |
| mul | multiplication (see "t") | df-mul 10963 |
(𝐴 · 𝐵) | Yes |
mulcl 11035, divmul 11716, mulcom 11037, mulass 11039 |
| n, not | not | |
¬ 𝜑 | Yes |
nan 827, notnotr 130 |
| ne | not equal | df-ne | 𝐴 ≠ 𝐵 |
Yes | exmidne 2951, neeqtrd 3011 |
| nel | not element of | df-nel | 𝐴 ∉ 𝐵
|
Yes | neli 3049, nnel 3056 |
| ne0 | not equal to zero (see n0) | |
≠ 0 | No |
negne0d 11410, ine0 11490, gt0ne0 11520 |
| nf | "not free in" (prefix) | |
| No | nfnd 1860 |
| ngp | normed group | df-ngp 23822 |
NrmGrp | Yes | isngp 23835, ngptps 23841 |
| nm | norm (on a group or ring) | df-nm 23821 |
(norm‘𝑊) | Yes |
nmval 23828, subgnm 23872 |
| nn | positive integers | df-nn 12054 |
ℕ | Yes | nnsscn 12058, nncn 12061 |
| nn0 | nonnegative integers | df-n0 12314 |
ℕ0 | Yes | nnnn0 12320, nn0cn 12323 |
| n0 | not the empty set (see ne0) | |
≠ ∅ | No | n0i 4278, vn0 4283, ssn0 4345 |
| OLD | old, obsolete (to be removed soon) | |
| No | 19.43OLD 1885 |
| on | ordinal number | df-on 6293 |
𝐴 ∈ On | Yes |
elon 6298, 1on 8358 onelon 6314 |
| op | ordered pair | df-op 4578 |
⟨𝐴, 𝐵⟩ | Yes | dfopif 4812, opth 5410 |
| or | or | df-or 845 |
(𝜑 ∨ 𝜓) | Yes |
orcom 867, anor 980 |
| ot | ordered triple | df-ot 4580 |
⟨𝐴, 𝐵, 𝐶⟩ | Yes |
euotd 5446, fnotovb 7367 |
| ov | operation value | df-ov 7320 |
(𝐴𝐹𝐵) | Yes
| fnotovb 7367, fnovrn 7489 |
| p | plus (see "add"), for all-constant
theorems | df-add 10962 |
(3 + 2) = 5 | Yes |
3p2e5 12204 |
| pfx | prefix | df-pfx 14463 |
(𝑊 prefix 𝐿) | Yes |
pfxlen 14475, ccatpfx 14493 |
| pm | Principia Mathematica | |
| No | pm2.27 42 |
| pm | partial mapping (operation) | df-pm 8668 |
(𝐴 ↑pm 𝐵) | Yes | elpmi 8684, pmsspw 8715 |
| pr | pair | df-pr 4574 |
{𝐴, 𝐵} | Yes |
elpr 4594, prcom 4678, prid1g 4706, prnz 4723 |
| prm, prime | prime (number) | df-prm 16454 |
ℙ | Yes | 1nprm 16461, dvdsprime 16469 |
| pss | proper subset | df-pss 3916 |
𝐴 ⊊ 𝐵 | Yes | pssss 4041, sspsstri 4048 |
| q | rational numbers ("quotients") | df-q 12769 |
ℚ | Yes | elq 12770 |
| r | right | |
| No | orcd 870, simprl 768 |
| rab | restricted class abstraction |
df-rab 3405 | {𝑥 ∈ 𝐴 ∣ 𝜑} | Yes |
rabswap 3413, df-oprab 7321 |
| ral | restricted universal quantification |
df-ral 3063 | ∀𝑥 ∈ 𝐴𝜑 | Yes |
ralnex 3073, ralrnmpo 7454 |
| rcl | reverse closure | |
| No | ndmfvrcl 6845, nnarcl 8497 |
| re | real numbers | df-r 10961 |
ℝ | Yes | recn 11041, 0re 11057 |
| rel | relation | df-rel 5615 | Rel 𝐴 |
Yes | brrelex1 5659, relmpoopab 7981 |
| res | restriction | df-res 5620 |
(𝐴 ↾ 𝐵) | Yes |
opelres 5917, f1ores 6768 |
| reu | restricted existential uniqueness |
df-reu 3351 | ∃!𝑥 ∈ 𝐴𝜑 | Yes |
nfreud 3401, reurex 3354 |
| rex | restricted existential quantification |
df-rex 3072 | ∃𝑥 ∈ 𝐴𝜑 | Yes |
rexnal 3100, rexrnmpo 7455 |
| rmo | restricted "at most one" |
df-rmo 3350 | ∃*𝑥 ∈ 𝐴𝜑 | Yes |
nfrmod 3400, nrexrmo 3371 |
| rn | range | df-rn 5619 | ran 𝐴 |
Yes | elrng 5821, rncnvcnv 5863 |
| rng | (unital) ring | df-ring 19860 |
Ring | Yes |
ringidval 19814, isring 19862, ringgrp 19863 |
| rot | rotation | |
| No | 3anrot 1099, 3orrot 1091 |
| s | eliminates need for syllogism (suffix) |
| | No | ancoms 459 |
| sb | (proper) substitution (of a set) |
df-sb 2067 | [𝑦 / 𝑥]𝜑 | Yes |
spsbe 2084, sbimi 2076 |
| sbc | (proper) substitution of a class |
df-sbc 3727 | [𝐴 / 𝑥]𝜑 | Yes |
sbc2or 3735, sbcth 3741 |
| sca | scalar | df-sca 17055 |
(Scalar‘𝐻) | Yes |
resssca 17130, mgpsca 19803 |
| simp | simple, simplification | |
| No | simpl 483, simp3r3 1282 |
| sn | singleton | df-sn 4572 |
{𝐴} | Yes | eldifsn 4732 |
| sp | specialization | |
| No | spsbe 2084, spei 2393 |
| ss | subset | df-ss 3914 |
𝐴 ⊆ 𝐵 | Yes | difss 4077 |
| struct | structure | df-struct 16925 |
Struct | Yes | brstruct 16926, structfn 16934 |
| sub | subtract | df-sub 11287 |
(𝐴 − 𝐵) | Yes |
subval 11292, subaddi 11388 |
| sup | supremum | df-sup 9278 |
sup(𝐴, 𝐵, < ) | Yes |
fisupcl 9305, supmo 9288 |
| supp | support (of a function) | df-supp 8027 |
(𝐹 supp 𝑍) | Yes |
ressuppfi 9231, mptsuppd 8052 |
| swap | swap (two parts within a theorem) |
| | No | rabswap 3413, 2reuswap 3691 |
| syl | syllogism | syl 17 |
| No | 3syl 18 |
| sym | symmetric | |
| No | df-symdif 4187, cnvsym 6040 |
| symg | symmetric group | df-symg 19051 |
(SymGrp‘𝐴) | Yes |
symghash 19061, pgrpsubgsymg 19093 |
| t |
times (see "mul"), for all-constant theorems |
df-mul 10963 |
(3 · 2) = 6 | Yes |
3t2e6 12219 |
| th, t |
theorem |
|
|
No |
nfth 1802, sbcth 3741, weth 10331, ancomst 465 |
| tp | triple | df-tp 4576 |
{𝐴, 𝐵, 𝐶} | Yes |
eltpi 4633, tpeq1 4688 |
| tr | transitive | |
| No | bitrd 278, biantr 803 |
| tru, t |
true, truth |
df-tru 1543 |
⊤ |
Yes |
bitru 1549, truanfal 1574, biimt 360 |
| un | union | df-un 3902 |
(𝐴 ∪ 𝐵) | Yes |
uneqri 4096, uncom 4098 |
| unit | unit (in a ring) |
df-unit 19959 | (Unit‘𝑅) | Yes |
isunit 19974, nzrunit 20621 |
| v |
setvar (especially for specializations of
theorems when a class is replaced by a setvar variable) |
|
x |
Yes |
cv 1539, vex 3445, velpw 4550, vtoclf 3506 |
| v |
disjoint variable condition used in place of nonfreeness
hypothesis (suffix) |
|
|
No |
spimv 2389 |
| vtx |
vertex |
df-vtx 27504 |
(Vtx‘𝐺) |
Yes |
vtxval0 27545, opvtxov 27511 |
| 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 2125, spnfw 1982 |
| wrd | word |
df-word 14297 | Word 𝑆 | Yes |
iswrdb 14302, wrdfn 14310, ffz0iswrd 14323 |
| xp | cross product (Cartesian product) |
df-xp 5614 | (𝐴 × 𝐵) | Yes |
elxp 5631, opelxpi 5645, xpundi 5674 |
| xr | eXtended reals | df-xr 11093 |
ℝ* | Yes | ressxr 11099, rexr 11101, 0xr 11102 |
| z | integers (from German "Zahlen") |
df-z 12400 | ℤ | Yes |
elz 12401, zcn 12404 |
| zn | ring of integers mod 𝑁 | df-zn 20791 |
(ℤ/nℤ‘𝑁) | Yes |
znval 20822, zncrng 20835, znhash 20849 |
| zring | ring of integers | df-zring 20754 |
ℤring | Yes | zringbas 20759, zringcrng 20755
|
| 0, z |
slashed zero (empty set) | df-nul 4268 |
∅ | Yes |
n0i 4278, vn0 4283; snnz 4722, prnz 4723 |
(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.) |
