| Description:
The following gives conventions used in the Metamath Proof Explorer
(MPE, set.mm) regarding labels.
For other conventions, see conventions 28764 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 3074"rgen.1 $e |- ( x e. A -> ph ) $."
or letters corresponding to the (main) class variable used in the
hypothesis, e.g., for mdet0 21755: "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 2664 and stirling 43630.
- 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 3140.
- 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... 15593. 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 3890, and thus its syntax label fragment is "dif". Similarly, the
subclass relation 𝐴 ⊆ 𝐵 has syntax label fragment "ss"
because it is defined in df-ss 3904. 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 4066. There are many other syntax label fragments, e.g.,
singleton construct {𝐴} has syntax label fragment "sn" (because it
is defined in df-sn 4562), and the pair construct {𝐴, 𝐵} has
fragment "pr" ( from df-pr 4564). 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 4720. An "n" is often used for negation (¬), e.g.,
nan 827.
- Exceptions.
Sometimes there is a definition df-NAME but the label fragment is not
the NAME part. The definition should note this exception as part of its
definition. In addition, the table below attempts to list all such
cases and marks them in bold. For example, the label fragment "cn"
represents complex numbers ℂ (even though its definition is in
df-c 10877) and "re" represents real numbers ℝ (Definition df-r 10881).
The empty set ∅ often uses fragment 0, even though it is defined
in df-nul 4257. The syntax construct (𝐴 + 𝐵) usually uses the
fragment "add" (which is consistent with df-add 10882), 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 12108.
- 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 15859 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 15780) we have value cosval 15832 and
closure coscl 15836.
- 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 28767 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 2576 derived from eu6 2574. 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 5365.
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 2409 (cbval 2398 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 3493.
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 3210 |
| abl | Abelian group | df-abl 19389 |
Abel | Yes | ablgrp 19391, zringabl 20674 |
| abs | absorption | | | No |
ressabs 16959 |
| abs | absolute value (of a complex number) |
df-abs 14947 | (abs‘𝐴) | Yes |
absval 14949, absneg 14989, abs1 15009 |
| ad | adding | |
| No | adantr 481, ad2antlr 724 |
| add | add (see "p") | df-add 10882 |
(𝐴 + 𝐵) | Yes |
addcl 10953, addcom 11161, addass 10958 |
| al | "for all" | |
∀𝑥𝜑 | No | alim 1813, alex 1828 |
| ALT | alternative/less preferred (suffix) | |
| No | idALT 23 |
| an | and | df-an 397 |
(𝜑 ∧ 𝜓) | Yes |
anor 980, iman 402, imnan 400 |
| ant | antecedent | |
| No | adantr 481 |
| ass | associative | |
| No | biass 386, orass 919, mulass 10959 |
| asym | asymmetric, antisymmetric | |
| No | intasym 6020, asymref 6021, posasymb 18037 |
| ax | axiom | |
| No | ax6dgen 2124, ax1cn 10905 |
| bas, base |
base (set of an extensible structure) | df-base 16913 |
(Base‘𝑆) | Yes |
baseval 16914, ressbas 16947, cnfldbas 20601 |
| b, bi | biconditional ("iff", "if and only if")
| df-bi 206 | (𝜑 ↔ 𝜓) | Yes |
impbid 211, sspwb 5365 |
| br | binary relation | df-br 5075 |
𝐴𝑅𝐵 | Yes | brab1 5122, brun 5125 |
| cbv | change bound variable | | |
No | cbvalivw 2010, cbvrex 3380 |
| cl | closure | | | No |
ifclda 4494, ovrcl 7316, zaddcl 12360 |
| cn | complex numbers | df-c 10877 |
ℂ | Yes | nnsscn 11978, nncn 11981 |
| cnfld | field of complex numbers | df-cnfld 20598 |
ℂfld | Yes | cnfldbas 20601, cnfldinv 20629 |
| cntz | centralizer | df-cntz 18923 |
(Cntz‘𝑀) | Yes |
cntzfval 18926, dprdfcntz 19618 |
| cnv | converse | df-cnv 5597 |
◡𝐴 | Yes | opelcnvg 5789, f1ocnv 6728 |
| co | composition | df-co 5598 |
(𝐴 ∘ 𝐵) | Yes | cnvco 5794, fmptco 7001 |
| com | commutative | |
| No | orcom 867, bicomi 223, eqcomi 2747 |
| con | contradiction, contraposition | |
| No | condan 815, con2d 134 |
| csb | class substitution | df-csb 3833 |
⦋𝐴 / 𝑥⦌𝐵 | Yes |
csbid 3845, csbie2g 3875 |
| cyg | cyclic group | df-cyg 19478 |
CycGrp | Yes |
iscyg 19479, zringcyg 20691 |
| d | deduction form (suffix) | |
| No | idd 24, impbid 211 |
| df | (alternate) definition (prefix) | |
| No | dfrel2 6092, dffn2 6602 |
| di, distr | distributive | |
| No |
andi 1005, imdi 391, ordi 1003, difindi 4215, ndmovdistr 7461 |
| dif | class difference | df-dif 3890 |
(𝐴 ∖ 𝐵) | Yes |
difss 4066, difindi 4215 |
| div | division | df-div 11633 |
(𝐴 / 𝐵) | Yes |
divcl 11639, divval 11635, divmul 11636 |
| dm | domain | df-dm 5599 |
dom 𝐴 | Yes | dmmpt 6143, iswrddm0 14241 |
| e, eq, equ | equals (equ for setvars, eq for
classes) | df-cleq 2730 |
𝐴 = 𝐵 | Yes |
2p2e4 12108, uneqri 4085, equtr 2024 |
| edg | edge | df-edg 27418 |
(Edg‘𝐺) | Yes |
edgopval 27421, usgredgppr 27563 |
| el | element of | |
𝐴 ∈ 𝐵 | Yes |
eldif 3897, eldifsn 4720, elssuni 4871 |
| en | equinumerous | df-en |
𝐴 ≈ 𝐵 | Yes | domen 8751, enfi 8973 |
| eu | "there exists exactly one" | eu6 2574 |
∃!𝑥𝜑 | Yes | euex 2577, euabsn 4662 |
| ex | exists (i.e. is a set) | |
∈ V | No | brrelex1 5640, 0ex 5231 |
| ex, e | "there exists (at least one)" |
df-ex 1783 |
∃𝑥𝜑 | Yes | exim 1836, alex 1828 |
| exp | export | |
| No | expt 177, expcom 414 |
| f | "not free in" (suffix) | |
| No | equs45f 2459, sbf 2263 |
| f | function | df-f 6437 |
𝐹:𝐴⟶𝐵 | Yes | fssxp 6628, opelf 6635 |
| fal | false | df-fal 1552 |
⊥ | Yes | bifal 1555, falantru 1574 |
| fi | finite intersection | df-fi 9170 |
(fi‘𝐵) | Yes | fival 9171, inelfi 9177 |
| fi, fin | finite | df-fin 8737 |
Fin | Yes |
isfi 8764, snfi 8834, onfin 9013 |
| fld | field (Note: there is an alternative
definition Fld of a field, see df-fld 36150) | df-field 19994 |
Field | Yes | isfld 20000, fldidom 20576 |
| fn | function with domain | df-fn 6436 |
𝐴 Fn 𝐵 | Yes | ffn 6600, fndm 6536 |
| frgp | free group | df-frgp 19316 |
(freeGrp‘𝐼) | Yes |
frgpval 19364, frgpadd 19369 |
| fsupp | finitely supported function |
df-fsupp 9129 | 𝑅 finSupp 𝑍 | Yes |
isfsupp 9132, fdmfisuppfi 9137, fsuppco 9161 |
| fun | function | df-fun 6435 |
Fun 𝐹 | Yes | funrel 6451, ffun 6603 |
| fv | function value | df-fv 6441 |
(𝐹‘𝐴) | Yes | fvres 6793, swrdfv 14361 |
| fz | finite set of sequential integers |
df-fz 13240 |
(𝑀...𝑁) | Yes | fzval 13241, eluzfz 13251 |
| fz0 | finite set of sequential nonnegative integers |
|
(0...𝑁) | Yes | nn0fz0 13354, fz0tp 13357 |
| fzo | half-open integer range | df-fzo 13383 |
(𝑀..^𝑁) | Yes |
elfzo 13389, elfzofz 13403 |
| g | more general (suffix); eliminates "is a set"
hypotheses | |
| No | uniexg 7593 |
| gr | graph | |
| No | uhgrf 27432, isumgr 27465, usgrres1 27682 |
| grp | group | df-grp 18580 |
Grp | Yes | isgrp 18583, tgpgrp 23229 |
| gsum | group sum | df-gsum 17153 |
(𝐺 Σg 𝐹) | Yes |
gsumval 18361, gsumwrev 18973 |
| hash | size (of a set) | df-hash 14045 |
(♯‘𝐴) | Yes |
hashgval 14047, hashfz1 14060, hashcl 14071 |
| hb | hypothesis builder (prefix) | |
| No | hbxfrbi 1827, hbald 2168, hbequid 36923 |
| hm | (monoid, group, ring) homomorphism | |
| No | ismhm 18432, isghm 18834, isrhm 19965 |
| i | inference (suffix) | |
| No | eleq1i 2829, tcsni 9501 |
| i | implication (suffix) | |
| No | brwdomi 9327, infeq5i 9394 |
| id | identity | |
| No | biid 260 |
| iedg | indexed edge | df-iedg 27369 |
(iEdg‘𝐺) | Yes |
iedgval0 27410, edgiedgb 27424 |
| idm | idempotent | |
| No | anidm 565, tpidm13 4692 |
| im, imp | implication (label often omitted) |
df-im 14812 | (𝐴 → 𝐵) | Yes |
iman 402, imnan 400, impbidd 209 |
| ima | image | df-ima 5602 |
(𝐴 “ 𝐵) | Yes | resima 5925, imaundi 6053 |
| imp | import | |
| No | biimpa 477, impcom 408 |
| in | intersection | df-in 3894 |
(𝐴 ∩ 𝐵) | Yes | elin 3903, incom 4135 |
| inf | infimum | df-inf 9202 |
inf(ℝ+, ℝ*, < ) | Yes |
fiinfcl 9260, infiso 9267 |
| is... | is (something a) ...? | |
| No | isring 19787 |
| j | joining, disjoining | |
| No | jc 161, jaoi 854 |
| l | left | |
| No | olcd 871, simpl 483 |
| map | mapping operation or set exponentiation |
df-map 8617 | (𝐴 ↑m 𝐵) | Yes |
mapvalg 8625, elmapex 8636 |
| mat | matrix | df-mat 21555 |
(𝑁 Mat 𝑅) | Yes |
matval 21558, matring 21592 |
| mdet | determinant (of a square matrix) |
df-mdet 21734 | (𝑁 maDet 𝑅) | Yes |
mdetleib 21736, mdetrlin 21751 |
| mgm | magma | df-mgm 18326 |
Magma | Yes |
mgmidmo 18344, mgmlrid 18351, ismgm 18327 |
| mgp | multiplicative group | df-mgp 19721 |
(mulGrp‘𝑅) | Yes |
mgpress 19735, ringmgp 19789 |
| mnd | monoid | df-mnd 18386 |
Mnd | Yes | mndass 18394, mndodcong 19150 |
| mo | "there exists at most one" | df-mo 2540 |
∃*𝑥𝜑 | Yes | eumo 2578, moim 2544 |
| mp | modus ponens | ax-mp 5 |
| No | mpd 15, mpi 20 |
| mpo | maps-to notation for an operation |
df-mpo 7280 | (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) | Yes |
mpompt 7388, resmpo 7394 |
| mpt | modus ponendo tollens | |
| No | mptnan 1771, mptxor 1772 |
| mpt | maps-to notation for a function |
df-mpt 5158 | (𝑥 ∈ 𝐴 ↦ 𝐵) | Yes |
fconstmpt 5649, resmpt 5945 |
| mpt2 | maps-to notation for an operation (deprecated).
We are in the process of replacing mpt2 with mpo in labels. |
df-mpo 7280 | (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) | Yes |
mpompt 7388, resmpo 7394 |
| mul | multiplication (see "t") | df-mul 10883 |
(𝐴 · 𝐵) | Yes |
mulcl 10955, divmul 11636, mulcom 10957, mulass 10959 |
| n, not | not | |
¬ 𝜑 | Yes |
nan 827, 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 11330, ine0 11410, gt0ne0 11440 |
| nf | "not free in" (prefix) | |
| No | nfnd 1861 |
| ngp | normed group | df-ngp 23739 |
NrmGrp | Yes | isngp 23752, ngptps 23758 |
| nm | norm (on a group or ring) | df-nm 23738 |
(norm‘𝑊) | Yes |
nmval 23745, subgnm 23789 |
| nn | positive integers | df-nn 11974 |
ℕ | Yes | nnsscn 11978, nncn 11981 |
| nn0 | nonnegative integers | df-n0 12234 |
ℕ0 | Yes | nnnn0 12240, nn0cn 12243 |
| n0 | not the empty set (see ne0) | |
≠ ∅ | No | n0i 4267, vn0 4272, ssn0 4334 |
| OLD | old, obsolete (to be removed soon) | |
| No | 19.43OLD 1886 |
| on | ordinal number | df-on 6270 |
𝐴 ∈ On | Yes |
elon 6275, 1on 8309 onelon 6291 |
| op | ordered pair | df-op 4568 |
⟨𝐴, 𝐵⟩ | Yes | dfopif 4800, opth 5391 |
| or | or | df-or 845 |
(𝜑 ∨ 𝜓) | Yes |
orcom 867, anor 980 |
| ot | ordered triple | df-ot 4570 |
⟨𝐴, 𝐵, 𝐶⟩ | Yes |
euotd 5427, fnotovb 7325 |
| ov | operation value | df-ov 7278 |
(𝐴𝐹𝐵) | Yes
| fnotovb 7325, fnovrn 7447 |
| p | plus (see "add"), for all-constant
theorems | df-add 10882 |
(3 + 2) = 5 | Yes |
3p2e5 12124 |
| pfx | prefix | df-pfx 14384 |
(𝑊 prefix 𝐿) | Yes |
pfxlen 14396, ccatpfx 14414 |
| pm | Principia Mathematica | |
| No | pm2.27 42 |
| pm | partial mapping (operation) | df-pm 8618 |
(𝐴 ↑pm 𝐵) | Yes | elpmi 8634, pmsspw 8665 |
| pr | pair | df-pr 4564 |
{𝐴, 𝐵} | Yes |
elpr 4584, prcom 4668, prid1g 4696, prnz 4713 |
| prm, prime | prime (number) | df-prm 16377 |
ℙ | Yes | 1nprm 16384, dvdsprime 16392 |
| pss | proper subset | df-pss 3906 |
𝐴 ⊊ 𝐵 | Yes | pssss 4030, sspsstri 4037 |
| q | rational numbers ("quotients") | df-q 12689 |
ℚ | Yes | elq 12690 |
| r | right | |
| No | orcd 870, simprl 768 |
| rab | restricted class abstraction |
df-rab 3073 | {𝑥 ∈ 𝐴 ∣ 𝜑} | Yes |
rabswap 3423, df-oprab 7279 |
| ral | restricted universal quantification |
df-ral 3069 | ∀𝑥 ∈ 𝐴𝜑 | Yes |
ralnex 3167, ralrnmpo 7412 |
| rcl | reverse closure | |
| No | ndmfvrcl 6805, nnarcl 8447 |
| re | real numbers | df-r 10881 |
ℝ | Yes | recn 10961, 0re 10977 |
| rel | relation | df-rel 5596 | Rel 𝐴 |
Yes | brrelex1 5640, relmpoopab 7934 |
| res | restriction | df-res 5601 |
(𝐴 ↾ 𝐵) | Yes |
opelres 5897, f1ores 6730 |
| reu | restricted existential uniqueness |
df-reu 3072 | ∃!𝑥 ∈ 𝐴𝜑 | Yes |
nfreud 3302, reurex 3362 |
| rex | restricted existential quantification |
df-rex 3070 | ∃𝑥 ∈ 𝐴𝜑 | Yes |
rexnal 3169, rexrnmpo 7413 |
| rmo | restricted "at most one" |
df-rmo 3071 | ∃*𝑥 ∈ 𝐴𝜑 | Yes |
nfrmod 3303, nrexrmo 3366 |
| rn | range | df-rn 5600 | ran 𝐴 |
Yes | elrng 5800, rncnvcnv 5843 |
| rng | (unital) ring | df-ring 19785 |
Ring | Yes |
ringidval 19739, isring 19787, ringgrp 19788 |
| rot | rotation | |
| No | 3anrot 1099, 3orrot 1091 |
| 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 3717 | [𝐴 / 𝑥]𝜑 | Yes |
sbc2or 3725, sbcth 3731 |
| sca | scalar | df-sca 16978 |
(Scalar‘𝐻) | Yes |
resssca 17053, mgpsca 19728 |
| simp | simple, simplification | |
| No | simpl 483, simp3r3 1282 |
| sn | singleton | df-sn 4562 |
{𝐴} | Yes | eldifsn 4720 |
| sp | specialization | |
| No | spsbe 2085, spei 2394 |
| ss | subset | df-ss 3904 |
𝐴 ⊆ 𝐵 | Yes | difss 4066 |
| struct | structure | df-struct 16848 |
Struct | Yes | brstruct 16849, structfn 16857 |
| sub | subtract | df-sub 11207 |
(𝐴 − 𝐵) | Yes |
subval 11212, subaddi 11308 |
| sup | supremum | df-sup 9201 |
sup(𝐴, 𝐵, < ) | Yes |
fisupcl 9228, supmo 9211 |
| supp | support (of a function) | df-supp 7978 |
(𝐹 supp 𝑍) | Yes |
ressuppfi 9154, mptsuppd 8003 |
| swap | swap (two parts within a theorem) |
| | No | rabswap 3423, 2reuswap 3681 |
| syl | syllogism | syl 17 |
| No | 3syl 18 |
| sym | symmetric | |
| No | df-symdif 4176, cnvsym 6019 |
| symg | symmetric group | df-symg 18975 |
(SymGrp‘𝐴) | Yes |
symghash 18985, pgrpsubgsymg 19017 |
| t |
times (see "mul"), for all-constant theorems |
df-mul 10883 |
(3 · 2) = 6 | Yes |
3t2e6 12139 |
| th, t |
theorem |
|
|
No |
nfth 1804, sbcth 3731, weth 10251, ancomst 465 |
| tp | triple | df-tp 4566 |
{𝐴, 𝐵, 𝐶} | Yes |
eltpi 4623, tpeq1 4678 |
| tr | transitive | |
| No | bitrd 278, biantr 803 |
| tru, t |
true, truth |
df-tru 1542 |
⊤ |
Yes |
bitru 1548, truanfal 1573, biimt 361 |
| un | union | df-un 3892 |
(𝐴 ∪ 𝐵) | Yes |
uneqri 4085, uncom 4087 |
| unit | unit (in a ring) |
df-unit 19884 | (Unit‘𝑅) | Yes |
isunit 19899, nzrunit 20538 |
| v |
setvar (especially for specializations of
theorems when a class is replaced by a setvar variable) |
|
x |
Yes |
cv 1538, vex 3436, velpw 4538, vtoclf 3497 |
| v |
disjoint variable condition used in place of nonfreeness
hypothesis (suffix) |
|
|
No |
spimv 2390 |
| vtx |
vertex |
df-vtx 27368 |
(Vtx‘𝐺) |
Yes |
vtxval0 27409, opvtxov 27375 |
| 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 14218 | Word 𝑆 | Yes |
iswrdb 14223, wrdfn 14231, ffz0iswrd 14244 |
| xp | cross product (Cartesian product) |
df-xp 5595 | (𝐴 × 𝐵) | Yes |
elxp 5612, opelxpi 5626, xpundi 5655 |
| xr | eXtended reals | df-xr 11013 |
ℝ* | Yes | ressxr 11019, rexr 11021, 0xr 11022 |
| z | integers (from German "Zahlen") |
df-z 12320 | ℤ | Yes |
elz 12321, zcn 12324 |
| zn | ring of integers mod 𝑁 | df-zn 20708 |
(ℤ/nℤ‘𝑁) | Yes |
znval 20739, zncrng 20752, znhash 20766 |
| zring | ring of integers | df-zring 20671 |
ℤring | Yes | zringbas 20676, zringcrng 20672
|
| 0, z |
slashed zero (empty set) | df-nul 4257 |
∅ | Yes |
n0i 4267, vn0 4272; snnz 4712, prnz 4713 |
(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.) |
