| Description:
The following gives conventions used in the Metamath Proof Explorer
(MPE, set.mm) regarding labels.
For other conventions, see conventions 30983 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 3079"rgen.1 $e |- ( x e. A -> ph ) $."
or letters corresponding to the (main) class variable used in the
hypothesis, e.g., for mdet0 22901: "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 2688 and stirling 47043.
- 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 3258.
- 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... 16030. 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 3902, and thus its syntax label fragment is "dif". Similarly, the
subclass relation 𝐴 ⊆ 𝐵 has syntax label fragment "ss"
because it is defined in df-ss 3916. 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 4083. There are many other syntax label fragments, e.g.,
singleton construct {𝐴} has syntax label fragment "sn" (because it
is defined in df-sn 4585), and the pair construct {𝐴, 𝐵} has
fragment "pr" ( from df-pr 4587). 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 4748. 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 11187) and "re" represents real numbers ℝ (Definition df-r 11191).
The empty set ∅ often uses fragment 0, even though it is defined
in df-nul 4280. The syntax construct (𝐴 + 𝐵) usually uses the
fragment "add" (which is consistent with df-add 11192), 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 12458.
- 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 16298 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 16216) we have value cosval 16271 and
closure coscl 16275.
- 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 30986 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 2244. This
often permits to prove the result using fewer axioms, and/or to
eliminate a nonfreeness hypothesis (such as Ⅎ𝑥𝜑 in 19.21 2244).
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 2602 derived from eu6 2600. 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 5417.
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 2439 (cbval 2428 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 3522.
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 3156 |
| abl | Abelian group | df-abl 19977 |
Abel | Yes | ablgrp 19979, zringabl 21737 |
| abs | absorption | | | No |
ressabs 17406 |
| abs | absolute value (of a complex number) |
df-abs 15383 | (abs‘𝐴) | Yes |
absval 15385, absneg 15424, abs1 15444 |
| ad | adding | |
| No | adantr 486, ad2antlr 740 |
| add | add (see "p") | df-add 11192 |
(𝐴 + 𝐵) | Yes |
addcl 11263, addcom 11477, addass 11268 |
| 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 11269 |
| asym | asymmetric, antisymmetric | |
| No | intasym 6107, asymref 6108, posasymb 18473 |
| ax | axiom | |
| No | ax6dgen 2165, ax1cn 11215 |
| bas, base |
base (set of an extensible structure) | df-base 17368 |
(Base‘𝑆) | Yes |
baseval 17369, ressbas 17394, cnfldbas 21662 |
| b, bi | biconditional ("iff", "if and only if")
| df-bi 210 | (𝜑 ↔ 𝜓) | Yes |
impbid 215, sspwb 5417 |
| br | binary relation | df-br 5104 |
𝐴𝑅𝐵 | Yes | brab1 5153, brun 5156 |
| c | commutes, commuted (suffix) | | |
No | biimpac 484 |
| c | contraction (suffix) | | |
No | sylc 66, syl2anc 596 |
| cbv | change bound variable | | |
No | cbvalivw 2040, cbvrex 3349 |
| cdm | codomain | |
| No | ffvelcdm 7073, focdmex 7957 |
| cl | closure | | | No |
ifclda 4518, ovrcl 7453, zaddcl 12717 |
| cn | complex numbers | df-c 11187 |
ℂ | Yes | nnsscn 12321, nncn 12324 |
| cnfld | field of complex numbers | df-cnfld 21659 |
ℂfld | Yes | cnfldbas 21662, cnfldinv 21689 |
| cntz | centralizer | df-cntz 19511 |
(Cntz‘𝑀) | Yes |
cntzfval 19514, dprdfcntz 20211 |
| cnv | converse | df-cnv 5659 |
◡𝐴 | Yes | opelcnvg 5858, f1ocnv 6829 |
| co | composition | df-co 5660 |
(𝐴 ∘ 𝐵) | Yes | cnvco 5867, fmptco 7122 |
| com | commutative | |
| No | orcom 884, bicomi 227, eqcomi 2770 |
| con | contradiction, contraposition | |
| No | condan 830, con2d 135 |
| csb | class substitution | df-csb 3848 |
⦋𝐴 / 𝑥⦌𝐵 | Yes |
csbid 3860, csbie2g 3887 |
| cyg | cyclic group | df-cyg 20072 |
CycGrp | Yes |
iscyg 20073, zringcyg 21755 |
| d | deduction form (suffix) | |
| No | idd 25, impbid 215 |
| df | (alternate) definition (prefix) | |
| No | dfrel2 6180, dffn2 6703 |
| di, distr | distributive | |
| No |
andi 1025, imdi 394, ordi 1023, difindi 4238, ndmovdistr 7602 |
| dif | class difference | df-dif 3902 |
(𝐴 ∖ 𝐵) | Yes |
difss 4083, difindi 4238 |
| div | division | df-div 11955 |
(𝐴 / 𝐵) | Yes |
divcl 11961, divval 11957, divmul 11958 |
| dm | domain | df-dm 5661 |
dom 𝐴 | Yes | dmmpt 6234, iswrddm0 14663 |
| e, eq, equ | equals (equ for setvars, eq for
classes) | df-cleq 2753 |
𝐴 = 𝐵 | Yes |
2p2e4 12458, uneqri 4103, equtr 2054 |
| edg | edge | df-edg 29608 |
(Edg‘𝐺) | Yes |
edgopval 29611, usgredgppr 29759 |
| el | element of | |
𝐴 ∈ 𝐵 | Yes |
eldif 3909, eldifsn 4748, elssuni 4899 |
| en | equinumerous | df-en |
𝐴 ≈ 𝐵 | Yes | domen 8972, enfi 9186 |
| eu | "there exists exactly one" | eu6 2600 |
∃!𝑥𝜑 | Yes | euex 2603, euabsn 4687 |
| ex | exists (i.e. is a set) | |
∈ V | No | brrelex1 5704, 0ex 5261 |
| 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 2489, sbf 2305 |
| f | function | df-f 6535 |
𝐹:𝐴⟶𝐵 | Yes | fssxp 6729, opelf 6735 |
| fal | false | df-fal 1583 |
⊥ | Yes | bifal 1586, falantru 1605 |
| fi | finite intersection | df-fi 9387 |
(fi‘𝐵) | Yes | fival 9388, inelfi 9394 |
| fi, fin | finite | df-fin 8961 |
Fin | Yes |
isfi 8986, snfi 9055, onfin 9214 |
| fld | field (Note: there is an alternative
definition Fld of a field, see df-fld 38894) | df-field 20963 |
Field | Yes | isfld 20973, fldidom 21009 |
| fn | function with domain | df-fn 6534 |
𝐴 Fn 𝐵 | Yes | ffn 6701, fndm 6634 |
| frgp | free group | df-frgp 19904 |
(freeGrp‘𝐼) | Yes |
frgpval 19952, frgpadd 19957 |
| fsupp | finitely supported function |
df-fsupp 9338 | 𝑅 finSupp 𝑍 | Yes |
isfsupp 9341, fdmfisuppfi 9350, fsuppco 9378 |
| fun | function | df-fun 6533 |
Fun 𝐹 | Yes | funrel 6548, ffun 6704 |
| fv | function value | df-fv 6539 |
(𝐹‘𝐴) | Yes | fvres 6896, swrdfv 14776 |
| fz | finite set of sequential integers |
df-fz 13621 |
(𝑀...𝑁) | Yes | fzval 13622, eluzfz 13632 |
| fz0 | finite set of sequential nonnegative integers |
|
(0...𝑁) | Yes | nn0fz0 13739, fz0tp 13742 |
| fzo | half-open integer range | df-fzo 13769 |
(𝑀..^𝑁) | Yes |
elfzo 13775, elfzofz 13790 |
| g | more general (suffix); eliminates "is a set"
hypotheses | |
| No | uniexg 7746 |
| gr | graph | |
| No | uhgrf 29622, isumgr 29655, usgrres1 29878 |
| grp | group | df-grp 19127 |
Grp | Yes | isgrp 19130, tgpgrp 24377 |
| gsum | group sum | df-gsum 17593 |
(𝐺 Σg 𝐹) | Yes |
gsumval 18846, gsumwrev 19560 |
| hash | size (of a set) | df-hash 14455 |
(♯‘𝐴) | Yes |
hashgval 14457, hashfz1 14470, hashcl 14480 |
| hb | hypothesis builder (prefix) | |
| No | hbxfrbi 1858, hbald 2205, hbequid 39934 |
| hm | (monoid, group, ring, ...) homomorphism |
| | No |
ismhm 18960, isghm 19410, isrhm 20689 |
| i | inference (suffix) | |
| No | eleq1i 2852, tcsni 9726 |
| i | implication (suffix) | |
| No | brwdomi 9546, infeq5i 9621 |
| id | identity | |
| No | biid 264 |
| iedg | indexed edge | df-iedg 29559 |
(iEdg‘𝐺) | Yes |
iedgval0 29600, edgiedgb 29614 |
| idm | idempotent | |
| No | anidm 575, tpidm13 4717 |
| im, imp | implication (label often omitted) |
df-im 15248 | (𝐴 → 𝐵) | Yes |
iman 407, imnan 405, impbidd 213 |
| im | (group, ring, ...) isomorphism | |
| No | isgim 19456, rimrcl 20692 |
| ima | image | df-ima 5664 |
(𝐴 “ 𝐵) | Yes | resima 6006, imaundi 6139 |
| imp | import | |
| No | biimpa 482, impcom 413 |
| in | intersection | df-in 3906 |
(𝐴 ∩ 𝐵) | Yes | elin 3915, incom 4155 |
| inf | infimum | df-inf 9419 |
inf(ℝ+, ℝ*, < ) | Yes |
fiinfcl 9479, infiso 9486 |
| is... | is (something a) ...? | |
| No | isring 20443 |
| j | joining, disjoining | |
| No | jc 162, jaoi 871 |
| l | left | |
| No | olcd 888, simpl 488 |
| map | mapping operation or set exponentiation |
df-map 8833 | (𝐴 ↑m 𝐵) | Yes |
mapvalg 8840, elmapex 8852 |
| mat | matrix | df-mat 22703 |
(𝑁 Mat 𝑅) | Yes |
matval 22706, matring 22738 |
| mdet | determinant (of a square matrix) |
df-mdet 22880 | (𝑁 maDet 𝑅) | Yes |
mdetleib 22882, mdetrlin 22897 |
| mgm | magma | df-mgm 18796 |
Magma | Yes |
mgmidmo 18818, mgmlrid 18827, ismgm 18797 |
| mgp | multiplicative group | df-mgp 20341 |
(mulGrp‘𝑅) | Yes |
mgpress 20350, ringmgp 20445 |
| mnd | monoid | df-mnd 18904 |
Mnd | Yes | mndass 18912, mndodcong 19736 |
| mo | "there exists at most one" | df-mo 2565 |
∃*𝑥𝜑 | Yes | eumo 2604, moim 2570 |
| mp | modus ponens | ax-mp 5 |
| No | mpd 16, mpi 21 |
| mpo | maps-to notation for an operation |
df-mpo 7417 | (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) | Yes |
mpompt 7526, resmpo 7532 |
| mpt | modus ponendo tollens | |
| No | mptnan 1801, mptxor 1802 |
| mpt | maps-to notation for a function |
df-mpt 5187 | (𝑥 ∈ 𝐴 ↦ 𝐵) | Yes |
fconstmpt 5713, resmpt 6031 |
| mul | multiplication (see "t") | df-mul 11193 |
(𝐴 · 𝐵) | Yes |
mulcl 11265, divmul 11958, mulcom 11267, mulass 11269 |
| n, not | not | |
¬ 𝜑 | Yes |
nan 843, notnotr 131 |
| ne | not equal | df-ne | 𝐴 ≠ 𝐵 |
Yes | exmidne 2966, neeqtrd 3025 |
| nel | not element of | df-nel | 𝐴 ∉ 𝐵
|
Yes | neli 3064, nnel 3072 |
| ne0 | not equal to zero (see n0) | |
≠ 0 | No |
negne0d 11648, ine0 11732, gt0ne0 11762 |
| nf | "not free in" (prefix) | df-nf 1817 |
Ⅎ𝑥𝜑 | Yes | nfnd 1891 |
| ngp | normed group | df-ngp 24882 |
NrmGrp | Yes | isngp 24895, ngptps 24901 |
| nm | norm (on a group or ring) | df-nm 24881 |
(norm‘𝑊) | Yes |
nmval 24888, subgnm 24932 |
| nn | positive integers | df-nn 12317 |
ℕ | Yes | nnsscn 12321, nncn 12324 |
| nn0 | nonnegative integers | df-n0 12588 |
ℕ0 | Yes | nnnn0 12594, nn0cn 12597 |
| n0 | not the empty set (see ne0) | |
≠ ∅ | No | n0i 4286, vn0 4291, ssn0 4355 |
| OLD | old, obsolete (to be removed soon) | |
| No | 19.43OLD 1916 |
| on | ordinal number | df-on 6359 |
𝐴 ∈ On | Yes |
elon 6364, 1on 8473 onelon 6380 |
| op | ordered pair | df-op 4591 |
⟨𝐴, 𝐵⟩ | Yes | dfopif 4830, opth 5445 |
| or | or | df-or 862 |
(𝜑 ∨ 𝜓) | Yes |
orcom 884, anor 998 |
| ot | ordered triple | df-ot 4593 |
⟨𝐴, 𝐵, 𝐶⟩ | Yes |
euotd 5486, fnotovb 7464 |
| ov | operation value | df-ov 7415 |
(𝐴𝐹𝐵) | Yes
| fnotovb 7464, fnovrn 7588 |
| p | plus (see "add"), for all-constant
theorems | df-add 11192 |
(3 + 2) = 5 | Yes |
3p2e5 12474 |
| pfx | prefix | df-pfx 14801 |
(𝑊 prefix 𝐿) | Yes |
pfxlen 14813, ccatpfx 14830 |
| pm | Principia Mathematica | |
| No | pm2.27 43 |
| pm | partial mapping (operation) | df-pm 8834 |
(𝐴 ↑pm 𝐵) | Yes | elpmi 8850, pmsspw 8889 |
| pr | pair | df-pr 4587 |
{𝐴, 𝐵} | Yes |
elpr 4609, prcom 4693, prid1g 4721, prnz 4738 |
| prm, prime | prime (number) | df-prm 16827 |
ℙ | Yes | 1nprm 16834, dvdsprime 16842 |
| pss | proper subset | df-pss 3919 |
𝐴 ⊊ 𝐵 | Yes | pssss 4046, sspsstri 4054 |
| q | rational numbers ("quotients") | df-q 13057 |
ℚ | Yes | elq 13058 |
| r | reversed (suffix) | |
| No | pm4.71r 568, caovdir 7647 |
| r | right | |
| No | orcd 887, simprl 783 |
| rab | restricted class abstraction |
df-rab 3414 | {𝑥 ∈ 𝐴 ∣ 𝜑} | Yes |
rabswap 3422, df-oprab 7416 |
| ral | restricted universal quantification |
df-ral 3078 | ∀𝑥 ∈ 𝐴𝜑 | Yes |
ralnex 3089, ralrnmpo 7551 |
| rcl | reverse closure | |
| No | ndmfvrcl 6910, nnarcl 8609 |
| re | real numbers | df-r 11191 |
ℝ | Yes | recn 11271, 0re 11291 |
| rel | relation | df-rel 5658 | Rel 𝐴 |
Yes | brrelex1 5704, relmpoopab 8094 |
| res | restriction | df-res 5663 |
(𝐴 ↾ 𝐵) | Yes |
opelres 5976, f1ores 6831 |
| reu | restricted existential uniqueness |
df-reu 3367 | ∃!𝑥 ∈ 𝐴𝜑 | Yes |
nfreud 3410, reurex 3370 |
| rex | restricted existential quantification |
df-rex 3088 | ∃𝑥 ∈ 𝐴𝜑 | Yes |
rexnal 3115, rexrnmpo 7552 |
| rmo | restricted "at most one" |
df-rmo 3366 | ∃*𝑥 ∈ 𝐴𝜑 | Yes |
nfrmod 3409, nrexrmo 3385 |
| rn | range | df-rn 5662 | ran 𝐴 |
Yes | elrng 5873, rncnvcnv 5916 |
| ring | (unital) ring | df-ring 20441 |
Ring | Yes |
ringidval 20389, isring 20443, ringgrp 20444 |
| rng | non-unital ring | df-rng 20355 |
Rng | Yes |
isrng 20356, rngabl 20357, rnglz 20367 |
| 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 3740 | [𝐴 / 𝑥]𝜑 | Yes |
sbc2or 3748, sbcth 3754 |
| sca | scalar | df-sca 17424 |
(Scalar‘𝐻) | Yes |
resssca 17494, mgpsca 20346 |
| simp | simple, simplification | |
| No | simpl 488, simp3r3 1302 |
| sn | singleton | df-sn 4585 |
{𝐴} | Yes | eldifsn 4748 |
| sp | specialization | |
| No | spsbe 2119, spei 2424 |
| ss | subset | df-ss 3916 |
𝐴 ⊆ 𝐵 | Yes | difss 4083 |
| struct | structure | df-struct 17305 |
Struct | Yes | brstruct 17306, structfn 17314 |
| sub | subtract | df-sub 11524 |
(𝐴 − 𝐵) | Yes |
subval 11529, subaddi 11626 |
| sup | supremum | df-sup 9418 |
sup(𝐴, 𝐵, < ) | Yes |
fisupcl 9446, supmo 9428 |
| supp | support (of a function) | df-supp 8162 |
(𝐹 supp 𝑍) | Yes |
ressuppfi 9371, mptsuppd 8188 |
| swap | swap (two parts within a theorem) |
| | No | rabswap 3422, 2reuswap 3704 |
| syl | syllogism | syl 18 |
| No | 3syl 19 |
| sym | symmetric | |
| No | df-symdif 4199, cnvsym 6106 |
| symg | symmetric group | df-symg 19564 |
(SymGrp‘𝐴) | Yes |
symghash 19572, pgrpsubgsymg 19603 |
| t |
times (see "mul"), for all-constant theorems |
df-mul 11193 |
(3 · 2) = 6 | Yes |
3t2e6 12489 |
| th, t |
theorem |
|
|
No |
nfth 1834, sbcth 3754, weth 10554, ancomst 470 |
| tp | triple | df-tp 4589 |
{𝐴, 𝐵, 𝐶} | Yes |
eltpi 4649, tpeq1 4703 |
| 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 3904 |
(𝐴 ∪ 𝐵) | Yes |
uneqri 4103, uncom 4105 |
| unit | unit (in a ring) |
df-unit 20568 | (Unit‘𝑅) | Yes |
isunit 20583, nzrunit 20755 |
| v |
setvar (especially for specializations of
theorems when a class is replaced by a setvar variable) |
|
x |
Yes |
cv 1569, vex 3455, velpw 4562, vtoclf 3526 |
| v |
disjoint variable condition used in place of nonfreeness
hypothesis (suffix) |
|
|
No |
spimv 2420 |
| vtx |
vertex |
df-vtx 29558 |
(Vtx‘𝐺) |
Yes |
vtxval0 29599, opvtxov 29565 |
| 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 2167, spnfw 2012 |
| wrd | word |
df-word 14639 | Word 𝑆 | Yes |
iswrdb 14645, wrdfn 14653, ffz0iswrd 14666 |
| xp | cross product (Cartesian product) |
df-xp 5657 | (𝐴 × 𝐵) | Yes |
elxp 5674, opelxpi 5688, xpundi 5720 |
| xr | eXtended reals | df-xr 11328 |
ℝ* | Yes | ressxr 11334, rexr 11336, 0xr 11337 |
| z | integers (from German "Zahlen") |
df-z 12675 | ℤ | Yes |
elz 12676, zcn 12679 |
| zn | ring of integers mod 𝑁 | df-zn 21792 |
(ℤ/nℤ‘𝑁) | Yes |
znval 21821, zncrng 21830, znhash 21844 |
| zring | ring of integers | df-zring 21733 |
ℤring | Yes | zringbas 21739, zringcrng 21734
|
| 0, z |
slashed zero (empty set) | df-nul 4280 |
∅ | Yes |
n0i 4286, vn0 4291; snnz 4737, prnz 4738 |
(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.) |
