| Description:
The following gives conventions used in the Metamath Proof Explorer
(MPE, set.mm) regarding labels.
For other conventions, see conventions 30327 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 3053"rgen.1 $e |- ( x e. A -> ph ) $."
or letters corresponding to the (main) class variable used in the
hypothesis, e.g., for mdet0 22542: "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 2662 and stirling 46066.
- 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 1839, and the restricted quantifier version of Theorem 21 from
Section 19 of [Margaris] p. 90 is labeled r19.21 3237.
- 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... 15895. 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 3929, and thus its syntax label fragment is "dif". Similarly, the
subclass relation 𝐴 ⊆ 𝐵 has syntax label fragment "ss"
because it is defined in df-ss 3943. 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 4111. There are many other syntax label fragments, e.g.,
singleton construct {𝐴} has syntax label fragment "sn" (because it
is defined in df-sn 4602), and the pair construct {𝐴, 𝐵} has
fragment "pr" ( from df-pr 4604). 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 4762. An "n" is often used for negation (¬), e.g.,
nan 829.
- 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 11133) and "re" represents real numbers ℝ (Definition df-r 11137).
The empty set ∅ often uses fragment 0, even though it is defined
in df-nul 4309. The syntax construct (𝐴 + 𝐵) usually uses the
fragment "add" (which is consistent with df-add 11138), 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 12373.
- 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 16166 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 16084) we have value cosval 16139 and
closure coscl 16143.
- 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 30330 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 1939 versus 19.21 2207. This
often permits to prove the result using fewer axioms, and/or to
eliminate a nonfreeness hypothesis (such as Ⅎ𝑥𝜑 in 19.21 2207).
If no constraint is put on axiom use, then the v-version can be proved
from the original theorem using nfv 1914. If two (resp. three) such
disjoint variable conditions are added, then the suffix "vv" (resp.
"vvv") is used, e.g., exlimivv 1932.
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 2575 derived from eu6 2573. 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 5424.
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 2413 (cbval 2402 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 3539.
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 3133 |
| abl | Abelian group | df-abl 19762 |
Abel | Yes | ablgrp 19764, zringabl 21410 |
| abs | absorption | | | No |
ressabs 17267 |
| abs | absolute value (of a complex number) |
df-abs 15253 | (abs‘𝐴) | Yes |
absval 15255, absneg 15294, abs1 15314 |
| ad | adding | |
| No | adantr 480, ad2antlr 727 |
| add | add (see "p") | df-add 11138 |
(𝐴 + 𝐵) | Yes |
addcl 11209, addcom 11419, addass 11214 |
| al | "for all" | |
∀𝑥𝜑 | No | alim 1810, alex 1826 |
| 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 11215 |
| asym | asymmetric, antisymmetric | |
| No | intasym 6104, asymref 6105, posasymb 18329 |
| ax | axiom | |
| No | ax6dgen 2128, ax1cn 11161 |
| bas, base |
base (set of an extensible structure) | df-base 17227 |
(Base‘𝑆) | Yes |
baseval 17228, ressbas 17255, cnfldbas 21317 |
| b, bi | biconditional ("iff", "if and only if")
| df-bi 207 | (𝜑 ↔ 𝜓) | Yes |
impbid 212, sspwb 5424 |
| br | binary relation | df-br 5120 |
𝐴𝑅𝐵 | Yes | brab1 5167, brun 5170 |
| c | commutes, commuted (suffix) | | |
No | biimpac 478 |
| c | contraction (suffix) | | |
No | sylc 65, syl2anc 584 |
| cbv | change bound variable | | |
No | cbvalivw 2006, cbvrex 3342 |
| cdm | codomain | |
| No | ffvelcdm 7070, focdmex 7952 |
| cl | closure | | | No |
ifclda 4536, ovrcl 7444, zaddcl 12630 |
| cn | complex numbers | df-c 11133 |
ℂ | Yes | nnsscn 12243, nncn 12246 |
| cnfld | field of complex numbers | df-cnfld 21314 |
ℂfld | Yes | cnfldbas 21317, cnfldinv 21363 |
| cntz | centralizer | df-cntz 19298 |
(Cntz‘𝑀) | Yes |
cntzfval 19301, dprdfcntz 19996 |
| cnv | converse | df-cnv 5662 |
◡𝐴 | Yes | opelcnvg 5860, f1ocnv 6829 |
| co | composition | df-co 5663 |
(𝐴 ∘ 𝐵) | Yes | cnvco 5865, fmptco 7118 |
| com | commutative | |
| No | orcom 870, bicomi 224, eqcomi 2744 |
| con | contradiction, contraposition | |
| No | condan 817, con2d 134 |
| csb | class substitution | df-csb 3875 |
⦋𝐴 / 𝑥⦌𝐵 | Yes |
csbid 3887, csbie2g 3914 |
| cyg | cyclic group | df-cyg 19857 |
CycGrp | Yes |
iscyg 19858, zringcyg 21428 |
| d | deduction form (suffix) | |
| No | idd 24, impbid 212 |
| df | (alternate) definition (prefix) | |
| No | dfrel2 6178, dffn2 6707 |
| di, distr | distributive | |
| No |
andi 1009, imdi 389, ordi 1007, difindi 4267, ndmovdistr 7594 |
| dif | class difference | df-dif 3929 |
(𝐴 ∖ 𝐵) | Yes |
difss 4111, difindi 4267 |
| div | division | df-div 11893 |
(𝐴 / 𝐵) | Yes |
divcl 11900, divval 11896, divmul 11897 |
| dm | domain | df-dm 5664 |
dom 𝐴 | Yes | dmmpt 6229, iswrddm0 14554 |
| e, eq, equ | equals (equ for setvars, eq for
classes) | df-cleq 2727 |
𝐴 = 𝐵 | Yes |
2p2e4 12373, uneqri 4131, equtr 2020 |
| edg | edge | df-edg 28973 |
(Edg‘𝐺) | Yes |
edgopval 28976, usgredgppr 29121 |
| el | element of | |
𝐴 ∈ 𝐵 | Yes |
eldif 3936, eldifsn 4762, elssuni 4913 |
| en | equinumerous | df-en |
𝐴 ≈ 𝐵 | Yes | domen 8974, enfi 9199 |
| eu | "there exists exactly one" | eu6 2573 |
∃!𝑥𝜑 | Yes | euex 2576, euabsn 4702 |
| ex | exists (i.e. is a set) | |
∈ V | No | brrelex1 5707, 0ex 5277 |
| ex, e | "there exists (at least one)" |
df-ex 1780 |
∃𝑥𝜑 | Yes | exim 1834, alex 1826 |
| exp | export | |
| No | expt 177, expcom 413 |
| f | "not free in" (suffix) | |
| No | equs45f 2463, sbf 2271 |
| f | function | df-f 6534 |
𝐹:𝐴⟶𝐵 | Yes | fssxp 6732, opelf 6738 |
| fal | false | df-fal 1553 |
⊥ | Yes | bifal 1556, falantru 1575 |
| fi | finite intersection | df-fi 9421 |
(fi‘𝐵) | Yes | fival 9422, inelfi 9428 |
| fi, fin | finite | df-fin 8961 |
Fin | Yes |
isfi 8988, snfi 9055, onfin 9237 |
| fld | field (Note: there is an alternative
definition Fld of a field, see df-fld 37962) | df-field 20690 |
Field | Yes | isfld 20698, fldidom 20729 |
| fn | function with domain | df-fn 6533 |
𝐴 Fn 𝐵 | Yes | ffn 6705, fndm 6640 |
| frgp | free group | df-frgp 19689 |
(freeGrp‘𝐼) | Yes |
frgpval 19737, frgpadd 19742 |
| fsupp | finitely supported function |
df-fsupp 9372 | 𝑅 finSupp 𝑍 | Yes |
isfsupp 9375, fdmfisuppfi 9384, fsuppco 9412 |
| fun | function | df-fun 6532 |
Fun 𝐹 | Yes | funrel 6552, ffun 6708 |
| fv | function value | df-fv 6538 |
(𝐹‘𝐴) | Yes | fvres 6894, swrdfv 14664 |
| fz | finite set of sequential integers |
df-fz 13523 |
(𝑀...𝑁) | Yes | fzval 13524, eluzfz 13534 |
| fz0 | finite set of sequential nonnegative integers |
|
(0...𝑁) | Yes | nn0fz0 13640, fz0tp 13643 |
| fzo | half-open integer range | df-fzo 13670 |
(𝑀..^𝑁) | Yes |
elfzo 13676, elfzofz 13690 |
| g | more general (suffix); eliminates "is a set"
hypotheses | |
| No | uniexg 7732 |
| gr | graph | |
| No | uhgrf 28987, isumgr 29020, usgrres1 29240 |
| grp | group | df-grp 18917 |
Grp | Yes | isgrp 18920, tgpgrp 24014 |
| gsum | group sum | df-gsum 17454 |
(𝐺 Σg 𝐹) | Yes |
gsumval 18653, gsumwrev 19347 |
| hash | size (of a set) | df-hash 14347 |
(♯‘𝐴) | Yes |
hashgval 14349, hashfz1 14362, hashcl 14372 |
| hb | hypothesis builder (prefix) | |
| No | hbxfrbi 1825, hbald 2168, hbequid 38873 |
| hm | (monoid, group, ring, ...) homomorphism |
| | No |
ismhm 18761, isghm 19196, isrhm 20436 |
| i | inference (suffix) | |
| No | eleq1i 2825, tcsni 9755 |
| i | implication (suffix) | |
| No | brwdomi 9580, infeq5i 9648 |
| id | identity | |
| No | biid 261 |
| iedg | indexed edge | df-iedg 28924 |
(iEdg‘𝐺) | Yes |
iedgval0 28965, edgiedgb 28979 |
| idm | idempotent | |
| No | anidm 564, tpidm13 4732 |
| im, imp | implication (label often omitted) |
df-im 15118 | (𝐴 → 𝐵) | Yes |
iman 401, imnan 399, impbidd 210 |
| im | (group, ring, ...) isomorphism | |
| No | isgim 19243, rimrcl 20440 |
| ima | image | df-ima 5667 |
(𝐴 “ 𝐵) | Yes | resima 6002, imaundi 6138 |
| imp | import | |
| No | biimpa 476, impcom 407 |
| in | intersection | df-in 3933 |
(𝐴 ∩ 𝐵) | Yes | elin 3942, incom 4184 |
| inf | infimum | df-inf 9453 |
inf(ℝ+, ℝ*, < ) | Yes |
fiinfcl 9513, infiso 9520 |
| is... | is (something a) ...? | |
| No | isring 20195 |
| j | joining, disjoining | |
| No | jc 161, jaoi 857 |
| l | left | |
| No | olcd 874, simpl 482 |
| map | mapping operation or set exponentiation |
df-map 8840 | (𝐴 ↑m 𝐵) | Yes |
mapvalg 8848, elmapex 8860 |
| mat | matrix | df-mat 22344 |
(𝑁 Mat 𝑅) | Yes |
matval 22347, matring 22379 |
| mdet | determinant (of a square matrix) |
df-mdet 22521 | (𝑁 maDet 𝑅) | Yes |
mdetleib 22523, mdetrlin 22538 |
| mgm | magma | df-mgm 18616 |
Magma | Yes |
mgmidmo 18636, mgmlrid 18643, ismgm 18617 |
| mgp | multiplicative group | df-mgp 20099 |
(mulGrp‘𝑅) | Yes |
mgpress 20108, ringmgp 20197 |
| mnd | monoid | df-mnd 18711 |
Mnd | Yes | mndass 18719, mndodcong 19521 |
| mo | "there exists at most one" | df-mo 2539 |
∃*𝑥𝜑 | Yes | eumo 2577, moim 2543 |
| mp | modus ponens | ax-mp 5 |
| No | mpd 15, mpi 20 |
| mpo | maps-to notation for an operation |
df-mpo 7408 | (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) | Yes |
mpompt 7519, resmpo 7525 |
| mpt | modus ponendo tollens | |
| No | mptnan 1768, mptxor 1769 |
| mpt | maps-to notation for a function |
df-mpt 5202 | (𝑥 ∈ 𝐴 ↦ 𝐵) | Yes |
fconstmpt 5716, resmpt 6024 |
| mul | multiplication (see "t") | df-mul 11139 |
(𝐴 · 𝐵) | Yes |
mulcl 11211, divmul 11897, mulcom 11213, mulass 11215 |
| n, not | not | |
¬ 𝜑 | Yes |
nan 829, notnotr 130 |
| ne | not equal | df-ne | 𝐴 ≠ 𝐵 |
Yes | exmidne 2942, neeqtrd 3001 |
| nel | not element of | df-nel | 𝐴 ∉ 𝐵
|
Yes | neli 3038, nnel 3046 |
| ne0 | not equal to zero (see n0) | |
≠ 0 | No |
negne0d 11590, ine0 11670, gt0ne0 11700 |
| nf | "not free in" (prefix) | df-nf 1784 |
Ⅎ𝑥𝜑 | Yes | nfnd 1858 |
| ngp | normed group | df-ngp 24520 |
NrmGrp | Yes | isngp 24533, ngptps 24539 |
| nm | norm (on a group or ring) | df-nm 24519 |
(norm‘𝑊) | Yes |
nmval 24526, subgnm 24570 |
| nn | positive integers | df-nn 12239 |
ℕ | Yes | nnsscn 12243, nncn 12246 |
| nn0 | nonnegative integers | df-n0 12500 |
ℕ0 | Yes | nnnn0 12506, nn0cn 12509 |
| n0 | not the empty set (see ne0) | |
≠ ∅ | No | n0i 4315, vn0 4320, ssn0 4379 |
| OLD | old, obsolete (to be removed soon) | |
| No | 19.43OLD 1883 |
| on | ordinal number | df-on 6356 |
𝐴 ∈ On | Yes |
elon 6361, 1on 8490 onelon 6377 |
| op | ordered pair | df-op 4608 |
⟨𝐴, 𝐵⟩ | Yes | dfopif 4846, opth 5451 |
| or | or | df-or 848 |
(𝜑 ∨ 𝜓) | Yes |
orcom 870, anor 984 |
| ot | ordered triple | df-ot 4610 |
⟨𝐴, 𝐵, 𝐶⟩ | Yes |
euotd 5488, fnotovb 7455 |
| ov | operation value | df-ov 7406 |
(𝐴𝐹𝐵) | Yes
| fnotovb 7455, fnovrn 7580 |
| p | plus (see "add"), for all-constant
theorems | df-add 11138 |
(3 + 2) = 5 | Yes |
3p2e5 12389 |
| pfx | prefix | df-pfx 14687 |
(𝑊 prefix 𝐿) | Yes |
pfxlen 14699, ccatpfx 14717 |
| pm | Principia Mathematica | |
| No | pm2.27 42 |
| pm | partial mapping (operation) | df-pm 8841 |
(𝐴 ↑pm 𝐵) | Yes | elpmi 8858, pmsspw 8889 |
| pr | pair | df-pr 4604 |
{𝐴, 𝐵} | Yes |
elpr 4626, prcom 4708, prid1g 4736, prnz 4753 |
| prm, prime | prime (number) | df-prm 16689 |
ℙ | Yes | 1nprm 16696, dvdsprime 16704 |
| pss | proper subset | df-pss 3946 |
𝐴 ⊊ 𝐵 | Yes | pssss 4073, sspsstri 4080 |
| q | rational numbers ("quotients") | df-q 12963 |
ℚ | Yes | elq 12964 |
| r | reversed (suffix) | |
| No | pm4.71r 558, caovdir 7639 |
| r | right | |
| No | orcd 873, simprl 770 |
| rab | restricted class abstraction |
df-rab 3416 | {𝑥 ∈ 𝐴 ∣ 𝜑} | Yes |
rabswap 3425, df-oprab 7407 |
| ral | restricted universal quantification |
df-ral 3052 | ∀𝑥 ∈ 𝐴𝜑 | Yes |
ralnex 3062, ralrnmpo 7544 |
| rcl | reverse closure | |
| No | ndmfvrcl 6911, nnarcl 8626 |
| re | real numbers | df-r 11137 |
ℝ | Yes | recn 11217, 0re 11235 |
| rel | relation | df-rel 5661 | Rel 𝐴 |
Yes | brrelex1 5707, relmpoopab 8091 |
| res | restriction | df-res 5666 |
(𝐴 ↾ 𝐵) | Yes |
opelres 5972, f1ores 6831 |
| reu | restricted existential uniqueness |
df-reu 3360 | ∃!𝑥 ∈ 𝐴𝜑 | Yes |
nfreud 3412, reurex 3363 |
| rex | restricted existential quantification |
df-rex 3061 | ∃𝑥 ∈ 𝐴𝜑 | Yes |
rexnal 3089, rexrnmpo 7545 |
| rmo | restricted "at most one" |
df-rmo 3359 | ∃*𝑥 ∈ 𝐴𝜑 | Yes |
nfrmod 3411, nrexrmo 3380 |
| rn | range | df-rn 5665 | ran 𝐴 |
Yes | elrng 5871, rncnvcnv 5914 |
| ring | (unital) ring | df-ring 20193 |
Ring | Yes |
ringidval 20141, isring 20195, ringgrp 20196 |
| rng | non-unital ring | df-rng 20111 |
Rng | Yes |
isrng 20112, rngabl 20113, rnglz 20123 |
| rot | rotation | |
| No | 3anrot 1099, 3orrot 1091 |
| s | eliminates need for syllogism (suffix) |
| | No | ancoms 458 |
| sb | (proper) substitution (of a set) |
df-sb 2065 | [𝑦 / 𝑥]𝜑 | Yes |
spsbe 2082, sbimi 2074 |
| sbc | (proper) substitution of a class |
df-sbc 3766 | [𝐴 / 𝑥]𝜑 | Yes |
sbc2or 3774, sbcth 3780 |
| sca | scalar | df-sca 17285 |
(Scalar‘𝐻) | Yes |
resssca 17355, mgpsca 20104 |
| simp | simple, simplification | |
| No | simpl 482, simp3r3 1284 |
| sn | singleton | df-sn 4602 |
{𝐴} | Yes | eldifsn 4762 |
| sp | specialization | |
| No | spsbe 2082, spei 2398 |
| ss | subset | df-ss 3943 |
𝐴 ⊆ 𝐵 | Yes | difss 4111 |
| struct | structure | df-struct 17164 |
Struct | Yes | brstruct 17165, structfn 17173 |
| sub | subtract | df-sub 11466 |
(𝐴 − 𝐵) | Yes |
subval 11471, subaddi 11568 |
| sup | supremum | df-sup 9452 |
sup(𝐴, 𝐵, < ) | Yes |
fisupcl 9480, supmo 9462 |
| supp | support (of a function) | df-supp 8158 |
(𝐹 supp 𝑍) | Yes |
ressuppfi 9405, mptsuppd 8184 |
| swap | swap (two parts within a theorem) |
| | No | rabswap 3425, 2reuswap 3729 |
| syl | syllogism | syl 17 |
| No | 3syl 18 |
| sym | symmetric | |
| No | df-symdif 4228, cnvsym 6101 |
| symg | symmetric group | df-symg 19349 |
(SymGrp‘𝐴) | Yes |
symghash 19357, pgrpsubgsymg 19388 |
| t |
times (see "mul"), for all-constant theorems |
df-mul 11139 |
(3 · 2) = 6 | Yes |
3t2e6 12404 |
| th, t |
theorem |
|
|
No |
nfth 1801, sbcth 3780, weth 10507, ancomst 464 |
| tp | triple | df-tp 4606 |
{𝐴, 𝐵, 𝐶} | Yes |
eltpi 4664, tpeq1 4718 |
| tr | transitive | |
| No | bitrd 279, biantr 805 |
| tru, t |
true, truth |
df-tru 1543 |
⊤ |
Yes |
bitru 1549, truanfal 1574, biimt 360 |
| un | union | df-un 3931 |
(𝐴 ∪ 𝐵) | Yes |
uneqri 4131, uncom 4133 |
| unit | unit (in a ring) |
df-unit 20316 | (Unit‘𝑅) | Yes |
isunit 20331, nzrunit 20482 |
| v |
setvar (especially for specializations of
theorems when a class is replaced by a setvar variable) |
|
x |
Yes |
cv 1539, vex 3463, velpw 4580, vtoclf 3543 |
| v |
disjoint variable condition used in place of nonfreeness
hypothesis (suffix) |
|
|
No |
spimv 2394 |
| vtx |
vertex |
df-vtx 28923 |
(Vtx‘𝐺) |
Yes |
vtxval0 28964, opvtxov 28930 |
| vv |
two disjoint variable conditions used in place of nonfreeness
hypotheses (suffix) |
|
|
No |
19.23vv 1943 |
| w | weak (version of a theorem) (suffix) | |
| No | ax11w 2130, spnfw 1979 |
| wrd | word |
df-word 14530 | Word 𝑆 | Yes |
iswrdb 14536, wrdfn 14544, ffz0iswrd 14557 |
| xp | cross product (Cartesian product) |
df-xp 5660 | (𝐴 × 𝐵) | Yes |
elxp 5677, opelxpi 5691, xpundi 5723 |
| xr | eXtended reals | df-xr 11271 |
ℝ* | Yes | ressxr 11277, rexr 11279, 0xr 11280 |
| z | integers (from German "Zahlen") |
df-z 12587 | ℤ | Yes |
elz 12588, zcn 12591 |
| zn | ring of integers mod 𝑁 | df-zn 21465 |
(ℤ/nℤ‘𝑁) | Yes |
znval 21494, zncrng 21503, znhash 21517 |
| zring | ring of integers | df-zring 21406 |
ℤring | Yes | zringbas 21412, zringcrng 21407
|
| 0, z |
slashed zero (empty set) | df-nul 4309 |
∅ | Yes |
n0i 4315, vn0 4320; snnz 4752, prnz 4753 |
(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.) |
