| Description:
The following gives conventions used in the Metamath Proof Explorer
(MPE, set.mm) regarding labels.
For other conventions, see conventions 30428 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 3060"rgen.1 $e |- ( x e. A -> ph ) $."
or letters corresponding to the (main) class variable used in the
hypothesis, e.g., for mdet0 22627: "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 2660 and stirling 46044.
- 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 1835, and the restricted quantifier version of Theorem 21 from
Section 19 of [Margaris] p. 90 is labeled r19.21 3251.
- 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... 15913. 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 3965, and thus its syntax label fragment is "dif". Similarly, the
subclass relation 𝐴 ⊆ 𝐵 has syntax label fragment "ss"
because it is defined in df-ss 3979. 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 4145. There are many other syntax label fragments, e.g.,
singleton construct {𝐴} has syntax label fragment "sn" (because it
is defined in df-sn 4631), and the pair construct {𝐴, 𝐵} has
fragment "pr" ( from df-pr 4633). 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 4790. 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 11158) and "re" represents real numbers ℝ (Definition df-r 11162).
The empty set ∅ often uses fragment 0, even though it is defined
in df-nul 4339. The syntax construct (𝐴 + 𝐵) usually uses the
fragment "add" (which is consistent with df-add 11163), 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 12398.
- 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 16182 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 16102) we have value cosval 16155 and
closure coscl 16159.
- 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 30431 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 1936 versus 19.21 2204. This
often permits to prove the result using fewer axioms, and/or to
eliminate a nonfreeness hypothesis (such as Ⅎ𝑥𝜑 in 19.21 2204).
If no constraint is put on axiom use, then the v-version can be proved
from the original theorem using nfv 1911. If two (resp. three) such
disjoint variable conditions are added, then the suffix "vv" (resp.
"vvv") is used, e.g., exlimivv 1929.
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 2573 derived from eu6 2571. 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 5459.
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 2411 (cbval 2400 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 3559.
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 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 3144 |
| abl | Abelian group | df-abl 19815 |
Abel | Yes | ablgrp 19817, zringabl 21479 |
| abs | absorption | | | No |
ressabs 17294 |
| abs | absolute value (of a complex number) |
df-abs 15271 | (abs‘𝐴) | Yes |
absval 15273, absneg 15312, abs1 15332 |
| ad | adding | |
| No | adantr 480, ad2antlr 727 |
| add | add (see "p") | df-add 11163 |
(𝐴 + 𝐵) | Yes |
addcl 11234, addcom 11444, addass 11239 |
| al | "for all" | |
∀𝑥𝜑 | No | alim 1806, alex 1822 |
| ALT | alternative/less preferred (suffix) | |
| No | idALT 23 |
| an | and | df-an 396 |
(𝜑 ∧ 𝜓) | Yes |
anor 984, iman 401, imnan 399 |
| ant | antecedent | |
| No | adantr 480 |
| ass | associative | |
| No | biass 384, orass 921, mulass 11240 |
| asym | asymmetric, antisymmetric | |
| No | intasym 6137, asymref 6138, posasymb 18376 |
| ax | axiom | |
| No | ax6dgen 2125, ax1cn 11186 |
| bas, base |
base (set of an extensible structure) | df-base 17245 |
(Base‘𝑆) | Yes |
baseval 17246, ressbas 17279, cnfldbas 21385 |
| b, bi | biconditional ("iff", "if and only if")
| df-bi 207 | (𝜑 ↔ 𝜓) | Yes |
impbid 212, sspwb 5459 |
| br | binary relation | df-br 5148 |
𝐴𝑅𝐵 | Yes | brab1 5195, brun 5198 |
| c | commutes, commuted (suffix) | | |
No | biimpac 478 |
| c | contraction (suffix) | | |
No | sylc 65, syl2anc 584 |
| cbv | change bound variable | | |
No | cbvalivw 2003, cbvrex 3360 |
| cdm | codomain | |
| No | ffvelcdm 7100, focdmex 7978 |
| cl | closure | | | No |
ifclda 4565, ovrcl 7471, zaddcl 12654 |
| cn | complex numbers | df-c 11158 |
ℂ | Yes | nnsscn 12268, nncn 12271 |
| cnfld | field of complex numbers | df-cnfld 21382 |
ℂfld | Yes | cnfldbas 21385, cnfldinv 21432 |
| cntz | centralizer | df-cntz 19347 |
(Cntz‘𝑀) | Yes |
cntzfval 19350, dprdfcntz 20049 |
| cnv | converse | df-cnv 5696 |
◡𝐴 | Yes | opelcnvg 5893, f1ocnv 6860 |
| co | composition | df-co 5697 |
(𝐴 ∘ 𝐵) | Yes | cnvco 5898, fmptco 7148 |
| com | commutative | |
| No | orcom 870, bicomi 224, eqcomi 2743 |
| con | contradiction, contraposition | |
| No | condan 818, con2d 134 |
| csb | class substitution | df-csb 3908 |
⦋𝐴 / 𝑥⦌𝐵 | Yes |
csbid 3920, csbie2g 3950 |
| cyg | cyclic group | df-cyg 19910 |
CycGrp | Yes |
iscyg 19911, zringcyg 21497 |
| d | deduction form (suffix) | |
| No | idd 24, impbid 212 |
| df | (alternate) definition (prefix) | |
| No | dfrel2 6210, dffn2 6738 |
| di, distr | distributive | |
| No |
andi 1009, imdi 389, ordi 1007, difindi 4297, ndmovdistr 7621 |
| dif | class difference | df-dif 3965 |
(𝐴 ∖ 𝐵) | Yes |
difss 4145, difindi 4297 |
| div | division | df-div 11918 |
(𝐴 / 𝐵) | Yes |
divcl 11925, divval 11921, divmul 11922 |
| dm | domain | df-dm 5698 |
dom 𝐴 | Yes | dmmpt 6261, iswrddm0 14572 |
| e, eq, equ | equals (equ for setvars, eq for
classes) | df-cleq 2726 |
𝐴 = 𝐵 | Yes |
2p2e4 12398, uneqri 4165, equtr 2017 |
| edg | edge | df-edg 29079 |
(Edg‘𝐺) | Yes |
edgopval 29082, usgredgppr 29227 |
| el | element of | |
𝐴 ∈ 𝐵 | Yes |
eldif 3972, eldifsn 4790, elssuni 4941 |
| en | equinumerous | df-en |
𝐴 ≈ 𝐵 | Yes | domen 9000, enfi 9224 |
| eu | "there exists exactly one" | eu6 2571 |
∃!𝑥𝜑 | Yes | euex 2574, euabsn 4730 |
| ex | exists (i.e. is a set) | |
∈ V | No | brrelex1 5741, 0ex 5312 |
| ex, e | "there exists (at least one)" |
df-ex 1776 |
∃𝑥𝜑 | Yes | exim 1830, alex 1822 |
| exp | export | |
| No | expt 177, expcom 413 |
| f | "not free in" (suffix) | |
| No | equs45f 2461, sbf 2268 |
| f | function | df-f 6566 |
𝐹:𝐴⟶𝐵 | Yes | fssxp 6763, opelf 6769 |
| fal | false | df-fal 1549 |
⊥ | Yes | bifal 1552, falantru 1571 |
| fi | finite intersection | df-fi 9448 |
(fi‘𝐵) | Yes | fival 9449, inelfi 9455 |
| fi, fin | finite | df-fin 8987 |
Fin | Yes |
isfi 9014, snfi 9081, onfin 9264 |
| fld | field (Note: there is an alternative
definition Fld of a field, see df-fld 37978) | df-field 20748 |
Field | Yes | isfld 20756, fldidom 20787 |
| fn | function with domain | df-fn 6565 |
𝐴 Fn 𝐵 | Yes | ffn 6736, fndm 6671 |
| frgp | free group | df-frgp 19742 |
(freeGrp‘𝐼) | Yes |
frgpval 19790, frgpadd 19795 |
| fsupp | finitely supported function |
df-fsupp 9399 | 𝑅 finSupp 𝑍 | Yes |
isfsupp 9402, fdmfisuppfi 9411, fsuppco 9439 |
| fun | function | df-fun 6564 |
Fun 𝐹 | Yes | funrel 6584, ffun 6739 |
| fv | function value | df-fv 6570 |
(𝐹‘𝐴) | Yes | fvres 6925, swrdfv 14682 |
| fz | finite set of sequential integers |
df-fz 13544 |
(𝑀...𝑁) | Yes | fzval 13545, eluzfz 13555 |
| fz0 | finite set of sequential nonnegative integers |
|
(0...𝑁) | Yes | nn0fz0 13661, fz0tp 13664 |
| fzo | half-open integer range | df-fzo 13691 |
(𝑀..^𝑁) | Yes |
elfzo 13697, elfzofz 13711 |
| g | more general (suffix); eliminates "is a set"
hypotheses | |
| No | uniexg 7758 |
| gr | graph | |
| No | uhgrf 29093, isumgr 29126, usgrres1 29346 |
| grp | group | df-grp 18966 |
Grp | Yes | isgrp 18969, tgpgrp 24101 |
| gsum | group sum | df-gsum 17488 |
(𝐺 Σg 𝐹) | Yes |
gsumval 18702, gsumwrev 19399 |
| hash | size (of a set) | df-hash 14366 |
(♯‘𝐴) | Yes |
hashgval 14368, hashfz1 14381, hashcl 14391 |
| hb | hypothesis builder (prefix) | |
| No | hbxfrbi 1821, hbald 2165, hbequid 38890 |
| hm | (monoid, group, ring, ...) homomorphism |
| | No |
ismhm 18810, isghm 19245, isrhm 20494 |
| i | inference (suffix) | |
| No | eleq1i 2829, tcsni 9780 |
| i | implication (suffix) | |
| No | brwdomi 9605, infeq5i 9673 |
| id | identity | |
| No | biid 261 |
| iedg | indexed edge | df-iedg 29030 |
(iEdg‘𝐺) | Yes |
iedgval0 29071, edgiedgb 29085 |
| idm | idempotent | |
| No | anidm 564, tpidm13 4760 |
| im, imp | implication (label often omitted) |
df-im 15136 | (𝐴 → 𝐵) | Yes |
iman 401, imnan 399, impbidd 210 |
| im | (group, ring, ...) isomorphism | |
| No | isgim 19292, rimrcl 20498 |
| ima | image | df-ima 5701 |
(𝐴 “ 𝐵) | Yes | resima 6034, imaundi 6171 |
| imp | import | |
| No | biimpa 476, impcom 407 |
| in | intersection | df-in 3969 |
(𝐴 ∩ 𝐵) | Yes | elin 3978, incom 4216 |
| inf | infimum | df-inf 9480 |
inf(ℝ+, ℝ*, < ) | Yes |
fiinfcl 9538, infiso 9545 |
| is... | is (something a) ...? | |
| No | isring 20254 |
| j | joining, disjoining | |
| No | jc 161, jaoi 857 |
| l | left | |
| No | olcd 874, simpl 482 |
| map | mapping operation or set exponentiation |
df-map 8866 | (𝐴 ↑m 𝐵) | Yes |
mapvalg 8874, elmapex 8886 |
| mat | matrix | df-mat 22427 |
(𝑁 Mat 𝑅) | Yes |
matval 22430, matring 22464 |
| mdet | determinant (of a square matrix) |
df-mdet 22606 | (𝑁 maDet 𝑅) | Yes |
mdetleib 22608, mdetrlin 22623 |
| mgm | magma | df-mgm 18665 |
Magma | Yes |
mgmidmo 18685, mgmlrid 18692, ismgm 18666 |
| mgp | multiplicative group | df-mgp 20152 |
(mulGrp‘𝑅) | Yes |
mgpress 20166, ringmgp 20256 |
| mnd | monoid | df-mnd 18760 |
Mnd | Yes | mndass 18768, mndodcong 19574 |
| mo | "there exists at most one" | df-mo 2537 |
∃*𝑥𝜑 | Yes | eumo 2575, moim 2541 |
| mp | modus ponens | ax-mp 5 |
| No | mpd 15, mpi 20 |
| mpo | maps-to notation for an operation |
df-mpo 7435 | (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) | Yes |
mpompt 7546, resmpo 7552 |
| mpt | modus ponendo tollens | |
| No | mptnan 1764, mptxor 1765 |
| mpt | maps-to notation for a function |
df-mpt 5231 | (𝑥 ∈ 𝐴 ↦ 𝐵) | Yes |
fconstmpt 5750, resmpt 6056 |
| mul | multiplication (see "t") | df-mul 11164 |
(𝐴 · 𝐵) | Yes |
mulcl 11236, divmul 11922, mulcom 11238, mulass 11240 |
| n, not | not | |
¬ 𝜑 | Yes |
nan 830, notnotr 130 |
| ne | not equal | df-ne | 𝐴 ≠ 𝐵 |
Yes | exmidne 2947, neeqtrd 3007 |
| nel | not element of | df-nel | 𝐴 ∉ 𝐵
|
Yes | neli 3045, nnel 3053 |
| ne0 | not equal to zero (see n0) | |
≠ 0 | No |
negne0d 11615, ine0 11695, gt0ne0 11725 |
| nf | "not free in" (prefix) | df-nf 1780 |
Ⅎ𝑥𝜑 | Yes | nfnd 1855 |
| ngp | normed group | df-ngp 24611 |
NrmGrp | Yes | isngp 24624, ngptps 24630 |
| nm | norm (on a group or ring) | df-nm 24610 |
(norm‘𝑊) | Yes |
nmval 24617, subgnm 24661 |
| nn | positive integers | df-nn 12264 |
ℕ | Yes | nnsscn 12268, nncn 12271 |
| nn0 | nonnegative integers | df-n0 12524 |
ℕ0 | Yes | nnnn0 12530, nn0cn 12533 |
| n0 | not the empty set (see ne0) | |
≠ ∅ | No | n0i 4345, vn0 4350, ssn0 4409 |
| OLD | old, obsolete (to be removed soon) | |
| No | 19.43OLD 1880 |
| on | ordinal number | df-on 6389 |
𝐴 ∈ On | Yes |
elon 6394, 1on 8516 onelon 6410 |
| op | ordered pair | df-op 4637 |
⟨𝐴, 𝐵⟩ | Yes | dfopif 4874, opth 5486 |
| or | or | df-or 848 |
(𝜑 ∨ 𝜓) | Yes |
orcom 870, anor 984 |
| ot | ordered triple | df-ot 4639 |
⟨𝐴, 𝐵, 𝐶⟩ | Yes |
euotd 5522, fnotovb 7482 |
| ov | operation value | df-ov 7433 |
(𝐴𝐹𝐵) | Yes
| fnotovb 7482, fnovrn 7607 |
| p | plus (see "add"), for all-constant
theorems | df-add 11163 |
(3 + 2) = 5 | Yes |
3p2e5 12414 |
| pfx | prefix | df-pfx 14705 |
(𝑊 prefix 𝐿) | Yes |
pfxlen 14717, ccatpfx 14735 |
| pm | Principia Mathematica | |
| No | pm2.27 42 |
| pm | partial mapping (operation) | df-pm 8867 |
(𝐴 ↑pm 𝐵) | Yes | elpmi 8884, pmsspw 8915 |
| pr | pair | df-pr 4633 |
{𝐴, 𝐵} | Yes |
elpr 4654, prcom 4736, prid1g 4764, prnz 4781 |
| prm, prime | prime (number) | df-prm 16705 |
ℙ | Yes | 1nprm 16712, dvdsprime 16720 |
| pss | proper subset | df-pss 3982 |
𝐴 ⊊ 𝐵 | Yes | pssss 4107, sspsstri 4114 |
| q | rational numbers ("quotients") | df-q 12988 |
ℚ | Yes | elq 12989 |
| r | reversed (suffix) | |
| No | pm4.71r 558, caovdir 7666 |
| r | right | |
| No | orcd 873, simprl 771 |
| rab | restricted class abstraction |
df-rab 3433 | {𝑥 ∈ 𝐴 ∣ 𝜑} | Yes |
rabswap 3442, df-oprab 7434 |
| ral | restricted universal quantification |
df-ral 3059 | ∀𝑥 ∈ 𝐴𝜑 | Yes |
ralnex 3069, ralrnmpo 7571 |
| rcl | reverse closure | |
| No | ndmfvrcl 6942, nnarcl 8652 |
| re | real numbers | df-r 11162 |
ℝ | Yes | recn 11242, 0re 11260 |
| rel | relation | df-rel 5695 | Rel 𝐴 |
Yes | brrelex1 5741, relmpoopab 8117 |
| res | restriction | df-res 5700 |
(𝐴 ↾ 𝐵) | Yes |
opelres 6005, f1ores 6862 |
| reu | restricted existential uniqueness |
df-reu 3378 | ∃!𝑥 ∈ 𝐴𝜑 | Yes |
nfreud 3429, reurex 3381 |
| rex | restricted existential quantification |
df-rex 3068 | ∃𝑥 ∈ 𝐴𝜑 | Yes |
rexnal 3097, rexrnmpo 7572 |
| rmo | restricted "at most one" |
df-rmo 3377 | ∃*𝑥 ∈ 𝐴𝜑 | Yes |
nfrmod 3428, nrexrmo 3398 |
| rn | range | df-rn 5699 | ran 𝐴 |
Yes | elrng 5904, rncnvcnv 5947 |
| ring | (unital) ring | df-ring 20252 |
Ring | Yes |
ringidval 20200, isring 20254, ringgrp 20255 |
| rng | non-unital ring | df-rng 20170 |
Rng | Yes |
isrng 20171, rngabl 20172, rnglz 20182 |
| rot | rotation | |
| No | 3anrot 1099, 3orrot 1091 |
| s | eliminates need for syllogism (suffix) |
| | No | ancoms 458 |
| sb | (proper) substitution (of a set) |
df-sb 2062 | [𝑦 / 𝑥]𝜑 | Yes |
spsbe 2079, sbimi 2071 |
| sbc | (proper) substitution of a class |
df-sbc 3791 | [𝐴 / 𝑥]𝜑 | Yes |
sbc2or 3799, sbcth 3805 |
| sca | scalar | df-sca 17313 |
(Scalar‘𝐻) | Yes |
resssca 17388, mgpsca 20159 |
| simp | simple, simplification | |
| No | simpl 482, simp3r3 1282 |
| sn | singleton | df-sn 4631 |
{𝐴} | Yes | eldifsn 4790 |
| sp | specialization | |
| No | spsbe 2079, spei 2396 |
| ss | subset | df-ss 3979 |
𝐴 ⊆ 𝐵 | Yes | difss 4145 |
| struct | structure | df-struct 17180 |
Struct | Yes | brstruct 17181, structfn 17189 |
| sub | subtract | df-sub 11491 |
(𝐴 − 𝐵) | Yes |
subval 11496, subaddi 11593 |
| sup | supremum | df-sup 9479 |
sup(𝐴, 𝐵, < ) | Yes |
fisupcl 9506, supmo 9489 |
| supp | support (of a function) | df-supp 8184 |
(𝐹 supp 𝑍) | Yes |
ressuppfi 9432, mptsuppd 8210 |
| swap | swap (two parts within a theorem) |
| | No | rabswap 3442, 2reuswap 3754 |
| syl | syllogism | syl 17 |
| No | 3syl 18 |
| sym | symmetric | |
| No | df-symdif 4258, cnvsym 6134 |
| symg | symmetric group | df-symg 19401 |
(SymGrp‘𝐴) | Yes |
symghash 19409, pgrpsubgsymg 19441 |
| t |
times (see "mul"), for all-constant theorems |
df-mul 11164 |
(3 · 2) = 6 | Yes |
3t2e6 12429 |
| th, t |
theorem |
|
|
No |
nfth 1797, sbcth 3805, weth 10532, ancomst 464 |
| tp | triple | df-tp 4635 |
{𝐴, 𝐵, 𝐶} | Yes |
eltpi 4692, tpeq1 4746 |
| tr | transitive | |
| No | bitrd 279, biantr 806 |
| tru, t |
true, truth |
df-tru 1539 |
⊤ |
Yes |
bitru 1545, truanfal 1570, biimt 360 |
| un | union | df-un 3967 |
(𝐴 ∪ 𝐵) | Yes |
uneqri 4165, uncom 4167 |
| unit | unit (in a ring) |
df-unit 20374 | (Unit‘𝑅) | Yes |
isunit 20389, nzrunit 20540 |
| v |
setvar (especially for specializations of
theorems when a class is replaced by a setvar variable) |
|
x |
Yes |
cv 1535, vex 3481, velpw 4609, vtoclf 3563 |
| v |
disjoint variable condition used in place of nonfreeness
hypothesis (suffix) |
|
|
No |
spimv 2392 |
| vtx |
vertex |
df-vtx 29029 |
(Vtx‘𝐺) |
Yes |
vtxval0 29070, opvtxov 29036 |
| vv |
two disjoint variable conditions used in place of nonfreeness
hypotheses (suffix) |
|
|
No |
19.23vv 1940 |
| w | weak (version of a theorem) (suffix) | |
| No | ax11w 2127, spnfw 1976 |
| wrd | word |
df-word 14549 | Word 𝑆 | Yes |
iswrdb 14554, wrdfn 14562, ffz0iswrd 14575 |
| xp | cross product (Cartesian product) |
df-xp 5694 | (𝐴 × 𝐵) | Yes |
elxp 5711, opelxpi 5725, xpundi 5756 |
| xr | eXtended reals | df-xr 11296 |
ℝ* | Yes | ressxr 11302, rexr 11304, 0xr 11305 |
| z | integers (from German "Zahlen") |
df-z 12611 | ℤ | Yes |
elz 12612, zcn 12615 |
| zn | ring of integers mod 𝑁 | df-zn 21534 |
(ℤ/nℤ‘𝑁) | Yes |
znval 21567, zncrng 21580, znhash 21594 |
| zring | ring of integers | df-zring 21475 |
ℤring | Yes | zringbas 21481, zringcrng 21476
|
| 0, z |
slashed zero (empty set) | df-nul 4339 |
∅ | Yes |
n0i 4345, vn0 4350; snnz 4780, prnz 4781 |
(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.) |
