| Description:
The following gives conventions used in the Metamath Proof Explorer
(MPE, set.mm) regarding labels.
For other conventions, see conventions 28179 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 3148"rgen.1 $e |- ( x e. A -> ph ) $."
or letters corresponding to the (main) class variable used in the
hypothesis, e.g. for mdet0 21215: "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 2748 and stirling 42394.
- 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 3215.
- 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... 15237. 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 3939, and thus its syntax label fragment is "dif". Similarly, the
subclass relation 𝐴 ⊆ 𝐵 has syntax label fragment "ss"
because it is defined in df-ss 3952. 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 4108. There are many other syntax label fragments, e.g.,
singleton construct {𝐴} has syntax label fragment "sn" (because it
is defined in df-sn 4568), and the pair construct {𝐴, 𝐵} has
fragment "pr" ( from df-pr 4570). 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 4719. An "n" is often used for negation (¬), e.g.,
nan 827.
- 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 10543) and "re" represents real numbers ℝ ( definition df-r 10547).
The empty set ∅ often uses fragment 0, even though it is defined
in df-nul 4292. The syntax construct (𝐴 + 𝐵) usually uses the
fragment "add" (which is consistent with df-add 10548), 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 11773.
- 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 15503 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 15424) we have value cosval 15476 and closure
coscl 15480.
- 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 28182 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 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 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 2661 derived from eu6 2659. 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 5342.
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 2430 (cbval 2416 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 3555.
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 586), commutes
(e.g., biimpac 481)
- 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 479, rexlimiva 3281 |
| abl | Abelian group | df-abl 18909 |
Abel | Yes | ablgrp 18911, zringabl 20621 |
| abs | absorption | | | No |
ressabs 16563 |
| abs | absolute value (of a complex number) |
df-abs 14595 | (abs‘𝐴) | Yes |
absval 14597, absneg 14637, abs1 14657 |
| ad | adding | |
| No | adantr 483, ad2antlr 725 |
| add | add (see "p") | df-add 10548 |
(𝐴 + 𝐵) | Yes |
addcl 10619, addcom 10826, addass 10624 |
| al | "for all" | |
∀𝑥𝜑 | No | alim 1811, alex 1826 |
| ALT | alternative/less preferred (suffix) | |
| No | idALT 23 |
| an | and | df-an 399 |
(𝜑 ∧ 𝜓) | Yes |
anor 979, iman 404, imnan 402 |
| ant | antecedent | |
| No | adantr 483 |
| ass | associative | |
| No | biass 388, orass 918, mulass 10625 |
| asym | asymmetric, antisymmetric | |
| No | intasym 5975, asymref 5976, posasymb 17562 |
| ax | axiom | |
| No | ax6dgen 2132, ax1cn 10571 |
| bas, base |
base (set of an extensible structure) | df-base 16489 |
(Base‘𝑆) | Yes |
baseval 16542, ressbas 16554, cnfldbas 20549 |
| b, bi | biconditional ("iff", "if and only if")
| df-bi 209 | (𝜑 ↔ 𝜓) | Yes |
impbid 214, sspwb 5342 |
| br | binary relation | df-br 5067 |
𝐴𝑅𝐵 | Yes | brab1 5114, brun 5117 |
| cbv | change bound variable | | |
No | cbvalivw 2014, cbvrex 3446 |
| cl | closure | | | No |
ifclda 4501, ovrcl 7197, zaddcl 12023 |
| cn | complex numbers | df-c 10543 |
ℂ | Yes | nnsscn 11643, nncn 11646 |
| cnfld | field of complex numbers | df-cnfld 20546 |
ℂfld | Yes | cnfldbas 20549, cnfldinv 20576 |
| cntz | centralizer | df-cntz 18447 |
(Cntz‘𝑀) | Yes |
cntzfval 18450, dprdfcntz 19137 |
| cnv | converse | df-cnv 5563 |
◡𝐴 | Yes | opelcnvg 5751, f1ocnv 6627 |
| co | composition | df-co 5564 |
(𝐴 ∘ 𝐵) | Yes | cnvco 5756, fmptco 6891 |
| com | commutative | |
| No | orcom 866, bicomi 226, eqcomi 2830 |
| con | contradiction, contraposition | |
| No | condan 816, con2d 136 |
| csb | class substitution | df-csb 3884 |
⦋𝐴 / 𝑥⦌𝐵 | Yes |
csbid 3896, csbie2g 3923 |
| cyg | cyclic group | df-cyg 18997 |
CycGrp | Yes |
iscyg 18998, zringcyg 20638 |
| d | deduction form (suffix) | |
| No | idd 24, impbid 214 |
| df | (alternate) definition (prefix) | |
| No | dfrel2 6046, dffn2 6516 |
| di, distr | distributive | |
| No |
andi 1004, imdi 393, ordi 1002, difindi 4258, ndmovdistr 7337 |
| dif | class difference | df-dif 3939 |
(𝐴 ∖ 𝐵) | Yes |
difss 4108, difindi 4258 |
| div | division | df-div 11298 |
(𝐴 / 𝐵) | Yes |
divcl 11304, divval 11300, divmul 11301 |
| dm | domain | df-dm 5565 |
dom 𝐴 | Yes | dmmpt 6094, iswrddm0 13888 |
| e, eq, equ | equals (equ for setvars, eq for
classes) | df-cleq 2814 |
𝐴 = 𝐵 | Yes |
2p2e4 11773, uneqri 4127, equtr 2028 |
| edg | edge | df-edg 26833 |
(Edg‘𝐺) | Yes |
edgopval 26836, usgredgppr 26978 |
| el | element of | |
𝐴 ∈ 𝐵 | Yes |
eldif 3946, eldifsn 4719, elssuni 4868 |
| en | equinumerous | df-en |
𝐴 ≈ 𝐵 | Yes | domen 8522, enfi 8734 |
| eu | "there exists exactly one" | eu6 2659 |
∃!𝑥𝜑 | Yes | euex 2662, euabsn 4662 |
| ex | exists (i.e. is a set) | |
∈ V | No | brrelex1 5605, 0ex 5211 |
| ex, e | "there exists (at least one)" |
df-ex 1781 |
∃𝑥𝜑 | Yes | exim 1834, alex 1826 |
| exp | export | |
| No | expt 179, expcom 416 |
| f | "not free in" (suffix) | |
| No | equs45f 2482, sbf 2271 |
| f | function | df-f 6359 |
𝐹:𝐴⟶𝐵 | Yes | fssxp 6534, opelf 6539 |
| fal | false | df-fal 1550 |
⊥ | Yes | bifal 1553, falantru 1572 |
| fi | finite intersection | df-fi 8875 |
(fi‘𝐵) | Yes | fival 8876, inelfi 8882 |
| fi, fin | finite | df-fin 8513 |
Fin | Yes |
isfi 8533, snfi 8594, onfin 8709 |
| fld | field (Note: there is an alternative
definition Fld of a field, see df-fld 35285) | df-field 19505 |
Field | Yes | isfld 19511, fldidom 20078 |
| fn | function with domain | df-fn 6358 |
𝐴 Fn 𝐵 | Yes | ffn 6514, fndm 6455 |
| frgp | free group | df-frgp 18836 |
(freeGrp‘𝐼) | Yes |
frgpval 18884, frgpadd 18889 |
| fsupp | finitely supported function |
df-fsupp 8834 | 𝑅 finSupp 𝑍 | Yes |
isfsupp 8837, fdmfisuppfi 8842, fsuppco 8865 |
| fun | function | df-fun 6357 |
Fun 𝐹 | Yes | funrel 6372, ffun 6517 |
| fv | function value | df-fv 6363 |
(𝐹‘𝐴) | Yes | fvres 6689, swrdfv 14010 |
| fz | finite set of sequential integers |
df-fz 12894 |
(𝑀...𝑁) | Yes | fzval 12895, eluzfz 12904 |
| fz0 | finite set of sequential nonnegative integers |
|
(0...𝑁) | Yes | nn0fz0 13006, fz0tp 13009 |
| fzo | half-open integer range | df-fzo 13035 |
(𝑀..^𝑁) | Yes |
elfzo 13041, elfzofz 13054 |
| g | more general (suffix); eliminates "is a set"
hypotheses | |
| No | uniexg 7466 |
| gr | graph | |
| No | uhgrf 26847, isumgr 26880, usgrres1 27097 |
| grp | group | df-grp 18106 |
Grp | Yes | isgrp 18109, tgpgrp 22686 |
| gsum | group sum | df-gsum 16716 |
(𝐺 Σg 𝐹) | Yes |
gsumval 17887, gsumwrev 18494 |
| hash | size (of a set) | df-hash 13692 |
(♯‘𝐴) | Yes |
hashgval 13694, hashfz1 13707, hashcl 13718 |
| hb | hypothesis builder (prefix) | |
| No | hbxfrbi 1825, hbald 2175, hbequid 36060 |
| hm | (monoid, group, ring) homomorphism | |
| No | ismhm 17958, isghm 18358, isrhm 19473 |
| i | inference (suffix) | |
| No | eleq1i 2903, tcsni 9185 |
| i | implication (suffix) | |
| No | brwdomi 9032, infeq5i 9099 |
| id | identity | |
| No | biid 263 |
| iedg | indexed edge | df-iedg 26784 |
(iEdg‘𝐺) | Yes |
iedgval0 26825, edgiedgb 26839 |
| idm | idempotent | |
| No | anidm 567, tpidm13 4692 |
| im, imp | implication (label often omitted) |
df-im 14460 | (𝐴 → 𝐵) | Yes |
iman 404, imnan 402, impbidd 212 |
| ima | image | df-ima 5568 |
(𝐴 “ 𝐵) | Yes | resima 5887, imaundi 6008 |
| imp | import | |
| No | biimpa 479, impcom 410 |
| in | intersection | df-in 3943 |
(𝐴 ∩ 𝐵) | Yes | elin 4169, incom 4178 |
| inf | infimum | df-inf 8907 |
inf(ℝ+, ℝ*, < ) | Yes |
fiinfcl 8965, infiso 8972 |
| is... | is (something a) ...? | |
| No | isring 19301 |
| j | joining, disjoining | |
| No | jc 163, jaoi 853 |
| l | left | |
| No | olcd 870, simpl 485 |
| map | mapping operation or set exponentiation |
df-map 8408 | (𝐴 ↑m 𝐵) | Yes |
mapvalg 8416, elmapex 8427 |
| mat | matrix | df-mat 21017 |
(𝑁 Mat 𝑅) | Yes |
matval 21020, matring 21052 |
| mdet | determinant (of a square matrix) |
df-mdet 21194 | (𝑁 maDet 𝑅) | Yes |
mdetleib 21196, mdetrlin 21211 |
| mgm | magma | df-mgm 17852 |
Magma | Yes |
mgmidmo 17870, mgmlrid 17877, ismgm 17853 |
| mgp | multiplicative group | df-mgp 19240 |
(mulGrp‘𝑅) | Yes |
mgpress 19250, ringmgp 19303 |
| mnd | monoid | df-mnd 17912 |
Mnd | Yes | mndass 17920, mndodcong 18670 |
| mo | "there exists at most one" | df-mo 2622 |
∃*𝑥𝜑 | Yes | eumo 2663, moim 2626 |
| mp | modus ponens | ax-mp 5 |
| No | mpd 15, mpi 20 |
| mpo | maps-to notation for an operation |
df-mpo 7161 | (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) | Yes |
mpompt 7266, resmpo 7272 |
| mpt | modus ponendo tollens | |
| No | mptnan 1769, mptxor 1770 |
| mpt | maps-to notation for a function |
df-mpt 5147 | (𝑥 ∈ 𝐴 ↦ 𝐵) | Yes |
fconstmpt 5614, resmpt 5905 |
| mpt2 | maps-to notation for an operation (deprecated).
We are in the process of replacing mpt2 with mpo in labels. |
df-mpo 7161 | (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) | Yes |
mpompt 7266, resmpo 7272 |
| mul | multiplication (see "t") | df-mul 10549 |
(𝐴 · 𝐵) | Yes |
mulcl 10621, divmul 11301, mulcom 10623, mulass 10625 |
| n, not | not | |
¬ 𝜑 | Yes |
nan 827, notnotr 132 |
| ne | not equal | df-ne | 𝐴 ≠ 𝐵 |
Yes | exmidne 3026, neeqtrd 3085 |
| nel | not element of | df-nel | 𝐴 ∉ 𝐵
|
Yes | neli 3125, nnel 3132 |
| ne0 | not equal to zero (see n0) | |
≠ 0 | No |
negne0d 10995, ine0 11075, gt0ne0 11105 |
| nf | "not free in" (prefix) | |
| No | nfnd 1858 |
| ngp | normed group | df-ngp 23193 |
NrmGrp | Yes | isngp 23205, ngptps 23211 |
| nm | norm (on a group or ring) | df-nm 23192 |
(norm‘𝑊) | Yes |
nmval 23199, subgnm 23242 |
| nn | positive integers | df-nn 11639 |
ℕ | Yes | nnsscn 11643, nncn 11646 |
| nn0 | nonnegative integers | df-n0 11899 |
ℕ0 | Yes | nnnn0 11905, nn0cn 11908 |
| n0 | not the empty set (see ne0) | |
≠ ∅ | No | n0i 4299, vn0 4304, ssn0 4354 |
| OLD | old, obsolete (to be removed soon) | |
| No | 19.43OLD 1884 |
| on | ordinal number | df-on 6195 |
𝐴 ∈ On | Yes |
elon 6200, 1on 8109 onelon 6216 |
| op | ordered pair | df-op 4574 |
⟨𝐴, 𝐵⟩ | Yes | dfopif 4800, opth 5368 |
| or | or | df-or 844 |
(𝜑 ∨ 𝜓) | Yes |
orcom 866, anor 979 |
| ot | ordered triple | df-ot 4576 |
⟨𝐴, 𝐵, 𝐶⟩ | Yes |
euotd 5403, fnotovb 7206 |
| ov | operation value | df-ov 7159 |
(𝐴𝐹𝐵) | Yes
| fnotovb 7206, fnovrn 7323 |
| p | plus (see "add"), for all-constant
theorems | df-add 10548 |
(3 + 2) = 5 | Yes |
3p2e5 11789 |
| pfx | prefix | df-pfx 14033 |
(𝑊 prefix 𝐿) | Yes |
pfxlen 14045, ccatpfx 14063 |
| pm | Principia Mathematica | |
| No | pm2.27 42 |
| pm | partial mapping (operation) | df-pm 8409 |
(𝐴 ↑pm 𝐵) | Yes | elpmi 8425, pmsspw 8441 |
| pr | pair | df-pr 4570 |
{𝐴, 𝐵} | Yes |
elpr 4590, prcom 4668, prid1g 4696, prnz 4712 |
| prm, prime | prime (number) | df-prm 16016 |
ℙ | Yes | 1nprm 16023, dvdsprime 16031 |
| pss | proper subset | df-pss 3954 |
𝐴 ⊊ 𝐵 | Yes | pssss 4072, sspsstri 4079 |
| q | rational numbers ("quotients") | df-q 12350 |
ℚ | Yes | elq 12351 |
| r | right | |
| No | orcd 869, simprl 769 |
| rab | restricted class abstraction |
df-rab 3147 | {𝑥 ∈ 𝐴 ∣ 𝜑} | Yes |
rabswap 3488, df-oprab 7160 |
| ral | restricted universal quantification |
df-ral 3143 | ∀𝑥 ∈ 𝐴𝜑 | Yes |
ralnex 3236, ralrnmpo 7289 |
| rcl | reverse closure | |
| No | ndmfvrcl 6701, nnarcl 8242 |
| re | real numbers | df-r 10547 |
ℝ | Yes | recn 10627, 0re 10643 |
| rel | relation | df-rel 5562 | Rel 𝐴 |
Yes | brrelex1 5605, relmpoopab 7789 |
| res | restriction | df-res 5567 |
(𝐴 ↾ 𝐵) | Yes |
opelres 5859, f1ores 6629 |
| reu | restricted existential uniqueness |
df-reu 3145 | ∃!𝑥 ∈ 𝐴𝜑 | Yes |
nfreud 3372, reurex 3431 |
| rex | restricted existential quantification |
df-rex 3144 | ∃𝑥 ∈ 𝐴𝜑 | Yes |
rexnal 3238, rexrnmpo 7290 |
| rmo | restricted "at most one" |
df-rmo 3146 | ∃*𝑥 ∈ 𝐴𝜑 | Yes |
nfrmod 3373, nrexrmo 3435 |
| rn | range | df-rn 5566 | ran 𝐴 |
Yes | elrng 5762, rncnvcnv 5804 |
| rng | (unital) ring | df-ring 19299 |
Ring | Yes |
ringidval 19253, isring 19301, ringgrp 19302 |
| rot | rotation | |
| No | 3anrot 1096, 3orrot 1088 |
| s | eliminates need for syllogism (suffix) |
| | No | ancoms 461 |
| sb | (proper) substitution (of a set) |
df-sb 2070 | [𝑦 / 𝑥]𝜑 | Yes |
spsbe 2088, sbimi 2079 |
| sbc | (proper) substitution of a class |
df-sbc 3773 | [𝐴 / 𝑥]𝜑 | Yes |
sbc2or 3781, sbcth 3787 |
| sca | scalar | df-sca 16581 |
(Scalar‘𝐻) | Yes |
resssca 16650, mgpsca 19246 |
| simp | simple, simplification | |
| No | simpl 485, simp3r3 1279 |
| sn | singleton | df-sn 4568 |
{𝐴} | Yes | eldifsn 4719 |
| sp | specialization | |
| No | spsbe 2088, spei 2412 |
| ss | subset | df-ss 3952 |
𝐴 ⊆ 𝐵 | Yes | difss 4108 |
| struct | structure | df-struct 16485 |
Struct | Yes | brstruct 16492, structfn 16500 |
| sub | subtract | df-sub 10872 |
(𝐴 − 𝐵) | Yes |
subval 10877, subaddi 10973 |
| sup | supremum | df-sup 8906 |
sup(𝐴, 𝐵, < ) | Yes |
fisupcl 8933, supmo 8916 |
| supp | support (of a function) | df-supp 7831 |
(𝐹 supp 𝑍) | Yes |
ressuppfi 8859, mptsuppd 7853 |
| swap | swap (two parts within a theorem) |
| | No | rabswap 3488, 2reuswap 3737 |
| syl | syllogism | syl 17 |
| No | 3syl 18 |
| sym | symmetric | |
| No | df-symdif 4219, cnvsym 5974 |
| symg | symmetric group | df-symg 18496 |
(SymGrp‘𝐴) | Yes |
symghash 18506, pgrpsubgsymg 18537 |
| t |
times (see "mul"), for all-constant theorems |
df-mul 10549 |
(3 · 2) = 6 | Yes |
3t2e6 11804 |
| th, t |
theorem |
|
|
No |
nfth 1802, sbcth 3787, weth 9917, ancomst 467 |
| tp | triple | df-tp 4572 |
{𝐴, 𝐵, 𝐶} | Yes |
eltpi 4625, tpeq1 4678 |
| tr | transitive | |
| No | bitrd 281, biantr 804 |
| tru, t |
true, truth |
df-tru 1540 |
⊤ |
Yes |
bitru 1546, truanfal 1571, biimt 363 |
| un | union | df-un 3941 |
(𝐴 ∪ 𝐵) | Yes |
uneqri 4127, uncom 4129 |
| unit | unit (in a ring) |
df-unit 19392 | (Unit‘𝑅) | Yes |
isunit 19407, nzrunit 20040 |
| v |
setvar (especially for specializations of
theorems when a class is replaced by a setvar variable) |
|
x |
Yes |
cv 1536, vex 3497, velpw 4544, vtoclf 3558 |
| v |
disjoint variable condition used in place of nonfreeness
hypothesis (suffix) |
|
|
No |
spimv 2408 |
| vtx |
vertex |
df-vtx 26783 |
(Vtx‘𝐺) |
Yes |
vtxval0 26824, opvtxov 26790 |
| 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 2134, spnfw 1984 |
| wrd | word |
df-word 13863 | Word 𝑆 | Yes |
iswrdb 13868, wrdfn 13877, ffz0iswrd 13891 |
| xp | cross product (Cartesian product) |
df-xp 5561 | (𝐴 × 𝐵) | Yes |
elxp 5578, opelxpi 5592, xpundi 5620 |
| xr | eXtended reals | df-xr 10679 |
ℝ* | Yes | ressxr 10685, rexr 10687, 0xr 10688 |
| z | integers (from German "Zahlen") |
df-z 11983 | ℤ | Yes |
elz 11984, zcn 11987 |
| zn | ring of integers mod 𝑁 | df-zn 20654 |
(ℤ/nℤ‘𝑁) | Yes |
znval 20682, zncrng 20691, znhash 20705 |
| zring | ring of integers | df-zring 20618 |
ℤring | Yes | zringbas 20623, zringcrng 20619
|
| 0, z |
slashed zero (empty set) | df-nul 4292 |
∅ | Yes |
n0i 4299, vn0 4304; snnz 4711, prnz 4712 |
(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.) |
