| Description:
The following gives conventions used in the Metamath Proof Explorer
(MPE, set.mm) regarding labels.
For other conventions, see conventions 28665 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 3073"rgen.1 $e |- ( x e. A -> ph ) $."
or letters corresponding to the (main) class variable used in the
hypothesis, e.g., for mdet0 21663: "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 2664 and stirling 43520.
- 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 1842, and the restricted quantifier version of Theorem 21 from
Section 19 of [Margaris] p. 90 is labeled r19.21 3138.
- 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... 15521. 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 3886, and thus its syntax label fragment is "dif". Similarly, the
subclass relation 𝐴 ⊆ 𝐵 has syntax label fragment "ss"
because it is defined in df-ss 3900. 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 4062. There are many other syntax label fragments, e.g.,
singleton construct {𝐴} has syntax label fragment "sn" (because it
is defined in df-sn 4559), and the pair construct {𝐴, 𝐵} has
fragment "pr" ( from df-pr 4561). 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 4717. An "n" is often used for negation (¬), e.g.,
nan 826.
- 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 10808) and "re" represents real numbers ℝ (Definition df-r 10812).
The empty set ∅ often uses fragment 0, even though it is defined
in df-nul 4254. The syntax construct (𝐴 + 𝐵) usually uses the
fragment "add" (which is consistent with df-add 10813), 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 12038.
- 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 15787 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 15708) we have value cosval 15760 and
closure coscl 15764.
- 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 28668 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 1943 versus 19.21 2203. This
often permits to prove the result using fewer axioms, and/or to
eliminate a nonfreeness hypothesis (such as Ⅎ𝑥𝜑 in 19.21 2203).
If no constraint is put on axiom use, then the v-version can be proved
from the original theorem using nfv 1918. If two (resp. three) such
disjoint variable conditions are added, then the suffix "vv" (resp.
"vvv") is used, e.g., exlimivv 1936.
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 2576 derived from eu6 2574. 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 5359.
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 2409 (cbval 2398 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 3483.
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 583), 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 3209 |
| abl | Abelian group | df-abl 19304 |
Abel | Yes | ablgrp 19306, zringabl 20586 |
| abs | absorption | | | No |
ressabs 16885 |
| abs | absolute value (of a complex number) |
df-abs 14875 | (abs‘𝐴) | Yes |
absval 14877, absneg 14917, abs1 14937 |
| ad | adding | |
| No | adantr 480, ad2antlr 723 |
| add | add (see "p") | df-add 10813 |
(𝐴 + 𝐵) | Yes |
addcl 10884, addcom 11091, addass 10889 |
| al | "for all" | |
∀𝑥𝜑 | No | alim 1814, alex 1829 |
| ALT | alternative/less preferred (suffix) | |
| No | idALT 23 |
| an | and | df-an 396 |
(𝜑 ∧ 𝜓) | Yes |
anor 979, iman 401, imnan 399 |
| ant | antecedent | |
| No | adantr 480 |
| ass | associative | |
| No | biass 385, orass 918, mulass 10890 |
| asym | asymmetric, antisymmetric | |
| No | intasym 6009, asymref 6010, posasymb 17952 |
| ax | axiom | |
| No | ax6dgen 2126, ax1cn 10836 |
| bas, base |
base (set of an extensible structure) | df-base 16841 |
(Base‘𝑆) | Yes |
baseval 16842, ressbas 16873, cnfldbas 20514 |
| b, bi | biconditional ("iff", "if and only if")
| df-bi 206 | (𝜑 ↔ 𝜓) | Yes |
impbid 211, sspwb 5359 |
| br | binary relation | df-br 5071 |
𝐴𝑅𝐵 | Yes | brab1 5118, brun 5121 |
| cbv | change bound variable | | |
No | cbvalivw 2011, cbvrex 3369 |
| cl | closure | | | No |
ifclda 4491, ovrcl 7296, zaddcl 12290 |
| cn | complex numbers | df-c 10808 |
ℂ | Yes | nnsscn 11908, nncn 11911 |
| cnfld | field of complex numbers | df-cnfld 20511 |
ℂfld | Yes | cnfldbas 20514, cnfldinv 20541 |
| cntz | centralizer | df-cntz 18838 |
(Cntz‘𝑀) | Yes |
cntzfval 18841, dprdfcntz 19533 |
| cnv | converse | df-cnv 5588 |
◡𝐴 | Yes | opelcnvg 5778, f1ocnv 6712 |
| co | composition | df-co 5589 |
(𝐴 ∘ 𝐵) | Yes | cnvco 5783, fmptco 6983 |
| com | commutative | |
| No | orcom 866, bicomi 223, eqcomi 2747 |
| con | contradiction, contraposition | |
| No | condan 814, con2d 134 |
| csb | class substitution | df-csb 3829 |
⦋𝐴 / 𝑥⦌𝐵 | Yes |
csbid 3841, csbie2g 3871 |
| cyg | cyclic group | df-cyg 19393 |
CycGrp | Yes |
iscyg 19394, zringcyg 20603 |
| d | deduction form (suffix) | |
| No | idd 24, impbid 211 |
| df | (alternate) definition (prefix) | |
| No | dfrel2 6081, dffn2 6586 |
| di, distr | distributive | |
| No |
andi 1004, imdi 390, ordi 1002, difindi 4212, ndmovdistr 7439 |
| dif | class difference | df-dif 3886 |
(𝐴 ∖ 𝐵) | Yes |
difss 4062, difindi 4212 |
| div | division | df-div 11563 |
(𝐴 / 𝐵) | Yes |
divcl 11569, divval 11565, divmul 11566 |
| dm | domain | df-dm 5590 |
dom 𝐴 | Yes | dmmpt 6132, iswrddm0 14169 |
| e, eq, equ | equals (equ for setvars, eq for
classes) | df-cleq 2730 |
𝐴 = 𝐵 | Yes |
2p2e4 12038, uneqri 4081, equtr 2025 |
| edg | edge | df-edg 27321 |
(Edg‘𝐺) | Yes |
edgopval 27324, usgredgppr 27466 |
| el | element of | |
𝐴 ∈ 𝐵 | Yes |
eldif 3893, eldifsn 4717, elssuni 4868 |
| en | equinumerous | df-en |
𝐴 ≈ 𝐵 | Yes | domen 8706, enfi 8933 |
| eu | "there exists exactly one" | eu6 2574 |
∃!𝑥𝜑 | Yes | euex 2577, euabsn 4659 |
| ex | exists (i.e. is a set) | |
∈ V | No | brrelex1 5631, 0ex 5226 |
| ex, e | "there exists (at least one)" |
df-ex 1784 |
∃𝑥𝜑 | Yes | exim 1837, alex 1829 |
| exp | export | |
| No | expt 177, expcom 413 |
| f | "not free in" (suffix) | |
| No | equs45f 2459, sbf 2266 |
| f | function | df-f 6422 |
𝐹:𝐴⟶𝐵 | Yes | fssxp 6612, opelf 6619 |
| fal | false | df-fal 1552 |
⊥ | Yes | bifal 1555, falantru 1574 |
| fi | finite intersection | df-fi 9100 |
(fi‘𝐵) | Yes | fival 9101, inelfi 9107 |
| fi, fin | finite | df-fin 8695 |
Fin | Yes |
isfi 8719, snfi 8788, onfin 8944 |
| fld | field (Note: there is an alternative
definition Fld of a field, see df-fld 36077) | df-field 19909 |
Field | Yes | isfld 19915, fldidom 20489 |
| fn | function with domain | df-fn 6421 |
𝐴 Fn 𝐵 | Yes | ffn 6584, fndm 6520 |
| frgp | free group | df-frgp 19231 |
(freeGrp‘𝐼) | Yes |
frgpval 19279, frgpadd 19284 |
| fsupp | finitely supported function |
df-fsupp 9059 | 𝑅 finSupp 𝑍 | Yes |
isfsupp 9062, fdmfisuppfi 9067, fsuppco 9091 |
| fun | function | df-fun 6420 |
Fun 𝐹 | Yes | funrel 6435, ffun 6587 |
| fv | function value | df-fv 6426 |
(𝐹‘𝐴) | Yes | fvres 6775, swrdfv 14289 |
| fz | finite set of sequential integers |
df-fz 13169 |
(𝑀...𝑁) | Yes | fzval 13170, eluzfz 13180 |
| fz0 | finite set of sequential nonnegative integers |
|
(0...𝑁) | Yes | nn0fz0 13283, fz0tp 13286 |
| fzo | half-open integer range | df-fzo 13312 |
(𝑀..^𝑁) | Yes |
elfzo 13318, elfzofz 13331 |
| g | more general (suffix); eliminates "is a set"
hypotheses | |
| No | uniexg 7571 |
| gr | graph | |
| No | uhgrf 27335, isumgr 27368, usgrres1 27585 |
| grp | group | df-grp 18495 |
Grp | Yes | isgrp 18498, tgpgrp 23137 |
| gsum | group sum | df-gsum 17070 |
(𝐺 Σg 𝐹) | Yes |
gsumval 18276, gsumwrev 18888 |
| hash | size (of a set) | df-hash 13973 |
(♯‘𝐴) | Yes |
hashgval 13975, hashfz1 13988, hashcl 13999 |
| hb | hypothesis builder (prefix) | |
| No | hbxfrbi 1828, hbald 2170, hbequid 36850 |
| hm | (monoid, group, ring) homomorphism | |
| No | ismhm 18347, isghm 18749, isrhm 19880 |
| i | inference (suffix) | |
| No | eleq1i 2829, tcsni 9432 |
| i | implication (suffix) | |
| No | brwdomi 9257, infeq5i 9324 |
| id | identity | |
| No | biid 260 |
| iedg | indexed edge | df-iedg 27272 |
(iEdg‘𝐺) | Yes |
iedgval0 27313, edgiedgb 27327 |
| idm | idempotent | |
| No | anidm 564, tpidm13 4689 |
| im, imp | implication (label often omitted) |
df-im 14740 | (𝐴 → 𝐵) | Yes |
iman 401, imnan 399, impbidd 209 |
| ima | image | df-ima 5593 |
(𝐴 “ 𝐵) | Yes | resima 5914, imaundi 6042 |
| imp | import | |
| No | biimpa 476, impcom 407 |
| in | intersection | df-in 3890 |
(𝐴 ∩ 𝐵) | Yes | elin 3899, incom 4131 |
| inf | infimum | df-inf 9132 |
inf(ℝ+, ℝ*, < ) | Yes |
fiinfcl 9190, infiso 9197 |
| is... | is (something a) ...? | |
| No | isring 19702 |
| j | joining, disjoining | |
| No | jc 161, jaoi 853 |
| l | left | |
| No | olcd 870, simpl 482 |
| map | mapping operation or set exponentiation |
df-map 8575 | (𝐴 ↑m 𝐵) | Yes |
mapvalg 8583, elmapex 8594 |
| mat | matrix | df-mat 21465 |
(𝑁 Mat 𝑅) | Yes |
matval 21468, matring 21500 |
| mdet | determinant (of a square matrix) |
df-mdet 21642 | (𝑁 maDet 𝑅) | Yes |
mdetleib 21644, mdetrlin 21659 |
| mgm | magma | df-mgm 18241 |
Magma | Yes |
mgmidmo 18259, mgmlrid 18266, ismgm 18242 |
| mgp | multiplicative group | df-mgp 19636 |
(mulGrp‘𝑅) | Yes |
mgpress 19650, ringmgp 19704 |
| mnd | monoid | df-mnd 18301 |
Mnd | Yes | mndass 18309, mndodcong 19065 |
| mo | "there exists at most one" | df-mo 2540 |
∃*𝑥𝜑 | Yes | eumo 2578, moim 2544 |
| mp | modus ponens | ax-mp 5 |
| No | mpd 15, mpi 20 |
| mpo | maps-to notation for an operation |
df-mpo 7260 | (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) | Yes |
mpompt 7366, resmpo 7372 |
| mpt | modus ponendo tollens | |
| No | mptnan 1772, mptxor 1773 |
| mpt | maps-to notation for a function |
df-mpt 5154 | (𝑥 ∈ 𝐴 ↦ 𝐵) | Yes |
fconstmpt 5640, resmpt 5934 |
| mpt2 | maps-to notation for an operation (deprecated).
We are in the process of replacing mpt2 with mpo in labels. |
df-mpo 7260 | (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) | Yes |
mpompt 7366, resmpo 7372 |
| mul | multiplication (see "t") | df-mul 10814 |
(𝐴 · 𝐵) | Yes |
mulcl 10886, divmul 11566, mulcom 10888, mulass 10890 |
| n, not | not | |
¬ 𝜑 | Yes |
nan 826, notnotr 130 |
| ne | not equal | df-ne | 𝐴 ≠ 𝐵 |
Yes | exmidne 2952, neeqtrd 3012 |
| nel | not element of | df-nel | 𝐴 ∉ 𝐵
|
Yes | neli 3050, nnel 3057 |
| ne0 | not equal to zero (see n0) | |
≠ 0 | No |
negne0d 11260, ine0 11340, gt0ne0 11370 |
| nf | "not free in" (prefix) | |
| No | nfnd 1862 |
| ngp | normed group | df-ngp 23645 |
NrmGrp | Yes | isngp 23658, ngptps 23664 |
| nm | norm (on a group or ring) | df-nm 23644 |
(norm‘𝑊) | Yes |
nmval 23651, subgnm 23695 |
| nn | positive integers | df-nn 11904 |
ℕ | Yes | nnsscn 11908, nncn 11911 |
| nn0 | nonnegative integers | df-n0 12164 |
ℕ0 | Yes | nnnn0 12170, nn0cn 12173 |
| n0 | not the empty set (see ne0) | |
≠ ∅ | No | n0i 4264, vn0 4269, ssn0 4331 |
| OLD | old, obsolete (to be removed soon) | |
| No | 19.43OLD 1887 |
| on | ordinal number | df-on 6255 |
𝐴 ∈ On | Yes |
elon 6260, 1on 8274 onelon 6276 |
| op | ordered pair | df-op 4565 |
⟨𝐴, 𝐵⟩ | Yes | dfopif 4797, opth 5385 |
| or | or | df-or 844 |
(𝜑 ∨ 𝜓) | Yes |
orcom 866, anor 979 |
| ot | ordered triple | df-ot 4567 |
⟨𝐴, 𝐵, 𝐶⟩ | Yes |
euotd 5421, fnotovb 7305 |
| ov | operation value | df-ov 7258 |
(𝐴𝐹𝐵) | Yes
| fnotovb 7305, fnovrn 7425 |
| p | plus (see "add"), for all-constant
theorems | df-add 10813 |
(3 + 2) = 5 | Yes |
3p2e5 12054 |
| pfx | prefix | df-pfx 14312 |
(𝑊 prefix 𝐿) | Yes |
pfxlen 14324, ccatpfx 14342 |
| pm | Principia Mathematica | |
| No | pm2.27 42 |
| pm | partial mapping (operation) | df-pm 8576 |
(𝐴 ↑pm 𝐵) | Yes | elpmi 8592, pmsspw 8623 |
| pr | pair | df-pr 4561 |
{𝐴, 𝐵} | Yes |
elpr 4581, prcom 4665, prid1g 4693, prnz 4710 |
| prm, prime | prime (number) | df-prm 16305 |
ℙ | Yes | 1nprm 16312, dvdsprime 16320 |
| pss | proper subset | df-pss 3902 |
𝐴 ⊊ 𝐵 | Yes | pssss 4026, sspsstri 4033 |
| q | rational numbers ("quotients") | df-q 12618 |
ℚ | Yes | elq 12619 |
| r | right | |
| No | orcd 869, simprl 767 |
| rab | restricted class abstraction |
df-rab 3072 | {𝑥 ∈ 𝐴 ∣ 𝜑} | Yes |
rabswap 3413, df-oprab 7259 |
| ral | restricted universal quantification |
df-ral 3068 | ∀𝑥 ∈ 𝐴𝜑 | Yes |
ralnex 3163, ralrnmpo 7390 |
| rcl | reverse closure | |
| No | ndmfvrcl 6787, nnarcl 8409 |
| re | real numbers | df-r 10812 |
ℝ | Yes | recn 10892, 0re 10908 |
| rel | relation | df-rel 5587 | Rel 𝐴 |
Yes | brrelex1 5631, relmpoopab 7905 |
| res | restriction | df-res 5592 |
(𝐴 ↾ 𝐵) | Yes |
opelres 5886, f1ores 6714 |
| reu | restricted existential uniqueness |
df-reu 3070 | ∃!𝑥 ∈ 𝐴𝜑 | Yes |
nfreud 3298, reurex 3352 |
| rex | restricted existential quantification |
df-rex 3069 | ∃𝑥 ∈ 𝐴𝜑 | Yes |
rexnal 3165, rexrnmpo 7391 |
| rmo | restricted "at most one" |
df-rmo 3071 | ∃*𝑥 ∈ 𝐴𝜑 | Yes |
nfrmod 3299, nrexrmo 3356 |
| rn | range | df-rn 5591 | ran 𝐴 |
Yes | elrng 5789, rncnvcnv 5832 |
| rng | (unital) ring | df-ring 19700 |
Ring | Yes |
ringidval 19654, isring 19702, ringgrp 19703 |
| rot | rotation | |
| No | 3anrot 1098, 3orrot 1090 |
| s | eliminates need for syllogism (suffix) |
| | No | ancoms 458 |
| sb | (proper) substitution (of a set) |
df-sb 2069 | [𝑦 / 𝑥]𝜑 | Yes |
spsbe 2086, sbimi 2078 |
| sbc | (proper) substitution of a class |
df-sbc 3712 | [𝐴 / 𝑥]𝜑 | Yes |
sbc2or 3720, sbcth 3726 |
| sca | scalar | df-sca 16904 |
(Scalar‘𝐻) | Yes |
resssca 16978, mgpsca 19643 |
| simp | simple, simplification | |
| No | simpl 482, simp3r3 1281 |
| sn | singleton | df-sn 4559 |
{𝐴} | Yes | eldifsn 4717 |
| sp | specialization | |
| No | spsbe 2086, spei 2394 |
| ss | subset | df-ss 3900 |
𝐴 ⊆ 𝐵 | Yes | difss 4062 |
| struct | structure | df-struct 16776 |
Struct | Yes | brstruct 16777, structfn 16785 |
| sub | subtract | df-sub 11137 |
(𝐴 − 𝐵) | Yes |
subval 11142, subaddi 11238 |
| sup | supremum | df-sup 9131 |
sup(𝐴, 𝐵, < ) | Yes |
fisupcl 9158, supmo 9141 |
| supp | support (of a function) | df-supp 7949 |
(𝐹 supp 𝑍) | Yes |
ressuppfi 9084, mptsuppd 7974 |
| swap | swap (two parts within a theorem) |
| | No | rabswap 3413, 2reuswap 3676 |
| syl | syllogism | syl 17 |
| No | 3syl 18 |
| sym | symmetric | |
| No | df-symdif 4173, cnvsym 6008 |
| symg | symmetric group | df-symg 18890 |
(SymGrp‘𝐴) | Yes |
symghash 18900, pgrpsubgsymg 18932 |
| t |
times (see "mul"), for all-constant theorems |
df-mul 10814 |
(3 · 2) = 6 | Yes |
3t2e6 12069 |
| th, t |
theorem |
|
|
No |
nfth 1805, sbcth 3726, weth 10182, ancomst 464 |
| tp | triple | df-tp 4563 |
{𝐴, 𝐵, 𝐶} | Yes |
eltpi 4620, tpeq1 4675 |
| tr | transitive | |
| No | bitrd 278, biantr 802 |
| tru, t |
true, truth |
df-tru 1542 |
⊤ |
Yes |
bitru 1548, truanfal 1573, biimt 360 |
| un | union | df-un 3888 |
(𝐴 ∪ 𝐵) | Yes |
uneqri 4081, uncom 4083 |
| unit | unit (in a ring) |
df-unit 19799 | (Unit‘𝑅) | Yes |
isunit 19814, nzrunit 20451 |
| v |
setvar (especially for specializations of
theorems when a class is replaced by a setvar variable) |
|
x |
Yes |
cv 1538, vex 3426, velpw 4535, vtoclf 3487 |
| v |
disjoint variable condition used in place of nonfreeness
hypothesis (suffix) |
|
|
No |
spimv 2390 |
| vtx |
vertex |
df-vtx 27271 |
(Vtx‘𝐺) |
Yes |
vtxval0 27312, opvtxov 27278 |
| vv |
two disjoint variable conditions used in place of nonfreeness
hypotheses (suffix) |
|
|
No |
19.23vv 1947 |
| w | weak (version of a theorem) (suffix) | |
| No | ax11w 2128, spnfw 1984 |
| wrd | word |
df-word 14146 | Word 𝑆 | Yes |
iswrdb 14151, wrdfn 14159, ffz0iswrd 14172 |
| xp | cross product (Cartesian product) |
df-xp 5586 | (𝐴 × 𝐵) | Yes |
elxp 5603, opelxpi 5617, xpundi 5646 |
| xr | eXtended reals | df-xr 10944 |
ℝ* | Yes | ressxr 10950, rexr 10952, 0xr 10953 |
| z | integers (from German "Zahlen") |
df-z 12250 | ℤ | Yes |
elz 12251, zcn 12254 |
| zn | ring of integers mod 𝑁 | df-zn 20620 |
(ℤ/nℤ‘𝑁) | Yes |
znval 20651, zncrng 20664, znhash 20678 |
| zring | ring of integers | df-zring 20583 |
ℤring | Yes | zringbas 20588, zringcrng 20584
|
| 0, z |
slashed zero (empty set) | df-nul 4254 |
∅ | Yes |
n0i 4264, vn0 4269; snnz 4709, prnz 4710 |
(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.) |
