| Description:
The following gives conventions used in the Metamath Proof Explorer
(MPE, set.mm) regarding labels.
For other conventions, see conventions 30888 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 3080"rgen.1 $e |- ( x e. A -> ph ) $."
or letters corresponding to the (main) class variable used in the
hypothesis, e.g., for mdet0 22834: "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 2689 and stirling 46925.
- 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 3259.
- 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... 15974. 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 3905, and thus its syntax label fragment is "dif". Similarly, the
subclass relation 𝐴 ⊆ 𝐵 has syntax label fragment "ss"
because it is defined in df-ss 3919. 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 4086. There are many other syntax label fragments, e.g.,
singleton construct {𝐴} has syntax label fragment "sn" (because it
is defined in df-sn 4588), and the pair construct {𝐴, 𝐵} has
fragment "pr" ( from df-pr 4590). 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 4751. 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 11134) and "re" represents real numbers ℝ (Definition df-r 11138).
The empty set ∅ often uses fragment 0, even though it is defined
in df-nul 4283. The syntax construct (𝐴 + 𝐵) usually uses the
fragment "add" (which is consistent with df-add 11139), 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 12403.
- 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 16244 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 16162) we have value cosval 16217 and
closure coscl 16221.
- 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 30891 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 2245. This
often permits to prove the result using fewer axioms, and/or to
eliminate a nonfreeness hypothesis (such as Ⅎ𝑥𝜑 in 19.21 2245).
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 2603 derived from eu6 2601. 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 5428.
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 2440 (cbval 2429 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 3524.
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 3157 |
| abl | Abelian group | df-abl 19916 |
Abel | Yes | ablgrp 19918, zringabl 21670 |
| abs | absorption | | | No |
ressabs 17346 |
| abs | absolute value (of a complex number) |
df-abs 15327 | (abs‘𝐴) | Yes |
absval 15329, absneg 15368, abs1 15388 |
| ad | adding | |
| No | adantr 486, ad2antlr 740 |
| add | add (see "p") | df-add 11139 |
(𝐴 + 𝐵) | Yes |
addcl 11210, addcom 11424, addass 11215 |
| 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 11216 |
| asym | asymmetric, antisymmetric | |
| No | intasym 6113, asymref 6114, posasymb 18413 |
| ax | axiom | |
| No | ax6dgen 2165, ax1cn 11162 |
| bas, base |
base (set of an extensible structure) | df-base 17308 |
(Base‘𝑆) | Yes |
baseval 17309, ressbas 17334, cnfldbas 21595 |
| b, bi | biconditional ("iff", "if and only if")
| df-bi 210 | (𝜑 ↔ 𝜓) | Yes |
impbid 215, sspwb 5428 |
| br | binary relation | df-br 5108 |
𝐴𝑅𝐵 | Yes | brab1 5157, brun 5160 |
| c | commutes, commuted (suffix) | | |
No | biimpac 484 |
| c | contraction (suffix) | | |
No | sylc 66, syl2anc 596 |
| cbv | change bound variable | | |
No | cbvalivw 2040, cbvrex 3350 |
| cdm | codomain | |
| No | ffvelcdm 7078, focdmex 7957 |
| cl | closure | | | No |
ifclda 4521, ovrcl 7458, zaddcl 12662 |
| cn | complex numbers | df-c 11134 |
ℂ | Yes | nnsscn 12266, nncn 12269 |
| cnfld | field of complex numbers | df-cnfld 21592 |
ℂfld | Yes | cnfldbas 21595, cnfldinv 21622 |
| cntz | centralizer | df-cntz 19450 |
(Cntz‘𝑀) | Yes |
cntzfval 19453, dprdfcntz 20150 |
| cnv | converse | df-cnv 5667 |
◡𝐴 | Yes | opelcnvg 5864, f1ocnv 6834 |
| co | composition | df-co 5668 |
(𝐴 ∘ 𝐵) | Yes | cnvco 5873, fmptco 7127 |
| com | commutative | |
| No | orcom 884, bicomi 227, eqcomi 2771 |
| con | contradiction, contraposition | |
| No | condan 830, con2d 135 |
| csb | class substitution | df-csb 3851 |
⦋𝐴 / 𝑥⦌𝐵 | Yes |
csbid 3863, csbie2g 3890 |
| cyg | cyclic group | df-cyg 20011 |
CycGrp | Yes |
iscyg 20012, zringcyg 21688 |
| d | deduction form (suffix) | |
| No | idd 25, impbid 215 |
| df | (alternate) definition (prefix) | |
| No | dfrel2 6186, dffn2 6708 |
| di, distr | distributive | |
| No |
andi 1025, imdi 394, ordi 1023, difindi 4241, ndmovdistr 7607 |
| dif | class difference | df-dif 3905 |
(𝐴 ∖ 𝐵) | Yes |
difss 4086, difindi 4241 |
| div | division | df-div 11900 |
(𝐴 / 𝐵) | Yes |
divcl 11906, divval 11902, divmul 11903 |
| dm | domain | df-dm 5669 |
dom 𝐴 | Yes | dmmpt 6240, iswrddm0 14607 |
| e, eq, equ | equals (equ for setvars, eq for
classes) | df-cleq 2754 |
𝐴 = 𝐵 | Yes |
2p2e4 12403, uneqri 4106, equtr 2054 |
| edg | edge | df-edg 29513 |
(Edg‘𝐺) | Yes |
edgopval 29516, usgredgppr 29664 |
| el | element of | |
𝐴 ∈ 𝐵 | Yes |
eldif 3912, eldifsn 4751, elssuni 4902 |
| en | equinumerous | df-en |
𝐴 ≈ 𝐵 | Yes | domen 8971, enfi 9185 |
| eu | "there exists exactly one" | eu6 2601 |
∃!𝑥𝜑 | Yes | euex 2604, euabsn 4690 |
| ex | exists (i.e. is a set) | |
∈ V | No | brrelex1 5712, 0ex 5268 |
| 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 2490, sbf 2306 |
| f | function | df-f 6541 |
𝐹:𝐴⟶𝐵 | Yes | fssxp 6734, opelf 6740 |
| fal | false | df-fal 1583 |
⊥ | Yes | bifal 1586, falantru 1605 |
| fi | finite intersection | df-fi 9385 |
(fi‘𝐵) | Yes | fival 9386, inelfi 9392 |
| fi, fin | finite | df-fin 8960 |
Fin | Yes |
isfi 8985, snfi 9054, onfin 9213 |
| fld | field (Note: there is an alternative
definition Fld of a field, see df-fld 38750) | df-field 20899 |
Field | Yes | isfld 20909, fldidom 20944 |
| fn | function with domain | df-fn 6540 |
𝐴 Fn 𝐵 | Yes | ffn 6706, fndm 6639 |
| frgp | free group | df-frgp 19843 |
(freeGrp‘𝐼) | Yes |
frgpval 19891, frgpadd 19896 |
| fsupp | finitely supported function |
df-fsupp 9336 | 𝑅 finSupp 𝑍 | Yes |
isfsupp 9339, fdmfisuppfi 9348, fsuppco 9376 |
| fun | function | df-fun 6539 |
Fun 𝐹 | Yes | funrel 6554, ffun 6709 |
| fv | function value | df-fv 6545 |
(𝐹‘𝐴) | Yes | fvres 6901, swrdfv 14720 |
| fz | finite set of sequential integers |
df-fz 13566 |
(𝑀...𝑁) | Yes | fzval 13567, eluzfz 13577 |
| fz0 | finite set of sequential nonnegative integers |
|
(0...𝑁) | Yes | nn0fz0 13684, fz0tp 13687 |
| fzo | half-open integer range | df-fzo 13714 |
(𝑀..^𝑁) | Yes |
elfzo 13720, elfzofz 13735 |
| g | more general (suffix); eliminates "is a set"
hypotheses | |
| No | uniexg 7746 |
| gr | graph | |
| No | uhgrf 29527, isumgr 29560, usgrres1 29783 |
| grp | group | df-grp 19066 |
Grp | Yes | isgrp 19069, tgpgrp 24310 |
| gsum | group sum | df-gsum 17533 |
(𝐺 Σg 𝐹) | Yes |
gsumval 18785, gsumwrev 19499 |
| hash | size (of a set) | df-hash 14399 |
(♯‘𝐴) | Yes |
hashgval 14401, hashfz1 14414, hashcl 14424 |
| hb | hypothesis builder (prefix) | |
| No | hbxfrbi 1858, hbald 2205, hbequid 39790 |
| hm | (monoid, group, ring, ...) homomorphism |
| | No |
ismhm 18899, isghm 19349, isrhm 20626 |
| i | inference (suffix) | |
| No | eleq1i 2853, tcsni 9724 |
| i | implication (suffix) | |
| No | brwdomi 9544, infeq5i 9619 |
| id | identity | |
| No | biid 264 |
| iedg | indexed edge | df-iedg 29464 |
(iEdg‘𝐺) | Yes |
iedgval0 29505, edgiedgb 29519 |
| idm | idempotent | |
| No | anidm 575, tpidm13 4720 |
| im, imp | implication (label often omitted) |
df-im 15192 | (𝐴 → 𝐵) | Yes |
iman 407, imnan 405, impbidd 213 |
| im | (group, ring, ...) isomorphism | |
| No | isgim 19395, rimrcl 20629 |
| ima | image | df-ima 5672 |
(𝐴 “ 𝐵) | Yes | resima 6012, imaundi 6145 |
| imp | import | |
| No | biimpa 482, impcom 413 |
| in | intersection | df-in 3909 |
(𝐴 ∩ 𝐵) | Yes | elin 3918, incom 4158 |
| inf | infimum | df-inf 9417 |
inf(ℝ+, ℝ*, < ) | Yes |
fiinfcl 9477, infiso 9484 |
| is... | is (something a) ...? | |
| No | isring 20382 |
| j | joining, disjoining | |
| No | jc 162, jaoi 871 |
| l | left | |
| No | olcd 888, simpl 488 |
| map | mapping operation or set exponentiation |
df-map 8832 | (𝐴 ↑m 𝐵) | Yes |
mapvalg 8839, elmapex 8851 |
| mat | matrix | df-mat 22636 |
(𝑁 Mat 𝑅) | Yes |
matval 22639, matring 22671 |
| mdet | determinant (of a square matrix) |
df-mdet 22813 | (𝑁 maDet 𝑅) | Yes |
mdetleib 22815, mdetrlin 22830 |
| mgm | magma | df-mgm 18736 |
Magma | Yes |
mgmidmo 18758, mgmlrid 18766, ismgm 18737 |
| mgp | multiplicative group | df-mgp 20280 |
(mulGrp‘𝑅) | Yes |
mgpress 20289, ringmgp 20384 |
| mnd | monoid | df-mnd 18843 |
Mnd | Yes | mndass 18851, mndodcong 19675 |
| mo | "there exists at most one" | df-mo 2566 |
∃*𝑥𝜑 | Yes | eumo 2605, moim 2571 |
| mp | modus ponens | ax-mp 5 |
| No | mpd 16, mpi 21 |
| mpo | maps-to notation for an operation |
df-mpo 7422 | (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) | Yes |
mpompt 7531, resmpo 7537 |
| mpt | modus ponendo tollens | |
| No | mptnan 1801, mptxor 1802 |
| mpt | maps-to notation for a function |
df-mpt 5191 | (𝑥 ∈ 𝐴 ↦ 𝐵) | Yes |
fconstmpt 5721, resmpt 6037 |
| mul | multiplication (see "t") | df-mul 11140 |
(𝐴 · 𝐵) | Yes |
mulcl 11212, divmul 11903, mulcom 11214, mulass 11216 |
| n, not | not | |
¬ 𝜑 | Yes |
nan 843, notnotr 131 |
| ne | not equal | df-ne | 𝐴 ≠ 𝐵 |
Yes | exmidne 2967, neeqtrd 3026 |
| nel | not element of | df-nel | 𝐴 ∉ 𝐵
|
Yes | neli 3065, nnel 3073 |
| ne0 | not equal to zero (see n0) | |
≠ 0 | No |
negne0d 11595, ine0 11677, gt0ne0 11707 |
| nf | "not free in" (prefix) | df-nf 1817 |
Ⅎ𝑥𝜑 | Yes | nfnd 1891 |
| ngp | normed group | df-ngp 24815 |
NrmGrp | Yes | isngp 24828, ngptps 24834 |
| nm | norm (on a group or ring) | df-nm 24814 |
(norm‘𝑊) | Yes |
nmval 24821, subgnm 24865 |
| nn | positive integers | df-nn 12262 |
ℕ | Yes | nnsscn 12266, nncn 12269 |
| nn0 | nonnegative integers | df-n0 12533 |
ℕ0 | Yes | nnnn0 12539, nn0cn 12542 |
| n0 | not the empty set (see ne0) | |
≠ ∅ | No | n0i 4289, vn0 4294, ssn0 4358 |
| OLD | old, obsolete (to be removed soon) | |
| No | 19.43OLD 1916 |
| on | ordinal number | df-on 6365 |
𝐴 ∈ On | Yes |
elon 6370, 1on 8472 onelon 6386 |
| op | ordered pair | df-op 4594 |
⟨𝐴, 𝐵⟩ | Yes | dfopif 4833, opth 5456 |
| or | or | df-or 862 |
(𝜑 ∨ 𝜓) | Yes |
orcom 884, anor 998 |
| ot | ordered triple | df-ot 4596 |
⟨𝐴, 𝐵, 𝐶⟩ | Yes |
euotd 5494, fnotovb 7469 |
| ov | operation value | df-ov 7420 |
(𝐴𝐹𝐵) | Yes
| fnotovb 7469, fnovrn 7593 |
| p | plus (see "add"), for all-constant
theorems | df-add 11139 |
(3 + 2) = 5 | Yes |
3p2e5 12419 |
| pfx | prefix | df-pfx 14745 |
(𝑊 prefix 𝐿) | Yes |
pfxlen 14757, ccatpfx 14774 |
| pm | Principia Mathematica | |
| No | pm2.27 43 |
| pm | partial mapping (operation) | df-pm 8833 |
(𝐴 ↑pm 𝐵) | Yes | elpmi 8849, pmsspw 8888 |
| pr | pair | df-pr 4590 |
{𝐴, 𝐵} | Yes |
elpr 4612, prcom 4696, prid1g 4724, prnz 4741 |
| prm, prime | prime (number) | df-prm 16768 |
ℙ | Yes | 1nprm 16775, dvdsprime 16783 |
| pss | proper subset | df-pss 3922 |
𝐴 ⊊ 𝐵 | Yes | pssss 4049, sspsstri 4057 |
| q | rational numbers ("quotients") | df-q 13002 |
ℚ | Yes | elq 13003 |
| r | reversed (suffix) | |
| No | pm4.71r 568, caovdir 7652 |
| r | right | |
| No | orcd 887, simprl 783 |
| rab | restricted class abstraction |
df-rab 3415 | {𝑥 ∈ 𝐴 ∣ 𝜑} | Yes |
rabswap 3423, df-oprab 7421 |
| ral | restricted universal quantification |
df-ral 3079 | ∀𝑥 ∈ 𝐴𝜑 | Yes |
ralnex 3090, ralrnmpo 7556 |
| rcl | reverse closure | |
| No | ndmfvrcl 6915, nnarcl 8608 |
| re | real numbers | df-r 11138 |
ℝ | Yes | recn 11218, 0re 11238 |
| rel | relation | df-rel 5666 | Rel 𝐴 |
Yes | brrelex1 5712, relmpoopab 8095 |
| res | restriction | df-res 5671 |
(𝐴 ↾ 𝐵) | Yes |
opelres 5982, f1ores 6836 |
| reu | restricted existential uniqueness |
df-reu 3368 | ∃!𝑥 ∈ 𝐴𝜑 | Yes |
nfreud 3411, reurex 3371 |
| rex | restricted existential quantification |
df-rex 3089 | ∃𝑥 ∈ 𝐴𝜑 | Yes |
rexnal 3116, rexrnmpo 7557 |
| rmo | restricted "at most one" |
df-rmo 3367 | ∃*𝑥 ∈ 𝐴𝜑 | Yes |
nfrmod 3410, nrexrmo 3386 |
| rn | range | df-rn 5670 | ran 𝐴 |
Yes | elrng 5879, rncnvcnv 5922 |
| ring | (unital) ring | df-ring 20380 |
Ring | Yes |
ringidval 20328, isring 20382, ringgrp 20383 |
| rng | non-unital ring | df-rng 20294 |
Rng | Yes |
isrng 20295, rngabl 20296, rnglz 20306 |
| 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 3743 | [𝐴 / 𝑥]𝜑 | Yes |
sbc2or 3751, sbcth 3757 |
| sca | scalar | df-sca 17364 |
(Scalar‘𝐻) | Yes |
resssca 17434, mgpsca 20285 |
| simp | simple, simplification | |
| No | simpl 488, simp3r3 1302 |
| sn | singleton | df-sn 4588 |
{𝐴} | Yes | eldifsn 4751 |
| sp | specialization | |
| No | spsbe 2119, spei 2425 |
| ss | subset | df-ss 3919 |
𝐴 ⊆ 𝐵 | Yes | difss 4086 |
| struct | structure | df-struct 17245 |
Struct | Yes | brstruct 17246, structfn 17254 |
| sub | subtract | df-sub 11471 |
(𝐴 − 𝐵) | Yes |
subval 11476, subaddi 11573 |
| sup | supremum | df-sup 9416 |
sup(𝐴, 𝐵, < ) | Yes |
fisupcl 9444, supmo 9426 |
| supp | support (of a function) | df-supp 8163 |
(𝐹 supp 𝑍) | Yes |
ressuppfi 9369, mptsuppd 8189 |
| swap | swap (two parts within a theorem) |
| | No | rabswap 3423, 2reuswap 3707 |
| syl | syllogism | syl 18 |
| No | 3syl 19 |
| sym | symmetric | |
| No | df-symdif 4202, cnvsym 6112 |
| symg | symmetric group | df-symg 19503 |
(SymGrp‘𝐴) | Yes |
symghash 19511, pgrpsubgsymg 19542 |
| t |
times (see "mul"), for all-constant theorems |
df-mul 11140 |
(3 · 2) = 6 | Yes |
3t2e6 12434 |
| th, t |
theorem |
|
|
No |
nfth 1834, sbcth 3757, weth 10501, ancomst 470 |
| tp | triple | df-tp 4592 |
{𝐴, 𝐵, 𝐶} | Yes |
eltpi 4652, tpeq1 4706 |
| 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 3907 |
(𝐴 ∪ 𝐵) | Yes |
uneqri 4106, uncom 4108 |
| unit | unit (in a ring) |
df-unit 20505 | (Unit‘𝑅) | Yes |
isunit 20520, nzrunit 20691 |
| v |
setvar (especially for specializations of
theorems when a class is replaced by a setvar variable) |
|
x |
Yes |
cv 1569, vex 3457, velpw 4565, vtoclf 3528 |
| v |
disjoint variable condition used in place of nonfreeness
hypothesis (suffix) |
|
|
No |
spimv 2421 |
| vtx |
vertex |
df-vtx 29463 |
(Vtx‘𝐺) |
Yes |
vtxval0 29504, opvtxov 29470 |
| 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 14583 | Word 𝑆 | Yes |
iswrdb 14589, wrdfn 14597, ffz0iswrd 14610 |
| xp | cross product (Cartesian product) |
df-xp 5665 | (𝐴 × 𝐵) | Yes |
elxp 5682, opelxpi 5696, xpundi 5728 |
| xr | eXtended reals | df-xr 11275 |
ℝ* | Yes | ressxr 11281, rexr 11283, 0xr 11284 |
| z | integers (from German "Zahlen") |
df-z 12620 | ℤ | Yes |
elz 12621, zcn 12624 |
| zn | ring of integers mod 𝑁 | df-zn 21725 |
(ℤ/nℤ‘𝑁) | Yes |
znval 21754, zncrng 21763, znhash 21777 |
| zring | ring of integers | df-zring 21666 |
ℤring | Yes | zringbas 21672, zringcrng 21667
|
| 0, z |
slashed zero (empty set) | df-nul 4283 |
∅ | Yes |
n0i 4289, vn0 4294; snnz 4740, prnz 4741 |
(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.) |
