| Description:
The following gives conventions used in the Metamath Proof Explorer
(MPE, set.mm) regarding labels.
For other conventions, see conventions 30548 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 3077"rgen.1 $e |- ( x e. A -> ph ) $."
or letters corresponding to the (main) class variable used in the
hypothesis, e.g., for mdet0 22646: "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 2688 and stirling 46627.
- 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 1858, and the restricted quantifier version of Theorem 21 from
Section 19 of [Margaris] p. 90 is labeled r19.21 3256.
- 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... 15894. 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 3907, and thus its syntax label fragment is "dif". Similarly, the
subclass relation 𝐴 ⊆ 𝐵 has syntax label fragment "ss"
because it is defined in df-ss 3921. 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 4582), and the pair construct {𝐴, 𝐵} has
fragment "pr" ( from df-pr 4584). 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 4745. An "n" is often used for negation (¬), e.g.,
nan 840.
- 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 11076) and "re" represents real numbers ℝ (Definition df-r 11080).
The empty set ∅ often uses fragment 0, even though it is defined
in df-nul 4286. The syntax construct (𝐴 + 𝐵) usually uses the
fragment "add" (which is consistent with df-add 11081), 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 12349.
- 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 16165 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 16083) we have value cosval 16138 and
closure coscl 16142.
- 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 30551 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 1958 versus 19.21 2241. This
often permits to prove the result using fewer axioms, and/or to
eliminate a nonfreeness hypothesis (such as Ⅎ𝑥𝜑 in 19.21 2241).
If no constraint is put on axiom use, then the v-version can be proved
from the original theorem using nfv 1933. If two (resp. three) such
disjoint variable conditions are added, then the suffix "vv" (resp.
"vvv") is used, e.g., exlimivv 1951.
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 2602 derived from eu6 2600. 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 5415.
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 2439 (cbval 2428 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 3526.
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 593), commutes
(e.g., biimpac 482)
- 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 480, rexlimiva 3154 |
| abl | Abelian group | df-abl 19806 |
Abel | Yes | ablgrp 19808, zringabl 21483 |
| abs | absorption | | | No |
ressabs 17267 |
| abs | absolute value (of a complex number) |
df-abs 15246 | (abs‘𝐴) | Yes |
absval 15248, absneg 15287, abs1 15307 |
| ad | adding | |
| No | adantr 484, ad2antlr 737 |
| add | add (see "p") | df-add 11081 |
(𝐴 + 𝐵) | Yes |
addcl 11152, addcom 11366, addass 11157 |
| al | "for all" | |
∀𝑥𝜑 | No | alim 1829, alex 1845 |
| ALT | alternative/less preferred (suffix) | |
| No | idALT 23 |
| an | and | df-an 400 |
(𝜑 ∧ 𝜓) | Yes |
anor 995, iman 405, imnan 403 |
| ant | antecedent | |
| No | adantr 484 |
| ass | associative | |
| No | biass 387, orass 932, mulass 11158 |
| asym | asymmetric, antisymmetric | |
| No | intasym 6099, asymref 6100, posasymb 18334 |
| ax | axiom | |
| No | ax6dgen 2161, ax1cn 11104 |
| bas, base |
base (set of an extensible structure) | df-base 17229 |
(Base‘𝑆) | Yes |
baseval 17230, ressbas 17255, cnfldbas 21408 |
| b, bi | biconditional ("iff", "if and only if")
| df-bi 209 | (𝜑 ↔ 𝜓) | Yes |
impbid 214, sspwb 5415 |
| br | binary relation | df-br 5100 |
𝐴𝑅𝐵 | Yes | brab1 5147, brun 5150 |
| c | commutes, commuted (suffix) | | |
No | biimpac 482 |
| c | contraction (suffix) | | |
No | sylc 65, syl2anc 593 |
| cbv | change bound variable | | |
No | cbvalivw 2026, cbvrex 3349 |
| cdm | codomain | |
| No | ffvelcdm 7058, focdmex 7933 |
| cl | closure | | | No |
ifclda 4515, ovrcl 7433, zaddcl 12608 |
| cn | complex numbers | df-c 11076 |
ℂ | Yes | nnsscn 12212, nncn 12215 |
| cnfld | field of complex numbers | df-cnfld 21405 |
ℂfld | Yes | cnfldbas 21408, cnfldinv 21435 |
| cntz | centralizer | df-cntz 19340 |
(Cntz‘𝑀) | Yes |
cntzfval 19343, dprdfcntz 20040 |
| cnv | converse | df-cnv 5653 |
◡𝐴 | Yes | opelcnvg 5850, f1ocnv 6815 |
| co | composition | df-co 5654 |
(𝐴 ∘ 𝐵) | Yes | cnvco 5859, fmptco 7107 |
| com | commutative | |
| No | orcom 881, bicomi 226, eqcomi 2770 |
| con | contradiction, contraposition | |
| No | condan 827, con2d 134 |
| csb | class substitution | df-csb 3853 |
⦋𝐴 / 𝑥⦌𝐵 | Yes |
csbid 3865, csbie2g 3892 |
| cyg | cyclic group | df-cyg 19901 |
CycGrp | Yes |
iscyg 19902, zringcyg 21501 |
| d | deduction form (suffix) | |
| No | idd 24, impbid 214 |
| df | (alternate) definition (prefix) | |
| No | dfrel2 6171, dffn2 6689 |
| di, distr | distributive | |
| No |
andi 1020, imdi 392, ordi 1018, difindi 4244, ndmovdistr 7581 |
| dif | class difference | df-dif 3907 |
(𝐴 ∖ 𝐵) | Yes |
difss 4089, difindi 4244 |
| div | division | df-div 11842 |
(𝐴 / 𝐵) | Yes |
divcl 11848, divval 11844, divmul 11845 |
| dm | domain | df-dm 5655 |
dom 𝐴 | Yes | dmmpt 6223, iswrddm0 14548 |
| e, eq, equ | equals (equ for setvars, eq for
classes) | df-cleq 2753 |
𝐴 = 𝐵 | Yes |
2p2e4 12349, uneqri 4109, equtr 2040 |
| edg | edge | df-edg 29195 |
(Edg‘𝐺) | Yes |
edgopval 29198, usgredgppr 29343 |
| el | element of | |
𝐴 ∈ 𝐵 | Yes |
eldif 3914, eldifsn 4745, elssuni 4896 |
| en | equinumerous | df-en |
𝐴 ≈ 𝐵 | Yes | domen 8938, enfi 9151 |
| eu | "there exists exactly one" | eu6 2600 |
∃!𝑥𝜑 | Yes | euex 2603, euabsn 4684 |
| ex | exists (i.e. is a set) | |
∈ V | No | brrelex1 5698, 0ex 5256 |
| ex, e | "there exists (at least one)" |
df-ex 1799 |
∃𝑥𝜑 | Yes | exim 1853, alex 1845 |
| exp | export | |
| No | expt 177, expcom 417 |
| f | "not free in" (suffix) | |
| No | equs45f 2489, sbf 2304 |
| f | function | df-f 6521 |
𝐹:𝐴⟶𝐵 | Yes | fssxp 6715, opelf 6721 |
| fal | false | df-fal 1572 |
⊥ | Yes | bifal 1575, falantru 1594 |
| fi | finite intersection | df-fi 9354 |
(fi‘𝐵) | Yes | fival 9355, inelfi 9361 |
| fi, fin | finite | df-fin 8927 |
Fin | Yes |
isfi 8952, snfi 9020, onfin 9179 |
| fld | field (Note: there is an alternative
definition Fld of a field, see df-fld 38455) | df-field 20761 |
Field | Yes | isfld 20769, fldidom 20800 |
| fn | function with domain | df-fn 6520 |
𝐴 Fn 𝐵 | Yes | ffn 6687, fndm 6620 |
| frgp | free group | df-frgp 19733 |
(freeGrp‘𝐼) | Yes |
frgpval 19781, frgpadd 19786 |
| fsupp | finitely supported function |
df-fsupp 9305 | 𝑅 finSupp 𝑍 | Yes |
isfsupp 9308, fdmfisuppfi 9317, fsuppco 9345 |
| fun | function | df-fun 6519 |
Fun 𝐹 | Yes | funrel 6534, ffun 6690 |
| fv | function value | df-fv 6525 |
(𝐹‘𝐴) | Yes | fvres 6882, swrdfv 14659 |
| fz | finite set of sequential integers |
df-fz 13510 |
(𝑀...𝑁) | Yes | fzval 13511, eluzfz 13521 |
| fz0 | finite set of sequential nonnegative integers |
|
(0...𝑁) | Yes | nn0fz0 13627, fz0tp 13630 |
| fzo | half-open integer range | df-fzo 13657 |
(𝑀..^𝑁) | Yes |
elfzo 13663, elfzofz 13678 |
| g | more general (suffix); eliminates "is a set"
hypotheses | |
| No | uniexg 7719 |
| gr | graph | |
| No | uhgrf 29209, isumgr 29242, usgrres1 29462 |
| grp | group | df-grp 18961 |
Grp | Yes | isgrp 18964, tgpgrp 24118 |
| gsum | group sum | df-gsum 17454 |
(𝐺 Σg 𝐹) | Yes |
gsumval 18694, gsumwrev 19389 |
| hash | size (of a set) | df-hash 14341 |
(♯‘𝐴) | Yes |
hashgval 14343, hashfz1 14356, hashcl 14366 |
| hb | hypothesis builder (prefix) | |
| No | hbxfrbi 1844, hbald 2201, hbequid 39497 |
| hm | (monoid, group, ring, ...) homomorphism |
| | No |
ismhm 18802, isghm 19239, isrhm 20506 |
| i | inference (suffix) | |
| No | eleq1i 2852, tcsni 9693 |
| i | implication (suffix) | |
| No | brwdomi 9513, infeq5i 9588 |
| id | identity | |
| No | biid 263 |
| iedg | indexed edge | df-iedg 29146 |
(iEdg‘𝐺) | Yes |
iedgval0 29187, edgiedgb 29201 |
| idm | idempotent | |
| No | anidm 572, tpidm13 4714 |
| im, imp | implication (label often omitted) |
df-im 15111 | (𝐴 → 𝐵) | Yes |
iman 405, imnan 403, impbidd 212 |
| im | (group, ring, ...) isomorphism | |
| No | isgim 19285, rimrcl 20509 |
| ima | image | df-ima 5658 |
(𝐴 “ 𝐵) | Yes | resima 5999, imaundi 6131 |
| imp | import | |
| No | biimpa 480, impcom 411 |
| in | intersection | df-in 3911 |
(𝐴 ∩ 𝐵) | Yes | elin 3920, incom 4161 |
| inf | infimum | df-inf 9386 |
inf(ℝ+, ℝ*, < ) | Yes |
fiinfcl 9446, infiso 9453 |
| is... | is (something a) ...? | |
| No | isring 20266 |
| j | joining, disjoining | |
| No | jc 161, jaoi 868 |
| l | left | |
| No | olcd 885, simpl 486 |
| map | mapping operation or set exponentiation |
df-map 8805 | (𝐴 ↑m 𝐵) | Yes |
mapvalg 8813, elmapex 8825 |
| mat | matrix | df-mat 22448 |
(𝑁 Mat 𝑅) | Yes |
matval 22451, matring 22483 |
| mdet | determinant (of a square matrix) |
df-mdet 22625 | (𝑁 maDet 𝑅) | Yes |
mdetleib 22627, mdetrlin 22642 |
| mgm | magma | df-mgm 18657 |
Magma | Yes |
mgmidmo 18677, mgmlrid 18684, ismgm 18658 |
| mgp | multiplicative group | df-mgp 20170 |
(mulGrp‘𝑅) | Yes |
mgpress 20179, ringmgp 20268 |
| mnd | monoid | df-mnd 18752 |
Mnd | Yes | mndass 18760, mndodcong 19565 |
| mo | "there exists at most one" | df-mo 2565 |
∃*𝑥𝜑 | Yes | eumo 2604, moim 2570 |
| mp | modus ponens | ax-mp 5 |
| No | mpd 15, mpi 20 |
| mpo | maps-to notation for an operation |
df-mpo 7397 | (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) | Yes |
mpompt 7506, resmpo 7512 |
| mpt | modus ponendo tollens | |
| No | mptnan 1787, mptxor 1788 |
| mpt | maps-to notation for a function |
df-mpt 5181 | (𝑥 ∈ 𝐴 ↦ 𝐵) | Yes |
fconstmpt 5707, resmpt 6023 |
| mul | multiplication (see "t") | df-mul 11082 |
(𝐴 · 𝐵) | Yes |
mulcl 11154, divmul 11845, mulcom 11156, mulass 11158 |
| n, not | not | |
¬ 𝜑 | Yes |
nan 840, notnotr 130 |
| ne | not equal | df-ne | 𝐴 ≠ 𝐵 |
Yes | exmidne 2966, neeqtrd 3025 |
| nel | not element of | df-nel | 𝐴 ∉ 𝐵
|
Yes | neli 3062, nnel 3070 |
| ne0 | not equal to zero (see n0) | |
≠ 0 | No |
negne0d 11537, ine0 11619, gt0ne0 11649 |
| nf | "not free in" (prefix) | df-nf 1803 |
Ⅎ𝑥𝜑 | Yes | nfnd 1877 |
| ngp | normed group | df-ngp 24623 |
NrmGrp | Yes | isngp 24636, ngptps 24642 |
| nm | norm (on a group or ring) | df-nm 24622 |
(norm‘𝑊) | Yes |
nmval 24629, subgnm 24673 |
| nn | positive integers | df-nn 12208 |
ℕ | Yes | nnsscn 12212, nncn 12215 |
| nn0 | nonnegative integers | df-n0 12479 |
ℕ0 | Yes | nnnn0 12485, nn0cn 12488 |
| n0 | not the empty set (see ne0) | |
≠ ∅ | No | n0i 4292, vn0 4297, ssn0 4357 |
| OLD | old, obsolete (to be removed soon) | |
| No | 19.43OLD 1902 |
| on | ordinal number | df-on 6346 |
𝐴 ∈ On | Yes |
elon 6351, 1on 8445 onelon 6367 |
| op | ordered pair | df-op 4588 |
⟨𝐴, 𝐵⟩ | Yes | dfopif 4827, opth 5443 |
| or | or | df-or 859 |
(𝜑 ∨ 𝜓) | Yes |
orcom 881, anor 995 |
| ot | ordered triple | df-ot 4590 |
⟨𝐴, 𝐵, 𝐶⟩ | Yes |
euotd 5481, fnotovb 7444 |
| ov | operation value | df-ov 7395 |
(𝐴𝐹𝐵) | Yes
| fnotovb 7444, fnovrn 7567 |
| p | plus (see "add"), for all-constant
theorems | df-add 11081 |
(3 + 2) = 5 | Yes |
3p2e5 12365 |
| pfx | prefix | df-pfx 14682 |
(𝑊 prefix 𝐿) | Yes |
pfxlen 14694, ccatpfx 14711 |
| pm | Principia Mathematica | |
| No | pm2.27 42 |
| pm | partial mapping (operation) | df-pm 8806 |
(𝐴 ↑pm 𝐵) | Yes | elpmi 8823, pmsspw 8855 |
| pr | pair | df-pr 4584 |
{𝐴, 𝐵} | Yes |
elpr 4606, prcom 4690, prid1g 4718, prnz 4735 |
| prm, prime | prime (number) | df-prm 16689 |
ℙ | Yes | 1nprm 16696, dvdsprime 16704 |
| pss | proper subset | df-pss 3924 |
𝐴 ⊊ 𝐵 | Yes | pssss 4051, sspsstri 4059 |
| q | rational numbers ("quotients") | df-q 12947 |
ℚ | Yes | elq 12948 |
| r | reversed (suffix) | |
| No | pm4.71r 566, caovdir 7626 |
| r | right | |
| No | orcd 884, simprl 780 |
| rab | restricted class abstraction |
df-rab 3414 | {𝑥 ∈ 𝐴 ∣ 𝜑} | Yes |
rabswap 3422, df-oprab 7396 |
| ral | restricted universal quantification |
df-ral 3076 | ∀𝑥 ∈ 𝐴𝜑 | Yes |
ralnex 3087, ralrnmpo 7531 |
| rcl | reverse closure | |
| No | ndmfvrcl 6896, nnarcl 8581 |
| re | real numbers | df-r 11080 |
ℝ | Yes | recn 11160, 0re 11180 |
| rel | relation | df-rel 5652 | Rel 𝐴 |
Yes | brrelex1 5698, relmpoopab 8068 |
| res | restriction | df-res 5657 |
(𝐴 ↾ 𝐵) | Yes |
opelres 5969, f1ores 6817 |
| reu | restricted existential uniqueness |
df-reu 3367 | ∃!𝑥 ∈ 𝐴𝜑 | Yes |
nfreud 3410, reurex 3370 |
| rex | restricted existential quantification |
df-rex 3086 | ∃𝑥 ∈ 𝐴𝜑 | Yes |
rexnal 3113, rexrnmpo 7532 |
| rmo | restricted "at most one" |
df-rmo 3366 | ∃*𝑥 ∈ 𝐴𝜑 | Yes |
nfrmod 3409, nrexrmo 3385 |
| rn | range | df-rn 5656 | ran 𝐴 |
Yes | elrng 5865, rncnvcnv 5908 |
| ring | (unital) ring | df-ring 20264 |
Ring | Yes |
ringidval 20212, isring 20266, ringgrp 20267 |
| rng | non-unital ring | df-rng 20182 |
Rng | Yes |
isrng 20183, rngabl 20184, rnglz 20194 |
| rot | rotation | |
| No | 3anrot 1111, 3orrot 1102 |
| s | eliminates need for syllogism (suffix) |
| | No | ancoms 462 |
| sb | (proper) substitution (of a set) |
df-sb 2090 | [𝑦 / 𝑥]𝜑 | Yes |
spsbe 2114, sbimi 2106 |
| sbc | (proper) substitution of a class |
df-sbc 3745 | [𝐴 / 𝑥]𝜑 | Yes |
sbc2or 3753, sbcth 3759 |
| sca | scalar | df-sca 17285 |
(Scalar‘𝐻) | Yes |
resssca 17355, mgpsca 20175 |
| simp | simple, simplification | |
| No | simpl 486, simp3r3 1296 |
| sn | singleton | df-sn 4582 |
{𝐴} | Yes | eldifsn 4745 |
| sp | specialization | |
| No | spsbe 2114, spei 2424 |
| ss | subset | df-ss 3921 |
𝐴 ⊆ 𝐵 | Yes | difss 4089 |
| struct | structure | df-struct 17166 |
Struct | Yes | brstruct 17167, structfn 17175 |
| sub | subtract | df-sub 11413 |
(𝐴 − 𝐵) | Yes |
subval 11418, subaddi 11515 |
| sup | supremum | df-sup 9385 |
sup(𝐴, 𝐵, < ) | Yes |
fisupcl 9413, supmo 9395 |
| supp | support (of a function) | df-supp 8136 |
(𝐹 supp 𝑍) | Yes |
ressuppfi 9338, mptsuppd 8162 |
| swap | swap (two parts within a theorem) |
| | No | rabswap 3422, 2reuswap 3708 |
| syl | syllogism | syl 17 |
| No | 3syl 18 |
| sym | symmetric | |
| No | df-symdif 4205, cnvsym 6098 |
| symg | symmetric group | df-symg 19393 |
(SymGrp‘𝐴) | Yes |
symghash 19401, pgrpsubgsymg 19432 |
| t |
times (see "mul"), for all-constant theorems |
df-mul 11082 |
(3 · 2) = 6 | Yes |
3t2e6 12380 |
| th, t |
theorem |
|
|
No |
nfth 1820, sbcth 3759, weth 10449, ancomst 468 |
| tp | triple | df-tp 4586 |
{𝐴, 𝐵, 𝐶} | Yes |
eltpi 4646, tpeq1 4700 |
| tr | transitive | |
| No | bitrd 281, biantr 815 |
| tru, t |
true, truth |
df-tru 1562 |
⊤ |
Yes |
bitru 1568, truanfal 1593, biimt 362 |
| un | union | df-un 3909 |
(𝐴 ∪ 𝐵) | Yes |
uneqri 4109, uncom 4111 |
| unit | unit (in a ring) |
df-unit 20386 | (Unit‘𝑅) | Yes |
isunit 20401, nzrunit 20553 |
| v |
setvar (especially for specializations of
theorems when a class is replaced by a setvar variable) |
|
x |
Yes |
cv 1558, vex 3457, velpw 4559, vtoclf 3530 |
| v |
disjoint variable condition used in place of nonfreeness
hypothesis (suffix) |
|
|
No |
spimv 2420 |
| vtx |
vertex |
df-vtx 29145 |
(Vtx‘𝐺) |
Yes |
vtxval0 29186, opvtxov 29152 |
| vv |
two disjoint variable conditions used in place of nonfreeness
hypotheses (suffix) |
|
|
No |
19.23vv 1962 |
| w | weak (version of a theorem) (suffix) | |
| No | ax11w 2163, spnfw 1998 |
| wrd | word |
df-word 14524 | Word 𝑆 | Yes |
iswrdb 14530, wrdfn 14538, ffz0iswrd 14551 |
| xp | cross product (Cartesian product) |
df-xp 5651 | (𝐴 × 𝐵) | Yes |
elxp 5668, opelxpi 5682, xpundi 5714 |
| xr | eXtended reals | df-xr 11217 |
ℝ* | Yes | ressxr 11223, rexr 11225, 0xr 11226 |
| z | integers (from German "Zahlen") |
df-z 12566 | ℤ | Yes |
elz 12567, zcn 12570 |
| zn | ring of integers mod 𝑁 | df-zn 21538 |
(ℤ/nℤ‘𝑁) | Yes |
znval 21567, zncrng 21576, znhash 21590 |
| zring | ring of integers | df-zring 21479 |
ℤring | Yes | zringbas 21485, zringcrng 21480
|
| 0, z |
slashed zero (empty set) | df-nul 4286 |
∅ | Yes |
n0i 4292, vn0 4297; snnz 4734, prnz 4735 |
(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.) |
