| Description:
The following gives conventions used in the Metamath Proof Explorer
(MPE, set.mm) regarding labels.
For other conventions, see conventions 30419 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 3063"rgen.1 $e |- ( x e. A -> ph ) $."
or letters corresponding to the (main) class variable used in the
hypothesis, e.g., for mdet0 22612: "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 2663 and stirling 46104.
- 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 3254.
- 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... 15917. 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 3954, and thus its syntax label fragment is "dif". Similarly, the
subclass relation 𝐴 ⊆ 𝐵 has syntax label fragment "ss"
because it is defined in df-ss 3968. 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 4136. There are many other syntax label fragments, e.g.,
singleton construct {𝐴} has syntax label fragment "sn" (because it
is defined in df-sn 4627), and the pair construct {𝐴, 𝐵} has
fragment "pr" ( from df-pr 4629). 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 4786. An "n" is often used for negation (¬), e.g.,
nan 830.
- 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 11161) and "re" represents real numbers ℝ (Definition df-r 11165).
The empty set ∅ often uses fragment 0, even though it is defined
in df-nul 4334. The syntax construct (𝐴 + 𝐵) usually uses the
fragment "add" (which is consistent with df-add 11166), 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 12401.
- 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 16186 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 16106) we have value cosval 16159 and
closure coscl 16163.
- 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 30422 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 2207. This
often permits to prove the result using fewer axioms, and/or to
eliminate a nonfreeness hypothesis (such as Ⅎ𝑥𝜑 in 19.21 2207).
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 2576 derived from eu6 2574. The "f" stands
for "not free in" which is less restrictive than "does not occur in."
The suffix "b" often means "biconditional" (↔, "iff" , "if and
only if"), e.g., sspwb 5454.
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 2414 (cbval 2403 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 3560.
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 3147 |
| abl | Abelian group | df-abl 19801 |
Abel | Yes | ablgrp 19803, zringabl 21462 |
| abs | absorption | | | No |
ressabs 17294 |
| abs | absolute value (of a complex number) |
df-abs 15275 | (abs‘𝐴) | Yes |
absval 15277, absneg 15316, abs1 15336 |
| ad | adding | |
| No | adantr 480, ad2antlr 727 |
| add | add (see "p") | df-add 11166 |
(𝐴 + 𝐵) | Yes |
addcl 11237, addcom 11447, addass 11242 |
| al | "for all" | |
∀𝑥𝜑 | No | alim 1810, alex 1826 |
| ALT | alternative/less preferred (suffix) | |
| No | idALT 23 |
| an | and | df-an 396 |
(𝜑 ∧ 𝜓) | Yes |
anor 985, iman 401, imnan 399 |
| ant | antecedent | |
| No | adantr 480 |
| ass | associative | |
| No | biass 384, orass 922, mulass 11243 |
| asym | asymmetric, antisymmetric | |
| No | intasym 6135, asymref 6136, posasymb 18365 |
| ax | axiom | |
| No | ax6dgen 2128, ax1cn 11189 |
| bas, base |
base (set of an extensible structure) | df-base 17248 |
(Base‘𝑆) | Yes |
baseval 17249, ressbas 17280, cnfldbas 21368 |
| b, bi | biconditional ("iff", "if and only if")
| df-bi 207 | (𝜑 ↔ 𝜓) | Yes |
impbid 212, sspwb 5454 |
| br | binary relation | df-br 5144 |
𝐴𝑅𝐵 | Yes | brab1 5191, brun 5194 |
| c | commutes, commuted (suffix) | | |
No | biimpac 478 |
| c | contraction (suffix) | | |
No | sylc 65, syl2anc 584 |
| cbv | change bound variable | | |
No | cbvalivw 2006, cbvrex 3363 |
| cdm | codomain | |
| No | ffvelcdm 7101, focdmex 7980 |
| cl | closure | | | No |
ifclda 4561, ovrcl 7472, zaddcl 12657 |
| cn | complex numbers | df-c 11161 |
ℂ | Yes | nnsscn 12271, nncn 12274 |
| cnfld | field of complex numbers | df-cnfld 21365 |
ℂfld | Yes | cnfldbas 21368, cnfldinv 21415 |
| cntz | centralizer | df-cntz 19335 |
(Cntz‘𝑀) | Yes |
cntzfval 19338, dprdfcntz 20035 |
| cnv | converse | df-cnv 5693 |
◡𝐴 | Yes | opelcnvg 5891, f1ocnv 6860 |
| co | composition | df-co 5694 |
(𝐴 ∘ 𝐵) | Yes | cnvco 5896, fmptco 7149 |
| com | commutative | |
| No | orcom 871, bicomi 224, eqcomi 2746 |
| con | contradiction, contraposition | |
| No | condan 818, con2d 134 |
| csb | class substitution | df-csb 3900 |
⦋𝐴 / 𝑥⦌𝐵 | Yes |
csbid 3912, csbie2g 3939 |
| cyg | cyclic group | df-cyg 19896 |
CycGrp | Yes |
iscyg 19897, zringcyg 21480 |
| d | deduction form (suffix) | |
| No | idd 24, impbid 212 |
| df | (alternate) definition (prefix) | |
| No | dfrel2 6209, dffn2 6738 |
| di, distr | distributive | |
| No |
andi 1010, imdi 389, ordi 1008, difindi 4292, ndmovdistr 7622 |
| dif | class difference | df-dif 3954 |
(𝐴 ∖ 𝐵) | Yes |
difss 4136, difindi 4292 |
| div | division | df-div 11921 |
(𝐴 / 𝐵) | Yes |
divcl 11928, divval 11924, divmul 11925 |
| dm | domain | df-dm 5695 |
dom 𝐴 | Yes | dmmpt 6260, iswrddm0 14576 |
| e, eq, equ | equals (equ for setvars, eq for
classes) | df-cleq 2729 |
𝐴 = 𝐵 | Yes |
2p2e4 12401, uneqri 4156, equtr 2020 |
| edg | edge | df-edg 29065 |
(Edg‘𝐺) | Yes |
edgopval 29068, usgredgppr 29213 |
| el | element of | |
𝐴 ∈ 𝐵 | Yes |
eldif 3961, eldifsn 4786, elssuni 4937 |
| en | equinumerous | df-en |
𝐴 ≈ 𝐵 | Yes | domen 9002, enfi 9227 |
| eu | "there exists exactly one" | eu6 2574 |
∃!𝑥𝜑 | Yes | euex 2577, euabsn 4726 |
| ex | exists (i.e. is a set) | |
∈ V | No | brrelex1 5738, 0ex 5307 |
| 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 2464, sbf 2271 |
| f | function | df-f 6565 |
𝐹:𝐴⟶𝐵 | Yes | fssxp 6763, opelf 6769 |
| fal | false | df-fal 1553 |
⊥ | Yes | bifal 1556, falantru 1575 |
| fi | finite intersection | df-fi 9451 |
(fi‘𝐵) | Yes | fival 9452, inelfi 9458 |
| fi, fin | finite | df-fin 8989 |
Fin | Yes |
isfi 9016, snfi 9083, onfin 9267 |
| fld | field (Note: there is an alternative
definition Fld of a field, see df-fld 37999) | df-field 20732 |
Field | Yes | isfld 20740, fldidom 20771 |
| fn | function with domain | df-fn 6564 |
𝐴 Fn 𝐵 | Yes | ffn 6736, fndm 6671 |
| frgp | free group | df-frgp 19728 |
(freeGrp‘𝐼) | Yes |
frgpval 19776, frgpadd 19781 |
| fsupp | finitely supported function |
df-fsupp 9402 | 𝑅 finSupp 𝑍 | Yes |
isfsupp 9405, fdmfisuppfi 9414, fsuppco 9442 |
| fun | function | df-fun 6563 |
Fun 𝐹 | Yes | funrel 6583, ffun 6739 |
| fv | function value | df-fv 6569 |
(𝐹‘𝐴) | Yes | fvres 6925, swrdfv 14686 |
| fz | finite set of sequential integers |
df-fz 13548 |
(𝑀...𝑁) | Yes | fzval 13549, eluzfz 13559 |
| fz0 | finite set of sequential nonnegative integers |
|
(0...𝑁) | Yes | nn0fz0 13665, fz0tp 13668 |
| fzo | half-open integer range | df-fzo 13695 |
(𝑀..^𝑁) | Yes |
elfzo 13701, elfzofz 13715 |
| g | more general (suffix); eliminates "is a set"
hypotheses | |
| No | uniexg 7760 |
| gr | graph | |
| No | uhgrf 29079, isumgr 29112, usgrres1 29332 |
| grp | group | df-grp 18954 |
Grp | Yes | isgrp 18957, tgpgrp 24086 |
| gsum | group sum | df-gsum 17487 |
(𝐺 Σg 𝐹) | Yes |
gsumval 18690, gsumwrev 19385 |
| hash | size (of a set) | df-hash 14370 |
(♯‘𝐴) | Yes |
hashgval 14372, hashfz1 14385, hashcl 14395 |
| hb | hypothesis builder (prefix) | |
| No | hbxfrbi 1825, hbald 2168, hbequid 38910 |
| hm | (monoid, group, ring, ...) homomorphism |
| | No |
ismhm 18798, isghm 19233, isrhm 20478 |
| i | inference (suffix) | |
| No | eleq1i 2832, tcsni 9783 |
| i | implication (suffix) | |
| No | brwdomi 9608, infeq5i 9676 |
| id | identity | |
| No | biid 261 |
| iedg | indexed edge | df-iedg 29016 |
(iEdg‘𝐺) | Yes |
iedgval0 29057, edgiedgb 29071 |
| idm | idempotent | |
| No | anidm 564, tpidm13 4756 |
| im, imp | implication (label often omitted) |
df-im 15140 | (𝐴 → 𝐵) | Yes |
iman 401, imnan 399, impbidd 210 |
| im | (group, ring, ...) isomorphism | |
| No | isgim 19280, rimrcl 20482 |
| ima | image | df-ima 5698 |
(𝐴 “ 𝐵) | Yes | resima 6033, imaundi 6169 |
| imp | import | |
| No | biimpa 476, impcom 407 |
| in | intersection | df-in 3958 |
(𝐴 ∩ 𝐵) | Yes | elin 3967, incom 4209 |
| inf | infimum | df-inf 9483 |
inf(ℝ+, ℝ*, < ) | Yes |
fiinfcl 9541, infiso 9548 |
| is... | is (something a) ...? | |
| No | isring 20234 |
| j | joining, disjoining | |
| No | jc 161, jaoi 858 |
| l | left | |
| No | olcd 875, simpl 482 |
| map | mapping operation or set exponentiation |
df-map 8868 | (𝐴 ↑m 𝐵) | Yes |
mapvalg 8876, elmapex 8888 |
| mat | matrix | df-mat 22412 |
(𝑁 Mat 𝑅) | Yes |
matval 22415, matring 22449 |
| mdet | determinant (of a square matrix) |
df-mdet 22591 | (𝑁 maDet 𝑅) | Yes |
mdetleib 22593, mdetrlin 22608 |
| mgm | magma | df-mgm 18653 |
Magma | Yes |
mgmidmo 18673, mgmlrid 18680, ismgm 18654 |
| mgp | multiplicative group | df-mgp 20138 |
(mulGrp‘𝑅) | Yes |
mgpress 20147, ringmgp 20236 |
| mnd | monoid | df-mnd 18748 |
Mnd | Yes | mndass 18756, mndodcong 19560 |
| mo | "there exists at most one" | df-mo 2540 |
∃*𝑥𝜑 | Yes | eumo 2578, moim 2544 |
| mp | modus ponens | ax-mp 5 |
| No | mpd 15, mpi 20 |
| mpo | maps-to notation for an operation |
df-mpo 7436 | (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) | Yes |
mpompt 7547, resmpo 7553 |
| mpt | modus ponendo tollens | |
| No | mptnan 1768, mptxor 1769 |
| mpt | maps-to notation for a function |
df-mpt 5226 | (𝑥 ∈ 𝐴 ↦ 𝐵) | Yes |
fconstmpt 5747, resmpt 6055 |
| mul | multiplication (see "t") | df-mul 11167 |
(𝐴 · 𝐵) | Yes |
mulcl 11239, divmul 11925, mulcom 11241, mulass 11243 |
| n, not | not | |
¬ 𝜑 | Yes |
nan 830, notnotr 130 |
| ne | not equal | df-ne | 𝐴 ≠ 𝐵 |
Yes | exmidne 2950, neeqtrd 3010 |
| nel | not element of | df-nel | 𝐴 ∉ 𝐵
|
Yes | neli 3048, nnel 3056 |
| ne0 | not equal to zero (see n0) | |
≠ 0 | No |
negne0d 11618, ine0 11698, gt0ne0 11728 |
| nf | "not free in" (prefix) | df-nf 1784 |
Ⅎ𝑥𝜑 | Yes | nfnd 1858 |
| ngp | normed group | df-ngp 24596 |
NrmGrp | Yes | isngp 24609, ngptps 24615 |
| nm | norm (on a group or ring) | df-nm 24595 |
(norm‘𝑊) | Yes |
nmval 24602, subgnm 24646 |
| nn | positive integers | df-nn 12267 |
ℕ | Yes | nnsscn 12271, nncn 12274 |
| nn0 | nonnegative integers | df-n0 12527 |
ℕ0 | Yes | nnnn0 12533, nn0cn 12536 |
| n0 | not the empty set (see ne0) | |
≠ ∅ | No | n0i 4340, vn0 4345, ssn0 4404 |
| OLD | old, obsolete (to be removed soon) | |
| No | 19.43OLD 1883 |
| on | ordinal number | df-on 6388 |
𝐴 ∈ On | Yes |
elon 6393, 1on 8518 onelon 6409 |
| op | ordered pair | df-op 4633 |
⟨𝐴, 𝐵⟩ | Yes | dfopif 4870, opth 5481 |
| or | or | df-or 849 |
(𝜑 ∨ 𝜓) | Yes |
orcom 871, anor 985 |
| ot | ordered triple | df-ot 4635 |
⟨𝐴, 𝐵, 𝐶⟩ | Yes |
euotd 5518, fnotovb 7483 |
| ov | operation value | df-ov 7434 |
(𝐴𝐹𝐵) | Yes
| fnotovb 7483, fnovrn 7608 |
| p | plus (see "add"), for all-constant
theorems | df-add 11166 |
(3 + 2) = 5 | Yes |
3p2e5 12417 |
| pfx | prefix | df-pfx 14709 |
(𝑊 prefix 𝐿) | Yes |
pfxlen 14721, ccatpfx 14739 |
| pm | Principia Mathematica | |
| No | pm2.27 42 |
| pm | partial mapping (operation) | df-pm 8869 |
(𝐴 ↑pm 𝐵) | Yes | elpmi 8886, pmsspw 8917 |
| pr | pair | df-pr 4629 |
{𝐴, 𝐵} | Yes |
elpr 4650, prcom 4732, prid1g 4760, prnz 4777 |
| prm, prime | prime (number) | df-prm 16709 |
ℙ | Yes | 1nprm 16716, dvdsprime 16724 |
| pss | proper subset | df-pss 3971 |
𝐴 ⊊ 𝐵 | Yes | pssss 4098, sspsstri 4105 |
| q | rational numbers ("quotients") | df-q 12991 |
ℚ | Yes | elq 12992 |
| r | reversed (suffix) | |
| No | pm4.71r 558, caovdir 7667 |
| r | right | |
| No | orcd 874, simprl 771 |
| rab | restricted class abstraction |
df-rab 3437 | {𝑥 ∈ 𝐴 ∣ 𝜑} | Yes |
rabswap 3446, df-oprab 7435 |
| ral | restricted universal quantification |
df-ral 3062 | ∀𝑥 ∈ 𝐴𝜑 | Yes |
ralnex 3072, ralrnmpo 7572 |
| rcl | reverse closure | |
| No | ndmfvrcl 6942, nnarcl 8654 |
| re | real numbers | df-r 11165 |
ℝ | Yes | recn 11245, 0re 11263 |
| rel | relation | df-rel 5692 | Rel 𝐴 |
Yes | brrelex1 5738, relmpoopab 8119 |
| res | restriction | df-res 5697 |
(𝐴 ↾ 𝐵) | Yes |
opelres 6003, f1ores 6862 |
| reu | restricted existential uniqueness |
df-reu 3381 | ∃!𝑥 ∈ 𝐴𝜑 | Yes |
nfreud 3433, reurex 3384 |
| rex | restricted existential quantification |
df-rex 3071 | ∃𝑥 ∈ 𝐴𝜑 | Yes |
rexnal 3100, rexrnmpo 7573 |
| rmo | restricted "at most one" |
df-rmo 3380 | ∃*𝑥 ∈ 𝐴𝜑 | Yes |
nfrmod 3432, nrexrmo 3401 |
| rn | range | df-rn 5696 | ran 𝐴 |
Yes | elrng 5902, rncnvcnv 5945 |
| ring | (unital) ring | df-ring 20232 |
Ring | Yes |
ringidval 20180, isring 20234, ringgrp 20235 |
| rng | non-unital ring | df-rng 20150 |
Rng | Yes |
isrng 20151, rngabl 20152, rnglz 20162 |
| 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 3789 | [𝐴 / 𝑥]𝜑 | Yes |
sbc2or 3797, sbcth 3803 |
| sca | scalar | df-sca 17313 |
(Scalar‘𝐻) | Yes |
resssca 17387, mgpsca 20143 |
| simp | simple, simplification | |
| No | simpl 482, simp3r3 1284 |
| sn | singleton | df-sn 4627 |
{𝐴} | Yes | eldifsn 4786 |
| sp | specialization | |
| No | spsbe 2082, spei 2399 |
| ss | subset | df-ss 3968 |
𝐴 ⊆ 𝐵 | Yes | difss 4136 |
| struct | structure | df-struct 17184 |
Struct | Yes | brstruct 17185, structfn 17193 |
| sub | subtract | df-sub 11494 |
(𝐴 − 𝐵) | Yes |
subval 11499, subaddi 11596 |
| sup | supremum | df-sup 9482 |
sup(𝐴, 𝐵, < ) | Yes |
fisupcl 9509, supmo 9492 |
| supp | support (of a function) | df-supp 8186 |
(𝐹 supp 𝑍) | Yes |
ressuppfi 9435, mptsuppd 8212 |
| swap | swap (two parts within a theorem) |
| | No | rabswap 3446, 2reuswap 3752 |
| syl | syllogism | syl 17 |
| No | 3syl 18 |
| sym | symmetric | |
| No | df-symdif 4253, cnvsym 6132 |
| symg | symmetric group | df-symg 19387 |
(SymGrp‘𝐴) | Yes |
symghash 19395, pgrpsubgsymg 19427 |
| t |
times (see "mul"), for all-constant theorems |
df-mul 11167 |
(3 · 2) = 6 | Yes |
3t2e6 12432 |
| th, t |
theorem |
|
|
No |
nfth 1801, sbcth 3803, weth 10535, ancomst 464 |
| tp | triple | df-tp 4631 |
{𝐴, 𝐵, 𝐶} | Yes |
eltpi 4688, tpeq1 4742 |
| tr | transitive | |
| No | bitrd 279, biantr 806 |
| tru, t |
true, truth |
df-tru 1543 |
⊤ |
Yes |
bitru 1549, truanfal 1574, biimt 360 |
| un | union | df-un 3956 |
(𝐴 ∪ 𝐵) | Yes |
uneqri 4156, uncom 4158 |
| unit | unit (in a ring) |
df-unit 20358 | (Unit‘𝑅) | Yes |
isunit 20373, nzrunit 20524 |
| v |
setvar (especially for specializations of
theorems when a class is replaced by a setvar variable) |
|
x |
Yes |
cv 1539, vex 3484, velpw 4605, vtoclf 3564 |
| v |
disjoint variable condition used in place of nonfreeness
hypothesis (suffix) |
|
|
No |
spimv 2395 |
| vtx |
vertex |
df-vtx 29015 |
(Vtx‘𝐺) |
Yes |
vtxval0 29056, opvtxov 29022 |
| 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 2130, spnfw 1979 |
| wrd | word |
df-word 14553 | Word 𝑆 | Yes |
iswrdb 14558, wrdfn 14566, ffz0iswrd 14579 |
| xp | cross product (Cartesian product) |
df-xp 5691 | (𝐴 × 𝐵) | Yes |
elxp 5708, opelxpi 5722, xpundi 5754 |
| xr | eXtended reals | df-xr 11299 |
ℝ* | Yes | ressxr 11305, rexr 11307, 0xr 11308 |
| z | integers (from German "Zahlen") |
df-z 12614 | ℤ | Yes |
elz 12615, zcn 12618 |
| zn | ring of integers mod 𝑁 | df-zn 21517 |
(ℤ/nℤ‘𝑁) | Yes |
znval 21550, zncrng 21563, znhash 21577 |
| zring | ring of integers | df-zring 21458 |
ℤring | Yes | zringbas 21464, zringcrng 21459
|
| 0, z |
slashed zero (empty set) | df-nul 4334 |
∅ | Yes |
n0i 4340, vn0 4345; snnz 4776, prnz 4777 |
(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.) |
