| Description:
The following gives conventions used in the Metamath Proof Explorer
(MPE, set.mm) regarding labels.
For other conventions, see conventions 27811 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 3131"rgen.1 $e |- ( x e. A -> ph ) $."
or letters corresponding to the (main) class variable used in the
hypothesis, e.g. for mdet0 20787: "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 2746 and stirling 41098.
- 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 1937, and the restricted quantifier version of Theorem 21 from
Section 19 of [Margaris] p. 90 is labeled r19.21 3165.
- 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... 14993. 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 3801, and thus its syntax label fragment is "dif". Similarly, the
subclass relation 𝐴 ⊆ 𝐵 has syntax label fragment "ss"
because it is defined in df-ss 3812. 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 3966. There are many other syntax label fragments, e.g.,
singleton construct {𝐴} has syntax label fragment "sn" (because it
is defined in df-sn 4400), and the pair construct {𝐴, 𝐵} has
fragment "pr" ( from df-pr 4402). 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 4538. An "n" is often used for negation (¬), e.g.,
nan 864.
- 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 10265) and "re" represents real numbers ℝ ( definition df-r 10269).
The empty set ∅ often uses fragment 0, even though it is defined
in df-nul 4147. The syntax construct (𝐴 + 𝐵) usually uses the
fragment "add" (which is consistent with df-add 10270), 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 11500.
- 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 15259 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 15180) we have value cosval 15232 and closure
coscl 15236.
- 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 27814 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 (see above).
Additionally, we sometimes suffix with "v" the label of a theorem
eliminating a hypothesis such as Ⅎ𝑥𝜑 in 19.21 2249 via the use of
disjoint variable conditions combined with nfv 2013. If two (or three)
such hypotheses are eliminated, the suffix "vv" resp. "vvv" is used,
e.g. exlimivv 2031.
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 2648 derived from eu6 2645. 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 5140.
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 2431 (cbval 2423 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 3472 or rabeqif 3404.
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 579), commutes
(e.g., biimpac 472)
- 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)
- 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
- OLD : old/obsolete version of a theorem/definition/proof
- 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 470, rexlimiva 3237 |
| abl | Abelian group | df-abl 18556 |
Abel | Yes | ablgrp 18558, zringabl 20189 |
| abs | absorption | | | No |
ressabs 16310 |
| abs | absolute value (of a complex number) |
df-abs 14360 | (abs‘𝐴) | Yes |
absval 14362, absneg 14401, abs1 14421 |
| ad | adding | |
| No | adantr 474, ad2antlr 718 |
| add | add (see "p") | df-add 10270 |
(𝐴 + 𝐵) | Yes |
addcl 10341, addcom 10548, addass 10346 |
| al | "for all" | |
∀𝑥𝜑 | No | alim 1909, alex 1924 |
| ALT | alternative/less preferred (suffix) | |
| No | idALT 23 |
| an | and | df-an 387 |
(𝜑 ∧ 𝜓) | Yes |
anor 1010, iman 392, imnan 390 |
| ant | antecedent | |
| No | adantr 474 |
| ass | associative | |
| No | biass 376, orass 950, mulass 10347 |
| asym | asymmetric, antisymmetric | |
| No | intasym 5757, asymref 5758, posasymb 17312 |
| ax | axiom | |
| No | ax6dgen 2179, ax1cn 10293 |
| bas, base |
base (set of an extensible structure) | df-base 16235 |
(Base‘𝑆) | Yes |
baseval 16288, ressbas 16300, cnfldbas 20117 |
| b, bi | biconditional ("iff", "if and only if")
| df-bi 199 | (𝜑 ↔ 𝜓) | Yes |
impbid 204, sspwb 5140 |
| br | binary relation | df-br 4876 |
𝐴𝑅𝐵 | Yes | brab1 4923, brun 4926 |
| cbv | change bound variable | | |
No | cbvalivw 2111, cbvrex 3380 |
| cl | closure | | | No |
ifclda 4342, ovrcl 6950, zaddcl 11752 |
| cn | complex numbers | df-c 10265 |
ℂ | Yes | nnsscn 11362, nncn 11366 |
| cnfld | field of complex numbers | df-cnfld 20114 |
ℂfld | Yes | cnfldbas 20117, cnfldinv 20144 |
| cntz | centralizer | df-cntz 18107 |
(Cntz‘𝑀) | Yes |
cntzfval 18110, dprdfcntz 18775 |
| cnv | converse | df-cnv 5354 |
◡𝐴 | Yes | opelcnvg 5539, f1ocnv 6394 |
| co | composition | df-co 5355 |
(𝐴 ∘ 𝐵) | Yes | cnvco 5544, fmptco 6651 |
| com | commutative | |
| No | orcom 901, bicomi 216, eqcomi 2834 |
| con | contradiction, contraposition | |
| No | condan 852, con2d 132 |
| csb | class substitution | df-csb 3758 |
⦋𝐴 / 𝑥⦌𝐵 | Yes |
csbid 3765, csbie2g 3788 |
| cyg | cyclic group | df-cyg 18640 |
CycGrp | Yes |
iscyg 18641, zringcyg 20206 |
| d | deduction form (suffix) | |
| No | idd 24, impbid 204 |
| df | (alternate) definition (prefix) | |
| No | dfrel2 5828, dffn2 6284 |
| di, distr | distributive | |
| No |
andi 1035, imdi 381, ordi 1033, difindi 4113, ndmovdistr 7088 |
| dif | class difference | df-dif 3801 |
(𝐴 ∖ 𝐵) | Yes |
difss 3966, difindi 4113 |
| div | division | df-div 11017 |
(𝐴 / 𝐵) | Yes |
divcl 11023, divval 11019, divmul 11020 |
| dm | domain | df-dm 5356 |
dom 𝐴 | Yes | dmmpt 5875, iswrddm0 13605 |
| e, eq, equ | equals | df-cleq 2818 |
𝐴 = 𝐵 | Yes |
2p2e4 11500, uneqri 3984, equtr 2125 |
| edg | edge | df-edg 26353 |
(Edg‘𝐺) | Yes |
edgopval 26356, usgredgppr 26499 |
| el | element of | |
𝐴 ∈ 𝐵 | Yes |
eldif 3808, eldifsn 4538, elssuni 4691 |
| en | equinumerous | df-en |
𝐴 ≈ 𝐵 | Yes | domen 8241, enfi 8451 |
| eu | "there exists exactly one" | eu6 2645 |
∃!𝑥𝜑 | Yes | euex 2650, euabsn 4481 |
| ex | exists (i.e. is a set) | |
∈ V | No | brrelex1 5394, 0ex 5016 |
| ex | "there exists (at least one)" | df-ex 1879 |
∃𝑥𝜑 | Yes | exim 1932, alex 1924 |
| exp | export | |
| No | expt 170, expcom 404 |
| f | "not free in" (suffix) | |
| No | equs45f 2480, sbf 2511 |
| f | function | df-f 6131 |
𝐹:𝐴⟶𝐵 | Yes | fssxp 6301, opelf 6306 |
| fal | false | df-fal 1670 |
⊥ | Yes | bifal 1673, falantru 1692 |
| fi | finite intersection | df-fi 8592 |
(fi‘𝐵) | Yes | fival 8593, inelfi 8599 |
| fi, fin | finite | df-fin 8232 |
Fin | Yes |
isfi 8252, snfi 8313, onfin 8426 |
| fld | field (Note: there is an alternative
definition Fld of a field, see df-fld 34332) | df-field 19113 |
Field | Yes | isfld 19119, fldidom 19673 |
| fn | function with domain | df-fn 6130 |
𝐴 Fn 𝐵 | Yes | ffn 6282, fndm 6227 |
| frgp | free group | df-frgp 18481 |
(freeGrp‘𝐼) | Yes |
frgpval 18531, frgpadd 18536 |
| fsupp | finitely supported function |
df-fsupp 8551 | 𝑅 finSupp 𝑍 | Yes |
isfsupp 8554, fdmfisuppfi 8559, fsuppco 8582 |
| fun | function | df-fun 6129 |
Fun 𝐹 | Yes | funrel 6144, ffun 6285 |
| fv | function value | df-fv 6135 |
(𝐹‘𝐴) | Yes | fvres 6456, swrdfv 13717 |
| fz | finite set of sequential integers |
df-fz 12627 |
(𝑀...𝑁) | Yes | fzval 12628, eluzfz 12637 |
| fz0 | finite set of sequential nonnegative integers |
|
(0...𝑁) | Yes | nn0fz0 12739, fz0tp 12742 |
| fzo | half-open integer range | df-fzo 12768 |
(𝑀..^𝑁) | Yes |
elfzo 12774, elfzofz 12787 |
| g | more general (suffix); eliminates "is a set"
hypotheses | |
| No | uniexg 7220 |
| gr | graph | |
| No | uhgrf 26367, isumgr 26400, usgrres1 26619 |
| grp | group | df-grp 17786 |
Grp | Yes | isgrp 17789, tgpgrp 22259 |
| gsum | group sum | df-gsum 16463 |
(𝐺 Σg 𝐹) | Yes |
gsumval 17631, gsumwrev 18153 |
| hash | size (of a set) | df-hash 13418 |
(♯‘𝐴) | Yes |
hashgval 13420, hashfz1 13433, hashcl 13444 |
| hb | hypothesis builder (prefix) | |
| No | hbxfrbi 1923, hbald 2218, hbequid 34983 |
| hm | (monoid, group, ring) homomorphism | |
| No | ismhm 17697, isghm 18018, isrhm 19084 |
| i | inference (suffix) | |
| No | eleq1i 2897, tcsni 8903 |
| i | implication (suffix) | |
| No | brwdomi 8749, infeq5i 8817 |
| id | identity | |
| No | biid 253 |
| iedg | indexed edge | df-iedg 26304 |
(iEdg‘𝐺) | Yes |
iedgval0 26345, edgiedgb 26359 |
| idm | idempotent | |
| No | anidm 560, tpidm13 4511 |
| im, imp | implication (label often omitted) |
df-im 14225 | (𝐴 → 𝐵) | Yes |
iman 392, imnan 390, impbidd 202 |
| ima | image | df-ima 5359 |
(𝐴 “ 𝐵) | Yes | resima 5671, imaundi 5790 |
| imp | import | |
| No | biimpa 470, impcom 398 |
| in | intersection | df-in 3805 |
(𝐴 ∩ 𝐵) | Yes | elin 4025, incom 4034 |
| inf | infimum | df-inf 8624 |
inf(ℝ+, ℝ*, < ) | Yes |
fiinfcl 8682, infiso 8689 |
| is... | is (something a) ...? | |
| No | isring 18912 |
| j | joining, disjoining | |
| No | jc 161, jaoi 888 |
| l | left | |
| No | olcd 905, simpl 476 |
| map | mapping operation or set exponentiation |
df-map 8129 | (𝐴 ↑𝑚 𝐵) | Yes |
mapvalg 8137, elmapex 8148 |
| mat | matrix | df-mat 20588 |
(𝑁 Mat 𝑅) | Yes |
matval 20591, matring 20623 |
| mdet | determinant (of a square matrix) |
df-mdet 20766 | (𝑁 maDet 𝑅) | Yes |
mdetleib 20768, mdetrlin 20783 |
| mgm | magma | df-mgm 17602 |
Magma | Yes |
mgmidmo 17619, mgmlrid 17626, ismgm 17603 |
| mgp | multiplicative group | df-mgp 18851 |
(mulGrp‘𝑅) | Yes |
mgpress 18861, ringmgp 18914 |
| mnd | monoid | df-mnd 17655 |
Mnd | Yes | mndass 17662, mndodcong 18319 |
| mo | "there exists at most one" | df-mo 2605 |
∃*𝑥𝜑 | Yes | eumo 2651, moim 2610 |
| mp | modus ponens | ax-mp 5 |
| No | mpd 15, mpi 20 |
| mpt | modus ponendo tollens | |
| No | mptnan 1867, mptxor 1868 |
| mpt | maps-to notation for a function |
df-mpt 4955 | (𝑥 ∈ 𝐴 ↦ 𝐵) | Yes |
fconstmpt 5402, resmpt 5690 |
| mpt2 | maps-to notation for an operation |
df-mpt2 6915 | (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) | Yes |
mpt2mpt 7017, resmpt2 7023 |
| mul | multiplication (see "t") | df-mul 10271 |
(𝐴 · 𝐵) | Yes |
mulcl 10343, divmul 11020, mulcom 10345, mulass 10347 |
| n, not | not | |
¬ 𝜑 | Yes |
nan 864, notnotr 128 |
| ne | not equal | df-ne | 𝐴 ≠ 𝐵 |
Yes | exmidne 3009, neeqtrd 3068 |
| nel | not element of | df-nel | 𝐴 ∉ 𝐵
|
Yes | neli 3104, nnel 3111 |
| ne0 | not equal to zero (see n0) | |
≠ 0 | No |
negne0d 10718, ine0 10796, gt0ne0 10824 |
| nf | "not free in" (prefix) | |
| No | nfnd 1958 |
| ngp | normed group | df-ngp 22765 |
NrmGrp | Yes | isngp 22777, ngptps 22783 |
| nm | norm (on a group or ring) | df-nm 22764 |
(norm‘𝑊) | Yes |
nmval 22771, subgnm 22814 |
| nn | positive integers | df-nn 11358 |
ℕ | Yes | nnsscn 11362, nncn 11366 |
| nn0 | nonnegative integers | df-n0 11626 |
ℕ0 | Yes | nnnn0 11633, nn0cn 11636 |
| n0 | not the empty set (see ne0) | |
≠ ∅ | No | n0i 4151, vn0 4156, ssn0 4203 |
| OLD | old, obsolete (to be removed soon) | |
| No | 19.43OLD 1986 |
| on | ordinal number | df-on 5971 |
𝐴 ∈ On | Yes |
elon 5976, 1on 7838 onelon 5992 |
| op | ordered pair | df-op 4406 |
⟨𝐴, 𝐵⟩ | Yes | dfopif 4622, opth 5167 |
| or | or | df-or 879 |
(𝜑 ∨ 𝜓) | Yes |
orcom 901, anor 1010 |
| ot | ordered triple | df-ot 4408 |
⟨𝐴, 𝐵, 𝐶⟩ | Yes |
euotd 5201, fnotovb 6959 |
| ov | operation value | df-ov 6913 |
(𝐴𝐹𝐵) | Yes
| fnotovb 6959, fnovrn 7074 |
| p | plus (see "add"), for all-constant
theorems | df-add 10270 |
(3 + 2) = 5 | Yes |
3p2e5 11516 |
| pfx | prefix | df-pfx 13757 |
(𝑊 prefix 𝐿) | Yes |
pfxlen 13769, ccatpfx 13787 |
| pm | Principia Mathematica | |
| No | pm2.27 42 |
| pm | partial mapping (operation) | df-pm 8130 |
(𝐴 ↑pm 𝐵) | Yes | elpmi 8146, pmsspw 8162 |
| pr | pair | df-pr 4402 |
{𝐴, 𝐵} | Yes |
elpr 4422, prcom 4487, prid1g 4515, prnz 4531 |
| prm, prime | prime (number) | df-prm 15765 |
ℙ | Yes | 1nprm 15771, dvdsprime 15779 |
| pss | proper subset | df-pss 3814 |
𝐴 ⊊ 𝐵 | Yes | pssss 3930, sspsstri 3937 |
| q | rational numbers ("quotients") | df-q 12079 |
ℚ | Yes | elq 12080 |
| r | right | |
| No | orcd 904, simprl 787 |
| rab | restricted class abstraction |
df-rab 3126 | {𝑥 ∈ 𝐴 ∣ 𝜑} | Yes |
rabswap 3332, df-oprab 6914 |
| ral | restricted universal quantification |
df-ral 3122 | ∀𝑥 ∈ 𝐴𝜑 | Yes |
ralnex 3201, ralrnmpt2 7040 |
| rcl | reverse closure | |
| No | ndmfvrcl 6468, nnarcl 7968 |
| re | real numbers | df-r 10269 |
ℝ | Yes | recn 10349, 0re 10365 |
| rel | relation | df-rel 5353 | Rel 𝐴 |
Yes | brrelex1 5394, relmpt2opab 7528 |
| res | restriction | df-res 5358 |
(𝐴 ↾ 𝐵) | Yes |
opelres 5639, f1ores 6396 |
| reu | restricted existential uniqueness |
df-reu 3124 | ∃!𝑥 ∈ 𝐴𝜑 | Yes |
nfreud 3322, reurex 3372 |
| rex | restricted existential quantification |
df-rex 3123 | ∃𝑥 ∈ 𝐴𝜑 | Yes |
rexnal 3203, rexrnmpt2 7041 |
| rmo | restricted "at most one" |
df-rmo 3125 | ∃*𝑥 ∈ 𝐴𝜑 | Yes |
nfrmod 3323, nrexrmo 3375 |
| rn | range | df-rn 5357 | ran 𝐴 |
Yes | elrng 5550, rncnvcnv 5585 |
| rng | (unital) ring | df-ring 18910 |
Ring | Yes |
ringidval 18864, isring 18912, ringgrp 18913 |
| rot | rotation | |
| No | 3anrot 1126, 3orrot 1116 |
| s | eliminates need for syllogism (suffix) |
| | No | ancoms 452 |
| sb | (proper) substitution (of a set) |
df-sb 2068 | [𝑦 / 𝑥]𝜑 | Yes |
spsbe 2071, sbimi 2073 |
| sbc | (proper) substitution of a class |
df-sbc 3663 | [𝐴 / 𝑥]𝜑 | Yes |
sbc2or 3671, sbcth 3677 |
| sca | scalar | df-sca 16328 |
(Scalar‘𝐻) | Yes |
resssca 16397, mgpsca 18857 |
| simp | simple, simplification | |
| No | simpl 476, simp3r3 1386 |
| sn | singleton | df-sn 4400 |
{𝐴} | Yes | eldifsn 4538 |
| sp | specialization | |
| No | spsbe 2071, spei 2414 |
| ss | subset | df-ss 3812 |
𝐴 ⊆ 𝐵 | Yes | difss 3966 |
| struct | structure | df-struct 16231 |
Struct | Yes | brstruct 16238, structfn 16246 |
| sub | subtract | df-sub 10594 |
(𝐴 − 𝐵) | Yes |
subval 10599, subaddi 10696 |
| sup | supremum | df-sup 8623 |
sup(𝐴, 𝐵, < ) | Yes |
fisupcl 8650, supmo 8633 |
| supp | support (of a function) | df-supp 7565 |
(𝐹 supp 𝑍) | Yes |
ressuppfi 8576, mptsuppd 7587 |
| swap | swap (two parts within a theorem) |
| | No | rabswap 3332, 2reuswap 3637 |
| syl | syllogism | syl 17 |
| No | 3syl 18 |
| sym | symmetric | |
| No | df-symdif 4072, cnvsym 5756 |
| symg | symmetric group | df-symg 18155 |
(SymGrp‘𝐴) | Yes |
symghash 18162, pgrpsubgsymg 18185 |
| t |
times (see "mul"), for all-constant theorems |
df-mul 10271 |
(3 · 2) = 6 | Yes |
3t2e6 11531 |
| th | theorem | |
| No | nfth 1900, sbcth 3677, weth 9639 |
| tp | triple | df-tp 4404 |
{𝐴, 𝐵, 𝐶} | Yes |
eltpi 4450, tpeq1 4497 |
| tr | transitive | |
| No | bitrd 271, biantr 840 |
| tru | true | df-tru 1660 |
⊤ | Yes | bitru 1666, truanfal 1691 |
| un | union | df-un 3803 |
(𝐴 ∪ 𝐵) | Yes |
uneqri 3984, uncom 3986 |
| unit | unit (in a ring) |
df-unit 19003 | (Unit‘𝑅) | Yes |
isunit 19018, nzrunit 19635 |
| v | disjoint variable conditions used when
a not-free hypothesis (suffix) |
| | No | spimv 2410 |
| vtx | vertex | df-vtx 26303 |
(Vtx‘𝐺) | Yes |
vtxval0 26344, opvtxov 26310 |
| vv | 2 disjoint variables (in a not-free hypothesis)
(suffix) | | | No | 19.23vv 2042 |
| w | weak (version of a theorem) (suffix) | |
| No | ax11w 2181, spnfw 2104 |
| wrd | word |
df-word 13582 | Word 𝑆 | Yes |
iswrdb 13587, wrdfn 13595, ffz0iswrd 13608 |
| xp | cross product (Cartesian product) |
df-xp 5352 | (𝐴 × 𝐵) | Yes |
elxp 5369, opelxpi 5383, xpundi 5408 |
| xr | eXtended reals | df-xr 10402 |
ℝ* | Yes | ressxr 10407, rexr 10409, 0xr 10410 |
| z | integers (from German "Zahlen") |
df-z 11712 | ℤ | Yes |
elz 11713, zcn 11716 |
| zn | ring of integers mod 𝑁 | df-zn 20222 |
(ℤ/nℤ‘𝑁) | Yes |
znval 20250, zncrng 20259, znhash 20273 |
| zring | ring of integers | df-zring 20186 |
ℤring | Yes | zringbas 20191, zringcrng 20187
|
| 0, z |
slashed zero (empty set) | df-nul 4147 |
∅ | Yes |
n0i 4151, vn0 4156; snnz 4530, prnz 4531 |
(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.) |
