| Description:
The following gives conventions used in the Metamath Proof Explorer
(MPE, set.mm) regarding labels.
For other conventions, see conventions 31007 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 3078"rgen.1 $e |- ( x e. A -> ph ) $."
or letters corresponding to the (main) class variable used in the
hypothesis, e.g., for mdet0 22927: "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 2687 and stirling 47193.
- 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 1871, and the restricted quantifier version of Theorem 21 from
Section 19 of [Margaris] p. 90 is labeled r19.21 3257.
- 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... 16056. 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 4047, and thus its syntax label fragment is "dif". Similarly, the
subclass relation 𝐴 ⊆ 𝐵 has syntax label fragment "ss"
because it is defined in df-ss 3896. 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 4072. 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 4744. 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 11210) and "re" represents real numbers ℝ (Definition df-r 11214).
The empty set ∅ often uses fragment 0, even though it is defined
in df-nul 4279. The syntax construct (𝐴 + 𝐵) usually uses the
fragment "add" (which is consistent with df-add 11215), 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 12481.
- 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 16324 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 16242) we have value cosval 16297 and
closure coscl 16301.
- 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 31010 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 1971 versus 19.21 2243. This
often permits to prove the result using fewer axioms, and/or to
eliminate a nonfreeness hypothesis (such as Ⅎ𝑥𝜑 in 19.21 2243).
If no constraint is put on axiom use, then the v-version can be proved
from the original theorem using nfv 1946. If two (resp. three) such
disjoint variable conditions are added, then the suffix "vv" (resp.
"vvv") is used, e.g., exlimivv 1964.
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 2601 derived from eu6 2599. 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 5416.
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 2438 (cbval 2427 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 3521.
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 3155 |
| abl | Abelian group | df-abl 20003 |
Abel | Yes | ablgrp 20005, zringabl 21763 |
| abs | absorption | | | No |
ressabs 17432 |
| abs | absolute value (of a complex number) |
df-abs 15409 | (abs‘𝐴) | Yes |
absval 15411, absneg 15450, abs1 15470 |
| ad | adding | |
| No | adantr 486, ad2antlr 740 |
| add | add (see "p") | df-add 11215 |
(𝐴 + 𝐵) | Yes |
addcl 11286, addcom 11500, addass 11291 |
| al | "for all" | |
∀𝑥𝜑 | No | alim 1842, alex 1858 |
| 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 11292 |
| asym | asymmetric, antisymmetric | |
| No | intasym 6108, asymref 6109, posasymb 18499 |
| ax | axiom | |
| No | ax6dgen 2164, ax1cn 11238 |
| bas, base |
base (set of an extensible structure) | df-base 17394 |
(Base‘𝑆) | Yes |
baseval 17395, ressbas 17420, cnfldbas 21688 |
| b, bi | biconditional ("iff", "if and only if")
| df-bi 210 | (𝜑 ↔ 𝜓) | Yes |
impbid 215, sspwb 5416 |
| br | binary relation | df-br 5103 |
𝐴𝑅𝐵 | Yes | brab1 5152, brun 5155 |
| c | commutes, commuted (suffix) | | |
No | biimpac 484 |
| c | contraction (suffix) | | |
No | sylc 66, syl2anc 596 |
| cbv | change bound variable | | |
No | cbvalivw 2039, cbvrex 3348 |
| cdm | codomain | |
| No | ffvelcdm 7082, focdmex 7969 |
| cl | closure | | | No |
ifclda 4517, ovrcl 7462, zaddcl 12740 |
| cn | complex numbers | df-c 11210 |
ℂ | Yes | nnsscn 12344, nncn 12347 |
| cnfld | field of complex numbers | df-cnfld 21685 |
ℂfld | Yes | cnfldbas 21688, cnfldinv 21715 |
| cntz | centralizer | df-cntz 19537 |
(Cntz‘𝑀) | Yes |
cntzfval 19540, dprdfcntz 20237 |
| cnv | converse | df-cnv 5658 |
◡𝐴 | Yes | opelcnvg 5857, f1ocnv 6838 |
| co | composition | df-co 5659 |
(𝐴 ∘ 𝐵) | Yes | cnvco 5866, fmptco 7131 |
| com | commutative | |
| No | orcom 884, bicomi 227, eqcomi 2769 |
| con | contradiction, contraposition | |
| No | condan 830, con2d 135 |
| csb | class substitution | df-csb 3847 |
⦋𝐴 / 𝑥⦌𝐵 | Yes |
csbid 3859, csbie2g 3886 |
| cyg | cyclic group | df-cyg 20098 |
CycGrp | Yes |
iscyg 20099, zringcyg 21781 |
| d | deduction form (suffix) | |
| No | idd 25, impbid 215 |
| df | (alternate) definition (prefix) | |
| No | dfrel2 6180, dffn2 6712 |
| di, distr | distributive | |
| No |
andi 1025, imdi 394, ordi 1023, difindi 4237, ndmovdistr 7611 |
| dif | class difference | df-dif 4047 |
(𝐴 ∖ 𝐵) | Yes |
difss 4072, difindi 4237 |
| div | division | df-div 11978 |
(𝐴 / 𝐵) | Yes |
divcl 11984, divval 11980, divmul 11981 |
| dm | domain | df-dm 5660 |
dom 𝐴 | Yes | dmmpt 6241, iswrddm0 14687 |
| e, eq, equ | equals (equ for setvars, eq for
classes) | df-cleq 2752 |
𝐴 = 𝐵 | Yes |
2p2e4 12481, uneqri 4155, equtr 2053 |
| edg | edge | df-edg 29632 |
(Edg‘𝐺) | Yes |
edgopval 29635, usgredgppr 29783 |
| el | element of | |
𝐴 ∈ 𝐵 | Yes |
eldif 4049, eldifsn 4744, elssuni 4898 |
| en | equinumerous | df-en |
𝐴 ≈ 𝐵 | Yes | domen 8992, enfi 9206 |
| eu | "there exists exactly one" | eu6 2599 |
∃!𝑥𝜑 | Yes | euex 2602, euabsn 4683 |
| ex | exists (i.e. is a set) | |
∈ V | No | brrelex1 5703, 0ex 5260 |
| ex, e | "there exists (at least one)" |
df-ex 1812 |
∃𝑥𝜑 | Yes | exim 1866, alex 1858 |
| exp | export | |
| No | expt 178, expcom 419 |
| f | "not free in" (suffix) | |
| No | equs45f 2488, sbf 2304 |
| f | function | df-f 6543 |
𝐹:𝐴⟶𝐵 | Yes | fssxp 6738, opelf 6744 |
| fal | false | df-fal 1582 |
⊥ | Yes | bifal 1585, falantru 1604 |
| fi | finite intersection | df-fi 9407 |
(fi‘𝐵) | Yes | fival 9408, inelfi 9414 |
| fi, fin | finite | df-fin 8981 |
Fin | Yes |
isfi 9006, snfi 9075, onfin 9234 |
| fld | field (Note: there is an alternative
definition Fld of a field, see df-fld 39020) | df-field 20989 |
Field | Yes | isfld 20999, fldidom 21035 |
| fn | function with domain | df-fn 6542 |
𝐴 Fn 𝐵 | Yes | ffn 6710, fndm 6643 |
| frgp | free group | df-frgp 19930 |
(freeGrp‘𝐼) | Yes |
frgpval 19978, frgpadd 19983 |
| fsupp | finitely supported function |
df-fsupp 9358 | 𝑅 finSupp 𝑍 | Yes |
isfsupp 9361, fdmfisuppfi 9370, fsuppco 9398 |
| fun | function | df-fun 6541 |
Fun 𝐹 | Yes | funrel 6557, ffun 6713 |
| fv | function value | df-fv 6547 |
(𝐹‘𝐴) | Yes | fvres 6905, swrdfv 14801 |
| fz | finite set of sequential integers |
df-fz 13644 |
(𝑀...𝑁) | Yes | fzval 13645, eluzfz 13655 |
| fz0 | finite set of sequential nonnegative integers |
|
(0...𝑁) | Yes | nn0fz0 13763, fz0tp 13766 |
| fzo | half-open integer range | df-fzo 13793 |
(𝑀..^𝑁) | Yes |
elfzo 13799, elfzofz 13814 |
| g | more general (suffix); eliminates "is a set"
hypotheses | |
| No | uniexg 7758 |
| gr | graph | |
| No | uhgrf 29646, isumgr 29679, usgrres1 29902 |
| grp | group | df-grp 19153 |
Grp | Yes | isgrp 19156, tgpgrp 24403 |
| gsum | group sum | df-gsum 17619 |
(𝐺 Σg 𝐹) | Yes |
gsumval 18872, gsumwrev 19586 |
| hash | size (of a set) | df-hash 14479 |
(♯‘𝐴) | Yes |
hashgval 14481, hashfz1 14494, hashcl 14504 |
| hb | hypothesis builder (prefix) | |
| No | hbxfrbi 1857, hbald 2204, hbequid 40060 |
| hm | (monoid, group, ring, ...) homomorphism |
| | No |
ismhm 18986, isghm 19436, isrhm 20715 |
| i | inference (suffix) | |
| No | eleq1i 2851, tcsni 9746 |
| i | implication (suffix) | |
| No | brwdomi 9566, infeq5i 9641 |
| id | identity | |
| No | biid 264 |
| iedg | indexed edge | df-iedg 29583 |
(iEdg‘𝐺) | Yes |
iedgval0 29624, edgiedgb 29638 |
| idm | idempotent | |
| No | anidm 575, tpidm13 4713 |
| im, imp | implication (label often omitted) |
df-im 15274 | (𝐴 → 𝐵) | Yes |
iman 407, imnan 405, impbidd 213 |
| im | (group, ring, ...) isomorphism | |
| No | isgim 19482, rimrcl 20718 |
| ima | image | df-ima 5663 |
(𝐴 “ 𝐵) | Yes | resima 6055, imaundi 6140 |
| imp | import | |
| No | biimpa 482, impcom 413 |
| in | intersection | df-in 4091 |
(𝐴 ∩ 𝐵) | Yes | elin 4093, incom 4106 |
| inf | infimum | df-inf 9439 |
inf(ℝ+, ℝ*, < ) | Yes |
fiinfcl 9499, infiso 9506 |
| is... | is (something a) ...? | |
| No | isring 20469 |
| j | joining, disjoining | |
| No | jc 162, jaoi 871 |
| l | left | |
| No | olcd 888, simpl 488 |
| map | mapping operation or set exponentiation |
df-map 8853 | (𝐴 ↑m 𝐵) | Yes |
mapvalg 8860, elmapex 8872 |
| mat | matrix | df-mat 22729 |
(𝑁 Mat 𝑅) | Yes |
matval 22732, matring 22764 |
| mdet | determinant (of a square matrix) |
df-mdet 22906 | (𝑁 maDet 𝑅) | Yes |
mdetleib 22908, mdetrlin 22923 |
| mgm | magma | df-mgm 18822 |
Magma | Yes |
mgmidmo 18844, mgmlrid 18853, ismgm 18823 |
| mgp | multiplicative group | df-mgp 20367 |
(mulGrp‘𝑅) | Yes |
mgpress 20376, ringmgp 20471 |
| mnd | monoid | df-mnd 18930 |
Mnd | Yes | mndass 18938, mndodcong 19762 |
| mo | "there exists at most one" | df-mo 2564 |
∃*𝑥𝜑 | Yes | eumo 2603, moim 2569 |
| mp | modus ponens | ax-mp 5 |
| No | mpd 16, mpi 21 |
| mpo | maps-to notation for an operation |
df-mpo 7426 | (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) | Yes |
mpompt 7535, resmpo 7541 |
| mpt | modus ponendo tollens | |
| No | mptnan 1800, mptxor 1801 |
| mpt | maps-to notation for a function |
df-mpt 5186 | (𝑥 ∈ 𝐴 ↦ 𝐵) | Yes |
fconstmpt 5712, resmpt 6028 |
| mul | multiplication (see "t") | df-mul 11216 |
(𝐴 · 𝐵) | Yes |
mulcl 11288, divmul 11981, mulcom 11290, mulass 11292 |
| n, not | not | |
¬ 𝜑 | Yes |
nan 843, notnotr 131 |
| ne | not equal | df-ne | 𝐴 ≠ 𝐵 |
Yes | exmidne 2965, neeqtrd 3024 |
| nel | not element of | df-nel | 𝐴 ∉ 𝐵
|
Yes | neli 3063, nnel 3071 |
| ne0 | not equal to zero (see n0) | |
≠ 0 | No |
negne0d 11671, ine0 11755, gt0ne0 11785 |
| nf | "not free in" (prefix) | df-nf 1816 |
Ⅎ𝑥𝜑 | Yes | nfnd 1890 |
| ngp | normed group | df-ngp 24908 |
NrmGrp | Yes | isngp 24921, ngptps 24927 |
| nm | norm (on a group or ring) | df-nm 24907 |
(norm‘𝑊) | Yes |
nmval 24914, subgnm 24958 |
| nn | positive integers | df-nn 12340 |
ℕ | Yes | nnsscn 12344, nncn 12347 |
| nn0 | nonnegative integers | df-n0 12611 |
ℕ0 | Yes | nnnn0 12617, nn0cn 12620 |
| n0 | not the empty set (see ne0) | |
≠ ∅ | No | n0i 4285, vn0 4290, ssn0 4354 |
| OLD | old, obsolete (to be removed soon) | |
| No | 19.43OLD 1915 |
| on | ordinal number | df-on 6366 |
𝐴 ∈ On | Yes |
elon 6371, 1on 8493 onelon 6387 |
| op | ordered pair | df-op 4835 |
⟨𝐴, 𝐵⟩ | Yes | dfopif 4836, opth 5444 |
| or | or | df-or 862 |
(𝜑 ∨ 𝜓) | Yes |
orcom 884, anor 998 |
| ot | ordered triple | df-ot 4858 |
⟨𝐴, 𝐵, 𝐶⟩ | Yes |
euotd 5485, fnotovb 7473 |
| ov | operation value | df-ov 7424 |
(𝐴𝐹𝐵) | Yes
| fnotovb 7473, fnovrn 7597 |
| p | plus (see "add"), for all-constant
theorems | df-add 11215 |
(3 + 2) = 5 | Yes |
3p2e5 12497 |
| pfx | prefix | df-pfx 14826 |
(𝑊 prefix 𝐿) | Yes |
pfxlen 14838, ccatpfx 14855 |
| pm | Principia Mathematica | |
| No | pm2.27 43 |
| pm | partial mapping (operation) | df-pm 8854 |
(𝐴 ↑pm 𝐵) | Yes | elpmi 8870, pmsspw 8909 |
| pr | pair | df-pr 4587 |
{𝐴, 𝐵} | Yes |
elpr 4605, prcom 4689, prid1g 4717, prnz 4734 |
| prm, prime | prime (number) | df-prm 16853 |
ℙ | Yes | 1nprm 16860, dvdsprime 16868 |
| pss | proper subset | df-pss 4014 |
𝐴 ⊊ 𝐵 | Yes | pssss 4025, sspsstri 4033 |
| q | rational numbers ("quotients") | df-q 13080 |
ℚ | Yes | elq 13081 |
| r | reversed (suffix) | |
| No | pm4.71r 568, caovdir 7656 |
| r | right | |
| No | orcd 887, simprl 783 |
| rab | restricted class abstraction |
df-rab 3413 | {𝑥 ∈ 𝐴 ∣ 𝜑} | Yes |
rabswap 3421, df-oprab 7425 |
| ral | restricted universal quantification |
df-ral 3077 | ∀𝑥 ∈ 𝐴𝜑 | Yes |
ralnex 3088, ralrnmpo 7560 |
| rcl | reverse closure | |
| No | ndmfvrcl 6919, nnarcl 8629 |
| re | real numbers | df-r 11214 |
ℝ | Yes | recn 11294, 0re 11314 |
| rel | relation | df-rel 5657 | Rel 𝐴 |
Yes | brrelex1 5703, relmpoopab 8107 |
| res | restriction | df-res 5662 |
(𝐴 ↾ 𝐵) | Yes |
opelres 5975, f1ores 6840 |
| reu | restricted existential uniqueness |
df-reu 3366 | ∃!𝑥 ∈ 𝐴𝜑 | Yes |
nfreud 3409, reurex 3369 |
| rex | restricted existential quantification |
df-rex 3087 | ∃𝑥 ∈ 𝐴𝜑 | Yes |
rexnal 3114, rexrnmpo 7561 |
| rmo | restricted "at most one" |
df-rmo 3365 | ∃*𝑥 ∈ 𝐴𝜑 | Yes |
nfrmod 3408, nrexrmo 3384 |
| rn | range | df-rn 5661 | ran 𝐴 |
Yes | elrng 5872, rncnvcnv 5915 |
| ring | (unital) ring | df-ring 20467 |
Ring | Yes |
ringidval 20415, isring 20469, ringgrp 20470 |
| rng | non-unital ring | df-rng 20381 |
Rng | Yes |
isrng 20382, rngabl 20383, rnglz 20393 |
| rot | rotation | |
| No | 3anrot 1117, 3orrot 1108 |
| s | eliminates need for syllogism (suffix) |
| | No | ancoms 464 |
| sb | (proper) substitution (of a set) |
df-sb 2099 | [𝑦 / 𝑥]𝜑 | Yes |
spsbe 2118, sbimi 2110 |
| sbc | (proper) substitution of a class |
df-sbc 3739 | [𝐴 / 𝑥]𝜑 | Yes |
sbc2or 3747, sbcth 3753 |
| sca | scalar | df-sca 17450 |
(Scalar‘𝐻) | Yes |
resssca 17520, mgpsca 20372 |
| simp | simple, simplification | |
| No | simpl 488, simp3r3 1302 |
| sn | singleton | df-sn 4585 |
{𝐴} | Yes | eldifsn 4744 |
| sp | specialization | |
| No | spsbe 2118, spei 2423 |
| ss | subset | df-ss 3896 |
𝐴 ⊆ 𝐵 | Yes | difss 4072 |
| struct | structure | df-struct 17331 |
Struct | Yes | brstruct 17332, structfn 17340 |
| sub | subtract | df-sub 11547 |
(𝐴 − 𝐵) | Yes |
subval 11552, subaddi 11649 |
| sup | supremum | df-sup 9438 |
sup(𝐴, 𝐵, < ) | Yes |
fisupcl 9466, supmo 9448 |
| supp | support (of a function) | df-supp 8181 |
(𝐹 supp 𝑍) | Yes |
ressuppfi 9391, mptsuppd 8208 |
| swap | swap (two parts within a theorem) |
| | No | rabswap 3421, 2reuswap 3703 |
| syl | syllogism | syl 18 |
| No | 3syl 19 |
| sym | symmetric | |
| No | df-symdif 4198, cnvsym 6107 |
| symg | symmetric group | df-symg 19590 |
(SymGrp‘𝐴) | Yes |
symghash 19598, pgrpsubgsymg 19629 |
| t |
times (see "mul"), for all-constant theorems |
df-mul 11216 |
(3 · 2) = 6 | Yes |
3t2e6 12512 |
| th, t |
theorem |
|
|
No |
nfth 1833, sbcth 3753, weth 10577, ancomst 470 |
| tp | triple | df-tp 4589 |
{𝐴, 𝐵, 𝐶} | Yes |
eltpi 4645, tpeq1 4699 |
| tr | transitive | |
| No | bitrd 282, biantr 818 |
| tru, t |
true, truth |
df-tru 1572 |
⊤ |
Yes |
bitru 1578, truanfal 1603, biimt 363 |
| un | union | df-un 4151 |
(𝐴 ∪ 𝐵) | Yes |
uneqri 4155, uncom 4157 |
| unit | unit (in a ring) |
df-unit 20594 | (Unit‘𝑅) | Yes |
isunit 20609, nzrunit 20781 |
| v |
setvar (especially for specializations of
theorems when a class is replaced by a setvar variable) |
|
x |
Yes |
cv 1568, vex 3454, velpw 4561, vtoclf 3525 |
| v |
disjoint variable condition used in place of nonfreeness
hypothesis (suffix) |
|
|
No |
spimv 2419 |
| vtx |
vertex |
df-vtx 29582 |
(Vtx‘𝐺) |
Yes |
vtxval0 29623, opvtxov 29589 |
| vv |
two disjoint variable conditions used in place of nonfreeness
hypotheses (suffix) |
|
|
No |
19.23vv 1975 |
| w | weak (version of a theorem) (suffix) | |
| No | ax11w 2166, spnfw 2011 |
| wrd | word |
df-word 14663 | Word 𝑆 | Yes |
iswrdb 14669, wrdfn 14677, ffz0iswrd 14690 |
| xp | cross product (Cartesian product) |
df-xp 5656 | (𝐴 × 𝐵) | Yes |
elxp 5673, opelxpi 5687, xpundi 5719 |
| xr | eXtended reals | df-xr 11351 |
ℝ* | Yes | ressxr 11357, rexr 11359, 0xr 11360 |
| z | integers (from German "Zahlen") |
df-z 12698 | ℤ | Yes |
elz 12699, zcn 12702 |
| zn | ring of integers mod 𝑁 | df-zn 21818 |
(ℤ/nℤ‘𝑁) | Yes |
znval 21847, zncrng 21856, znhash 21870 |
| zring | ring of integers | df-zring 21759 |
ℤring | Yes | zringbas 21765, zringcrng 21760
|
| 0, z |
slashed zero (empty set) | df-nul 4279 |
∅ | Yes |
n0i 4285, vn0 4290; snnz 4733, prnz 4734 |
(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.) |
