Description:
The following gives conventions used in the Metamath Proof Explorer
(MPE, set.mm) regarding labels.
For other conventions, see conventions 30197 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 3058"rgen.1 $e |- ( x e. A -> ph ) $."
or letters corresponding to the (main) class variable used in the
hypothesis, e.g., for mdet0 22495: "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 2653 and stirling 45400.
- 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 1834, and the restricted quantifier version of Theorem 21 from
Section 19 of [Margaris] p. 90 is labeled r19.21 3246.
- 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... 15851. 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 3947, and thus its syntax label fragment is "dif". Similarly, the
subclass relation π΄ β π΅ has syntax label fragment "ss"
because it is defined in df-ss 3961. 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 4127. There are many other syntax label fragments, e.g.,
singleton construct {π΄} has syntax label fragment "sn" (because it
is defined in df-sn 4625), and the pair construct {π΄, π΅} has
fragment "pr" ( from df-pr 4627). 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 4786. 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 11136) and "re" represents real numbers β (Definition df-r 11140).
The empty set β
often uses fragment 0, even though it is defined
in df-nul 4319. The syntax construct (π΄ + π΅) usually uses the
fragment "add" (which is consistent with df-add 11141), 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 12369.
- 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 16118 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 16038) we have value cosval 16091 and
closure coscl 16095.
- 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 30200 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 1935 versus 19.21 2193. This
often permits to prove the result using fewer axioms, and/or to
eliminate a nonfreeness hypothesis (such as β²π₯π in 19.21 2193).
If no constraint is put on axiom use, then the v-version can be proved
from the original theorem using nfv 1910. If two (resp. three) such
disjoint variable conditions are added, then the suffix "vv" (resp.
"vvv") is used, e.g., exlimivv 1928.
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 2565 derived from eu6 2563. 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 5445.
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 2403 (cbval 2392 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 3542.
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 3142 |
abl | Abelian group | df-abl 19729 |
Abel | Yes | ablgrp 19731, zringabl 21364 |
abs | absorption | | | No |
ressabs 17221 |
abs | absolute value (of a complex number) |
df-abs 15207 | (absβπ΄) | Yes |
absval 15209, absneg 15248, abs1 15268 |
ad | adding | |
| No | adantr 480, ad2antlr 726 |
add | add (see "p") | df-add 11141 |
(π΄ + π΅) | Yes |
addcl 11212, addcom 11422, addass 11217 |
al | "for all" | |
βπ₯π | No | alim 1805, alex 1821 |
ALT | alternative/less preferred (suffix) | |
| No | idALT 23 |
an | and | df-an 396 |
(π β§ π) | Yes |
anor 981, iman 401, imnan 399 |
ant | antecedent | |
| No | adantr 480 |
ass | associative | |
| No | biass 384, orass 920, mulass 11218 |
asym | asymmetric, antisymmetric | |
| No | intasym 6115, asymref 6116, posasymb 18302 |
ax | axiom | |
| No | ax6dgen 2117, ax1cn 11164 |
bas, base |
base (set of an extensible structure) | df-base 17172 |
(Baseβπ) | Yes |
baseval 17173, ressbas 17206, cnfldbas 21270 |
b, bi | biconditional ("iff", "if and only if")
| df-bi 206 | (π β π) | Yes |
impbid 211, sspwb 5445 |
br | binary relation | df-br 5143 |
π΄π
π΅ | Yes | brab1 5190, brun 5193 |
c | commutes, commuted (suffix) | | |
No | biimpac 478 |
c | contraction (suffix) | | |
No | sylc 65, syl2anc 583 |
cbv | change bound variable | | |
No | cbvalivw 2003, cbvrex 3354 |
cdm | codomain | |
| No | ffvelcdm 7085, focdmex 7953 |
cl | closure | | | No |
ifclda 4559, ovrcl 7455, zaddcl 12624 |
cn | complex numbers | df-c 11136 |
β | Yes | nnsscn 12239, nncn 12242 |
cnfld | field of complex numbers | df-cnfld 21267 |
βfld | Yes | cnfldbas 21270, cnfldinv 21317 |
cntz | centralizer | df-cntz 19259 |
(Cntzβπ) | Yes |
cntzfval 19262, dprdfcntz 19963 |
cnv | converse | df-cnv 5680 |
β‘π΄ | Yes | opelcnvg 5877, f1ocnv 6845 |
co | composition | df-co 5681 |
(π΄ β π΅) | Yes | cnvco 5882, fmptco 7132 |
com | commutative | |
| No | orcom 869, bicomi 223, eqcomi 2736 |
con | contradiction, contraposition | |
| No | condan 817, con2d 134 |
csb | class substitution | df-csb 3890 |
β¦π΄ / π₯β¦π΅ | Yes |
csbid 3902, csbie2g 3932 |
cyg | cyclic group | df-cyg 19824 |
CycGrp | Yes |
iscyg 19825, zringcyg 21382 |
d | deduction form (suffix) | |
| No | idd 24, impbid 211 |
df | (alternate) definition (prefix) | |
| No | dfrel2 6187, dffn2 6718 |
di, distr | distributive | |
| No |
andi 1006, imdi 389, ordi 1004, difindi 4277, ndmovdistr 7604 |
dif | class difference | df-dif 3947 |
(π΄ β π΅) | Yes |
difss 4127, difindi 4277 |
div | division | df-div 11894 |
(π΄ / π΅) | Yes |
divcl 11900, divval 11896, divmul 11897 |
dm | domain | df-dm 5682 |
dom π΄ | Yes | dmmpt 6238, iswrddm0 14512 |
e, eq, equ | equals (equ for setvars, eq for
classes) | df-cleq 2719 |
π΄ = π΅ | Yes |
2p2e4 12369, uneqri 4147, equtr 2017 |
edg | edge | df-edg 28848 |
(EdgβπΊ) | Yes |
edgopval 28851, usgredgppr 28996 |
el | element of | |
π΄ β π΅ | Yes |
eldif 3954, eldifsn 4786, elssuni 4935 |
en | equinumerous | df-en |
π΄ β π΅ | Yes | domen 8973, enfi 9206 |
eu | "there exists exactly one" | eu6 2563 |
β!π₯π | Yes | euex 2566, euabsn 4726 |
ex | exists (i.e. is a set) | |
β V | No | brrelex1 5725, 0ex 5301 |
ex, e | "there exists (at least one)" |
df-ex 1775 |
βπ₯π | Yes | exim 1829, alex 1821 |
exp | export | |
| No | expt 177, expcom 413 |
f | "not free in" (suffix) | |
| No | equs45f 2453, sbf 2255 |
f | function | df-f 6546 |
πΉ:π΄βΆπ΅ | Yes | fssxp 6745, opelf 6752 |
fal | false | df-fal 1547 |
β₯ | Yes | bifal 1550, falantru 1569 |
fi | finite intersection | df-fi 9426 |
(fiβπ΅) | Yes | fival 9427, inelfi 9433 |
fi, fin | finite | df-fin 8959 |
Fin | Yes |
isfi 8988, snfi 9060, onfin 9246 |
fld | field (Note: there is an alternative
definition Fld of a field, see df-fld 37400) | df-field 20616 |
Field | Yes | isfld 20624, fldidom 21245 |
fn | function with domain | df-fn 6545 |
π΄ Fn π΅ | Yes | ffn 6716, fndm 6651 |
frgp | free group | df-frgp 19656 |
(freeGrpβπΌ) | Yes |
frgpval 19704, frgpadd 19709 |
fsupp | finitely supported function |
df-fsupp 9378 | π
finSupp π | Yes |
isfsupp 9381, fdmfisuppfi 9389, fsuppco 9417 |
fun | function | df-fun 6544 |
Fun πΉ | Yes | funrel 6564, ffun 6719 |
fv | function value | df-fv 6550 |
(πΉβπ΄) | Yes | fvres 6910, swrdfv 14622 |
fz | finite set of sequential integers |
df-fz 13509 |
(π...π) | Yes | fzval 13510, eluzfz 13520 |
fz0 | finite set of sequential nonnegative integers |
|
(0...π) | Yes | nn0fz0 13623, fz0tp 13626 |
fzo | half-open integer range | df-fzo 13652 |
(π..^π) | Yes |
elfzo 13658, elfzofz 13672 |
g | more general (suffix); eliminates "is a set"
hypotheses | |
| No | uniexg 7739 |
gr | graph | |
| No | uhgrf 28862, isumgr 28895, usgrres1 29115 |
grp | group | df-grp 18884 |
Grp | Yes | isgrp 18887, tgpgrp 23969 |
gsum | group sum | df-gsum 17415 |
(πΊ Ξ£g πΉ) | Yes |
gsumval 18628, gsumwrev 19311 |
hash | size (of a set) | df-hash 14314 |
(β―βπ΄) | Yes |
hashgval 14316, hashfz1 14329, hashcl 14339 |
hb | hypothesis builder (prefix) | |
| No | hbxfrbi 1820, hbald 2161, hbequid 38318 |
hm | (monoid, group, ring, ...) homomorphism |
| | No |
ismhm 18733, isghm 19161, isrhm 20406 |
i | inference (suffix) | |
| No | eleq1i 2819, tcsni 9758 |
i | implication (suffix) | |
| No | brwdomi 9583, infeq5i 9651 |
id | identity | |
| No | biid 261 |
iedg | indexed edge | df-iedg 28799 |
(iEdgβπΊ) | Yes |
iedgval0 28840, edgiedgb 28854 |
idm | idempotent | |
| No | anidm 564, tpidm13 4756 |
im, imp | implication (label often omitted) |
df-im 15072 | (π΄ β π΅) | Yes |
iman 401, imnan 399, impbidd 209 |
im | (group, ring, ...) isomorphism | |
| No | isgim 19207, rimrcl 20410 |
ima | image | df-ima 5685 |
(π΄ β π΅) | Yes | resima 6013, imaundi 6148 |
imp | import | |
| No | biimpa 476, impcom 407 |
in | intersection | df-in 3951 |
(π΄ β© π΅) | Yes | elin 3960, incom 4197 |
inf | infimum | df-inf 9458 |
inf(β+, β*, < ) | Yes |
fiinfcl 9516, infiso 9523 |
is... | is (something a) ...? | |
| No | isring 20168 |
j | joining, disjoining | |
| No | jc 161, jaoi 856 |
l | left | |
| No | olcd 873, simpl 482 |
map | mapping operation or set exponentiation |
df-map 8838 | (π΄ βm π΅) | Yes |
mapvalg 8846, elmapex 8858 |
mat | matrix | df-mat 22295 |
(π Mat π
) | Yes |
matval 22298, matring 22332 |
mdet | determinant (of a square matrix) |
df-mdet 22474 | (π maDet π
) | Yes |
mdetleib 22476, mdetrlin 22491 |
mgm | magma | df-mgm 18591 |
Magma | Yes |
mgmidmo 18611, mgmlrid 18618, ismgm 18592 |
mgp | multiplicative group | df-mgp 20066 |
(mulGrpβπ
) | Yes |
mgpress 20080, ringmgp 20170 |
mnd | monoid | df-mnd 18686 |
Mnd | Yes | mndass 18694, mndodcong 19488 |
mo | "there exists at most one" | df-mo 2529 |
β*π₯π | Yes | eumo 2567, moim 2533 |
mp | modus ponens | ax-mp 5 |
| No | mpd 15, mpi 20 |
mpo | maps-to notation for an operation |
df-mpo 7419 | (π₯ β π΄, π¦ β π΅ β¦ πΆ) | Yes |
mpompt 7528, resmpo 7534 |
mpt | modus ponendo tollens | |
| No | mptnan 1763, mptxor 1764 |
mpt | maps-to notation for a function |
df-mpt 5226 | (π₯ β π΄ β¦ π΅) | Yes |
fconstmpt 5734, resmpt 6035 |
mpt2 | maps-to notation for an operation (deprecated).
We are in the process of replacing mpt2 with mpo in labels. |
df-mpo 7419 | (π₯ β π΄, π¦ β π΅ β¦ πΆ) | Yes |
mpompt 7528, resmpo 7534 |
mul | multiplication (see "t") | df-mul 11142 |
(π΄ Β· π΅) | Yes |
mulcl 11214, divmul 11897, mulcom 11216, mulass 11218 |
n, not | not | |
Β¬ π | Yes |
nan 829, notnotr 130 |
ne | not equal | df-ne | π΄ β π΅ |
Yes | exmidne 2945, neeqtrd 3005 |
nel | not element of | df-nel | π΄ β π΅
|
Yes | neli 3043, nnel 3051 |
ne0 | not equal to zero (see n0) | |
β 0 | No |
negne0d 11591, ine0 11671, gt0ne0 11701 |
nf | "not free in" (prefix) | df-nf 1779 |
β²π₯π | Yes | nfnd 1854 |
ngp | normed group | df-ngp 24479 |
NrmGrp | Yes | isngp 24492, ngptps 24498 |
nm | norm (on a group or ring) | df-nm 24478 |
(normβπ) | Yes |
nmval 24485, subgnm 24529 |
nn | positive integers | df-nn 12235 |
β | Yes | nnsscn 12239, nncn 12242 |
nn0 | nonnegative integers | df-n0 12495 |
β0 | Yes | nnnn0 12501, nn0cn 12504 |
n0 | not the empty set (see ne0) | |
β β
| No | n0i 4329, vn0 4334, ssn0 4396 |
OLD | old, obsolete (to be removed soon) | |
| No | 19.43OLD 1879 |
on | ordinal number | df-on 6367 |
π΄ β On | Yes |
elon 6372, 1on 8492 onelon 6388 |
op | ordered pair | df-op 4631 |
β¨π΄, π΅β© | Yes | dfopif 4866, opth 5472 |
or | or | df-or 847 |
(π β¨ π) | Yes |
orcom 869, anor 981 |
ot | ordered triple | df-ot 4633 |
β¨π΄, π΅, πΆβ© | Yes |
euotd 5509, fnotovb 7464 |
ov | operation value | df-ov 7417 |
(π΄πΉπ΅) | Yes
| fnotovb 7464, fnovrn 7590 |
p | plus (see "add"), for all-constant
theorems | df-add 11141 |
(3 + 2) = 5 | Yes |
3p2e5 12385 |
pfx | prefix | df-pfx 14645 |
(π prefix πΏ) | Yes |
pfxlen 14657, ccatpfx 14675 |
pm | Principia Mathematica | |
| No | pm2.27 42 |
pm | partial mapping (operation) | df-pm 8839 |
(π΄ βpm π΅) | Yes | elpmi 8856, pmsspw 8887 |
pr | pair | df-pr 4627 |
{π΄, π΅} | Yes |
elpr 4647, prcom 4732, prid1g 4760, prnz 4777 |
prm, prime | prime (number) | df-prm 16634 |
β | Yes | 1nprm 16641, dvdsprime 16649 |
pss | proper subset | df-pss 3963 |
π΄ β π΅ | Yes | pssss 4091, sspsstri 4098 |
q | rational numbers ("quotients") | df-q 12955 |
β | Yes | elq 12956 |
r | reversed (suffix) | |
| No | pm4.71r 558, caovdir 7649 |
r | right | |
| No | orcd 872, simprl 770 |
rab | restricted class abstraction |
df-rab 3428 | {π₯ β π΄ β£ π} | Yes |
rabswap 3436, df-oprab 7418 |
ral | restricted universal quantification |
df-ral 3057 | βπ₯ β π΄π | Yes |
ralnex 3067, ralrnmpo 7554 |
rcl | reverse closure | |
| No | ndmfvrcl 6927, nnarcl 8630 |
re | real numbers | df-r 11140 |
β | Yes | recn 11220, 0re 11238 |
rel | relation | df-rel 5679 | Rel π΄ |
Yes | brrelex1 5725, relmpoopab 8093 |
res | restriction | df-res 5684 |
(π΄ βΎ π΅) | Yes |
opelres 5985, f1ores 6847 |
reu | restricted existential uniqueness |
df-reu 3372 | β!π₯ β π΄π | Yes |
nfreud 3424, reurex 3375 |
rex | restricted existential quantification |
df-rex 3066 | βπ₯ β π΄π | Yes |
rexnal 3095, rexrnmpo 7555 |
rmo | restricted "at most one" |
df-rmo 3371 | β*π₯ β π΄π | Yes |
nfrmod 3423, nrexrmo 3392 |
rn | range | df-rn 5683 | ran π΄ |
Yes | elrng 5888, rncnvcnv 5930 |
ring | (unital) ring | df-ring 20166 |
Ring | Yes |
ringidval 20114, isring 20168, ringgrp 20169 |
rng | non-unital ring | df-rng 20084 |
Rng | Yes |
isrng 20085, rngabl 20086, rnglz 20096 |
rot | rotation | |
| No | 3anrot 1098, 3orrot 1090 |
s | eliminates need for syllogism (suffix) |
| | No | ancoms 458 |
sb | (proper) substitution (of a set) |
df-sb 2061 | [π¦ / π₯]π | Yes |
spsbe 2078, sbimi 2070 |
sbc | (proper) substitution of a class |
df-sbc 3775 | [π΄ / π₯]π | Yes |
sbc2or 3783, sbcth 3789 |
sca | scalar | df-sca 17240 |
(Scalarβπ») | Yes |
resssca 17315, mgpsca 20073 |
simp | simple, simplification | |
| No | simpl 482, simp3r3 1281 |
sn | singleton | df-sn 4625 |
{π΄} | Yes | eldifsn 4786 |
sp | specialization | |
| No | spsbe 2078, spei 2388 |
ss | subset | df-ss 3961 |
π΄ β π΅ | Yes | difss 4127 |
struct | structure | df-struct 17107 |
Struct | Yes | brstruct 17108, structfn 17116 |
sub | subtract | df-sub 11468 |
(π΄ β π΅) | Yes |
subval 11473, subaddi 11569 |
sup | supremum | df-sup 9457 |
sup(π΄, π΅, < ) | Yes |
fisupcl 9484, supmo 9467 |
supp | support (of a function) | df-supp 8160 |
(πΉ supp π) | Yes |
ressuppfi 9410, mptsuppd 8185 |
swap | swap (two parts within a theorem) |
| | No | rabswap 3436, 2reuswap 3739 |
syl | syllogism | syl 17 |
| No | 3syl 18 |
sym | symmetric | |
| No | df-symdif 4238, cnvsym 6112 |
symg | symmetric group | df-symg 19313 |
(SymGrpβπ΄) | Yes |
symghash 19323, pgrpsubgsymg 19355 |
t |
times (see "mul"), for all-constant theorems |
df-mul 11142 |
(3 Β· 2) = 6 | Yes |
3t2e6 12400 |
th, t |
theorem |
|
|
No |
nfth 1796, sbcth 3789, weth 10510, ancomst 464 |
tp | triple | df-tp 4629 |
{π΄, π΅, πΆ} | Yes |
eltpi 4687, tpeq1 4742 |
tr | transitive | |
| No | bitrd 279, biantr 805 |
tru, t |
true, truth |
df-tru 1537 |
β€ |
Yes |
bitru 1543, truanfal 1568, biimt 360 |
un | union | df-un 3949 |
(π΄ βͺ π΅) | Yes |
uneqri 4147, uncom 4149 |
unit | unit (in a ring) |
df-unit 20286 | (Unitβπ
) | Yes |
isunit 20301, nzrunit 20450 |
v |
setvar (especially for specializations of
theorems when a class is replaced by a setvar variable) |
|
x |
Yes |
cv 1533, vex 3473, velpw 4603, vtoclf 3547 |
v |
disjoint variable condition used in place of nonfreeness
hypothesis (suffix) |
|
|
No |
spimv 2384 |
vtx |
vertex |
df-vtx 28798 |
(VtxβπΊ) |
Yes |
vtxval0 28839, opvtxov 28805 |
vv |
two disjoint variable conditions used in place of nonfreeness
hypotheses (suffix) |
|
|
No |
19.23vv 1939 |
w | weak (version of a theorem) (suffix) | |
| No | ax11w 2119, spnfw 1976 |
wrd | word |
df-word 14489 | Word π | Yes |
iswrdb 14494, wrdfn 14502, ffz0iswrd 14515 |
xp | cross product (Cartesian product) |
df-xp 5678 | (π΄ Γ π΅) | Yes |
elxp 5695, opelxpi 5709, xpundi 5740 |
xr | eXtended reals | df-xr 11274 |
β* | Yes | ressxr 11280, rexr 11282, 0xr 11283 |
z | integers (from German "Zahlen") |
df-z 12581 | β€ | Yes |
elz 12582, zcn 12585 |
zn | ring of integers mod π | df-zn 21419 |
(β€/nβ€βπ) | Yes |
znval 21452, zncrng 21465, znhash 21479 |
zring | ring of integers | df-zring 21360 |
β€ring | Yes | zringbas 21366, zringcrng 21361
|
0, z |
slashed zero (empty set) | df-nul 4319 |
β
| Yes |
n0i 4329, vn0 4334; snnz 4776, prnz 4777 |
(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.) |