| Description:
The following gives conventions used in the Metamath Proof Explorer
(MPE, set.mm) regarding labels.
For other conventions, see conventions 30788 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 3084"rgen.1 $e |- ( x e. A -> ph ) $."
or letters corresponding to the (main) class variable used in the
hypothesis, e.g., for mdet0 22800: "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 2693 and stirling 46844.
- 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 1872, and the restricted quantifier version of Theorem 21 from
Section 19 of [Margaris] p. 90 is labeled r19.21 3263.
- 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... 15961. 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 3911, and thus its syntax label fragment is "dif". Similarly, the
subclass relation 𝐴 ⊆ 𝐵 has syntax label fragment "ss"
because it is defined in df-ss 3925. 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 4093. There are many other syntax label fragments, e.g.,
singleton construct {𝐴} has syntax label fragment "sn" (because it
is defined in df-sn 4595), and the pair construct {𝐴, 𝐵} has
fragment "pr" ( from df-pr 4597). 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 4758. An "n" is often used for negation (¬), e.g.,
nan 843.
- 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 11124) and "re" represents real numbers ℝ (Definition df-r 11128).
The empty set ∅ often uses fragment 0, even though it is defined
in df-nul 4290. The syntax construct (𝐴 + 𝐵) usually uses the
fragment "add" (which is consistent with df-add 11129), 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 12393.
- 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 16231 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 16149) we have value cosval 16204 and
closure coscl 16208.
- 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 30791 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 1972 versus 19.21 2246. This
often permits to prove the result using fewer axioms, and/or to
eliminate a nonfreeness hypothesis (such as Ⅎ𝑥𝜑 in 19.21 2246).
If no constraint is put on axiom use, then the v-version can be proved
from the original theorem using nfv 1947. If two (resp. three) such
disjoint variable conditions are added, then the suffix "vv" (resp.
"vvv") is used, e.g., exlimivv 1965.
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 2607 derived from eu6 2605. 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 5435.
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 2444 (cbval 2433 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 596), commutes
(e.g., biimpac 484)
- 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 482, rexlimiva 3161 |
| abl | Abelian group | df-abl 19884 |
Abel | Yes | ablgrp 19886, zringabl 21638 |
| abs | absorption | | | No |
ressabs 17333 |
| abs | absolute value (of a complex number) |
df-abs 15313 | (abs‘𝐴) | Yes |
absval 15315, absneg 15354, abs1 15374 |
| ad | adding | |
| No | adantr 486, ad2antlr 740 |
| add | add (see "p") | df-add 11129 |
(𝐴 + 𝐵) | Yes |
addcl 11200, addcom 11414, addass 11205 |
| al | "for all" | |
∀𝑥𝜑 | No | alim 1843, alex 1859 |
| ALT | alternative/less preferred (suffix) | |
| No | idALT 24 |
| an | and | df-an 402 |
(𝜑 ∧ 𝜓) | Yes |
anor 998, iman 407, imnan 405 |
| ant | antecedent | |
| No | adantr 486 |
| ass | associative | |
| No | biass 388, orass 935, mulass 11206 |
| asym | asymmetric, antisymmetric | |
| No | intasym 6120, asymref 6121, posasymb 18400 |
| ax | axiom | |
| No | ax6dgen 2166, ax1cn 11152 |
| bas, base |
base (set of an extensible structure) | df-base 17295 |
(Base‘𝑆) | Yes |
baseval 17296, ressbas 17321, cnfldbas 21563 |
| b, bi | biconditional ("iff", "if and only if")
| df-bi 210 | (𝜑 ↔ 𝜓) | Yes |
impbid 215, sspwb 5435 |
| br | binary relation | df-br 5115 |
𝐴𝑅𝐵 | Yes | brab1 5164, brun 5167 |
| c | commutes, commuted (suffix) | | |
No | biimpac 484 |
| c | contraction (suffix) | | |
No | sylc 66, syl2anc 596 |
| cbv | change bound variable | | |
No | cbvalivw 2040, cbvrex 3355 |
| cdm | codomain | |
| No | ffvelcdm 7083, focdmex 7962 |
| cl | closure | | | No |
ifclda 4528, ovrcl 7464, zaddcl 12652 |
| cn | complex numbers | df-c 11124 |
ℂ | Yes | nnsscn 12256, nncn 12259 |
| cnfld | field of complex numbers | df-cnfld 21560 |
ℂfld | Yes | cnfldbas 21563, cnfldinv 21590 |
| cntz | centralizer | df-cntz 19418 |
(Cntz‘𝑀) | Yes |
cntzfval 19421, dprdfcntz 20118 |
| cnv | converse | df-cnv 5674 |
◡𝐴 | Yes | opelcnvg 5871, f1ocnv 6840 |
| co | composition | df-co 5675 |
(𝐴 ∘ 𝐵) | Yes | cnvco 5880, fmptco 7132 |
| com | commutative | |
| No | orcom 884, bicomi 227, eqcomi 2775 |
| con | contradiction, contraposition | |
| No | condan 830, con2d 135 |
| csb | class substitution | df-csb 3857 |
⦋𝐴 / 𝑥⦌𝐵 | Yes |
csbid 3869, csbie2g 3896 |
| cyg | cyclic group | df-cyg 19979 |
CycGrp | Yes |
iscyg 19980, zringcyg 21656 |
| d | deduction form (suffix) | |
| No | idd 25, impbid 215 |
| df | (alternate) definition (prefix) | |
| No | dfrel2 6192, dffn2 6714 |
| di, distr | distributive | |
| No |
andi 1025, imdi 394, ordi 1023, difindi 4248, ndmovdistr 7612 |
| dif | class difference | df-dif 3911 |
(𝐴 ∖ 𝐵) | Yes |
difss 4093, difindi 4248 |
| div | division | df-div 11890 |
(𝐴 / 𝐵) | Yes |
divcl 11896, divval 11892, divmul 11893 |
| dm | domain | df-dm 5676 |
dom 𝐴 | Yes | dmmpt 6246, iswrddm0 14595 |
| e, eq, equ | equals (equ for setvars, eq for
classes) | df-cleq 2758 |
𝐴 = 𝐵 | Yes |
2p2e4 12393, uneqri 4113, equtr 2054 |
| edg | edge | df-edg 29435 |
(Edg‘𝐺) | Yes |
edgopval 29438, usgredgppr 29583 |
| el | element of | |
𝐴 ∈ 𝐵 | Yes |
eldif 3918, eldifsn 4758, elssuni 4909 |
| en | equinumerous | df-en |
𝐴 ≈ 𝐵 | Yes | domen 8967, enfi 9181 |
| eu | "there exists exactly one" | eu6 2605 |
∃!𝑥𝜑 | Yes | euex 2608, euabsn 4697 |
| ex | exists (i.e. is a set) | |
∈ V | No | brrelex1 5719, 0ex 5275 |
| ex, e | "there exists (at least one)" |
df-ex 1813 |
∃𝑥𝜑 | Yes | exim 1867, alex 1859 |
| exp | export | |
| No | expt 178, expcom 419 |
| f | "not free in" (suffix) | |
| No | equs45f 2494, sbf 2309 |
| f | function | df-f 6547 |
𝐹:𝐴⟶𝐵 | Yes | fssxp 6740, opelf 6746 |
| fal | false | df-fal 1583 |
⊥ | Yes | bifal 1586, falantru 1605 |
| fi | finite intersection | df-fi 9381 |
(fi‘𝐵) | Yes | fival 9382, inelfi 9388 |
| fi, fin | finite | df-fin 8956 |
Fin | Yes |
isfi 8981, snfi 9050, onfin 9209 |
| fld | field (Note: there is an alternative
definition Fld of a field, see df-fld 38684) | df-field 20867 |
Field | Yes | isfld 20877, fldidom 20912 |
| fn | function with domain | df-fn 6546 |
𝐴 Fn 𝐵 | Yes | ffn 6712, fndm 6645 |
| frgp | free group | df-frgp 19811 |
(freeGrp‘𝐼) | Yes |
frgpval 19859, frgpadd 19864 |
| fsupp | finitely supported function |
df-fsupp 9332 | 𝑅 finSupp 𝑍 | Yes |
isfsupp 9335, fdmfisuppfi 9344, fsuppco 9372 |
| fun | function | df-fun 6545 |
Fun 𝐹 | Yes | funrel 6560, ffun 6715 |
| fv | function value | df-fv 6551 |
(𝐹‘𝐴) | Yes | fvres 6907, swrdfv 14708 |
| fz | finite set of sequential integers |
df-fz 13554 |
(𝑀...𝑁) | Yes | fzval 13555, eluzfz 13565 |
| fz0 | finite set of sequential nonnegative integers |
|
(0...𝑁) | Yes | nn0fz0 13672, fz0tp 13675 |
| fzo | half-open integer range | df-fzo 13702 |
(𝑀..^𝑁) | Yes |
elfzo 13708, elfzofz 13723 |
| g | more general (suffix); eliminates "is a set"
hypotheses | |
| No | uniexg 7751 |
| gr | graph | |
| No | uhgrf 29449, isumgr 29482, usgrres1 29702 |
| grp | group | df-grp 19034 |
Grp | Yes | isgrp 19037, tgpgrp 24272 |
| gsum | group sum | df-gsum 17520 |
(𝐺 Σg 𝐹) | Yes |
gsumval 18764, gsumwrev 19467 |
| hash | size (of a set) | df-hash 14387 |
(♯‘𝐴) | Yes |
hashgval 14389, hashfz1 14402, hashcl 14412 |
| hb | hypothesis builder (prefix) | |
| No | hbxfrbi 1858, hbald 2206, hbequid 39724 |
| hm | (monoid, group, ring, ...) homomorphism |
| | No |
ismhm 18874, isghm 19317, isrhm 20594 |
| i | inference (suffix) | |
| No | eleq1i 2857, tcsni 9720 |
| i | implication (suffix) | |
| No | brwdomi 9540, infeq5i 9615 |
| id | identity | |
| No | biid 264 |
| iedg | indexed edge | df-iedg 29386 |
(iEdg‘𝐺) | Yes |
iedgval0 29427, edgiedgb 29441 |
| idm | idempotent | |
| No | anidm 575, tpidm13 4727 |
| im, imp | implication (label often omitted) |
df-im 15178 | (𝐴 → 𝐵) | Yes |
iman 407, imnan 405, impbidd 213 |
| im | (group, ring, ...) isomorphism | |
| No | isgim 19363, rimrcl 20597 |
| ima | image | df-ima 5679 |
(𝐴 “ 𝐵) | Yes | resima 6019, imaundi 6152 |
| imp | import | |
| No | biimpa 482, impcom 413 |
| in | intersection | df-in 3915 |
(𝐴 ∩ 𝐵) | Yes | elin 3924, incom 4165 |
| inf | infimum | df-inf 9413 |
inf(ℝ+, ℝ*, < ) | Yes |
fiinfcl 9473, infiso 9480 |
| is... | is (something a) ...? | |
| No | isring 20350 |
| j | joining, disjoining | |
| No | jc 162, jaoi 871 |
| l | left | |
| No | olcd 888, simpl 488 |
| map | mapping operation or set exponentiation |
df-map 8835 | (𝐴 ↑m 𝐵) | Yes |
mapvalg 8842, elmapex 8854 |
| mat | matrix | df-mat 22602 |
(𝑁 Mat 𝑅) | Yes |
matval 22605, matring 22637 |
| mdet | determinant (of a square matrix) |
df-mdet 22779 | (𝑁 maDet 𝑅) | Yes |
mdetleib 22781, mdetrlin 22796 |
| mgm | magma | df-mgm 18723 |
Magma | Yes |
mgmidmo 18743, mgmlrid 18750, ismgm 18724 |
| mgp | multiplicative group | df-mgp 20248 |
(mulGrp‘𝑅) | Yes |
mgpress 20257, ringmgp 20352 |
| mnd | monoid | df-mnd 18822 |
Mnd | Yes | mndass 18830, mndodcong 19643 |
| mo | "there exists at most one" | df-mo 2570 |
∃*𝑥𝜑 | Yes | eumo 2609, moim 2575 |
| mp | modus ponens | ax-mp 5 |
| No | mpd 16, mpi 21 |
| mpo | maps-to notation for an operation |
df-mpo 7428 | (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) | Yes |
mpompt 7537, resmpo 7543 |
| mpt | modus ponendo tollens | |
| No | mptnan 1801, mptxor 1802 |
| mpt | maps-to notation for a function |
df-mpt 5198 | (𝑥 ∈ 𝐴 ↦ 𝐵) | Yes |
fconstmpt 5728, resmpt 6044 |
| mul | multiplication (see "t") | df-mul 11130 |
(𝐴 · 𝐵) | Yes |
mulcl 11202, divmul 11893, mulcom 11204, mulass 11206 |
| n, not | not | |
¬ 𝜑 | Yes |
nan 843, notnotr 131 |
| ne | not equal | df-ne | 𝐴 ≠ 𝐵 |
Yes | exmidne 2971, neeqtrd 3030 |
| nel | not element of | df-nel | 𝐴 ∉ 𝐵
|
Yes | neli 3069, nnel 3077 |
| ne0 | not equal to zero (see n0) | |
≠ 0 | No |
negne0d 11585, ine0 11667, gt0ne0 11697 |
| nf | "not free in" (prefix) | df-nf 1817 |
Ⅎ𝑥𝜑 | Yes | nfnd 1891 |
| ngp | normed group | df-ngp 24777 |
NrmGrp | Yes | isngp 24790, ngptps 24796 |
| nm | norm (on a group or ring) | df-nm 24776 |
(norm‘𝑊) | Yes |
nmval 24783, subgnm 24827 |
| nn | positive integers | df-nn 12252 |
ℕ | Yes | nnsscn 12256, nncn 12259 |
| nn0 | nonnegative integers | df-n0 12523 |
ℕ0 | Yes | nnnn0 12529, nn0cn 12532 |
| n0 | not the empty set (see ne0) | |
≠ ∅ | No | n0i 4296, vn0 4301, ssn0 4365 |
| OLD | old, obsolete (to be removed soon) | |
| No | 19.43OLD 1916 |
| on | ordinal number | df-on 6371 |
𝐴 ∈ On | Yes |
elon 6376, 1on 8475 onelon 6392 |
| op | ordered pair | df-op 4601 |
⟨𝐴, 𝐵⟩ | Yes | dfopif 4840, opth 5463 |
| or | or | df-or 862 |
(𝜑 ∨ 𝜓) | Yes |
orcom 884, anor 998 |
| ot | ordered triple | df-ot 4603 |
⟨𝐴, 𝐵, 𝐶⟩ | Yes |
euotd 5501, fnotovb 7475 |
| ov | operation value | df-ov 7426 |
(𝐴𝐹𝐵) | Yes
| fnotovb 7475, fnovrn 7598 |
| p | plus (see "add"), for all-constant
theorems | df-add 11129 |
(3 + 2) = 5 | Yes |
3p2e5 12409 |
| pfx | prefix | df-pfx 14733 |
(𝑊 prefix 𝐿) | Yes |
pfxlen 14745, ccatpfx 14762 |
| pm | Principia Mathematica | |
| No | pm2.27 43 |
| pm | partial mapping (operation) | df-pm 8836 |
(𝐴 ↑pm 𝐵) | Yes | elpmi 8852, pmsspw 8884 |
| pr | pair | df-pr 4597 |
{𝐴, 𝐵} | Yes |
elpr 4619, prcom 4703, prid1g 4731, prnz 4748 |
| prm, prime | prime (number) | df-prm 16755 |
ℙ | Yes | 1nprm 16762, dvdsprime 16770 |
| pss | proper subset | df-pss 3928 |
𝐴 ⊊ 𝐵 | Yes | pssss 4055, sspsstri 4063 |
| q | rational numbers ("quotients") | df-q 12991 |
ℚ | Yes | elq 12992 |
| r | reversed (suffix) | |
| No | pm4.71r 568, caovdir 7657 |
| r | right | |
| No | orcd 887, simprl 783 |
| rab | restricted class abstraction |
df-rab 3420 | {𝑥 ∈ 𝐴 ∣ 𝜑} | Yes |
rabswap 3428, df-oprab 7427 |
| ral | restricted universal quantification |
df-ral 3083 | ∀𝑥 ∈ 𝐴𝜑 | Yes |
ralnex 3094, ralrnmpo 7562 |
| rcl | reverse closure | |
| No | ndmfvrcl 6921, nnarcl 8611 |
| re | real numbers | df-r 11128 |
ℝ | Yes | recn 11208, 0re 11228 |
| rel | relation | df-rel 5673 | Rel 𝐴 |
Yes | brrelex1 5719, relmpoopab 8098 |
| res | restriction | df-res 5678 |
(𝐴 ↾ 𝐵) | Yes |
opelres 5989, f1ores 6842 |
| reu | restricted existential uniqueness |
df-reu 3373 | ∃!𝑥 ∈ 𝐴𝜑 | Yes |
nfreud 3416, reurex 3376 |
| rex | restricted existential quantification |
df-rex 3093 | ∃𝑥 ∈ 𝐴𝜑 | Yes |
rexnal 3120, rexrnmpo 7563 |
| rmo | restricted "at most one" |
df-rmo 3372 | ∃*𝑥 ∈ 𝐴𝜑 | Yes |
nfrmod 3415, nrexrmo 3391 |
| rn | range | df-rn 5677 | ran 𝐴 |
Yes | elrng 5886, rncnvcnv 5929 |
| ring | (unital) ring | df-ring 20348 |
Ring | Yes |
ringidval 20296, isring 20350, ringgrp 20351 |
| rng | non-unital ring | df-rng 20262 |
Rng | Yes |
isrng 20263, rngabl 20264, rnglz 20274 |
| rot | rotation | |
| No | 3anrot 1117, 3orrot 1108 |
| s | eliminates need for syllogism (suffix) |
| | No | ancoms 464 |
| sb | (proper) substitution (of a set) |
df-sb 2100 | [𝑦 / 𝑥]𝜑 | Yes |
spsbe 2119, sbimi 2111 |
| sbc | (proper) substitution of a class |
df-sbc 3748 | [𝐴 / 𝑥]𝜑 | Yes |
sbc2or 3756, sbcth 3762 |
| sca | scalar | df-sca 17351 |
(Scalar‘𝐻) | Yes |
resssca 17421, mgpsca 20253 |
| simp | simple, simplification | |
| No | simpl 488, simp3r3 1302 |
| sn | singleton | df-sn 4595 |
{𝐴} | Yes | eldifsn 4758 |
| sp | specialization | |
| No | spsbe 2119, spei 2429 |
| ss | subset | df-ss 3925 |
𝐴 ⊆ 𝐵 | Yes | difss 4093 |
| struct | structure | df-struct 17232 |
Struct | Yes | brstruct 17233, structfn 17241 |
| sub | subtract | df-sub 11461 |
(𝐴 − 𝐵) | Yes |
subval 11466, subaddi 11563 |
| sup | supremum | df-sup 9412 |
sup(𝐴, 𝐵, < ) | Yes |
fisupcl 9440, supmo 9422 |
| supp | support (of a function) | df-supp 8166 |
(𝐹 supp 𝑍) | Yes |
ressuppfi 9365, mptsuppd 8192 |
| swap | swap (two parts within a theorem) |
| | No | rabswap 3428, 2reuswap 3712 |
| syl | syllogism | syl 18 |
| No | 3syl 19 |
| sym | symmetric | |
| No | df-symdif 4209, cnvsym 6119 |
| symg | symmetric group | df-symg 19471 |
(SymGrp‘𝐴) | Yes |
symghash 19479, pgrpsubgsymg 19510 |
| t |
times (see "mul"), for all-constant theorems |
df-mul 11130 |
(3 · 2) = 6 | Yes |
3t2e6 12424 |
| th, t |
theorem |
|
|
No |
nfth 1834, sbcth 3762, weth 10497, ancomst 470 |
| tp | triple | df-tp 4599 |
{𝐴, 𝐵, 𝐶} | Yes |
eltpi 4659, tpeq1 4713 |
| tr | transitive | |
| No | bitrd 282, biantr 818 |
| tru, t |
true, truth |
df-tru 1573 |
⊤ |
Yes |
bitru 1579, truanfal 1604, biimt 363 |
| un | union | df-un 3913 |
(𝐴 ∪ 𝐵) | Yes |
uneqri 4113, uncom 4115 |
| unit | unit (in a ring) |
df-unit 20473 | (Unit‘𝑅) | Yes |
isunit 20488, nzrunit 20659 |
| v |
setvar (especially for specializations of
theorems when a class is replaced by a setvar variable) |
|
x |
Yes |
cv 1569, vex 3462, velpw 4572, vtoclf 3533 |
| v |
disjoint variable condition used in place of nonfreeness
hypothesis (suffix) |
|
|
No |
spimv 2425 |
| vtx |
vertex |
df-vtx 29385 |
(Vtx‘𝐺) |
Yes |
vtxval0 29426, opvtxov 29392 |
| vv |
two disjoint variable conditions used in place of nonfreeness
hypotheses (suffix) |
|
|
No |
19.23vv 1976 |
| w | weak (version of a theorem) (suffix) | |
| No | ax11w 2168, spnfw 2012 |
| wrd | word |
df-word 14571 | Word 𝑆 | Yes |
iswrdb 14577, wrdfn 14585, ffz0iswrd 14598 |
| xp | cross product (Cartesian product) |
df-xp 5672 | (𝐴 × 𝐵) | Yes |
elxp 5689, opelxpi 5703, xpundi 5735 |
| xr | eXtended reals | df-xr 11265 |
ℝ* | Yes | ressxr 11271, rexr 11273, 0xr 11274 |
| z | integers (from German "Zahlen") |
df-z 12610 | ℤ | Yes |
elz 12611, zcn 12614 |
| zn | ring of integers mod 𝑁 | df-zn 21693 |
(ℤ/nℤ‘𝑁) | Yes |
znval 21722, zncrng 21731, znhash 21745 |
| zring | ring of integers | df-zring 21634 |
ℤring | Yes | zringbas 21640, zringcrng 21635
|
| 0, z |
slashed zero (empty set) | df-nul 4290 |
∅ | Yes |
n0i 4296, vn0 4301; snnz 4747, prnz 4748 |
(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.) |
