| Description:
The following gives conventions used in the Metamath Proof Explorer
(MPE, set.mm) regarding labels.
For other conventions, see conventions 30362 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 3046"rgen.1 $e |- ( x e. A -> ph ) $."
or letters corresponding to the (main) class variable used in the
hypothesis, e.g., for mdet0 22509: "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 2656 and stirling 46071.
- 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 1839, and the restricted quantifier version of Theorem 21 from
Section 19 of [Margaris] p. 90 is labeled r19.21 3224.
- 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... 15806. 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 3908, and thus its syntax label fragment is "dif". Similarly, the
subclass relation 𝐴 ⊆ 𝐵 has syntax label fragment "ss"
because it is defined in df-ss 3922. 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 4089. There are many other syntax label fragments, e.g.,
singleton construct {𝐴} has syntax label fragment "sn" (because it
is defined in df-sn 4580), and the pair construct {𝐴, 𝐵} has
fragment "pr" ( from df-pr 4582). 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 4740. 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 11034) and "re" represents real numbers ℝ (Definition df-r 11038).
The empty set ∅ often uses fragment 0, even though it is defined
in df-nul 4287. The syntax construct (𝐴 + 𝐵) usually uses the
fragment "add" (which is consistent with df-add 11039), 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 12276.
- 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 16077 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 15995) we have value cosval 16050 and
closure coscl 16054.
- 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 30365 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 1939 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 1914. If two (resp. three) such
disjoint variable conditions are added, then the suffix "vv" (resp.
"vvv") is used, e.g., exlimivv 1932.
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 2569 derived from eu6 2567. 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 5396.
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 3517.
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 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 3122 |
| abl | Abelian group | df-abl 19680 |
Abel | Yes | ablgrp 19682, zringabl 21376 |
| abs | absorption | | | No |
ressabs 17177 |
| abs | absolute value (of a complex number) |
df-abs 15161 | (abs‘𝐴) | Yes |
absval 15163, absneg 15202, abs1 15222 |
| ad | adding | |
| No | adantr 480, ad2antlr 727 |
| add | add (see "p") | df-add 11039 |
(𝐴 + 𝐵) | Yes |
addcl 11110, addcom 11320, addass 11115 |
| al | "for all" | |
∀𝑥𝜑 | No | alim 1810, alex 1826 |
| ALT | alternative/less preferred (suffix) | |
| No | idALT 23 |
| an | and | df-an 396 |
(𝜑 ∧ 𝜓) | Yes |
anor 984, iman 401, imnan 399 |
| ant | antecedent | |
| No | adantr 480 |
| ass | associative | |
| No | biass 384, orass 921, mulass 11116 |
| asym | asymmetric, antisymmetric | |
| No | intasym 6068, asymref 6069, posasymb 18243 |
| ax | axiom | |
| No | ax6dgen 2129, ax1cn 11062 |
| bas, base |
base (set of an extensible structure) | df-base 17139 |
(Base‘𝑆) | Yes |
baseval 17140, ressbas 17165, cnfldbas 21283 |
| b, bi | biconditional ("iff", "if and only if")
| df-bi 207 | (𝜑 ↔ 𝜓) | Yes |
impbid 212, sspwb 5396 |
| br | binary relation | df-br 5096 |
𝐴𝑅𝐵 | Yes | brab1 5143, brun 5146 |
| c | commutes, commuted (suffix) | | |
No | biimpac 478 |
| c | contraction (suffix) | | |
No | sylc 65, syl2anc 584 |
| cbv | change bound variable | | |
No | cbvalivw 2007, cbvrex 3328 |
| cdm | codomain | |
| No | ffvelcdm 7019, focdmex 7898 |
| cl | closure | | | No |
ifclda 4514, ovrcl 7394, zaddcl 12533 |
| cn | complex numbers | df-c 11034 |
ℂ | Yes | nnsscn 12151, nncn 12154 |
| cnfld | field of complex numbers | df-cnfld 21280 |
ℂfld | Yes | cnfldbas 21283, cnfldinv 21327 |
| cntz | centralizer | df-cntz 19214 |
(Cntz‘𝑀) | Yes |
cntzfval 19217, dprdfcntz 19914 |
| cnv | converse | df-cnv 5631 |
◡𝐴 | Yes | opelcnvg 5827, f1ocnv 6780 |
| co | composition | df-co 5632 |
(𝐴 ∘ 𝐵) | Yes | cnvco 5832, fmptco 7067 |
| com | commutative | |
| No | orcom 870, bicomi 224, eqcomi 2738 |
| con | contradiction, contraposition | |
| No | condan 817, con2d 134 |
| csb | class substitution | df-csb 3854 |
⦋𝐴 / 𝑥⦌𝐵 | Yes |
csbid 3866, csbie2g 3893 |
| cyg | cyclic group | df-cyg 19775 |
CycGrp | Yes |
iscyg 19776, zringcyg 21394 |
| d | deduction form (suffix) | |
| No | idd 24, impbid 212 |
| df | (alternate) definition (prefix) | |
| No | dfrel2 6142, dffn2 6658 |
| di, distr | distributive | |
| No |
andi 1009, imdi 389, ordi 1007, difindi 4245, ndmovdistr 7542 |
| dif | class difference | df-dif 3908 |
(𝐴 ∖ 𝐵) | Yes |
difss 4089, difindi 4245 |
| div | division | df-div 11796 |
(𝐴 / 𝐵) | Yes |
divcl 11803, divval 11799, divmul 11800 |
| dm | domain | df-dm 5633 |
dom 𝐴 | Yes | dmmpt 6193, iswrddm0 14463 |
| e, eq, equ | equals (equ for setvars, eq for
classes) | df-cleq 2721 |
𝐴 = 𝐵 | Yes |
2p2e4 12276, uneqri 4109, equtr 2021 |
| edg | edge | df-edg 29011 |
(Edg‘𝐺) | Yes |
edgopval 29014, usgredgppr 29159 |
| el | element of | |
𝐴 ∈ 𝐵 | Yes |
eldif 3915, eldifsn 4740, elssuni 4891 |
| en | equinumerous | df-en |
𝐴 ≈ 𝐵 | Yes | domen 8894, enfi 9111 |
| eu | "there exists exactly one" | eu6 2567 |
∃!𝑥𝜑 | Yes | euex 2570, euabsn 4680 |
| ex | exists (i.e. is a set) | |
∈ V | No | brrelex1 5676, 0ex 5249 |
| ex, e | "there exists (at least one)" |
df-ex 1780 |
∃𝑥𝜑 | Yes | exim 1834, alex 1826 |
| exp | export | |
| No | expt 177, expcom 413 |
| f | "not free in" (suffix) | |
| No | equs45f 2457, sbf 2271 |
| f | function | df-f 6490 |
𝐹:𝐴⟶𝐵 | Yes | fssxp 6683, opelf 6689 |
| fal | false | df-fal 1553 |
⊥ | Yes | bifal 1556, falantru 1575 |
| fi | finite intersection | df-fi 9320 |
(fi‘𝐵) | Yes | fival 9321, inelfi 9327 |
| fi, fin | finite | df-fin 8883 |
Fin | Yes |
isfi 8908, snfi 8975, onfin 9139 |
| fld | field (Note: there is an alternative
definition Fld of a field, see df-fld 37971) | df-field 20635 |
Field | Yes | isfld 20643, fldidom 20674 |
| fn | function with domain | df-fn 6489 |
𝐴 Fn 𝐵 | Yes | ffn 6656, fndm 6589 |
| frgp | free group | df-frgp 19607 |
(freeGrp‘𝐼) | Yes |
frgpval 19655, frgpadd 19660 |
| fsupp | finitely supported function |
df-fsupp 9271 | 𝑅 finSupp 𝑍 | Yes |
isfsupp 9274, fdmfisuppfi 9283, fsuppco 9311 |
| fun | function | df-fun 6488 |
Fun 𝐹 | Yes | funrel 6503, ffun 6659 |
| fv | function value | df-fv 6494 |
(𝐹‘𝐴) | Yes | fvres 6845, swrdfv 14573 |
| fz | finite set of sequential integers |
df-fz 13429 |
(𝑀...𝑁) | Yes | fzval 13430, eluzfz 13440 |
| fz0 | finite set of sequential nonnegative integers |
|
(0...𝑁) | Yes | nn0fz0 13546, fz0tp 13549 |
| fzo | half-open integer range | df-fzo 13576 |
(𝑀..^𝑁) | Yes |
elfzo 13582, elfzofz 13596 |
| g | more general (suffix); eliminates "is a set"
hypotheses | |
| No | uniexg 7680 |
| gr | graph | |
| No | uhgrf 29025, isumgr 29058, usgrres1 29278 |
| grp | group | df-grp 18833 |
Grp | Yes | isgrp 18836, tgpgrp 23981 |
| gsum | group sum | df-gsum 17364 |
(𝐺 Σg 𝐹) | Yes |
gsumval 18569, gsumwrev 19263 |
| hash | size (of a set) | df-hash 14256 |
(♯‘𝐴) | Yes |
hashgval 14258, hashfz1 14271, hashcl 14281 |
| hb | hypothesis builder (prefix) | |
| No | hbxfrbi 1825, hbald 2169, hbequid 38887 |
| hm | (monoid, group, ring, ...) homomorphism |
| | No |
ismhm 18677, isghm 19112, isrhm 20381 |
| i | inference (suffix) | |
| No | eleq1i 2819, tcsni 9658 |
| i | implication (suffix) | |
| No | brwdomi 9479, infeq5i 9551 |
| id | identity | |
| No | biid 261 |
| iedg | indexed edge | df-iedg 28962 |
(iEdg‘𝐺) | Yes |
iedgval0 29003, edgiedgb 29017 |
| idm | idempotent | |
| No | anidm 564, tpidm13 4710 |
| im, imp | implication (label often omitted) |
df-im 15026 | (𝐴 → 𝐵) | Yes |
iman 401, imnan 399, impbidd 210 |
| im | (group, ring, ...) isomorphism | |
| No | isgim 19159, rimrcl 20385 |
| ima | image | df-ima 5636 |
(𝐴 “ 𝐵) | Yes | resima 5970, imaundi 6102 |
| imp | import | |
| No | biimpa 476, impcom 407 |
| in | intersection | df-in 3912 |
(𝐴 ∩ 𝐵) | Yes | elin 3921, incom 4162 |
| inf | infimum | df-inf 9352 |
inf(ℝ+, ℝ*, < ) | Yes |
fiinfcl 9412, infiso 9419 |
| is... | is (something a) ...? | |
| No | isring 20140 |
| j | joining, disjoining | |
| No | jc 161, jaoi 857 |
| l | left | |
| No | olcd 874, simpl 482 |
| map | mapping operation or set exponentiation |
df-map 8762 | (𝐴 ↑m 𝐵) | Yes |
mapvalg 8770, elmapex 8782 |
| mat | matrix | df-mat 22311 |
(𝑁 Mat 𝑅) | Yes |
matval 22314, matring 22346 |
| mdet | determinant (of a square matrix) |
df-mdet 22488 | (𝑁 maDet 𝑅) | Yes |
mdetleib 22490, mdetrlin 22505 |
| mgm | magma | df-mgm 18532 |
Magma | Yes |
mgmidmo 18552, mgmlrid 18559, ismgm 18533 |
| mgp | multiplicative group | df-mgp 20044 |
(mulGrp‘𝑅) | Yes |
mgpress 20053, ringmgp 20142 |
| mnd | monoid | df-mnd 18627 |
Mnd | Yes | mndass 18635, mndodcong 19439 |
| mo | "there exists at most one" | df-mo 2533 |
∃*𝑥𝜑 | Yes | eumo 2571, moim 2537 |
| mp | modus ponens | ax-mp 5 |
| No | mpd 15, mpi 20 |
| mpo | maps-to notation for an operation |
df-mpo 7358 | (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) | Yes |
mpompt 7467, resmpo 7473 |
| mpt | modus ponendo tollens | |
| No | mptnan 1768, mptxor 1769 |
| mpt | maps-to notation for a function |
df-mpt 5177 | (𝑥 ∈ 𝐴 ↦ 𝐵) | Yes |
fconstmpt 5685, resmpt 5992 |
| mul | multiplication (see "t") | df-mul 11040 |
(𝐴 · 𝐵) | Yes |
mulcl 11112, divmul 11800, mulcom 11114, mulass 11116 |
| n, not | not | |
¬ 𝜑 | Yes |
nan 829, notnotr 130 |
| ne | not equal | df-ne | 𝐴 ≠ 𝐵 |
Yes | exmidne 2935, neeqtrd 2994 |
| nel | not element of | df-nel | 𝐴 ∉ 𝐵
|
Yes | neli 3031, nnel 3039 |
| ne0 | not equal to zero (see n0) | |
≠ 0 | No |
negne0d 11491, ine0 11573, gt0ne0 11603 |
| nf | "not free in" (prefix) | df-nf 1784 |
Ⅎ𝑥𝜑 | Yes | nfnd 1858 |
| ngp | normed group | df-ngp 24487 |
NrmGrp | Yes | isngp 24500, ngptps 24506 |
| nm | norm (on a group or ring) | df-nm 24486 |
(norm‘𝑊) | Yes |
nmval 24493, subgnm 24537 |
| nn | positive integers | df-nn 12147 |
ℕ | Yes | nnsscn 12151, nncn 12154 |
| nn0 | nonnegative integers | df-n0 12403 |
ℕ0 | Yes | nnnn0 12409, nn0cn 12412 |
| n0 | not the empty set (see ne0) | |
≠ ∅ | No | n0i 4293, vn0 4298, ssn0 4357 |
| OLD | old, obsolete (to be removed soon) | |
| No | 19.43OLD 1883 |
| on | ordinal number | df-on 6315 |
𝐴 ∈ On | Yes |
elon 6320, 1on 8407 onelon 6336 |
| op | ordered pair | df-op 4586 |
⟨𝐴, 𝐵⟩ | Yes | dfopif 4824, opth 5423 |
| or | or | df-or 848 |
(𝜑 ∨ 𝜓) | Yes |
orcom 870, anor 984 |
| ot | ordered triple | df-ot 4588 |
⟨𝐴, 𝐵, 𝐶⟩ | Yes |
euotd 5460, fnotovb 7405 |
| ov | operation value | df-ov 7356 |
(𝐴𝐹𝐵) | Yes
| fnotovb 7405, fnovrn 7528 |
| p | plus (see "add"), for all-constant
theorems | df-add 11039 |
(3 + 2) = 5 | Yes |
3p2e5 12292 |
| pfx | prefix | df-pfx 14596 |
(𝑊 prefix 𝐿) | Yes |
pfxlen 14608, ccatpfx 14625 |
| pm | Principia Mathematica | |
| No | pm2.27 42 |
| pm | partial mapping (operation) | df-pm 8763 |
(𝐴 ↑pm 𝐵) | Yes | elpmi 8780, pmsspw 8811 |
| pr | pair | df-pr 4582 |
{𝐴, 𝐵} | Yes |
elpr 4604, prcom 4686, prid1g 4714, prnz 4731 |
| prm, prime | prime (number) | df-prm 16601 |
ℙ | Yes | 1nprm 16608, dvdsprime 16616 |
| pss | proper subset | df-pss 3925 |
𝐴 ⊊ 𝐵 | Yes | pssss 4051, sspsstri 4058 |
| q | rational numbers ("quotients") | df-q 12868 |
ℚ | Yes | elq 12869 |
| r | reversed (suffix) | |
| No | pm4.71r 558, caovdir 7587 |
| r | right | |
| No | orcd 873, simprl 770 |
| rab | restricted class abstraction |
df-rab 3397 | {𝑥 ∈ 𝐴 ∣ 𝜑} | Yes |
rabswap 3406, df-oprab 7357 |
| ral | restricted universal quantification |
df-ral 3045 | ∀𝑥 ∈ 𝐴𝜑 | Yes |
ralnex 3055, ralrnmpo 7492 |
| rcl | reverse closure | |
| No | ndmfvrcl 6860, nnarcl 8541 |
| re | real numbers | df-r 11038 |
ℝ | Yes | recn 11118, 0re 11136 |
| rel | relation | df-rel 5630 | Rel 𝐴 |
Yes | brrelex1 5676, relmpoopab 8034 |
| res | restriction | df-res 5635 |
(𝐴 ↾ 𝐵) | Yes |
opelres 5940, f1ores 6782 |
| reu | restricted existential uniqueness |
df-reu 3346 | ∃!𝑥 ∈ 𝐴𝜑 | Yes |
nfreud 3393, reurex 3349 |
| rex | restricted existential quantification |
df-rex 3054 | ∃𝑥 ∈ 𝐴𝜑 | Yes |
rexnal 3081, rexrnmpo 7493 |
| rmo | restricted "at most one" |
df-rmo 3345 | ∃*𝑥 ∈ 𝐴𝜑 | Yes |
nfrmod 3392, nrexrmo 3366 |
| rn | range | df-rn 5634 | ran 𝐴 |
Yes | elrng 5838, rncnvcnv 5880 |
| ring | (unital) ring | df-ring 20138 |
Ring | Yes |
ringidval 20086, isring 20140, ringgrp 20141 |
| rng | non-unital ring | df-rng 20056 |
Rng | Yes |
isrng 20057, rngabl 20058, rnglz 20068 |
| rot | rotation | |
| No | 3anrot 1099, 3orrot 1091 |
| s | eliminates need for syllogism (suffix) |
| | No | ancoms 458 |
| sb | (proper) substitution (of a set) |
df-sb 2066 | [𝑦 / 𝑥]𝜑 | Yes |
spsbe 2083, sbimi 2075 |
| sbc | (proper) substitution of a class |
df-sbc 3745 | [𝐴 / 𝑥]𝜑 | Yes |
sbc2or 3753, sbcth 3759 |
| sca | scalar | df-sca 17195 |
(Scalar‘𝐻) | Yes |
resssca 17265, mgpsca 20049 |
| simp | simple, simplification | |
| No | simpl 482, simp3r3 1284 |
| sn | singleton | df-sn 4580 |
{𝐴} | Yes | eldifsn 4740 |
| sp | specialization | |
| No | spsbe 2083, spei 2392 |
| ss | subset | df-ss 3922 |
𝐴 ⊆ 𝐵 | Yes | difss 4089 |
| struct | structure | df-struct 17076 |
Struct | Yes | brstruct 17077, structfn 17085 |
| sub | subtract | df-sub 11367 |
(𝐴 − 𝐵) | Yes |
subval 11372, subaddi 11469 |
| sup | supremum | df-sup 9351 |
sup(𝐴, 𝐵, < ) | Yes |
fisupcl 9379, supmo 9361 |
| supp | support (of a function) | df-supp 8101 |
(𝐹 supp 𝑍) | Yes |
ressuppfi 9304, mptsuppd 8127 |
| swap | swap (two parts within a theorem) |
| | No | rabswap 3406, 2reuswap 3708 |
| syl | syllogism | syl 17 |
| No | 3syl 18 |
| sym | symmetric | |
| No | df-symdif 4206, cnvsym 6067 |
| symg | symmetric group | df-symg 19267 |
(SymGrp‘𝐴) | Yes |
symghash 19275, pgrpsubgsymg 19306 |
| t |
times (see "mul"), for all-constant theorems |
df-mul 11040 |
(3 · 2) = 6 | Yes |
3t2e6 12307 |
| th, t |
theorem |
|
|
No |
nfth 1801, sbcth 3759, weth 10408, ancomst 464 |
| tp | triple | df-tp 4584 |
{𝐴, 𝐵, 𝐶} | Yes |
eltpi 4642, tpeq1 4696 |
| tr | transitive | |
| No | bitrd 279, biantr 805 |
| tru, t |
true, truth |
df-tru 1543 |
⊤ |
Yes |
bitru 1549, truanfal 1574, biimt 360 |
| un | union | df-un 3910 |
(𝐴 ∪ 𝐵) | Yes |
uneqri 4109, uncom 4111 |
| unit | unit (in a ring) |
df-unit 20261 | (Unit‘𝑅) | Yes |
isunit 20276, nzrunit 20427 |
| v |
setvar (especially for specializations of
theorems when a class is replaced by a setvar variable) |
|
x |
Yes |
cv 1539, vex 3442, velpw 4558, vtoclf 3521 |
| v |
disjoint variable condition used in place of nonfreeness
hypothesis (suffix) |
|
|
No |
spimv 2388 |
| vtx |
vertex |
df-vtx 28961 |
(Vtx‘𝐺) |
Yes |
vtxval0 29002, opvtxov 28968 |
| vv |
two disjoint variable conditions used in place of nonfreeness
hypotheses (suffix) |
|
|
No |
19.23vv 1943 |
| w | weak (version of a theorem) (suffix) | |
| No | ax11w 2131, spnfw 1979 |
| wrd | word |
df-word 14439 | Word 𝑆 | Yes |
iswrdb 14445, wrdfn 14453, ffz0iswrd 14466 |
| xp | cross product (Cartesian product) |
df-xp 5629 | (𝐴 × 𝐵) | Yes |
elxp 5646, opelxpi 5660, xpundi 5692 |
| xr | eXtended reals | df-xr 11172 |
ℝ* | Yes | ressxr 11178, rexr 11180, 0xr 11181 |
| z | integers (from German "Zahlen") |
df-z 12490 | ℤ | Yes |
elz 12491, zcn 12494 |
| zn | ring of integers mod 𝑁 | df-zn 21431 |
(ℤ/nℤ‘𝑁) | Yes |
znval 21460, zncrng 21469, znhash 21483 |
| zring | ring of integers | df-zring 21372 |
ℤring | Yes | zringbas 21378, zringcrng 21373
|
| 0, z |
slashed zero (empty set) | df-nul 4287 |
∅ | Yes |
n0i 4293, vn0 4298; snnz 4730, prnz 4731 |
(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.) |
