| Description:
The following gives conventions used in the Metamath Proof Explorer
(MPE, set.mm) regarding labels.
For other conventions, see conventions 30424 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 3069"rgen.1 $e |- ( x e. A -> ph ) $."
or letters corresponding to the (main) class variable used in the
hypothesis, e.g., for mdet0 22625: "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 2666 and stirling 45999.
- 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 1837, and the restricted quantifier version of Theorem 21 from
Section 19 of [Margaris] p. 90 is labeled r19.21 3260.
- 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... 15923. 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 3979, and thus its syntax label fragment is "dif". Similarly, the
subclass relation 𝐴 ⊆ 𝐵 has syntax label fragment "ss"
because it is defined in df-ss 3993. 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 4159. There are many other syntax label fragments, e.g.,
singleton construct {𝐴} has syntax label fragment "sn" (because it
is defined in df-sn 4649), and the pair construct {𝐴, 𝐵} has
fragment "pr" ( from df-pr 4651). 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 4811. 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 11184) and "re" represents real numbers ℝ (Definition df-r 11188).
The empty set ∅ often uses fragment 0, even though it is defined
in df-nul 4353. The syntax construct (𝐴 + 𝐵) usually uses the
fragment "add" (which is consistent with df-add 11189), 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 12422.
- 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 16192 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 16112) we have value cosval 16165 and
closure coscl 16169.
- 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 30427 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 1938 versus 19.21 2208. This
often permits to prove the result using fewer axioms, and/or to
eliminate a nonfreeness hypothesis (such as Ⅎ𝑥𝜑 in 19.21 2208).
If no constraint is put on axiom use, then the v-version can be proved
from the original theorem using nfv 1913. If two (resp. three) such
disjoint variable conditions are added, then the suffix "vv" (resp.
"vvv") is used, e.g., exlimivv 1931.
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 2579 derived from eu6 2577. 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 5469.
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 2417 (cbval 2406 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 3572.
Here is a non-exhaustive list of common suffixes:
- a : theorem having a conjunction as antecedent
- b : theorem expressing a logical equivalence
- c : contraction (e.g., sylc 65, syl2anc 583), commutes
(e.g., biimpac 478)
- d : theorem in deduction form
- f : theorem with a hypothesis such as Ⅎ𝑥𝜑
- g : theorem in closed form having an "is a set" antecedent
- i : theorem in inference form
- l : theorem concerning something at the left
- r : theorem concerning something at the right
- r : theorem with something reversed (e.g., a biconditional)
- s : inference that manipulates an antecedent ("s" refers to an
application of syl 17 that is eliminated)
- t : theorem in closed form (not having an "is a set" antecedent)
- v : theorem with one (main) disjoint variable condition
- vv : theorem with two (main) disjoint variable conditions
- w : weak(er) form of a theorem
- ALT : alternate proof of a theorem
- ALTV : alternate version of a theorem or definition (mathbox
only)
- OLD : old/obsolete version of a theorem (or proof) or definition
- Reuse.
When creating a new theorem or axiom, try to reuse abbreviations used
elsewhere. A comment should explain the first use of an abbreviation.
The following table shows some commonly used abbreviations in labels, in
alphabetical order. For each abbreviation we provide a mnenomic, the
source theorem or the assumption defining it, an expression showing what
it looks like, whether or not it is a "syntax fragment" (an abbreviation
that indicates a particular kind of syntax), and hyperlinks to label
examples that use the abbreviation. The abbreviation is bolded if there
is a df-NAME definition but the label fragment is not NAME. This is
not a complete list of abbreviations, though we do want this to
eventually be a complete list of exceptions.
| Abbreviation | Mnenomic | Source |
Expression | Syntax? | Example(s) |
|---|
| a | and (suffix) | |
| No | biimpa 476, rexlimiva 3153 |
| abl | Abelian group | df-abl 19819 |
Abel | Yes | ablgrp 19821, zringabl 21479 |
| abs | absorption | | | No |
ressabs 17302 |
| abs | absolute value (of a complex number) |
df-abs 15279 | (abs‘𝐴) | Yes |
absval 15281, absneg 15320, abs1 15340 |
| ad | adding | |
| No | adantr 480, ad2antlr 726 |
| add | add (see "p") | df-add 11189 |
(𝐴 + 𝐵) | Yes |
addcl 11260, addcom 11470, addass 11265 |
| al | "for all" | |
∀𝑥𝜑 | No | alim 1808, alex 1824 |
| ALT | alternative/less preferred (suffix) | |
| No | idALT 23 |
| an | and | df-an 396 |
(𝜑 ∧ 𝜓) | Yes |
anor 983, iman 401, imnan 399 |
| ant | antecedent | |
| No | adantr 480 |
| ass | associative | |
| No | biass 384, orass 920, mulass 11266 |
| asym | asymmetric, antisymmetric | |
| No | intasym 6142, asymref 6143, posasymb 18383 |
| ax | axiom | |
| No | ax6dgen 2128, ax1cn 11212 |
| bas, base |
base (set of an extensible structure) | df-base 17253 |
(Base‘𝑆) | Yes |
baseval 17254, ressbas 17287, cnfldbas 21385 |
| b, bi | biconditional ("iff", "if and only if")
| df-bi 207 | (𝜑 ↔ 𝜓) | Yes |
impbid 212, sspwb 5469 |
| br | binary relation | df-br 5167 |
𝐴𝑅𝐵 | Yes | brab1 5214, brun 5217 |
| c | commutes, commuted (suffix) | | |
No | biimpac 478 |
| c | contraction (suffix) | | |
No | sylc 65, syl2anc 583 |
| cbv | change bound variable | | |
No | cbvalivw 2006, cbvrex 3371 |
| cdm | codomain | |
| No | ffvelcdm 7110, focdmex 7990 |
| cl | closure | | | No |
ifclda 4583, ovrcl 7484, zaddcl 12677 |
| cn | complex numbers | df-c 11184 |
ℂ | Yes | nnsscn 12292, nncn 12295 |
| cnfld | field of complex numbers | df-cnfld 21382 |
ℂfld | Yes | cnfldbas 21385, cnfldinv 21432 |
| cntz | centralizer | df-cntz 19351 |
(Cntz‘𝑀) | Yes |
cntzfval 19354, dprdfcntz 20053 |
| cnv | converse | df-cnv 5703 |
◡𝐴 | Yes | opelcnvg 5900, f1ocnv 6869 |
| co | composition | df-co 5704 |
(𝐴 ∘ 𝐵) | Yes | cnvco 5905, fmptco 7158 |
| com | commutative | |
| No | orcom 869, bicomi 224, eqcomi 2749 |
| con | contradiction, contraposition | |
| No | condan 817, con2d 134 |
| csb | class substitution | df-csb 3922 |
⦋𝐴 / 𝑥⦌𝐵 | Yes |
csbid 3934, csbie2g 3964 |
| cyg | cyclic group | df-cyg 19914 |
CycGrp | Yes |
iscyg 19915, zringcyg 21497 |
| d | deduction form (suffix) | |
| No | idd 24, impbid 212 |
| df | (alternate) definition (prefix) | |
| No | dfrel2 6215, dffn2 6744 |
| di, distr | distributive | |
| No |
andi 1008, imdi 389, ordi 1006, difindi 4311, ndmovdistr 7633 |
| dif | class difference | df-dif 3979 |
(𝐴 ∖ 𝐵) | Yes |
difss 4159, difindi 4311 |
| div | division | df-div 11942 |
(𝐴 / 𝐵) | Yes |
divcl 11949, divval 11945, divmul 11946 |
| dm | domain | df-dm 5705 |
dom 𝐴 | Yes | dmmpt 6266, iswrddm0 14580 |
| e, eq, equ | equals (equ for setvars, eq for
classes) | df-cleq 2732 |
𝐴 = 𝐵 | Yes |
2p2e4 12422, uneqri 4179, equtr 2020 |
| edg | edge | df-edg 29075 |
(Edg‘𝐺) | Yes |
edgopval 29078, usgredgppr 29223 |
| el | element of | |
𝐴 ∈ 𝐵 | Yes |
eldif 3986, eldifsn 4811, elssuni 4961 |
| en | equinumerous | df-en |
𝐴 ≈ 𝐵 | Yes | domen 9015, enfi 9247 |
| eu | "there exists exactly one" | eu6 2577 |
∃!𝑥𝜑 | Yes | euex 2580, euabsn 4751 |
| ex | exists (i.e. is a set) | |
∈ V | No | brrelex1 5748, 0ex 5325 |
| ex, e | "there exists (at least one)" |
df-ex 1778 |
∃𝑥𝜑 | Yes | exim 1832, alex 1824 |
| exp | export | |
| No | expt 177, expcom 413 |
| f | "not free in" (suffix) | |
| No | equs45f 2467, sbf 2272 |
| f | function | df-f 6572 |
𝐹:𝐴⟶𝐵 | Yes | fssxp 6770, opelf 6777 |
| fal | false | df-fal 1550 |
⊥ | Yes | bifal 1553, falantru 1572 |
| fi | finite intersection | df-fi 9474 |
(fi‘𝐵) | Yes | fival 9475, inelfi 9481 |
| fi, fin | finite | df-fin 9001 |
Fin | Yes |
isfi 9030, snfi 9103, onfin 9287 |
| fld | field (Note: there is an alternative
definition Fld of a field, see df-fld 37944) | df-field 20748 |
Field | Yes | isfld 20756, fldidom 20787 |
| fn | function with domain | df-fn 6571 |
𝐴 Fn 𝐵 | Yes | ffn 6742, fndm 6677 |
| frgp | free group | df-frgp 19746 |
(freeGrp‘𝐼) | Yes |
frgpval 19794, frgpadd 19799 |
| fsupp | finitely supported function |
df-fsupp 9426 | 𝑅 finSupp 𝑍 | Yes |
isfsupp 9429, fdmfisuppfi 9437, fsuppco 9465 |
| fun | function | df-fun 6570 |
Fun 𝐹 | Yes | funrel 6590, ffun 6745 |
| fv | function value | df-fv 6576 |
(𝐹‘𝐴) | Yes | fvres 6934, swrdfv 14690 |
| fz | finite set of sequential integers |
df-fz 13562 |
(𝑀...𝑁) | Yes | fzval 13563, eluzfz 13573 |
| fz0 | finite set of sequential nonnegative integers |
|
(0...𝑁) | Yes | nn0fz0 13676, fz0tp 13679 |
| fzo | half-open integer range | df-fzo 13706 |
(𝑀..^𝑁) | Yes |
elfzo 13712, elfzofz 13726 |
| g | more general (suffix); eliminates "is a set"
hypotheses | |
| No | uniexg 7769 |
| gr | graph | |
| No | uhgrf 29089, isumgr 29122, usgrres1 29342 |
| grp | group | df-grp 18970 |
Grp | Yes | isgrp 18973, tgpgrp 24099 |
| gsum | group sum | df-gsum 17496 |
(𝐺 Σg 𝐹) | Yes |
gsumval 18709, gsumwrev 19403 |
| hash | size (of a set) | df-hash 14374 |
(♯‘𝐴) | Yes |
hashgval 14376, hashfz1 14389, hashcl 14399 |
| hb | hypothesis builder (prefix) | |
| No | hbxfrbi 1823, hbald 2169, hbequid 38857 |
| hm | (monoid, group, ring, ...) homomorphism |
| | No |
ismhm 18814, isghm 19249, isrhm 20498 |
| i | inference (suffix) | |
| No | eleq1i 2835, tcsni 9806 |
| i | implication (suffix) | |
| No | brwdomi 9631, infeq5i 9699 |
| id | identity | |
| No | biid 261 |
| iedg | indexed edge | df-iedg 29026 |
(iEdg‘𝐺) | Yes |
iedgval0 29067, edgiedgb 29081 |
| idm | idempotent | |
| No | anidm 564, tpidm13 4781 |
| im, imp | implication (label often omitted) |
df-im 15144 | (𝐴 → 𝐵) | Yes |
iman 401, imnan 399, impbidd 210 |
| im | (group, ring, ...) isomorphism | |
| No | isgim 19296, rimrcl 20502 |
| ima | image | df-ima 5708 |
(𝐴 “ 𝐵) | Yes | resima 6039, imaundi 6176 |
| imp | import | |
| No | biimpa 476, impcom 407 |
| in | intersection | df-in 3983 |
(𝐴 ∩ 𝐵) | Yes | elin 3992, incom 4230 |
| inf | infimum | df-inf 9506 |
inf(ℝ+, ℝ*, < ) | Yes |
fiinfcl 9564, infiso 9571 |
| is... | is (something a) ...? | |
| No | isring 20258 |
| j | joining, disjoining | |
| No | jc 161, jaoi 856 |
| l | left | |
| No | olcd 873, simpl 482 |
| map | mapping operation or set exponentiation |
df-map 8880 | (𝐴 ↑m 𝐵) | Yes |
mapvalg 8888, elmapex 8900 |
| mat | matrix | df-mat 22425 |
(𝑁 Mat 𝑅) | Yes |
matval 22428, matring 22462 |
| mdet | determinant (of a square matrix) |
df-mdet 22604 | (𝑁 maDet 𝑅) | Yes |
mdetleib 22606, mdetrlin 22621 |
| mgm | magma | df-mgm 18672 |
Magma | Yes |
mgmidmo 18692, mgmlrid 18699, ismgm 18673 |
| mgp | multiplicative group | df-mgp 20156 |
(mulGrp‘𝑅) | Yes |
mgpress 20170, ringmgp 20260 |
| mnd | monoid | df-mnd 18767 |
Mnd | Yes | mndass 18775, mndodcong 19578 |
| mo | "there exists at most one" | df-mo 2543 |
∃*𝑥𝜑 | Yes | eumo 2581, moim 2547 |
| mp | modus ponens | ax-mp 5 |
| No | mpd 15, mpi 20 |
| mpo | maps-to notation for an operation |
df-mpo 7448 | (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) | Yes |
mpompt 7558, resmpo 7564 |
| mpt | modus ponendo tollens | |
| No | mptnan 1766, mptxor 1767 |
| mpt | maps-to notation for a function |
df-mpt 5250 | (𝑥 ∈ 𝐴 ↦ 𝐵) | Yes |
fconstmpt 5757, resmpt 6061 |
| mul | multiplication (see "t") | df-mul 11190 |
(𝐴 · 𝐵) | Yes |
mulcl 11262, divmul 11946, mulcom 11264, mulass 11266 |
| n, not | not | |
¬ 𝜑 | Yes |
nan 829, notnotr 130 |
| ne | not equal | df-ne | 𝐴 ≠ 𝐵 |
Yes | exmidne 2956, neeqtrd 3016 |
| nel | not element of | df-nel | 𝐴 ∉ 𝐵
|
Yes | neli 3054, nnel 3062 |
| ne0 | not equal to zero (see n0) | |
≠ 0 | No |
negne0d 11639, ine0 11719, gt0ne0 11749 |
| nf | "not free in" (prefix) | df-nf 1782 |
Ⅎ𝑥𝜑 | Yes | nfnd 1857 |
| ngp | normed group | df-ngp 24609 |
NrmGrp | Yes | isngp 24622, ngptps 24628 |
| nm | norm (on a group or ring) | df-nm 24608 |
(norm‘𝑊) | Yes |
nmval 24615, subgnm 24659 |
| nn | positive integers | df-nn 12288 |
ℕ | Yes | nnsscn 12292, nncn 12295 |
| nn0 | nonnegative integers | df-n0 12548 |
ℕ0 | Yes | nnnn0 12554, nn0cn 12557 |
| n0 | not the empty set (see ne0) | |
≠ ∅ | No | n0i 4363, vn0 4368, ssn0 4427 |
| OLD | old, obsolete (to be removed soon) | |
| No | 19.43OLD 1882 |
| on | ordinal number | df-on 6394 |
𝐴 ∈ On | Yes |
elon 6399, 1on 8528 onelon 6415 |
| op | ordered pair | df-op 4655 |
⟨𝐴, 𝐵⟩ | Yes | dfopif 4894, opth 5496 |
| or | or | df-or 847 |
(𝜑 ∨ 𝜓) | Yes |
orcom 869, anor 983 |
| ot | ordered triple | df-ot 4657 |
⟨𝐴, 𝐵, 𝐶⟩ | Yes |
euotd 5532, fnotovb 7494 |
| ov | operation value | df-ov 7446 |
(𝐴𝐹𝐵) | Yes
| fnotovb 7494, fnovrn 7619 |
| p | plus (see "add"), for all-constant
theorems | df-add 11189 |
(3 + 2) = 5 | Yes |
3p2e5 12438 |
| pfx | prefix | df-pfx 14713 |
(𝑊 prefix 𝐿) | Yes |
pfxlen 14725, ccatpfx 14743 |
| pm | Principia Mathematica | |
| No | pm2.27 42 |
| pm | partial mapping (operation) | df-pm 8881 |
(𝐴 ↑pm 𝐵) | Yes | elpmi 8898, pmsspw 8929 |
| pr | pair | df-pr 4651 |
{𝐴, 𝐵} | Yes |
elpr 4672, prcom 4757, prid1g 4785, prnz 4802 |
| prm, prime | prime (number) | df-prm 16713 |
ℙ | Yes | 1nprm 16720, dvdsprime 16728 |
| pss | proper subset | df-pss 3996 |
𝐴 ⊊ 𝐵 | Yes | pssss 4121, sspsstri 4128 |
| q | rational numbers ("quotients") | df-q 13008 |
ℚ | Yes | elq 13009 |
| r | reversed (suffix) | |
| No | pm4.71r 558, caovdir 7678 |
| r | right | |
| No | orcd 872, simprl 770 |
| rab | restricted class abstraction |
df-rab 3444 | {𝑥 ∈ 𝐴 ∣ 𝜑} | Yes |
rabswap 3453, df-oprab 7447 |
| ral | restricted universal quantification |
df-ral 3068 | ∀𝑥 ∈ 𝐴𝜑 | Yes |
ralnex 3078, ralrnmpo 7583 |
| rcl | reverse closure | |
| No | ndmfvrcl 6951, nnarcl 8666 |
| re | real numbers | df-r 11188 |
ℝ | Yes | recn 11268, 0re 11286 |
| rel | relation | df-rel 5702 | Rel 𝐴 |
Yes | brrelex1 5748, relmpoopab 8129 |
| res | restriction | df-res 5707 |
(𝐴 ↾ 𝐵) | Yes |
opelres 6010, f1ores 6871 |
| reu | restricted existential uniqueness |
df-reu 3389 | ∃!𝑥 ∈ 𝐴𝜑 | Yes |
nfreud 3440, reurex 3392 |
| rex | restricted existential quantification |
df-rex 3077 | ∃𝑥 ∈ 𝐴𝜑 | Yes |
rexnal 3106, rexrnmpo 7584 |
| rmo | restricted "at most one" |
df-rmo 3388 | ∃*𝑥 ∈ 𝐴𝜑 | Yes |
nfrmod 3439, nrexrmo 3409 |
| rn | range | df-rn 5706 | ran 𝐴 |
Yes | elrng 5911, rncnvcnv 5954 |
| ring | (unital) ring | df-ring 20256 |
Ring | Yes |
ringidval 20204, isring 20258, ringgrp 20259 |
| rng | non-unital ring | df-rng 20174 |
Rng | Yes |
isrng 20175, rngabl 20176, rnglz 20186 |
| rot | rotation | |
| No | 3anrot 1100, 3orrot 1092 |
| s | eliminates need for syllogism (suffix) |
| | No | ancoms 458 |
| sb | (proper) substitution (of a set) |
df-sb 2065 | [𝑦 / 𝑥]𝜑 | Yes |
spsbe 2082, sbimi 2074 |
| sbc | (proper) substitution of a class |
df-sbc 3805 | [𝐴 / 𝑥]𝜑 | Yes |
sbc2or 3813, sbcth 3819 |
| sca | scalar | df-sca 17321 |
(Scalar‘𝐻) | Yes |
resssca 17396, mgpsca 20163 |
| simp | simple, simplification | |
| No | simpl 482, simp3r3 1283 |
| sn | singleton | df-sn 4649 |
{𝐴} | Yes | eldifsn 4811 |
| sp | specialization | |
| No | spsbe 2082, spei 2402 |
| ss | subset | df-ss 3993 |
𝐴 ⊆ 𝐵 | Yes | difss 4159 |
| struct | structure | df-struct 17188 |
Struct | Yes | brstruct 17189, structfn 17197 |
| sub | subtract | df-sub 11516 |
(𝐴 − 𝐵) | Yes |
subval 11521, subaddi 11617 |
| sup | supremum | df-sup 9505 |
sup(𝐴, 𝐵, < ) | Yes |
fisupcl 9532, supmo 9515 |
| supp | support (of a function) | df-supp 8196 |
(𝐹 supp 𝑍) | Yes |
ressuppfi 9458, mptsuppd 8222 |
| swap | swap (two parts within a theorem) |
| | No | rabswap 3453, 2reuswap 3768 |
| syl | syllogism | syl 17 |
| No | 3syl 18 |
| sym | symmetric | |
| No | df-symdif 4272, cnvsym 6139 |
| symg | symmetric group | df-symg 19405 |
(SymGrp‘𝐴) | Yes |
symghash 19413, pgrpsubgsymg 19445 |
| t |
times (see "mul"), for all-constant theorems |
df-mul 11190 |
(3 · 2) = 6 | Yes |
3t2e6 12453 |
| th, t |
theorem |
|
|
No |
nfth 1799, sbcth 3819, weth 10558, ancomst 464 |
| tp | triple | df-tp 4653 |
{𝐴, 𝐵, 𝐶} | Yes |
eltpi 4711, tpeq1 4767 |
| tr | transitive | |
| No | bitrd 279, biantr 805 |
| tru, t |
true, truth |
df-tru 1540 |
⊤ |
Yes |
bitru 1546, truanfal 1571, biimt 360 |
| un | union | df-un 3981 |
(𝐴 ∪ 𝐵) | Yes |
uneqri 4179, uncom 4181 |
| unit | unit (in a ring) |
df-unit 20378 | (Unit‘𝑅) | Yes |
isunit 20393, nzrunit 20544 |
| v |
setvar (especially for specializations of
theorems when a class is replaced by a setvar variable) |
|
x |
Yes |
cv 1536, vex 3492, velpw 4627, vtoclf 3576 |
| v |
disjoint variable condition used in place of nonfreeness
hypothesis (suffix) |
|
|
No |
spimv 2398 |
| vtx |
vertex |
df-vtx 29025 |
(Vtx‘𝐺) |
Yes |
vtxval0 29066, opvtxov 29032 |
| vv |
two disjoint variable conditions used in place of nonfreeness
hypotheses (suffix) |
|
|
No |
19.23vv 1942 |
| w | weak (version of a theorem) (suffix) | |
| No | ax11w 2130, spnfw 1979 |
| wrd | word |
df-word 14557 | Word 𝑆 | Yes |
iswrdb 14562, wrdfn 14570, ffz0iswrd 14583 |
| xp | cross product (Cartesian product) |
df-xp 5701 | (𝐴 × 𝐵) | Yes |
elxp 5718, opelxpi 5732, xpundi 5763 |
| xr | eXtended reals | df-xr 11322 |
ℝ* | Yes | ressxr 11328, rexr 11330, 0xr 11331 |
| z | integers (from German "Zahlen") |
df-z 12634 | ℤ | Yes |
elz 12635, zcn 12638 |
| zn | ring of integers mod 𝑁 | df-zn 21534 |
(ℤ/nℤ‘𝑁) | Yes |
znval 21567, zncrng 21580, znhash 21594 |
| zring | ring of integers | df-zring 21475 |
ℤring | Yes | zringbas 21481, zringcrng 21476
|
| 0, z |
slashed zero (empty set) | df-nul 4353 |
∅ | Yes |
n0i 4363, vn0 4368; snnz 4801, prnz 4802 |
(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.) |
