| Description:
The following gives conventions used in the Metamath Proof Explorer
(MPE, set.mm) regarding labels.
For other conventions, see conventions 28185 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 3116"rgen.1 $e |- ( x e. A -> ph ) $."
or letters corresponding to the (main) class variable used in the
hypothesis, e.g. for mdet0 21211: "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 2725 and stirling 42731.
- 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 1840, and the restricted quantifier version of Theorem 21 from
Section 19 of [Margaris] p. 90 is labeled r19.21 3179.
- 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... 15229. 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 3884, and thus its syntax label fragment is "dif". Similarly, the
subclass relation 𝐴 ⊆ 𝐵 has syntax label fragment "ss"
because it is defined in df-ss 3898. 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 4059. There are many other syntax label fragments, e.g.,
singleton construct {𝐴} has syntax label fragment "sn" (because it
is defined in df-sn 4526), and the pair construct {𝐴, 𝐵} has
fragment "pr" ( from df-pr 4528). 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 4680. An "n" is often used for negation (¬), e.g.,
nan 828.
- 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 10532) and "re" represents real numbers ℝ ( definition df-r 10536).
The empty set ∅ often uses fragment 0, even though it is defined
in df-nul 4244. The syntax construct (𝐴 + 𝐵) usually uses the
fragment "add" (which is consistent with df-add 10537), 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 11760.
- 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 15495 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 labeld "NAMEcl".
E.g., for cosine (df-cos 15416) we have value cosval 15468 and closure
coscl 15472.
- 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 28188 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 1940 versus 19.21 2205. This
often permits to prove the result using fewer axioms, and/or to
eliminate a nonfreeness hypothesis (such as Ⅎ𝑥𝜑 in 19.21 2205).
If no constraint is put on axiom use, then the v-version can be proved
from the original theorem using nfv 1915. If two (resp. three) such
disjoint variable conditions are added, then the suffix "vv" (resp.
"vvv") is used, e.g., exlimivv 1933.
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 2636 derived from eu6 2634. 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 5307.
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 2419 (cbval 2405 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 3503.
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 587), commutes
(e.g., biimpac 482)
- 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 480, rexlimiva 3240 |
| abl | Abelian group | df-abl 18901 |
Abel | Yes | ablgrp 18903, zringabl 20167 |
| abs | absorption | | | No |
ressabs 16555 |
| abs | absolute value (of a complex number) |
df-abs 14587 | (abs‘𝐴) | Yes |
absval 14589, absneg 14629, abs1 14649 |
| ad | adding | |
| No | adantr 484, ad2antlr 726 |
| add | add (see "p") | df-add 10537 |
(𝐴 + 𝐵) | Yes |
addcl 10608, addcom 10815, addass 10613 |
| al | "for all" | |
∀𝑥𝜑 | No | alim 1812, alex 1827 |
| ALT | alternative/less preferred (suffix) | |
| No | idALT 23 |
| an | and | df-an 400 |
(𝜑 ∧ 𝜓) | Yes |
anor 980, iman 405, imnan 403 |
| ant | antecedent | |
| No | adantr 484 |
| ass | associative | |
| No | biass 389, orass 919, mulass 10614 |
| asym | asymmetric, antisymmetric | |
| No | intasym 5942, asymref 5943, posasymb 17554 |
| ax | axiom | |
| No | ax6dgen 2129, ax1cn 10560 |
| bas, base |
base (set of an extensible structure) | df-base 16481 |
(Base‘𝑆) | Yes |
baseval 16534, ressbas 16546, cnfldbas 20095 |
| b, bi | biconditional ("iff", "if and only if")
| df-bi 210 | (𝜑 ↔ 𝜓) | Yes |
impbid 215, sspwb 5307 |
| br | binary relation | df-br 5031 |
𝐴𝑅𝐵 | Yes | brab1 5078, brun 5081 |
| cbv | change bound variable | | |
No | cbvalivw 2014, cbvrex 3393 |
| cl | closure | | | No |
ifclda 4459, ovrcl 7176, zaddcl 12010 |
| cn | complex numbers | df-c 10532 |
ℂ | Yes | nnsscn 11630, nncn 11633 |
| cnfld | field of complex numbers | df-cnfld 20092 |
ℂfld | Yes | cnfldbas 20095, cnfldinv 20122 |
| cntz | centralizer | df-cntz 18439 |
(Cntz‘𝑀) | Yes |
cntzfval 18442, dprdfcntz 19130 |
| cnv | converse | df-cnv 5527 |
◡𝐴 | Yes | opelcnvg 5715, f1ocnv 6602 |
| co | composition | df-co 5528 |
(𝐴 ∘ 𝐵) | Yes | cnvco 5720, fmptco 6868 |
| com | commutative | |
| No | orcom 867, bicomi 227, eqcomi 2807 |
| con | contradiction, contraposition | |
| No | condan 817, con2d 136 |
| csb | class substitution | df-csb 3829 |
⦋𝐴 / 𝑥⦌𝐵 | Yes |
csbid 3841, csbie2g 3868 |
| cyg | cyclic group | df-cyg 18990 |
CycGrp | Yes |
iscyg 18991, zringcyg 20184 |
| d | deduction form (suffix) | |
| No | idd 24, impbid 215 |
| df | (alternate) definition (prefix) | |
| No | dfrel2 6013, dffn2 6489 |
| di, distr | distributive | |
| No |
andi 1005, imdi 394, ordi 1003, difindi 4208, ndmovdistr 7317 |
| dif | class difference | df-dif 3884 |
(𝐴 ∖ 𝐵) | Yes |
difss 4059, difindi 4208 |
| div | division | df-div 11287 |
(𝐴 / 𝐵) | Yes |
divcl 11293, divval 11289, divmul 11290 |
| dm | domain | df-dm 5529 |
dom 𝐴 | Yes | dmmpt 6061, iswrddm0 13881 |
| e, eq, equ | equals (equ for setvars, eq for
classes) | df-cleq 2791 |
𝐴 = 𝐵 | Yes |
2p2e4 11760, uneqri 4078, equtr 2028 |
| edg | edge | df-edg 26841 |
(Edg‘𝐺) | Yes |
edgopval 26844, usgredgppr 26986 |
| el | element of | |
𝐴 ∈ 𝐵 | Yes |
eldif 3891, eldifsn 4680, elssuni 4830 |
| en | equinumerous | df-en |
𝐴 ≈ 𝐵 | Yes | domen 8505, enfi 8718 |
| eu | "there exists exactly one" | eu6 2634 |
∃!𝑥𝜑 | Yes | euex 2637, euabsn 4622 |
| ex | exists (i.e. is a set) | |
∈ V | No | brrelex1 5569, 0ex 5175 |
| ex, e | "there exists (at least one)" |
df-ex 1782 |
∃𝑥𝜑 | Yes | exim 1835, alex 1827 |
| exp | export | |
| No | expt 180, expcom 417 |
| f | "not free in" (suffix) | |
| No | equs45f 2471, sbf 2268 |
| f | function | df-f 6328 |
𝐹:𝐴⟶𝐵 | Yes | fssxp 6508, opelf 6513 |
| fal | false | df-fal 1551 |
⊥ | Yes | bifal 1554, falantru 1573 |
| fi | finite intersection | df-fi 8859 |
(fi‘𝐵) | Yes | fival 8860, inelfi 8866 |
| fi, fin | finite | df-fin 8496 |
Fin | Yes |
isfi 8516, snfi 8577, onfin 8694 |
| fld | field (Note: there is an alternative
definition Fld of a field, see df-fld 35430) | df-field 19498 |
Field | Yes | isfld 19504, fldidom 20071 |
| fn | function with domain | df-fn 6327 |
𝐴 Fn 𝐵 | Yes | ffn 6487, fndm 6425 |
| frgp | free group | df-frgp 18828 |
(freeGrp‘𝐼) | Yes |
frgpval 18876, frgpadd 18881 |
| fsupp | finitely supported function |
df-fsupp 8818 | 𝑅 finSupp 𝑍 | Yes |
isfsupp 8821, fdmfisuppfi 8826, fsuppco 8849 |
| fun | function | df-fun 6326 |
Fun 𝐹 | Yes | funrel 6341, ffun 6490 |
| fv | function value | df-fv 6332 |
(𝐹‘𝐴) | Yes | fvres 6664, swrdfv 14001 |
| fz | finite set of sequential integers |
df-fz 12886 |
(𝑀...𝑁) | Yes | fzval 12887, eluzfz 12897 |
| fz0 | finite set of sequential nonnegative integers |
|
(0...𝑁) | Yes | nn0fz0 13000, fz0tp 13003 |
| fzo | half-open integer range | df-fzo 13029 |
(𝑀..^𝑁) | Yes |
elfzo 13035, elfzofz 13048 |
| g | more general (suffix); eliminates "is a set"
hypotheses | |
| No | uniexg 7446 |
| gr | graph | |
| No | uhgrf 26855, isumgr 26888, usgrres1 27105 |
| grp | group | df-grp 18098 |
Grp | Yes | isgrp 18101, tgpgrp 22683 |
| gsum | group sum | df-gsum 16708 |
(𝐺 Σg 𝐹) | Yes |
gsumval 17879, gsumwrev 18486 |
| hash | size (of a set) | df-hash 13687 |
(♯‘𝐴) | Yes |
hashgval 13689, hashfz1 13702, hashcl 13713 |
| hb | hypothesis builder (prefix) | |
| No | hbxfrbi 1826, hbald 2172, hbequid 36205 |
| hm | (monoid, group, ring) homomorphism | |
| No | ismhm 17950, isghm 18350, isrhm 19469 |
| i | inference (suffix) | |
| No | eleq1i 2880, tcsni 9169 |
| i | implication (suffix) | |
| No | brwdomi 9016, infeq5i 9083 |
| id | identity | |
| No | biid 264 |
| iedg | indexed edge | df-iedg 26792 |
(iEdg‘𝐺) | Yes |
iedgval0 26833, edgiedgb 26847 |
| idm | idempotent | |
| No | anidm 568, tpidm13 4652 |
| im, imp | implication (label often omitted) |
df-im 14452 | (𝐴 → 𝐵) | Yes |
iman 405, imnan 403, impbidd 213 |
| ima | image | df-ima 5532 |
(𝐴 “ 𝐵) | Yes | resima 5852, imaundi 5975 |
| imp | import | |
| No | biimpa 480, impcom 411 |
| in | intersection | df-in 3888 |
(𝐴 ∩ 𝐵) | Yes | elin 3897, incom 4128 |
| inf | infimum | df-inf 8891 |
inf(ℝ+, ℝ*, < ) | Yes |
fiinfcl 8949, infiso 8956 |
| is... | is (something a) ...? | |
| No | isring 19294 |
| j | joining, disjoining | |
| No | jc 164, jaoi 854 |
| l | left | |
| No | olcd 871, simpl 486 |
| map | mapping operation or set exponentiation |
df-map 8391 | (𝐴 ↑m 𝐵) | Yes |
mapvalg 8399, elmapex 8410 |
| mat | matrix | df-mat 21013 |
(𝑁 Mat 𝑅) | Yes |
matval 21016, matring 21048 |
| mdet | determinant (of a square matrix) |
df-mdet 21190 | (𝑁 maDet 𝑅) | Yes |
mdetleib 21192, mdetrlin 21207 |
| mgm | magma | df-mgm 17844 |
Magma | Yes |
mgmidmo 17862, mgmlrid 17869, ismgm 17845 |
| mgp | multiplicative group | df-mgp 19233 |
(mulGrp‘𝑅) | Yes |
mgpress 19243, ringmgp 19296 |
| mnd | monoid | df-mnd 17904 |
Mnd | Yes | mndass 17912, mndodcong 18662 |
| mo | "there exists at most one" | df-mo 2598 |
∃*𝑥𝜑 | Yes | eumo 2638, moim 2602 |
| mp | modus ponens | ax-mp 5 |
| No | mpd 15, mpi 20 |
| mpo | maps-to notation for an operation |
df-mpo 7140 | (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) | Yes |
mpompt 7245, resmpo 7251 |
| mpt | modus ponendo tollens | |
| No | mptnan 1770, mptxor 1771 |
| mpt | maps-to notation for a function |
df-mpt 5111 | (𝑥 ∈ 𝐴 ↦ 𝐵) | Yes |
fconstmpt 5578, resmpt 5872 |
| mpt2 | maps-to notation for an operation (deprecated).
We are in the process of replacing mpt2 with mpo in labels. |
df-mpo 7140 | (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) | Yes |
mpompt 7245, resmpo 7251 |
| mul | multiplication (see "t") | df-mul 10538 |
(𝐴 · 𝐵) | Yes |
mulcl 10610, divmul 11290, mulcom 10612, mulass 10614 |
| n, not | not | |
¬ 𝜑 | Yes |
nan 828, notnotr 132 |
| ne | not equal | df-ne | 𝐴 ≠ 𝐵 |
Yes | exmidne 2997, neeqtrd 3056 |
| nel | not element of | df-nel | 𝐴 ∉ 𝐵
|
Yes | neli 3093, nnel 3100 |
| ne0 | not equal to zero (see n0) | |
≠ 0 | No |
negne0d 10984, ine0 11064, gt0ne0 11094 |
| nf | "not free in" (prefix) | |
| No | nfnd 1859 |
| ngp | normed group | df-ngp 23190 |
NrmGrp | Yes | isngp 23202, ngptps 23208 |
| nm | norm (on a group or ring) | df-nm 23189 |
(norm‘𝑊) | Yes |
nmval 23196, subgnm 23239 |
| nn | positive integers | df-nn 11626 |
ℕ | Yes | nnsscn 11630, nncn 11633 |
| nn0 | nonnegative integers | df-n0 11886 |
ℕ0 | Yes | nnnn0 11892, nn0cn 11895 |
| n0 | not the empty set (see ne0) | |
≠ ∅ | No | n0i 4249, vn0 4254, ssn0 4308 |
| OLD | old, obsolete (to be removed soon) | |
| No | 19.43OLD 1884 |
| on | ordinal number | df-on 6163 |
𝐴 ∈ On | Yes |
elon 6168, 1on 8092 onelon 6184 |
| op | ordered pair | df-op 4532 |
⟨𝐴, 𝐵⟩ | Yes | dfopif 4760, opth 5333 |
| or | or | df-or 845 |
(𝜑 ∨ 𝜓) | Yes |
orcom 867, anor 980 |
| ot | ordered triple | df-ot 4534 |
⟨𝐴, 𝐵, 𝐶⟩ | Yes |
euotd 5368, fnotovb 7185 |
| ov | operation value | df-ov 7138 |
(𝐴𝐹𝐵) | Yes
| fnotovb 7185, fnovrn 7303 |
| p | plus (see "add"), for all-constant
theorems | df-add 10537 |
(3 + 2) = 5 | Yes |
3p2e5 11776 |
| pfx | prefix | df-pfx 14024 |
(𝑊 prefix 𝐿) | Yes |
pfxlen 14036, ccatpfx 14054 |
| pm | Principia Mathematica | |
| No | pm2.27 42 |
| pm | partial mapping (operation) | df-pm 8392 |
(𝐴 ↑pm 𝐵) | Yes | elpmi 8408, pmsspw 8424 |
| pr | pair | df-pr 4528 |
{𝐴, 𝐵} | Yes |
elpr 4548, prcom 4628, prid1g 4656, prnz 4673 |
| prm, prime | prime (number) | df-prm 16006 |
ℙ | Yes | 1nprm 16013, dvdsprime 16021 |
| pss | proper subset | df-pss 3900 |
𝐴 ⊊ 𝐵 | Yes | pssss 4023, sspsstri 4030 |
| q | rational numbers ("quotients") | df-q 12337 |
ℚ | Yes | elq 12338 |
| r | right | |
| No | orcd 870, simprl 770 |
| rab | restricted class abstraction |
df-rab 3115 | {𝑥 ∈ 𝐴 ∣ 𝜑} | Yes |
rabswap 3436, df-oprab 7139 |
| ral | restricted universal quantification |
df-ral 3111 | ∀𝑥 ∈ 𝐴𝜑 | Yes |
ralnex 3199, ralrnmpo 7268 |
| rcl | reverse closure | |
| No | ndmfvrcl 6676, nnarcl 8225 |
| re | real numbers | df-r 10536 |
ℝ | Yes | recn 10616, 0re 10632 |
| rel | relation | df-rel 5526 | Rel 𝐴 |
Yes | brrelex1 5569, relmpoopab 7772 |
| res | restriction | df-res 5531 |
(𝐴 ↾ 𝐵) | Yes |
opelres 5824, f1ores 6604 |
| reu | restricted existential uniqueness |
df-reu 3113 | ∃!𝑥 ∈ 𝐴𝜑 | Yes |
nfreud 3325, reurex 3376 |
| rex | restricted existential quantification |
df-rex 3112 | ∃𝑥 ∈ 𝐴𝜑 | Yes |
rexnal 3201, rexrnmpo 7269 |
| rmo | restricted "at most one" |
df-rmo 3114 | ∃*𝑥 ∈ 𝐴𝜑 | Yes |
nfrmod 3326, nrexrmo 3380 |
| rn | range | df-rn 5530 | ran 𝐴 |
Yes | elrng 5726, rncnvcnv 5768 |
| rng | (unital) ring | df-ring 19292 |
Ring | Yes |
ringidval 19246, isring 19294, ringgrp 19295 |
| rot | rotation | |
| No | 3anrot 1097, 3orrot 1089 |
| s | eliminates need for syllogism (suffix) |
| | No | ancoms 462 |
| sb | (proper) substitution (of a set) |
df-sb 2070 | [𝑦 / 𝑥]𝜑 | Yes |
spsbe 2087, sbimi 2079 |
| sbc | (proper) substitution of a class |
df-sbc 3721 | [𝐴 / 𝑥]𝜑 | Yes |
sbc2or 3729, sbcth 3735 |
| sca | scalar | df-sca 16573 |
(Scalar‘𝐻) | Yes |
resssca 16642, mgpsca 19239 |
| simp | simple, simplification | |
| No | simpl 486, simp3r3 1280 |
| sn | singleton | df-sn 4526 |
{𝐴} | Yes | eldifsn 4680 |
| sp | specialization | |
| No | spsbe 2087, spei 2401 |
| ss | subset | df-ss 3898 |
𝐴 ⊆ 𝐵 | Yes | difss 4059 |
| struct | structure | df-struct 16477 |
Struct | Yes | brstruct 16484, structfn 16492 |
| sub | subtract | df-sub 10861 |
(𝐴 − 𝐵) | Yes |
subval 10866, subaddi 10962 |
| sup | supremum | df-sup 8890 |
sup(𝐴, 𝐵, < ) | Yes |
fisupcl 8917, supmo 8900 |
| supp | support (of a function) | df-supp 7814 |
(𝐹 supp 𝑍) | Yes |
ressuppfi 8843, mptsuppd 7836 |
| swap | swap (two parts within a theorem) |
| | No | rabswap 3436, 2reuswap 3685 |
| syl | syllogism | syl 17 |
| No | 3syl 18 |
| sym | symmetric | |
| No | df-symdif 4169, cnvsym 5941 |
| symg | symmetric group | df-symg 18488 |
(SymGrp‘𝐴) | Yes |
symghash 18498, pgrpsubgsymg 18529 |
| t |
times (see "mul"), for all-constant theorems |
df-mul 10538 |
(3 · 2) = 6 | Yes |
3t2e6 11791 |
| th, t |
theorem |
|
|
No |
nfth 1803, sbcth 3735, weth 9906, ancomst 468 |
| tp | triple | df-tp 4530 |
{𝐴, 𝐵, 𝐶} | Yes |
eltpi 4585, tpeq1 4638 |
| tr | transitive | |
| No | bitrd 282, biantr 805 |
| tru, t |
true, truth |
df-tru 1541 |
⊤ |
Yes |
bitru 1547, truanfal 1572, biimt 364 |
| un | union | df-un 3886 |
(𝐴 ∪ 𝐵) | Yes |
uneqri 4078, uncom 4080 |
| unit | unit (in a ring) |
df-unit 19388 | (Unit‘𝑅) | Yes |
isunit 19403, nzrunit 20033 |
| v |
setvar (especially for specializations of
theorems when a class is replaced by a setvar variable) |
|
x |
Yes |
cv 1537, vex 3444, velpw 4502, vtoclf 3506 |
| v |
disjoint variable condition used in place of nonfreeness
hypothesis (suffix) |
|
|
No |
spimv 2397 |
| vtx |
vertex |
df-vtx 26791 |
(Vtx‘𝐺) |
Yes |
vtxval0 26832, opvtxov 26798 |
| vv |
two disjoint variable conditions used in place of nonfreeness
hypotheses (suffix) |
|
|
No |
19.23vv 1944 |
| w | weak (version of a theorem) (suffix) | |
| No | ax11w 2131, spnfw 1984 |
| wrd | word |
df-word 13858 | Word 𝑆 | Yes |
iswrdb 13863, wrdfn 13871, ffz0iswrd 13884 |
| xp | cross product (Cartesian product) |
df-xp 5525 | (𝐴 × 𝐵) | Yes |
elxp 5542, opelxpi 5556, xpundi 5584 |
| xr | eXtended reals | df-xr 10668 |
ℝ* | Yes | ressxr 10674, rexr 10676, 0xr 10677 |
| z | integers (from German "Zahlen") |
df-z 11970 | ℤ | Yes |
elz 11971, zcn 11974 |
| zn | ring of integers mod 𝑁 | df-zn 20200 |
(ℤ/nℤ‘𝑁) | Yes |
znval 20227, zncrng 20236, znhash 20250 |
| zring | ring of integers | df-zring 20164 |
ℤring | Yes | zringbas 20169, zringcrng 20165
|
| 0, z |
slashed zero (empty set) | df-nul 4244 |
∅ | Yes |
n0i 4249, vn0 4254; snnz 4672, prnz 4673 |
(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.) |
