| Description:
The following gives conventions used in the Metamath Proof Explorer
(MPE, set.mm) regarding labels.
For other conventions, see conventions 30282 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 3052"rgen.1 $e |- ( x e. A -> ph ) $."
or letters corresponding to the (main) class variable used in the
hypothesis, e.g., for mdet0 22552: "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 2651 and stirling 45615.
- 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 1833, and the restricted quantifier version of Theorem 21 from
Section 19 of [Margaris] p. 90 is labeled r19.21 3241.
- 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... 15863. 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 3947, and thus its syntax label fragment is "dif". Similarly, the
subclass relation 𝐴 ⊆ 𝐵 has syntax label fragment "ss"
because it is defined in df-ss 3961. 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 4128. There are many other syntax label fragments, e.g.,
singleton construct {𝐴} has syntax label fragment "sn" (because it
is defined in df-sn 4631), and the pair construct {𝐴, 𝐵} has
fragment "pr" ( from df-pr 4633). 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 4792. 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 11146) and "re" represents real numbers ℝ (Definition df-r 11150).
The empty set ∅ often uses fragment 0, even though it is defined
in df-nul 4323. The syntax construct (𝐴 + 𝐵) usually uses the
fragment "add" (which is consistent with df-add 11151), 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 12380.
- 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 16130 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 16050) we have value cosval 16103 and
closure coscl 16107.
- 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 30285 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 1934 versus 19.21 2195. This
often permits to prove the result using fewer axioms, and/or to
eliminate a nonfreeness hypothesis (such as Ⅎ𝑥𝜑 in 19.21 2195).
If no constraint is put on axiom use, then the v-version can be proved
from the original theorem using nfv 1909. If two (resp. three) such
disjoint variable conditions are added, then the suffix "vv" (resp.
"vvv") is used, e.g., exlimivv 1927.
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 2564 derived from eu6 2562. 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 5451.
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 2402 (cbval 2391 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 3537.
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 582), commutes
(e.g., biimpac 477)
- 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 475, rexlimiva 3136 |
| abl | Abelian group | df-abl 19750 |
Abel | Yes | ablgrp 19752, zringabl 21394 |
| abs | absorption | | | No |
ressabs 17233 |
| abs | absolute value (of a complex number) |
df-abs 15219 | (abs‘𝐴) | Yes |
absval 15221, absneg 15260, abs1 15280 |
| ad | adding | |
| No | adantr 479, ad2antlr 725 |
| add | add (see "p") | df-add 11151 |
(𝐴 + 𝐵) | Yes |
addcl 11222, addcom 11432, addass 11227 |
| al | "for all" | |
∀𝑥𝜑 | No | alim 1804, alex 1820 |
| ALT | alternative/less preferred (suffix) | |
| No | idALT 23 |
| an | and | df-an 395 |
(𝜑 ∧ 𝜓) | Yes |
anor 980, iman 400, imnan 398 |
| ant | antecedent | |
| No | adantr 479 |
| ass | associative | |
| No | biass 383, orass 919, mulass 11228 |
| asym | asymmetric, antisymmetric | |
| No | intasym 6122, asymref 6123, posasymb 18314 |
| ax | axiom | |
| No | ax6dgen 2116, ax1cn 11174 |
| bas, base |
base (set of an extensible structure) | df-base 17184 |
(Base‘𝑆) | Yes |
baseval 17185, ressbas 17218, cnfldbas 21300 |
| b, bi | biconditional ("iff", "if and only if")
| df-bi 206 | (𝜑 ↔ 𝜓) | Yes |
impbid 211, sspwb 5451 |
| br | binary relation | df-br 5150 |
𝐴𝑅𝐵 | Yes | brab1 5197, brun 5200 |
| c | commutes, commuted (suffix) | | |
No | biimpac 477 |
| c | contraction (suffix) | | |
No | sylc 65, syl2anc 582 |
| cbv | change bound variable | | |
No | cbvalivw 2002, cbvrex 3346 |
| cdm | codomain | |
| No | ffvelcdm 7090, focdmex 7960 |
| cl | closure | | | No |
ifclda 4565, ovrcl 7460, zaddcl 12635 |
| cn | complex numbers | df-c 11146 |
ℂ | Yes | nnsscn 12250, nncn 12253 |
| cnfld | field of complex numbers | df-cnfld 21297 |
ℂfld | Yes | cnfldbas 21300, cnfldinv 21347 |
| cntz | centralizer | df-cntz 19280 |
(Cntz‘𝑀) | Yes |
cntzfval 19283, dprdfcntz 19984 |
| cnv | converse | df-cnv 5686 |
◡𝐴 | Yes | opelcnvg 5883, f1ocnv 6850 |
| co | composition | df-co 5687 |
(𝐴 ∘ 𝐵) | Yes | cnvco 5888, fmptco 7138 |
| com | commutative | |
| No | orcom 868, bicomi 223, eqcomi 2734 |
| con | contradiction, contraposition | |
| No | condan 816, con2d 134 |
| csb | class substitution | df-csb 3890 |
⦋𝐴 / 𝑥⦌𝐵 | Yes |
csbid 3902, csbie2g 3932 |
| cyg | cyclic group | df-cyg 19845 |
CycGrp | Yes |
iscyg 19846, zringcyg 21412 |
| d | deduction form (suffix) | |
| No | idd 24, impbid 211 |
| df | (alternate) definition (prefix) | |
| No | dfrel2 6195, dffn2 6725 |
| di, distr | distributive | |
| No |
andi 1005, imdi 388, ordi 1003, difindi 4280, ndmovdistr 7610 |
| dif | class difference | df-dif 3947 |
(𝐴 ∖ 𝐵) | Yes |
difss 4128, difindi 4280 |
| div | division | df-div 11904 |
(𝐴 / 𝐵) | Yes |
divcl 11911, divval 11907, divmul 11908 |
| dm | domain | df-dm 5688 |
dom 𝐴 | Yes | dmmpt 6246, iswrddm0 14524 |
| e, eq, equ | equals (equ for setvars, eq for
classes) | df-cleq 2717 |
𝐴 = 𝐵 | Yes |
2p2e4 12380, uneqri 4148, equtr 2016 |
| edg | edge | df-edg 28933 |
(Edg‘𝐺) | Yes |
edgopval 28936, usgredgppr 29081 |
| el | element of | |
𝐴 ∈ 𝐵 | Yes |
eldif 3954, eldifsn 4792, elssuni 4941 |
| en | equinumerous | df-en |
𝐴 ≈ 𝐵 | Yes | domen 8982, enfi 9215 |
| eu | "there exists exactly one" | eu6 2562 |
∃!𝑥𝜑 | Yes | euex 2565, euabsn 4732 |
| ex | exists (i.e. is a set) | |
∈ V | No | brrelex1 5731, 0ex 5308 |
| ex, e | "there exists (at least one)" |
df-ex 1774 |
∃𝑥𝜑 | Yes | exim 1828, alex 1820 |
| exp | export | |
| No | expt 177, expcom 412 |
| f | "not free in" (suffix) | |
| No | equs45f 2452, sbf 2257 |
| f | function | df-f 6553 |
𝐹:𝐴⟶𝐵 | Yes | fssxp 6751, opelf 6758 |
| fal | false | df-fal 1546 |
⊥ | Yes | bifal 1549, falantru 1568 |
| fi | finite intersection | df-fi 9436 |
(fi‘𝐵) | Yes | fival 9437, inelfi 9443 |
| fi, fin | finite | df-fin 8968 |
Fin | Yes |
isfi 8997, snfi 9069, onfin 9255 |
| fld | field (Note: there is an alternative
definition Fld of a field, see df-fld 37596) | df-field 20639 |
Field | Yes | isfld 20647, fldidom 21275 |
| fn | function with domain | df-fn 6552 |
𝐴 Fn 𝐵 | Yes | ffn 6723, fndm 6658 |
| frgp | free group | df-frgp 19677 |
(freeGrp‘𝐼) | Yes |
frgpval 19725, frgpadd 19730 |
| fsupp | finitely supported function |
df-fsupp 9388 | 𝑅 finSupp 𝑍 | Yes |
isfsupp 9391, fdmfisuppfi 9399, fsuppco 9427 |
| fun | function | df-fun 6551 |
Fun 𝐹 | Yes | funrel 6571, ffun 6726 |
| fv | function value | df-fv 6557 |
(𝐹‘𝐴) | Yes | fvres 6915, swrdfv 14634 |
| fz | finite set of sequential integers |
df-fz 13520 |
(𝑀...𝑁) | Yes | fzval 13521, eluzfz 13531 |
| fz0 | finite set of sequential nonnegative integers |
|
(0...𝑁) | Yes | nn0fz0 13634, fz0tp 13637 |
| fzo | half-open integer range | df-fzo 13663 |
(𝑀..^𝑁) | Yes |
elfzo 13669, elfzofz 13683 |
| g | more general (suffix); eliminates "is a set"
hypotheses | |
| No | uniexg 7746 |
| gr | graph | |
| No | uhgrf 28947, isumgr 28980, usgrres1 29200 |
| grp | group | df-grp 18901 |
Grp | Yes | isgrp 18904, tgpgrp 24026 |
| gsum | group sum | df-gsum 17427 |
(𝐺 Σg 𝐹) | Yes |
gsumval 18640, gsumwrev 19332 |
| hash | size (of a set) | df-hash 14326 |
(♯‘𝐴) | Yes |
hashgval 14328, hashfz1 14341, hashcl 14351 |
| hb | hypothesis builder (prefix) | |
| No | hbxfrbi 1819, hbald 2157, hbequid 38511 |
| hm | (monoid, group, ring, ...) homomorphism |
| | No |
ismhm 18745, isghm 19178, isrhm 20429 |
| i | inference (suffix) | |
| No | eleq1i 2816, tcsni 9768 |
| i | implication (suffix) | |
| No | brwdomi 9593, infeq5i 9661 |
| id | identity | |
| No | biid 260 |
| iedg | indexed edge | df-iedg 28884 |
(iEdg‘𝐺) | Yes |
iedgval0 28925, edgiedgb 28939 |
| idm | idempotent | |
| No | anidm 563, tpidm13 4762 |
| im, imp | implication (label often omitted) |
df-im 15084 | (𝐴 → 𝐵) | Yes |
iman 400, imnan 398, impbidd 209 |
| im | (group, ring, ...) isomorphism | |
| No | isgim 19225, rimrcl 20433 |
| ima | image | df-ima 5691 |
(𝐴 “ 𝐵) | Yes | resima 6020, imaundi 6156 |
| imp | import | |
| No | biimpa 475, impcom 406 |
| in | intersection | df-in 3951 |
(𝐴 ∩ 𝐵) | Yes | elin 3960, incom 4199 |
| inf | infimum | df-inf 9468 |
inf(ℝ+, ℝ*, < ) | Yes |
fiinfcl 9526, infiso 9533 |
| is... | is (something a) ...? | |
| No | isring 20189 |
| j | joining, disjoining | |
| No | jc 161, jaoi 855 |
| l | left | |
| No | olcd 872, simpl 481 |
| map | mapping operation or set exponentiation |
df-map 8847 | (𝐴 ↑m 𝐵) | Yes |
mapvalg 8855, elmapex 8867 |
| mat | matrix | df-mat 22352 |
(𝑁 Mat 𝑅) | Yes |
matval 22355, matring 22389 |
| mdet | determinant (of a square matrix) |
df-mdet 22531 | (𝑁 maDet 𝑅) | Yes |
mdetleib 22533, mdetrlin 22548 |
| mgm | magma | df-mgm 18603 |
Magma | Yes |
mgmidmo 18623, mgmlrid 18630, ismgm 18604 |
| mgp | multiplicative group | df-mgp 20087 |
(mulGrp‘𝑅) | Yes |
mgpress 20101, ringmgp 20191 |
| mnd | monoid | df-mnd 18698 |
Mnd | Yes | mndass 18706, mndodcong 19509 |
| mo | "there exists at most one" | df-mo 2528 |
∃*𝑥𝜑 | Yes | eumo 2566, moim 2532 |
| mp | modus ponens | ax-mp 5 |
| No | mpd 15, mpi 20 |
| mpo | maps-to notation for an operation |
df-mpo 7424 | (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) | Yes |
mpompt 7534, resmpo 7540 |
| mpt | modus ponendo tollens | |
| No | mptnan 1762, mptxor 1763 |
| mpt | maps-to notation for a function |
df-mpt 5233 | (𝑥 ∈ 𝐴 ↦ 𝐵) | Yes |
fconstmpt 5740, resmpt 6042 |
| mpt2 | maps-to notation for an operation (deprecated).
We are in the process of replacing mpt2 with mpo in labels. |
df-mpo 7424 | (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) | Yes |
mpompt 7534, resmpo 7540 |
| mul | multiplication (see "t") | df-mul 11152 |
(𝐴 · 𝐵) | Yes |
mulcl 11224, divmul 11908, mulcom 11226, mulass 11228 |
| n, not | not | |
¬ 𝜑 | Yes |
nan 828, notnotr 130 |
| ne | not equal | df-ne | 𝐴 ≠ 𝐵 |
Yes | exmidne 2939, neeqtrd 2999 |
| nel | not element of | df-nel | 𝐴 ∉ 𝐵
|
Yes | neli 3037, nnel 3045 |
| ne0 | not equal to zero (see n0) | |
≠ 0 | No |
negne0d 11601, ine0 11681, gt0ne0 11711 |
| nf | "not free in" (prefix) | df-nf 1778 |
Ⅎ𝑥𝜑 | Yes | nfnd 1853 |
| ngp | normed group | df-ngp 24536 |
NrmGrp | Yes | isngp 24549, ngptps 24555 |
| nm | norm (on a group or ring) | df-nm 24535 |
(norm‘𝑊) | Yes |
nmval 24542, subgnm 24586 |
| nn | positive integers | df-nn 12246 |
ℕ | Yes | nnsscn 12250, nncn 12253 |
| nn0 | nonnegative integers | df-n0 12506 |
ℕ0 | Yes | nnnn0 12512, nn0cn 12515 |
| n0 | not the empty set (see ne0) | |
≠ ∅ | No | n0i 4333, vn0 4338, ssn0 4402 |
| OLD | old, obsolete (to be removed soon) | |
| No | 19.43OLD 1878 |
| on | ordinal number | df-on 6375 |
𝐴 ∈ On | Yes |
elon 6380, 1on 8499 onelon 6396 |
| op | ordered pair | df-op 4637 |
⟨𝐴, 𝐵⟩ | Yes | dfopif 4872, opth 5478 |
| or | or | df-or 846 |
(𝜑 ∨ 𝜓) | Yes |
orcom 868, anor 980 |
| ot | ordered triple | df-ot 4639 |
⟨𝐴, 𝐵, 𝐶⟩ | Yes |
euotd 5515, fnotovb 7470 |
| ov | operation value | df-ov 7422 |
(𝐴𝐹𝐵) | Yes
| fnotovb 7470, fnovrn 7596 |
| p | plus (see "add"), for all-constant
theorems | df-add 11151 |
(3 + 2) = 5 | Yes |
3p2e5 12396 |
| pfx | prefix | df-pfx 14657 |
(𝑊 prefix 𝐿) | Yes |
pfxlen 14669, ccatpfx 14687 |
| pm | Principia Mathematica | |
| No | pm2.27 42 |
| pm | partial mapping (operation) | df-pm 8848 |
(𝐴 ↑pm 𝐵) | Yes | elpmi 8865, pmsspw 8896 |
| pr | pair | df-pr 4633 |
{𝐴, 𝐵} | Yes |
elpr 4654, prcom 4738, prid1g 4766, prnz 4783 |
| prm, prime | prime (number) | df-prm 16646 |
ℙ | Yes | 1nprm 16653, dvdsprime 16661 |
| pss | proper subset | df-pss 3964 |
𝐴 ⊊ 𝐵 | Yes | pssss 4091, sspsstri 4098 |
| q | rational numbers ("quotients") | df-q 12966 |
ℚ | Yes | elq 12967 |
| r | reversed (suffix) | |
| No | pm4.71r 557, caovdir 7655 |
| r | right | |
| No | orcd 871, simprl 769 |
| rab | restricted class abstraction |
df-rab 3419 | {𝑥 ∈ 𝐴 ∣ 𝜑} | Yes |
rabswap 3428, df-oprab 7423 |
| ral | restricted universal quantification |
df-ral 3051 | ∀𝑥 ∈ 𝐴𝜑 | Yes |
ralnex 3061, ralrnmpo 7560 |
| rcl | reverse closure | |
| No | ndmfvrcl 6932, nnarcl 8637 |
| re | real numbers | df-r 11150 |
ℝ | Yes | recn 11230, 0re 11248 |
| rel | relation | df-rel 5685 | Rel 𝐴 |
Yes | brrelex1 5731, relmpoopab 8099 |
| res | restriction | df-res 5690 |
(𝐴 ↾ 𝐵) | Yes |
opelres 5991, f1ores 6852 |
| reu | restricted existential uniqueness |
df-reu 3364 | ∃!𝑥 ∈ 𝐴𝜑 | Yes |
nfreud 3415, reurex 3367 |
| rex | restricted existential quantification |
df-rex 3060 | ∃𝑥 ∈ 𝐴𝜑 | Yes |
rexnal 3089, rexrnmpo 7561 |
| rmo | restricted "at most one" |
df-rmo 3363 | ∃*𝑥 ∈ 𝐴𝜑 | Yes |
nfrmod 3414, nrexrmo 3384 |
| rn | range | df-rn 5689 | ran 𝐴 |
Yes | elrng 5894, rncnvcnv 5936 |
| ring | (unital) ring | df-ring 20187 |
Ring | Yes |
ringidval 20135, isring 20189, ringgrp 20190 |
| rng | non-unital ring | df-rng 20105 |
Rng | Yes |
isrng 20106, rngabl 20107, rnglz 20117 |
| rot | rotation | |
| No | 3anrot 1097, 3orrot 1089 |
| s | eliminates need for syllogism (suffix) |
| | No | ancoms 457 |
| sb | (proper) substitution (of a set) |
df-sb 2060 | [𝑦 / 𝑥]𝜑 | Yes |
spsbe 2077, sbimi 2069 |
| sbc | (proper) substitution of a class |
df-sbc 3774 | [𝐴 / 𝑥]𝜑 | Yes |
sbc2or 3782, sbcth 3788 |
| sca | scalar | df-sca 17252 |
(Scalar‘𝐻) | Yes |
resssca 17327, mgpsca 20094 |
| simp | simple, simplification | |
| No | simpl 481, simp3r3 1280 |
| sn | singleton | df-sn 4631 |
{𝐴} | Yes | eldifsn 4792 |
| sp | specialization | |
| No | spsbe 2077, spei 2387 |
| ss | subset | df-ss 3961 |
𝐴 ⊆ 𝐵 | Yes | difss 4128 |
| struct | structure | df-struct 17119 |
Struct | Yes | brstruct 17120, structfn 17128 |
| sub | subtract | df-sub 11478 |
(𝐴 − 𝐵) | Yes |
subval 11483, subaddi 11579 |
| sup | supremum | df-sup 9467 |
sup(𝐴, 𝐵, < ) | Yes |
fisupcl 9494, supmo 9477 |
| supp | support (of a function) | df-supp 8166 |
(𝐹 supp 𝑍) | Yes |
ressuppfi 9420, mptsuppd 8192 |
| swap | swap (two parts within a theorem) |
| | No | rabswap 3428, 2reuswap 3738 |
| syl | syllogism | syl 17 |
| No | 3syl 18 |
| sym | symmetric | |
| No | df-symdif 4241, cnvsym 6119 |
| symg | symmetric group | df-symg 19334 |
(SymGrp‘𝐴) | Yes |
symghash 19344, pgrpsubgsymg 19376 |
| t |
times (see "mul"), for all-constant theorems |
df-mul 11152 |
(3 · 2) = 6 | Yes |
3t2e6 12411 |
| th, t |
theorem |
|
|
No |
nfth 1795, sbcth 3788, weth 10520, ancomst 463 |
| tp | triple | df-tp 4635 |
{𝐴, 𝐵, 𝐶} | Yes |
eltpi 4693, tpeq1 4748 |
| tr | transitive | |
| No | bitrd 278, biantr 804 |
| tru, t |
true, truth |
df-tru 1536 |
⊤ |
Yes |
bitru 1542, truanfal 1567, biimt 359 |
| un | union | df-un 3949 |
(𝐴 ∪ 𝐵) | Yes |
uneqri 4148, uncom 4150 |
| unit | unit (in a ring) |
df-unit 20309 | (Unit‘𝑅) | Yes |
isunit 20324, nzrunit 20473 |
| v |
setvar (especially for specializations of
theorems when a class is replaced by a setvar variable) |
|
x |
Yes |
cv 1532, vex 3465, velpw 4609, vtoclf 3542 |
| v |
disjoint variable condition used in place of nonfreeness
hypothesis (suffix) |
|
|
No |
spimv 2383 |
| vtx |
vertex |
df-vtx 28883 |
(Vtx‘𝐺) |
Yes |
vtxval0 28924, opvtxov 28890 |
| vv |
two disjoint variable conditions used in place of nonfreeness
hypotheses (suffix) |
|
|
No |
19.23vv 1938 |
| w | weak (version of a theorem) (suffix) | |
| No | ax11w 2118, spnfw 1975 |
| wrd | word |
df-word 14501 | Word 𝑆 | Yes |
iswrdb 14506, wrdfn 14514, ffz0iswrd 14527 |
| xp | cross product (Cartesian product) |
df-xp 5684 | (𝐴 × 𝐵) | Yes |
elxp 5701, opelxpi 5715, xpundi 5746 |
| xr | eXtended reals | df-xr 11284 |
ℝ* | Yes | ressxr 11290, rexr 11292, 0xr 11293 |
| z | integers (from German "Zahlen") |
df-z 12592 | ℤ | Yes |
elz 12593, zcn 12596 |
| zn | ring of integers mod 𝑁 | df-zn 21449 |
(ℤ/nℤ‘𝑁) | Yes |
znval 21482, zncrng 21495, znhash 21509 |
| zring | ring of integers | df-zring 21390 |
ℤring | Yes | zringbas 21396, zringcrng 21391
|
| 0, z |
slashed zero (empty set) | df-nul 4323 |
∅ | Yes |
n0i 4333, vn0 4338; snnz 4782, prnz 4783 |
(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.) |
