| Description:
The following gives conventions used in the Metamath Proof Explorer
(MPE, set.mm) regarding labels.
For other conventions, see conventions 29344 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 3066"rgen.1 $e |- ( x e. A -> ph ) $."
or letters corresponding to the (main) class variable used in the
hypothesis, e.g., for mdet0 21955: "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 2662 and stirling 44320.
- 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 1841, and the restricted quantifier version of Theorem 21 from
Section 19 of [Margaris] p. 90 is labeled r19.21 3237.
- 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... 15766. 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 3913, and thus its syntax label fragment is "dif". Similarly, the
subclass relation 𝐴 ⊆ 𝐵 has syntax label fragment "ss"
because it is defined in df-ss 3927. 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 4091. There are many other syntax label fragments, e.g.,
singleton construct {𝐴} has syntax label fragment "sn" (because it
is defined in df-sn 4587), and the pair construct {𝐴, 𝐵} has
fragment "pr" ( from df-pr 4589). 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 4747. An "n" is often used for negation (¬), e.g.,
nan 828.
- 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 11057) and "re" represents real numbers ℝ (Definition df-r 11061).
The empty set ∅ often uses fragment 0, even though it is defined
in df-nul 4283. The syntax construct (𝐴 + 𝐵) usually uses the
fragment "add" (which is consistent with df-add 11062), 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 12288.
- 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 16032 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 15953) we have value cosval 16005 and
closure coscl 16009.
- 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 29347 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 1942 versus 19.21 2200. This
often permits to prove the result using fewer axioms, and/or to
eliminate a nonfreeness hypothesis (such as Ⅎ𝑥𝜑 in 19.21 2200).
If no constraint is put on axiom use, then the v-version can be proved
from the original theorem using nfv 1917. If two (resp. three) such
disjoint variable conditions are added, then the suffix "vv" (resp.
"vvv") is used, e.g., exlimivv 1935.
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 2574 derived from eu6 2572. 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 5406.
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 2407 (cbval 2396 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 3510.
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 584), commutes
(e.g., biimpac 479)
- 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 477, rexlimiva 3144 |
| abl | Abelian group | df-abl 19565 |
Abel | Yes | ablgrp 19567, zringabl 20873 |
| abs | absorption | | | No |
ressabs 17130 |
| abs | absolute value (of a complex number) |
df-abs 15121 | (abs‘𝐴) | Yes |
absval 15123, absneg 15162, abs1 15182 |
| ad | adding | |
| No | adantr 481, ad2antlr 725 |
| add | add (see "p") | df-add 11062 |
(𝐴 + 𝐵) | Yes |
addcl 11133, addcom 11341, addass 11138 |
| al | "for all" | |
∀𝑥𝜑 | No | alim 1812, alex 1828 |
| ALT | alternative/less preferred (suffix) | |
| No | idALT 23 |
| an | and | df-an 397 |
(𝜑 ∧ 𝜓) | Yes |
anor 981, iman 402, imnan 400 |
| ant | antecedent | |
| No | adantr 481 |
| ass | associative | |
| No | biass 385, orass 920, mulass 11139 |
| asym | asymmetric, antisymmetric | |
| No | intasym 6069, asymref 6070, posasymb 18208 |
| ax | axiom | |
| No | ax6dgen 2124, ax1cn 11085 |
| bas, base |
base (set of an extensible structure) | df-base 17084 |
(Base‘𝑆) | Yes |
baseval 17085, ressbas 17118, cnfldbas 20800 |
| b, bi | biconditional ("iff", "if and only if")
| df-bi 206 | (𝜑 ↔ 𝜓) | Yes |
impbid 211, sspwb 5406 |
| br | binary relation | df-br 5106 |
𝐴𝑅𝐵 | Yes | brab1 5153, brun 5156 |
| cbv | change bound variable | | |
No | cbvalivw 2010, cbvrex 3336 |
| cdm | codomain | |
| No | ffvelcdm 7032, focdmex 7888 |
| cl | closure | | | No |
ifclda 4521, ovrcl 7398, zaddcl 12543 |
| cn | complex numbers | df-c 11057 |
ℂ | Yes | nnsscn 12158, nncn 12161 |
| cnfld | field of complex numbers | df-cnfld 20797 |
ℂfld | Yes | cnfldbas 20800, cnfldinv 20828 |
| cntz | centralizer | df-cntz 19097 |
(Cntz‘𝑀) | Yes |
cntzfval 19100, dprdfcntz 19794 |
| cnv | converse | df-cnv 5641 |
◡𝐴 | Yes | opelcnvg 5836, f1ocnv 6796 |
| co | composition | df-co 5642 |
(𝐴 ∘ 𝐵) | Yes | cnvco 5841, fmptco 7075 |
| com | commutative | |
| No | orcom 868, bicomi 223, eqcomi 2745 |
| con | contradiction, contraposition | |
| No | condan 816, con2d 134 |
| csb | class substitution | df-csb 3856 |
⦋𝐴 / 𝑥⦌𝐵 | Yes |
csbid 3868, csbie2g 3898 |
| cyg | cyclic group | df-cyg 19655 |
CycGrp | Yes |
iscyg 19656, zringcyg 20890 |
| d | deduction form (suffix) | |
| No | idd 24, impbid 211 |
| df | (alternate) definition (prefix) | |
| No | dfrel2 6141, dffn2 6670 |
| di, distr | distributive | |
| No |
andi 1006, imdi 390, ordi 1004, difindi 4241, ndmovdistr 7543 |
| dif | class difference | df-dif 3913 |
(𝐴 ∖ 𝐵) | Yes |
difss 4091, difindi 4241 |
| div | division | df-div 11813 |
(𝐴 / 𝐵) | Yes |
divcl 11819, divval 11815, divmul 11816 |
| dm | domain | df-dm 5643 |
dom 𝐴 | Yes | dmmpt 6192, iswrddm0 14426 |
| e, eq, equ | equals (equ for setvars, eq for
classes) | df-cleq 2728 |
𝐴 = 𝐵 | Yes |
2p2e4 12288, uneqri 4111, equtr 2024 |
| edg | edge | df-edg 27999 |
(Edg‘𝐺) | Yes |
edgopval 28002, usgredgppr 28144 |
| el | element of | |
𝐴 ∈ 𝐵 | Yes |
eldif 3920, eldifsn 4747, elssuni 4898 |
| en | equinumerous | df-en |
𝐴 ≈ 𝐵 | Yes | domen 8901, enfi 9134 |
| eu | "there exists exactly one" | eu6 2572 |
∃!𝑥𝜑 | Yes | euex 2575, euabsn 4687 |
| ex | exists (i.e. is a set) | |
∈ V | No | brrelex1 5685, 0ex 5264 |
| ex, e | "there exists (at least one)" |
df-ex 1782 |
∃𝑥𝜑 | Yes | exim 1836, alex 1828 |
| exp | export | |
| No | expt 177, expcom 414 |
| f | "not free in" (suffix) | |
| No | equs45f 2457, sbf 2262 |
| f | function | df-f 6500 |
𝐹:𝐴⟶𝐵 | Yes | fssxp 6696, opelf 6703 |
| fal | false | df-fal 1554 |
⊥ | Yes | bifal 1557, falantru 1576 |
| fi | finite intersection | df-fi 9347 |
(fi‘𝐵) | Yes | fival 9348, inelfi 9354 |
| fi, fin | finite | df-fin 8887 |
Fin | Yes |
isfi 8916, snfi 8988, onfin 9174 |
| fld | field (Note: there is an alternative
definition Fld of a field, see df-fld 36451) | df-field 20188 |
Field | Yes | isfld 20196, fldidom 20775 |
| fn | function with domain | df-fn 6499 |
𝐴 Fn 𝐵 | Yes | ffn 6668, fndm 6605 |
| frgp | free group | df-frgp 19492 |
(freeGrp‘𝐼) | Yes |
frgpval 19540, frgpadd 19545 |
| fsupp | finitely supported function |
df-fsupp 9306 | 𝑅 finSupp 𝑍 | Yes |
isfsupp 9309, fdmfisuppfi 9314, fsuppco 9338 |
| fun | function | df-fun 6498 |
Fun 𝐹 | Yes | funrel 6518, ffun 6671 |
| fv | function value | df-fv 6504 |
(𝐹‘𝐴) | Yes | fvres 6861, swrdfv 14536 |
| fz | finite set of sequential integers |
df-fz 13425 |
(𝑀...𝑁) | Yes | fzval 13426, eluzfz 13436 |
| fz0 | finite set of sequential nonnegative integers |
|
(0...𝑁) | Yes | nn0fz0 13539, fz0tp 13542 |
| fzo | half-open integer range | df-fzo 13568 |
(𝑀..^𝑁) | Yes |
elfzo 13574, elfzofz 13588 |
| g | more general (suffix); eliminates "is a set"
hypotheses | |
| No | uniexg 7677 |
| gr | graph | |
| No | uhgrf 28013, isumgr 28046, usgrres1 28263 |
| grp | group | df-grp 18751 |
Grp | Yes | isgrp 18754, tgpgrp 23429 |
| gsum | group sum | df-gsum 17324 |
(𝐺 Σg 𝐹) | Yes |
gsumval 18532, gsumwrev 19147 |
| hash | size (of a set) | df-hash 14231 |
(♯‘𝐴) | Yes |
hashgval 14233, hashfz1 14246, hashcl 14256 |
| hb | hypothesis builder (prefix) | |
| No | hbxfrbi 1827, hbald 2168, hbequid 37371 |
| hm | (monoid, group, ring) homomorphism | |
| No | ismhm 18603, isghm 19008, isrhm 20152 |
| i | inference (suffix) | |
| No | eleq1i 2828, tcsni 9679 |
| i | implication (suffix) | |
| No | brwdomi 9504, infeq5i 9572 |
| id | identity | |
| No | biid 260 |
| iedg | indexed edge | df-iedg 27950 |
(iEdg‘𝐺) | Yes |
iedgval0 27991, edgiedgb 28005 |
| idm | idempotent | |
| No | anidm 565, tpidm13 4717 |
| im, imp | implication (label often omitted) |
df-im 14986 | (𝐴 → 𝐵) | Yes |
iman 402, imnan 400, impbidd 209 |
| ima | image | df-ima 5646 |
(𝐴 “ 𝐵) | Yes | resima 5971, imaundi 6102 |
| imp | import | |
| No | biimpa 477, impcom 408 |
| in | intersection | df-in 3917 |
(𝐴 ∩ 𝐵) | Yes | elin 3926, incom 4161 |
| inf | infimum | df-inf 9379 |
inf(ℝ+, ℝ*, < ) | Yes |
fiinfcl 9437, infiso 9444 |
| is... | is (something a) ...? | |
| No | isring 19968 |
| j | joining, disjoining | |
| No | jc 161, jaoi 855 |
| l | left | |
| No | olcd 872, simpl 483 |
| map | mapping operation or set exponentiation |
df-map 8767 | (𝐴 ↑m 𝐵) | Yes |
mapvalg 8775, elmapex 8786 |
| mat | matrix | df-mat 21755 |
(𝑁 Mat 𝑅) | Yes |
matval 21758, matring 21792 |
| mdet | determinant (of a square matrix) |
df-mdet 21934 | (𝑁 maDet 𝑅) | Yes |
mdetleib 21936, mdetrlin 21951 |
| mgm | magma | df-mgm 18497 |
Magma | Yes |
mgmidmo 18515, mgmlrid 18522, ismgm 18498 |
| mgp | multiplicative group | df-mgp 19897 |
(mulGrp‘𝑅) | Yes |
mgpress 19911, ringmgp 19970 |
| mnd | monoid | df-mnd 18557 |
Mnd | Yes | mndass 18565, mndodcong 19324 |
| mo | "there exists at most one" | df-mo 2538 |
∃*𝑥𝜑 | Yes | eumo 2576, moim 2542 |
| mp | modus ponens | ax-mp 5 |
| No | mpd 15, mpi 20 |
| mpo | maps-to notation for an operation |
df-mpo 7362 | (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) | Yes |
mpompt 7470, resmpo 7476 |
| mpt | modus ponendo tollens | |
| No | mptnan 1770, mptxor 1771 |
| mpt | maps-to notation for a function |
df-mpt 5189 | (𝑥 ∈ 𝐴 ↦ 𝐵) | Yes |
fconstmpt 5694, resmpt 5991 |
| mpt2 | maps-to notation for an operation (deprecated).
We are in the process of replacing mpt2 with mpo in labels. |
df-mpo 7362 | (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) | Yes |
mpompt 7470, resmpo 7476 |
| mul | multiplication (see "t") | df-mul 11063 |
(𝐴 · 𝐵) | Yes |
mulcl 11135, divmul 11816, mulcom 11137, mulass 11139 |
| n, not | not | |
¬ 𝜑 | Yes |
nan 828, notnotr 130 |
| ne | not equal | df-ne | 𝐴 ≠ 𝐵 |
Yes | exmidne 2953, neeqtrd 3013 |
| nel | not element of | df-nel | 𝐴 ∉ 𝐵
|
Yes | neli 3051, nnel 3058 |
| ne0 | not equal to zero (see n0) | |
≠ 0 | No |
negne0d 11510, ine0 11590, gt0ne0 11620 |
| nf | "not free in" (prefix) | |
| No | nfnd 1861 |
| ngp | normed group | df-ngp 23939 |
NrmGrp | Yes | isngp 23952, ngptps 23958 |
| nm | norm (on a group or ring) | df-nm 23938 |
(norm‘𝑊) | Yes |
nmval 23945, subgnm 23989 |
| nn | positive integers | df-nn 12154 |
ℕ | Yes | nnsscn 12158, nncn 12161 |
| nn0 | nonnegative integers | df-n0 12414 |
ℕ0 | Yes | nnnn0 12420, nn0cn 12423 |
| n0 | not the empty set (see ne0) | |
≠ ∅ | No | n0i 4293, vn0 4298, ssn0 4360 |
| OLD | old, obsolete (to be removed soon) | |
| No | 19.43OLD 1886 |
| on | ordinal number | df-on 6321 |
𝐴 ∈ On | Yes |
elon 6326, 1on 8424 onelon 6342 |
| op | ordered pair | df-op 4593 |
⟨𝐴, 𝐵⟩ | Yes | dfopif 4827, opth 5433 |
| or | or | df-or 846 |
(𝜑 ∨ 𝜓) | Yes |
orcom 868, anor 981 |
| ot | ordered triple | df-ot 4595 |
⟨𝐴, 𝐵, 𝐶⟩ | Yes |
euotd 5470, fnotovb 7407 |
| ov | operation value | df-ov 7360 |
(𝐴𝐹𝐵) | Yes
| fnotovb 7407, fnovrn 7529 |
| p | plus (see "add"), for all-constant
theorems | df-add 11062 |
(3 + 2) = 5 | Yes |
3p2e5 12304 |
| pfx | prefix | df-pfx 14559 |
(𝑊 prefix 𝐿) | Yes |
pfxlen 14571, ccatpfx 14589 |
| pm | Principia Mathematica | |
| No | pm2.27 42 |
| pm | partial mapping (operation) | df-pm 8768 |
(𝐴 ↑pm 𝐵) | Yes | elpmi 8784, pmsspw 8815 |
| pr | pair | df-pr 4589 |
{𝐴, 𝐵} | Yes |
elpr 4609, prcom 4693, prid1g 4721, prnz 4738 |
| prm, prime | prime (number) | df-prm 16548 |
ℙ | Yes | 1nprm 16555, dvdsprime 16563 |
| pss | proper subset | df-pss 3929 |
𝐴 ⊊ 𝐵 | Yes | pssss 4055, sspsstri 4062 |
| q | rational numbers ("quotients") | df-q 12874 |
ℚ | Yes | elq 12875 |
| r | right | |
| No | orcd 871, simprl 769 |
| rab | restricted class abstraction |
df-rab 3408 | {𝑥 ∈ 𝐴 ∣ 𝜑} | Yes |
rabswap 3416, df-oprab 7361 |
| ral | restricted universal quantification |
df-ral 3065 | ∀𝑥 ∈ 𝐴𝜑 | Yes |
ralnex 3075, ralrnmpo 7494 |
| rcl | reverse closure | |
| No | ndmfvrcl 6878, nnarcl 8563 |
| re | real numbers | df-r 11061 |
ℝ | Yes | recn 11141, 0re 11157 |
| rel | relation | df-rel 5640 | Rel 𝐴 |
Yes | brrelex1 5685, relmpoopab 8026 |
| res | restriction | df-res 5645 |
(𝐴 ↾ 𝐵) | Yes |
opelres 5943, f1ores 6798 |
| reu | restricted existential uniqueness |
df-reu 3354 | ∃!𝑥 ∈ 𝐴𝜑 | Yes |
nfreud 3404, reurex 3357 |
| rex | restricted existential quantification |
df-rex 3074 | ∃𝑥 ∈ 𝐴𝜑 | Yes |
rexnal 3103, rexrnmpo 7495 |
| rmo | restricted "at most one" |
df-rmo 3353 | ∃*𝑥 ∈ 𝐴𝜑 | Yes |
nfrmod 3403, nrexrmo 3374 |
| rn | range | df-rn 5644 | ran 𝐴 |
Yes | elrng 5847, rncnvcnv 5889 |
| ring | (unital) ring | df-ring 19966 |
Ring | Yes |
ringidval 19915, isring 19968, ringgrp 19969 |
| rng | non-unital ring | df-rng 46163 |
Rng | Yes |
isrng 46164, rngabl 46165, rnglz 46172 |
| rot | rotation | |
| No | 3anrot 1100, 3orrot 1092 |
| s | eliminates need for syllogism (suffix) |
| | No | ancoms 459 |
| sb | (proper) substitution (of a set) |
df-sb 2068 | [𝑦 / 𝑥]𝜑 | Yes |
spsbe 2085, sbimi 2077 |
| sbc | (proper) substitution of a class |
df-sbc 3740 | [𝐴 / 𝑥]𝜑 | Yes |
sbc2or 3748, sbcth 3754 |
| sca | scalar | df-sca 17149 |
(Scalar‘𝐻) | Yes |
resssca 17224, mgpsca 19904 |
| simp | simple, simplification | |
| No | simpl 483, simp3r3 1283 |
| sn | singleton | df-sn 4587 |
{𝐴} | Yes | eldifsn 4747 |
| sp | specialization | |
| No | spsbe 2085, spei 2392 |
| ss | subset | df-ss 3927 |
𝐴 ⊆ 𝐵 | Yes | difss 4091 |
| struct | structure | df-struct 17019 |
Struct | Yes | brstruct 17020, structfn 17028 |
| sub | subtract | df-sub 11387 |
(𝐴 − 𝐵) | Yes |
subval 11392, subaddi 11488 |
| sup | supremum | df-sup 9378 |
sup(𝐴, 𝐵, < ) | Yes |
fisupcl 9405, supmo 9388 |
| supp | support (of a function) | df-supp 8093 |
(𝐹 supp 𝑍) | Yes |
ressuppfi 9331, mptsuppd 8118 |
| swap | swap (two parts within a theorem) |
| | No | rabswap 3416, 2reuswap 3704 |
| syl | syllogism | syl 17 |
| No | 3syl 18 |
| sym | symmetric | |
| No | df-symdif 4202, cnvsym 6066 |
| symg | symmetric group | df-symg 19149 |
(SymGrp‘𝐴) | Yes |
symghash 19159, pgrpsubgsymg 19191 |
| t |
times (see "mul"), for all-constant theorems |
df-mul 11063 |
(3 · 2) = 6 | Yes |
3t2e6 12319 |
| th, t |
theorem |
|
|
No |
nfth 1803, sbcth 3754, weth 10431, ancomst 465 |
| tp | triple | df-tp 4591 |
{𝐴, 𝐵, 𝐶} | Yes |
eltpi 4648, tpeq1 4703 |
| tr | transitive | |
| No | bitrd 278, biantr 804 |
| tru, t |
true, truth |
df-tru 1544 |
⊤ |
Yes |
bitru 1550, truanfal 1575, biimt 360 |
| un | union | df-un 3915 |
(𝐴 ∪ 𝐵) | Yes |
uneqri 4111, uncom 4113 |
| unit | unit (in a ring) |
df-unit 20071 | (Unit‘𝑅) | Yes |
isunit 20086, nzrunit 20737 |
| v |
setvar (especially for specializations of
theorems when a class is replaced by a setvar variable) |
|
x |
Yes |
cv 1540, vex 3449, velpw 4565, vtoclf 3516 |
| v |
disjoint variable condition used in place of nonfreeness
hypothesis (suffix) |
|
|
No |
spimv 2388 |
| vtx |
vertex |
df-vtx 27949 |
(Vtx‘𝐺) |
Yes |
vtxval0 27990, opvtxov 27956 |
| vv |
two disjoint variable conditions used in place of nonfreeness
hypotheses (suffix) |
|
|
No |
19.23vv 1946 |
| w | weak (version of a theorem) (suffix) | |
| No | ax11w 2126, spnfw 1983 |
| wrd | word |
df-word 14403 | Word 𝑆 | Yes |
iswrdb 14408, wrdfn 14416, ffz0iswrd 14429 |
| xp | cross product (Cartesian product) |
df-xp 5639 | (𝐴 × 𝐵) | Yes |
elxp 5656, opelxpi 5670, xpundi 5700 |
| xr | eXtended reals | df-xr 11193 |
ℝ* | Yes | ressxr 11199, rexr 11201, 0xr 11202 |
| z | integers (from German "Zahlen") |
df-z 12500 | ℤ | Yes |
elz 12501, zcn 12504 |
| zn | ring of integers mod 𝑁 | df-zn 20907 |
(ℤ/nℤ‘𝑁) | Yes |
znval 20938, zncrng 20951, znhash 20965 |
| zring | ring of integers | df-zring 20870 |
ℤring | Yes | zringbas 20875, zringcrng 20871
|
| 0, z |
slashed zero (empty set) | df-nul 4283 |
∅ | Yes |
n0i 4293, vn0 4298; snnz 4737, prnz 4738 |
(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.) |
