Description:
The following gives conventions used in the Metamath Proof Explorer
(MPE, set.mm) regarding labels.
For other conventions, see conventions 29386 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 3067"rgen.1 $e |- ( x e. A -> ph ) $."
or letters corresponding to the (main) class variable used in the
hypothesis, e.g., for mdet0 21971: "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 2663 and stirling 44404.
- 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 3240.
- 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... 15773. 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 3918, and thus its syntax label fragment is "dif". Similarly, the
subclass relation π΄ β π΅ has syntax label fragment "ss"
because it is defined in df-ss 3932. 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 4096. There are many other syntax label fragments, e.g.,
singleton construct {π΄} has syntax label fragment "sn" (because it
is defined in df-sn 4592), and the pair construct {π΄, π΅} has
fragment "pr" ( from df-pr 4594). 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 4752. 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 11064) and "re" represents real numbers β (Definition df-r 11068).
The empty set β
often uses fragment 0, even though it is defined
in df-nul 4288. The syntax construct (π΄ + π΅) usually uses the
fragment "add" (which is consistent with df-add 11069), 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 12295.
- 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 16039 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 15960) we have value cosval 16012 and
closure coscl 16016.
- 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 29389 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 2201. This
often permits to prove the result using fewer axioms, and/or to
eliminate a nonfreeness hypothesis (such as β²π₯π in 19.21 2201).
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 2575 derived from eu6 2573. The "f" stands
for "not free in" which is less restrictive than "does not occur in."
The suffix "b" often means "biconditional" (β, "iff" , "if and
only if"), e.g., sspwb 5411.
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 2408 (cbval 2397 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 3513.
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 585), commutes
(e.g., biimpac 480)
- 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 478, rexlimiva 3145 |
abl | Abelian group | df-abl 19572 |
Abel | Yes | ablgrp 19574, zringabl 20889 |
abs | absorption | | | No |
ressabs 17137 |
abs | absolute value (of a complex number) |
df-abs 15128 | (absβπ΄) | Yes |
absval 15130, absneg 15169, abs1 15189 |
ad | adding | |
| No | adantr 482, ad2antlr 726 |
add | add (see "p") | df-add 11069 |
(π΄ + π΅) | Yes |
addcl 11140, addcom 11348, addass 11145 |
al | "for all" | |
βπ₯π | No | alim 1813, alex 1829 |
ALT | alternative/less preferred (suffix) | |
| No | idALT 23 |
an | and | df-an 398 |
(π β§ π) | Yes |
anor 982, iman 403, imnan 401 |
ant | antecedent | |
| No | adantr 482 |
ass | associative | |
| No | biass 386, orass 921, mulass 11146 |
asym | asymmetric, antisymmetric | |
| No | intasym 6074, asymref 6075, posasymb 18215 |
ax | axiom | |
| No | ax6dgen 2125, ax1cn 11092 |
bas, base |
base (set of an extensible structure) | df-base 17091 |
(Baseβπ) | Yes |
baseval 17092, ressbas 17125, cnfldbas 20816 |
b, bi | biconditional ("iff", "if and only if")
| df-bi 206 | (π β π) | Yes |
impbid 211, sspwb 5411 |
br | binary relation | df-br 5111 |
π΄π
π΅ | Yes | brab1 5158, brun 5161 |
cbv | change bound variable | | |
No | cbvalivw 2011, cbvrex 3339 |
cdm | codomain | |
| No | ffvelcdm 7037, focdmex 7893 |
cl | closure | | | No |
ifclda 4526, ovrcl 7403, zaddcl 12550 |
cn | complex numbers | df-c 11064 |
β | Yes | nnsscn 12165, nncn 12168 |
cnfld | field of complex numbers | df-cnfld 20813 |
βfld | Yes | cnfldbas 20816, cnfldinv 20844 |
cntz | centralizer | df-cntz 19104 |
(Cntzβπ) | Yes |
cntzfval 19107, dprdfcntz 19801 |
cnv | converse | df-cnv 5646 |
β‘π΄ | Yes | opelcnvg 5841, f1ocnv 6801 |
co | composition | df-co 5647 |
(π΄ β π΅) | Yes | cnvco 5846, fmptco 7080 |
com | commutative | |
| No | orcom 869, bicomi 223, eqcomi 2746 |
con | contradiction, contraposition | |
| No | condan 817, con2d 134 |
csb | class substitution | df-csb 3861 |
β¦π΄ / π₯β¦π΅ | Yes |
csbid 3873, csbie2g 3903 |
cyg | cyclic group | df-cyg 19662 |
CycGrp | Yes |
iscyg 19663, zringcyg 20906 |
d | deduction form (suffix) | |
| No | idd 24, impbid 211 |
df | (alternate) definition (prefix) | |
| No | dfrel2 6146, dffn2 6675 |
di, distr | distributive | |
| No |
andi 1007, imdi 391, ordi 1005, difindi 4246, ndmovdistr 7548 |
dif | class difference | df-dif 3918 |
(π΄ β π΅) | Yes |
difss 4096, difindi 4246 |
div | division | df-div 11820 |
(π΄ / π΅) | Yes |
divcl 11826, divval 11822, divmul 11823 |
dm | domain | df-dm 5648 |
dom π΄ | Yes | dmmpt 6197, iswrddm0 14433 |
e, eq, equ | equals (equ for setvars, eq for
classes) | df-cleq 2729 |
π΄ = π΅ | Yes |
2p2e4 12295, uneqri 4116, equtr 2025 |
edg | edge | df-edg 28041 |
(EdgβπΊ) | Yes |
edgopval 28044, usgredgppr 28186 |
el | element of | |
π΄ β π΅ | Yes |
eldif 3925, eldifsn 4752, elssuni 4903 |
en | equinumerous | df-en |
π΄ β π΅ | Yes | domen 8908, enfi 9141 |
eu | "there exists exactly one" | eu6 2573 |
β!π₯π | Yes | euex 2576, euabsn 4692 |
ex | exists (i.e. is a set) | |
β V | No | brrelex1 5690, 0ex 5269 |
ex, e | "there exists (at least one)" |
df-ex 1783 |
βπ₯π | Yes | exim 1837, alex 1829 |
exp | export | |
| No | expt 177, expcom 415 |
f | "not free in" (suffix) | |
| No | equs45f 2458, sbf 2263 |
f | function | df-f 6505 |
πΉ:π΄βΆπ΅ | Yes | fssxp 6701, opelf 6708 |
fal | false | df-fal 1555 |
β₯ | Yes | bifal 1558, falantru 1577 |
fi | finite intersection | df-fi 9354 |
(fiβπ΅) | Yes | fival 9355, inelfi 9361 |
fi, fin | finite | df-fin 8894 |
Fin | Yes |
isfi 8923, snfi 8995, onfin 9181 |
fld | field (Note: there is an alternative
definition Fld of a field, see df-fld 36480) | df-field 20202 |
Field | Yes | isfld 20210, fldidom 20791 |
fn | function with domain | df-fn 6504 |
π΄ Fn π΅ | Yes | ffn 6673, fndm 6610 |
frgp | free group | df-frgp 19499 |
(freeGrpβπΌ) | Yes |
frgpval 19547, frgpadd 19552 |
fsupp | finitely supported function |
df-fsupp 9313 | π
finSupp π | Yes |
isfsupp 9316, fdmfisuppfi 9321, fsuppco 9345 |
fun | function | df-fun 6503 |
Fun πΉ | Yes | funrel 6523, ffun 6676 |
fv | function value | df-fv 6509 |
(πΉβπ΄) | Yes | fvres 6866, swrdfv 14543 |
fz | finite set of sequential integers |
df-fz 13432 |
(π...π) | Yes | fzval 13433, eluzfz 13443 |
fz0 | finite set of sequential nonnegative integers |
|
(0...π) | Yes | nn0fz0 13546, fz0tp 13549 |
fzo | half-open integer range | df-fzo 13575 |
(π..^π) | Yes |
elfzo 13581, elfzofz 13595 |
g | more general (suffix); eliminates "is a set"
hypotheses | |
| No | uniexg 7682 |
gr | graph | |
| No | uhgrf 28055, isumgr 28088, usgrres1 28305 |
grp | group | df-grp 18758 |
Grp | Yes | isgrp 18761, tgpgrp 23445 |
gsum | group sum | df-gsum 17331 |
(πΊ Ξ£g πΉ) | Yes |
gsumval 18539, gsumwrev 19154 |
hash | size (of a set) | df-hash 14238 |
(β―βπ΄) | Yes |
hashgval 14240, hashfz1 14253, hashcl 14263 |
hb | hypothesis builder (prefix) | |
| No | hbxfrbi 1828, hbald 2169, hbequid 37400 |
hm | (monoid, group, ring) homomorphism | |
| No | ismhm 18610, isghm 19015, isrhm 20161 |
i | inference (suffix) | |
| No | eleq1i 2829, tcsni 9686 |
i | implication (suffix) | |
| No | brwdomi 9511, infeq5i 9579 |
id | identity | |
| No | biid 261 |
iedg | indexed edge | df-iedg 27992 |
(iEdgβπΊ) | Yes |
iedgval0 28033, edgiedgb 28047 |
idm | idempotent | |
| No | anidm 566, tpidm13 4722 |
im, imp | implication (label often omitted) |
df-im 14993 | (π΄ β π΅) | Yes |
iman 403, imnan 401, impbidd 209 |
ima | image | df-ima 5651 |
(π΄ β π΅) | Yes | resima 5976, imaundi 6107 |
imp | import | |
| No | biimpa 478, impcom 409 |
in | intersection | df-in 3922 |
(π΄ β© π΅) | Yes | elin 3931, incom 4166 |
inf | infimum | df-inf 9386 |
inf(β+, β*, < ) | Yes |
fiinfcl 9444, infiso 9451 |
is... | is (something a) ...? | |
| No | isring 19975 |
j | joining, disjoining | |
| No | jc 161, jaoi 856 |
l | left | |
| No | olcd 873, simpl 484 |
map | mapping operation or set exponentiation |
df-map 8774 | (π΄ βm π΅) | Yes |
mapvalg 8782, elmapex 8793 |
mat | matrix | df-mat 21771 |
(π Mat π
) | Yes |
matval 21774, matring 21808 |
mdet | determinant (of a square matrix) |
df-mdet 21950 | (π maDet π
) | Yes |
mdetleib 21952, mdetrlin 21967 |
mgm | magma | df-mgm 18504 |
Magma | Yes |
mgmidmo 18522, mgmlrid 18529, ismgm 18505 |
mgp | multiplicative group | df-mgp 19904 |
(mulGrpβπ
) | Yes |
mgpress 19918, ringmgp 19977 |
mnd | monoid | df-mnd 18564 |
Mnd | Yes | mndass 18572, mndodcong 19331 |
mo | "there exists at most one" | df-mo 2539 |
β*π₯π | Yes | eumo 2577, moim 2543 |
mp | modus ponens | ax-mp 5 |
| No | mpd 15, mpi 20 |
mpo | maps-to notation for an operation |
df-mpo 7367 | (π₯ β π΄, π¦ β π΅ β¦ πΆ) | Yes |
mpompt 7475, resmpo 7481 |
mpt | modus ponendo tollens | |
| No | mptnan 1771, mptxor 1772 |
mpt | maps-to notation for a function |
df-mpt 5194 | (π₯ β π΄ β¦ π΅) | Yes |
fconstmpt 5699, resmpt 5996 |
mpt2 | maps-to notation for an operation (deprecated).
We are in the process of replacing mpt2 with mpo in labels. |
df-mpo 7367 | (π₯ β π΄, π¦ β π΅ β¦ πΆ) | Yes |
mpompt 7475, resmpo 7481 |
mul | multiplication (see "t") | df-mul 11070 |
(π΄ Β· π΅) | Yes |
mulcl 11142, divmul 11823, mulcom 11144, mulass 11146 |
n, not | not | |
Β¬ π | Yes |
nan 829, notnotr 130 |
ne | not equal | df-ne | π΄ β π΅ |
Yes | exmidne 2954, neeqtrd 3014 |
nel | not element of | df-nel | π΄ β π΅
|
Yes | neli 3052, nnel 3059 |
ne0 | not equal to zero (see n0) | |
β 0 | No |
negne0d 11517, ine0 11597, gt0ne0 11627 |
nf | "not free in" (prefix) | |
| No | nfnd 1862 |
ngp | normed group | df-ngp 23955 |
NrmGrp | Yes | isngp 23968, ngptps 23974 |
nm | norm (on a group or ring) | df-nm 23954 |
(normβπ) | Yes |
nmval 23961, subgnm 24005 |
nn | positive integers | df-nn 12161 |
β | Yes | nnsscn 12165, nncn 12168 |
nn0 | nonnegative integers | df-n0 12421 |
β0 | Yes | nnnn0 12427, nn0cn 12430 |
n0 | not the empty set (see ne0) | |
β β
| No | n0i 4298, vn0 4303, ssn0 4365 |
OLD | old, obsolete (to be removed soon) | |
| No | 19.43OLD 1887 |
on | ordinal number | df-on 6326 |
π΄ β On | Yes |
elon 6331, 1on 8429 onelon 6347 |
op | ordered pair | df-op 4598 |
β¨π΄, π΅β© | Yes | dfopif 4832, opth 5438 |
or | or | df-or 847 |
(π β¨ π) | Yes |
orcom 869, anor 982 |
ot | ordered triple | df-ot 4600 |
β¨π΄, π΅, πΆβ© | Yes |
euotd 5475, fnotovb 7412 |
ov | operation value | df-ov 7365 |
(π΄πΉπ΅) | Yes
| fnotovb 7412, fnovrn 7534 |
p | plus (see "add"), for all-constant
theorems | df-add 11069 |
(3 + 2) = 5 | Yes |
3p2e5 12311 |
pfx | prefix | df-pfx 14566 |
(π prefix πΏ) | Yes |
pfxlen 14578, ccatpfx 14596 |
pm | Principia Mathematica | |
| No | pm2.27 42 |
pm | partial mapping (operation) | df-pm 8775 |
(π΄ βpm π΅) | Yes | elpmi 8791, pmsspw 8822 |
pr | pair | df-pr 4594 |
{π΄, π΅} | Yes |
elpr 4614, prcom 4698, prid1g 4726, prnz 4743 |
prm, prime | prime (number) | df-prm 16555 |
β | Yes | 1nprm 16562, dvdsprime 16570 |
pss | proper subset | df-pss 3934 |
π΄ β π΅ | Yes | pssss 4060, sspsstri 4067 |
q | rational numbers ("quotients") | df-q 12881 |
β | Yes | elq 12882 |
r | right | |
| No | orcd 872, simprl 770 |
rab | restricted class abstraction |
df-rab 3411 | {π₯ β π΄ β£ π} | Yes |
rabswap 3419, df-oprab 7366 |
ral | restricted universal quantification |
df-ral 3066 | βπ₯ β π΄π | Yes |
ralnex 3076, ralrnmpo 7499 |
rcl | reverse closure | |
| No | ndmfvrcl 6883, nnarcl 8568 |
re | real numbers | df-r 11068 |
β | Yes | recn 11148, 0re 11164 |
rel | relation | df-rel 5645 | Rel π΄ |
Yes | brrelex1 5690, relmpoopab 8031 |
res | restriction | df-res 5650 |
(π΄ βΎ π΅) | Yes |
opelres 5948, f1ores 6803 |
reu | restricted existential uniqueness |
df-reu 3357 | β!π₯ β π΄π | Yes |
nfreud 3407, reurex 3360 |
rex | restricted existential quantification |
df-rex 3075 | βπ₯ β π΄π | Yes |
rexnal 3104, rexrnmpo 7500 |
rmo | restricted "at most one" |
df-rmo 3356 | β*π₯ β π΄π | Yes |
nfrmod 3406, nrexrmo 3377 |
rn | range | df-rn 5649 | ran π΄ |
Yes | elrng 5852, rncnvcnv 5894 |
ring | (unital) ring | df-ring 19973 |
Ring | Yes |
ringidval 19922, isring 19975, ringgrp 19976 |
rng | non-unital ring | df-rng 46247 |
Rng | Yes |
isrng 46248, rngabl 46249, rnglz 46256 |
rot | rotation | |
| No | 3anrot 1101, 3orrot 1093 |
s | eliminates need for syllogism (suffix) |
| | No | ancoms 460 |
sb | (proper) substitution (of a set) |
df-sb 2069 | [π¦ / π₯]π | Yes |
spsbe 2086, sbimi 2078 |
sbc | (proper) substitution of a class |
df-sbc 3745 | [π΄ / π₯]π | Yes |
sbc2or 3753, sbcth 3759 |
sca | scalar | df-sca 17156 |
(Scalarβπ») | Yes |
resssca 17231, mgpsca 19911 |
simp | simple, simplification | |
| No | simpl 484, simp3r3 1284 |
sn | singleton | df-sn 4592 |
{π΄} | Yes | eldifsn 4752 |
sp | specialization | |
| No | spsbe 2086, spei 2393 |
ss | subset | df-ss 3932 |
π΄ β π΅ | Yes | difss 4096 |
struct | structure | df-struct 17026 |
Struct | Yes | brstruct 17027, structfn 17035 |
sub | subtract | df-sub 11394 |
(π΄ β π΅) | Yes |
subval 11399, subaddi 11495 |
sup | supremum | df-sup 9385 |
sup(π΄, π΅, < ) | Yes |
fisupcl 9412, supmo 9395 |
supp | support (of a function) | df-supp 8098 |
(πΉ supp π) | Yes |
ressuppfi 9338, mptsuppd 8123 |
swap | swap (two parts within a theorem) |
| | No | rabswap 3419, 2reuswap 3709 |
syl | syllogism | syl 17 |
| No | 3syl 18 |
sym | symmetric | |
| No | df-symdif 4207, cnvsym 6071 |
symg | symmetric group | df-symg 19156 |
(SymGrpβπ΄) | Yes |
symghash 19166, pgrpsubgsymg 19198 |
t |
times (see "mul"), for all-constant theorems |
df-mul 11070 |
(3 Β· 2) = 6 | Yes |
3t2e6 12326 |
th, t |
theorem |
|
|
No |
nfth 1804, sbcth 3759, weth 10438, ancomst 466 |
tp | triple | df-tp 4596 |
{π΄, π΅, πΆ} | Yes |
eltpi 4653, tpeq1 4708 |
tr | transitive | |
| No | bitrd 279, biantr 805 |
tru, t |
true, truth |
df-tru 1545 |
β€ |
Yes |
bitru 1551, truanfal 1576, biimt 361 |
un | union | df-un 3920 |
(π΄ βͺ π΅) | Yes |
uneqri 4116, uncom 4118 |
unit | unit (in a ring) |
df-unit 20078 | (Unitβπ
) | Yes |
isunit 20093, nzrunit 20753 |
v |
setvar (especially for specializations of
theorems when a class is replaced by a setvar variable) |
|
x |
Yes |
cv 1541, vex 3452, velpw 4570, vtoclf 3519 |
v |
disjoint variable condition used in place of nonfreeness
hypothesis (suffix) |
|
|
No |
spimv 2389 |
vtx |
vertex |
df-vtx 27991 |
(VtxβπΊ) |
Yes |
vtxval0 28032, opvtxov 27998 |
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 2127, spnfw 1984 |
wrd | word |
df-word 14410 | Word π | Yes |
iswrdb 14415, wrdfn 14423, ffz0iswrd 14436 |
xp | cross product (Cartesian product) |
df-xp 5644 | (π΄ Γ π΅) | Yes |
elxp 5661, opelxpi 5675, xpundi 5705 |
xr | eXtended reals | df-xr 11200 |
β* | Yes | ressxr 11206, rexr 11208, 0xr 11209 |
z | integers (from German "Zahlen") |
df-z 12507 | β€ | Yes |
elz 12508, zcn 12511 |
zn | ring of integers mod π | df-zn 20923 |
(β€/nβ€βπ) | Yes |
znval 20954, zncrng 20967, znhash 20981 |
zring | ring of integers | df-zring 20886 |
β€ring | Yes | zringbas 20891, zringcrng 20887
|
0, z |
slashed zero (empty set) | df-nul 4288 |
β
| Yes |
n0i 4298, vn0 4303; snnz 4742, prnz 4743 |
(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.) |