| Description:
The following gives conventions used in the Metamath Proof Explorer
(MPE, set.mm) regarding labels.
For other conventions, see conventions 30729 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 3081"rgen.1 $e |- ( x e. A -> ph ) $."
or letters corresponding to the (main) class variable used in the
hypothesis, e.g., for mdet0 22744: "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 2690 and stirling 46783.
- 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 43.
- 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 1869, and the restricted quantifier version of Theorem 21 from
Section 19 of [Margaris] p. 90 is labeled r19.21 3260.
- Characters to be used for labels.
Although the specification of Metamath allows for dots/periods "." in
any label, it is usually used only in labels for hypotheses (see above).
Exceptions are the labels of theorems from Principia Mathematica and the
19.x series of theorems from Section 19 of [Margaris] p. 90 (see above)
and 0.999... 15937. 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 3909, and thus its syntax label fragment is "dif". Similarly, the
subclass relation 𝐴 ⊆ 𝐵 has syntax label fragment "ss"
because it is defined in df-ss 3923. 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 4091. There are many other syntax label fragments, e.g.,
singleton construct {𝐴} has syntax label fragment "sn" (because it
is defined in df-sn 4591), and the pair construct {𝐴, 𝐵} has
fragment "pr" ( from df-pr 4593). 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 4754. An "n" is often used for negation (¬), e.g.,
nan 842.
- 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 11107) and "re" represents real numbers ℝ (Definition df-r 11111).
The empty set ∅ often uses fragment 0, even though it is defined
in df-nul 4288. The syntax construct (𝐴 + 𝐵) usually uses the
fragment "add" (which is consistent with df-add 11112), 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 12376.
- 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 16207 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 16125) we have value cosval 16180 and
closure coscl 16184.
- 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 18 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 30732 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 1969 versus 19.21 2243. This
often permits to prove the result using fewer axioms, and/or to
eliminate a nonfreeness hypothesis (such as Ⅎ𝑥𝜑 in 19.21 2243).
If no constraint is put on axiom use, then the v-version can be proved
from the original theorem using nfv 1944. If two (resp. three) such
disjoint variable conditions are added, then the suffix "vv" (resp.
"vvv") is used, e.g., exlimivv 1962.
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 2604 derived from eu6 2602. 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 5432.
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 18) -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 2441 (cbval 2430 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 3527.
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 66, syl2anc 595), commutes
(e.g., biimpac 483)
- 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 18 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 481, rexlimiva 3158 |
| abl | Abelian group | df-abl 19854 |
Abel | Yes | ablgrp 19856, zringabl 21582 |
| abs | absorption | | | No |
ressabs 17309 |
| abs | absolute value (of a complex number) |
df-abs 15289 | (abs‘𝐴) | Yes |
absval 15291, absneg 15330, abs1 15350 |
| ad | adding | |
| No | adantr 485, ad2antlr 739 |
| add | add (see "p") | df-add 11112 |
(𝐴 + 𝐵) | Yes |
addcl 11183, addcom 11397, addass 11188 |
| al | "for all" | |
∀𝑥𝜑 | No | alim 1840, alex 1856 |
| ALT | alternative/less preferred (suffix) | |
| No | idALT 24 |
| an | and | df-an 401 |
(𝜑 ∧ 𝜓) | Yes |
anor 998, iman 406, imnan 404 |
| ant | antecedent | |
| No | adantr 485 |
| ass | associative | |
| No | biass 388, orass 934, mulass 11189 |
| asym | asymmetric, antisymmetric | |
| No | intasym 6117, asymref 6118, posasymb 18376 |
| ax | axiom | |
| No | ax6dgen 2163, ax1cn 11135 |
| bas, base |
base (set of an extensible structure) | df-base 17271 |
(Base‘𝑆) | Yes |
baseval 17272, ressbas 17297, cnfldbas 21507 |
| b, bi | biconditional ("iff", "if and only if")
| df-bi 210 | (𝜑 ↔ 𝜓) | Yes |
impbid 215, sspwb 5432 |
| br | binary relation | df-br 5111 |
𝐴𝑅𝐵 | Yes | brab1 5160, brun 5163 |
| c | commutes, commuted (suffix) | | |
No | biimpac 483 |
| c | contraction (suffix) | | |
No | sylc 66, syl2anc 595 |
| cbv | change bound variable | | |
No | cbvalivw 2037, cbvrex 3352 |
| cdm | codomain | |
| No | ffvelcdm 7078, focdmex 7954 |
| cl | closure | | | No |
ifclda 4524, ovrcl 7453, zaddcl 12635 |
| cn | complex numbers | df-c 11107 |
ℂ | Yes | nnsscn 12239, nncn 12242 |
| cnfld | field of complex numbers | df-cnfld 21504 |
ℂfld | Yes | cnfldbas 21507, cnfldinv 21534 |
| cntz | centralizer | df-cntz 19388 |
(Cntz‘𝑀) | Yes |
cntzfval 19391, dprdfcntz 20088 |
| cnv | converse | df-cnv 5671 |
◡𝐴 | Yes | opelcnvg 5868, f1ocnv 6835 |
| co | composition | df-co 5672 |
(𝐴 ∘ 𝐵) | Yes | cnvco 5877, fmptco 7127 |
| com | commutative | |
| No | orcom 883, bicomi 227, eqcomi 2772 |
| con | contradiction, contraposition | |
| No | condan 829, con2d 135 |
| csb | class substitution | df-csb 3855 |
⦋𝐴 / 𝑥⦌𝐵 | Yes |
csbid 3867, csbie2g 3894 |
| cyg | cyclic group | df-cyg 19949 |
CycGrp | Yes |
iscyg 19950, zringcyg 21600 |
| d | deduction form (suffix) | |
| No | idd 25, impbid 215 |
| df | (alternate) definition (prefix) | |
| No | dfrel2 6189, dffn2 6709 |
| di, distr | distributive | |
| No |
andi 1025, imdi 393, ordi 1023, difindi 4246, ndmovdistr 7601 |
| dif | class difference | df-dif 3909 |
(𝐴 ∖ 𝐵) | Yes |
difss 4091, difindi 4246 |
| div | division | df-div 11873 |
(𝐴 / 𝐵) | Yes |
divcl 11879, divval 11875, divmul 11876 |
| dm | domain | df-dm 5673 |
dom 𝐴 | Yes | dmmpt 6243, iswrddm0 14577 |
| e, eq, equ | equals (equ for setvars, eq for
classes) | df-cleq 2755 |
𝐴 = 𝐵 | Yes |
2p2e4 12376, uneqri 4111, equtr 2051 |
| edg | edge | df-edg 29376 |
(Edg‘𝐺) | Yes |
edgopval 29379, usgredgppr 29524 |
| el | element of | |
𝐴 ∈ 𝐵 | Yes |
eldif 3916, eldifsn 4754, elssuni 4905 |
| en | equinumerous | df-en |
𝐴 ≈ 𝐵 | Yes | domen 8959, enfi 9172 |
| eu | "there exists exactly one" | eu6 2602 |
∃!𝑥𝜑 | Yes | euex 2605, euabsn 4693 |
| ex | exists (i.e. is a set) | |
∈ V | No | brrelex1 5716, 0ex 5271 |
| ex, e | "there exists (at least one)" |
df-ex 1810 |
∃𝑥𝜑 | Yes | exim 1864, alex 1856 |
| exp | export | |
| No | expt 178, expcom 418 |
| f | "not free in" (suffix) | |
| No | equs45f 2491, sbf 2306 |
| f | function | df-f 6542 |
𝐹:𝐴⟶𝐵 | Yes | fssxp 6735, opelf 6741 |
| fal | false | df-fal 1583 |
⊥ | Yes | bifal 1586, falantru 1605 |
| fi | finite intersection | df-fi 9372 |
(fi‘𝐵) | Yes | fival 9373, inelfi 9379 |
| fi, fin | finite | df-fin 8948 |
Fin | Yes |
isfi 8973, snfi 9041, onfin 9200 |
| fld | field (Note: there is an alternative
definition Fld of a field, see df-fld 38621) | df-field 20817 |
Field | Yes | isfld 20827, fldidom 20856 |
| fn | function with domain | df-fn 6541 |
𝐴 Fn 𝐵 | Yes | ffn 6707, fndm 6640 |
| frgp | free group | df-frgp 19781 |
(freeGrp‘𝐼) | Yes |
frgpval 19829, frgpadd 19834 |
| fsupp | finitely supported function |
df-fsupp 9323 | 𝑅 finSupp 𝑍 | Yes |
isfsupp 9326, fdmfisuppfi 9335, fsuppco 9363 |
| fun | function | df-fun 6540 |
Fun 𝐹 | Yes | funrel 6555, ffun 6710 |
| fv | function value | df-fv 6546 |
(𝐹‘𝐴) | Yes | fvres 6902, swrdfv 14688 |
| fz | finite set of sequential integers |
df-fz 13537 |
(𝑀...𝑁) | Yes | fzval 13538, eluzfz 13548 |
| fz0 | finite set of sequential nonnegative integers |
|
(0...𝑁) | Yes | nn0fz0 13655, fz0tp 13658 |
| fzo | half-open integer range | df-fzo 13685 |
(𝑀..^𝑁) | Yes |
elfzo 13691, elfzofz 13706 |
| g | more general (suffix); eliminates "is a set"
hypotheses | |
| No | uniexg 7740 |
| gr | graph | |
| No | uhgrf 29390, isumgr 29423, usgrres1 29643 |
| grp | group | df-grp 19004 |
Grp | Yes | isgrp 19007, tgpgrp 24216 |
| gsum | group sum | df-gsum 17496 |
(𝐺 Σg 𝐹) | Yes |
gsumval 18736, gsumwrev 19437 |
| hash | size (of a set) | df-hash 14369 |
(♯‘𝐴) | Yes |
hashgval 14371, hashfz1 14384, hashcl 14394 |
| hb | hypothesis builder (prefix) | |
| No | hbxfrbi 1855, hbald 2203, hbequid 39661 |
| hm | (monoid, group, ring, ...) homomorphism |
| | No |
ismhm 18844, isghm 19287, isrhm 20561 |
| i | inference (suffix) | |
| No | eleq1i 2854, tcsni 9711 |
| i | implication (suffix) | |
| No | brwdomi 9531, infeq5i 9606 |
| id | identity | |
| No | biid 264 |
| iedg | indexed edge | df-iedg 29327 |
(iEdg‘𝐺) | Yes |
iedgval0 29368, edgiedgb 29382 |
| idm | idempotent | |
| No | anidm 574, tpidm13 4723 |
| im, imp | implication (label often omitted) |
df-im 15154 | (𝐴 → 𝐵) | Yes |
iman 406, imnan 404, impbidd 213 |
| im | (group, ring, ...) isomorphism | |
| No | isgim 19333, rimrcl 20564 |
| ima | image | df-ima 5676 |
(𝐴 “ 𝐵) | Yes | resima 6016, imaundi 6149 |
| imp | import | |
| No | biimpa 481, impcom 412 |
| in | intersection | df-in 3913 |
(𝐴 ∩ 𝐵) | Yes | elin 3922, incom 4163 |
| inf | infimum | df-inf 9404 |
inf(ℝ+, ℝ*, < ) | Yes |
fiinfcl 9464, infiso 9471 |
| is... | is (something a) ...? | |
| No | isring 20320 |
| j | joining, disjoining | |
| No | jc 162, jaoi 870 |
| l | left | |
| No | olcd 887, simpl 487 |
| map | mapping operation or set exponentiation |
df-map 8827 | (𝐴 ↑m 𝐵) | Yes |
mapvalg 8834, elmapex 8846 |
| mat | matrix | df-mat 22546 |
(𝑁 Mat 𝑅) | Yes |
matval 22549, matring 22581 |
| mdet | determinant (of a square matrix) |
df-mdet 22723 | (𝑁 maDet 𝑅) | Yes |
mdetleib 22725, mdetrlin 22740 |
| mgm | magma | df-mgm 18699 |
Magma | Yes |
mgmidmo 18719, mgmlrid 18726, ismgm 18700 |
| mgp | multiplicative group | df-mgp 20218 |
(mulGrp‘𝑅) | Yes |
mgpress 20227, ringmgp 20322 |
| mnd | monoid | df-mnd 18794 |
Mnd | Yes | mndass 18802, mndodcong 19613 |
| mo | "there exists at most one" | df-mo 2567 |
∃*𝑥𝜑 | Yes | eumo 2606, moim 2572 |
| mp | modus ponens | ax-mp 5 |
| No | mpd 16, mpi 21 |
| mpo | maps-to notation for an operation |
df-mpo 7417 | (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) | Yes |
mpompt 7526, resmpo 7532 |
| mpt | modus ponendo tollens | |
| No | mptnan 1798, mptxor 1799 |
| mpt | maps-to notation for a function |
df-mpt 5194 | (𝑥 ∈ 𝐴 ↦ 𝐵) | Yes |
fconstmpt 5725, resmpt 6041 |
| mul | multiplication (see "t") | df-mul 11113 |
(𝐴 · 𝐵) | Yes |
mulcl 11185, divmul 11876, mulcom 11187, mulass 11189 |
| n, not | not | |
¬ 𝜑 | Yes |
nan 842, notnotr 131 |
| ne | not equal | df-ne | 𝐴 ≠ 𝐵 |
Yes | exmidne 2968, neeqtrd 3027 |
| nel | not element of | df-nel | 𝐴 ∉ 𝐵
|
Yes | neli 3066, nnel 3074 |
| ne0 | not equal to zero (see n0) | |
≠ 0 | No |
negne0d 11568, ine0 11650, gt0ne0 11680 |
| nf | "not free in" (prefix) | df-nf 1814 |
Ⅎ𝑥𝜑 | Yes | nfnd 1888 |
| ngp | normed group | df-ngp 24721 |
NrmGrp | Yes | isngp 24734, ngptps 24740 |
| nm | norm (on a group or ring) | df-nm 24720 |
(norm‘𝑊) | Yes |
nmval 24727, subgnm 24771 |
| nn | positive integers | df-nn 12235 |
ℕ | Yes | nnsscn 12239, nncn 12242 |
| nn0 | nonnegative integers | df-n0 12506 |
ℕ0 | Yes | nnnn0 12512, nn0cn 12515 |
| n0 | not the empty set (see ne0) | |
≠ ∅ | No | n0i 4294, vn0 4299, ssn0 4363 |
| OLD | old, obsolete (to be removed soon) | |
| No | 19.43OLD 1913 |
| on | ordinal number | df-on 6366 |
𝐴 ∈ On | Yes |
elon 6371, 1on 8467 onelon 6387 |
| op | ordered pair | df-op 4597 |
⟨𝐴, 𝐵⟩ | Yes | dfopif 4836, opth 5460 |
| or | or | df-or 861 |
(𝜑 ∨ 𝜓) | Yes |
orcom 883, anor 998 |
| ot | ordered triple | df-ot 4599 |
⟨𝐴, 𝐵, 𝐶⟩ | Yes |
euotd 5498, fnotovb 7464 |
| ov | operation value | df-ov 7415 |
(𝐴𝐹𝐵) | Yes
| fnotovb 7464, fnovrn 7587 |
| p | plus (see "add"), for all-constant
theorems | df-add 11112 |
(3 + 2) = 5 | Yes |
3p2e5 12392 |
| pfx | prefix | df-pfx 14711 |
(𝑊 prefix 𝐿) | Yes |
pfxlen 14723, ccatpfx 14740 |
| pm | Principia Mathematica | |
| No | pm2.27 43 |
| pm | partial mapping (operation) | df-pm 8828 |
(𝐴 ↑pm 𝐵) | Yes | elpmi 8844, pmsspw 8876 |
| pr | pair | df-pr 4593 |
{𝐴, 𝐵} | Yes |
elpr 4615, prcom 4699, prid1g 4727, prnz 4744 |
| prm, prime | prime (number) | df-prm 16731 |
ℙ | Yes | 1nprm 16738, dvdsprime 16746 |
| pss | proper subset | df-pss 3926 |
𝐴 ⊊ 𝐵 | Yes | pssss 4053, sspsstri 4061 |
| q | rational numbers ("quotients") | df-q 12974 |
ℚ | Yes | elq 12975 |
| r | reversed (suffix) | |
| No | pm4.71r 567, caovdir 7646 |
| r | right | |
| No | orcd 886, simprl 782 |
| rab | restricted class abstraction |
df-rab 3417 | {𝑥 ∈ 𝐴 ∣ 𝜑} | Yes |
rabswap 3425, df-oprab 7416 |
| ral | restricted universal quantification |
df-ral 3080 | ∀𝑥 ∈ 𝐴𝜑 | Yes |
ralnex 3091, ralrnmpo 7551 |
| rcl | reverse closure | |
| No | ndmfvrcl 6916, nnarcl 8603 |
| re | real numbers | df-r 11111 |
ℝ | Yes | recn 11191, 0re 11211 |
| rel | relation | df-rel 5670 | Rel 𝐴 |
Yes | brrelex1 5716, relmpoopab 8090 |
| res | restriction | df-res 5675 |
(𝐴 ↾ 𝐵) | Yes |
opelres 5986, f1ores 6837 |
| reu | restricted existential uniqueness |
df-reu 3370 | ∃!𝑥 ∈ 𝐴𝜑 | Yes |
nfreud 3413, reurex 3373 |
| rex | restricted existential quantification |
df-rex 3090 | ∃𝑥 ∈ 𝐴𝜑 | Yes |
rexnal 3117, rexrnmpo 7552 |
| rmo | restricted "at most one" |
df-rmo 3369 | ∃*𝑥 ∈ 𝐴𝜑 | Yes |
nfrmod 3412, nrexrmo 3388 |
| rn | range | df-rn 5674 | ran 𝐴 |
Yes | elrng 5883, rncnvcnv 5926 |
| ring | (unital) ring | df-ring 20318 |
Ring | Yes |
ringidval 20266, isring 20320, ringgrp 20321 |
| rng | non-unital ring | df-rng 20232 |
Rng | Yes |
isrng 20233, rngabl 20234, rnglz 20244 |
| rot | rotation | |
| No | 3anrot 1117, 3orrot 1108 |
| s | eliminates need for syllogism (suffix) |
| | No | ancoms 463 |
| sb | (proper) substitution (of a set) |
df-sb 2097 | [𝑦 / 𝑥]𝜑 | Yes |
spsbe 2116, sbimi 2108 |
| sbc | (proper) substitution of a class |
df-sbc 3746 | [𝐴 / 𝑥]𝜑 | Yes |
sbc2or 3754, sbcth 3760 |
| sca | scalar | df-sca 17327 |
(Scalar‘𝐻) | Yes |
resssca 17397, mgpsca 20223 |
| simp | simple, simplification | |
| No | simpl 487, simp3r3 1302 |
| sn | singleton | df-sn 4591 |
{𝐴} | Yes | eldifsn 4754 |
| sp | specialization | |
| No | spsbe 2116, spei 2426 |
| ss | subset | df-ss 3923 |
𝐴 ⊆ 𝐵 | Yes | difss 4091 |
| struct | structure | df-struct 17208 |
Struct | Yes | brstruct 17209, structfn 17217 |
| sub | subtract | df-sub 11444 |
(𝐴 − 𝐵) | Yes |
subval 11449, subaddi 11546 |
| sup | supremum | df-sup 9403 |
sup(𝐴, 𝐵, < ) | Yes |
fisupcl 9431, supmo 9413 |
| supp | support (of a function) | df-supp 8158 |
(𝐹 supp 𝑍) | Yes |
ressuppfi 9356, mptsuppd 8184 |
| swap | swap (two parts within a theorem) |
| | No | rabswap 3425, 2reuswap 3710 |
| syl | syllogism | syl 18 |
| No | 3syl 19 |
| sym | symmetric | |
| No | df-symdif 4207, cnvsym 6116 |
| symg | symmetric group | df-symg 19441 |
(SymGrp‘𝐴) | Yes |
symghash 19449, pgrpsubgsymg 19480 |
| t |
times (see "mul"), for all-constant theorems |
df-mul 11113 |
(3 · 2) = 6 | Yes |
3t2e6 12407 |
| th, t |
theorem |
|
|
No |
nfth 1831, sbcth 3760, weth 10480, ancomst 469 |
| tp | triple | df-tp 4595 |
{𝐴, 𝐵, 𝐶} | Yes |
eltpi 4655, tpeq1 4709 |
| tr | transitive | |
| No | bitrd 282, biantr 817 |
| tru, t |
true, truth |
df-tru 1573 |
⊤ |
Yes |
bitru 1579, truanfal 1604, biimt 363 |
| un | union | df-un 3911 |
(𝐴 ∪ 𝐵) | Yes |
uneqri 4111, uncom 4113 |
| unit | unit (in a ring) |
df-unit 20441 | (Unit‘𝑅) | Yes |
isunit 20456, nzrunit 20609 |
| v |
setvar (especially for specializations of
theorems when a class is replaced by a setvar variable) |
|
x |
Yes |
cv 1569, vex 3459, velpw 4568, vtoclf 3531 |
| v |
disjoint variable condition used in place of nonfreeness
hypothesis (suffix) |
|
|
No |
spimv 2422 |
| vtx |
vertex |
df-vtx 29326 |
(Vtx‘𝐺) |
Yes |
vtxval0 29367, opvtxov 29333 |
| vv |
two disjoint variable conditions used in place of nonfreeness
hypotheses (suffix) |
|
|
No |
19.23vv 1973 |
| w | weak (version of a theorem) (suffix) | |
| No | ax11w 2165, spnfw 2009 |
| wrd | word |
df-word 14553 | Word 𝑆 | Yes |
iswrdb 14559, wrdfn 14567, ffz0iswrd 14580 |
| xp | cross product (Cartesian product) |
df-xp 5669 | (𝐴 × 𝐵) | Yes |
elxp 5686, opelxpi 5700, xpundi 5732 |
| xr | eXtended reals | df-xr 11248 |
ℝ* | Yes | ressxr 11254, rexr 11256, 0xr 11257 |
| z | integers (from German "Zahlen") |
df-z 12593 | ℤ | Yes |
elz 12594, zcn 12597 |
| zn | ring of integers mod 𝑁 | df-zn 21637 |
(ℤ/nℤ‘𝑁) | Yes |
znval 21666, zncrng 21675, znhash 21689 |
| zring | ring of integers | df-zring 21578 |
ℤring | Yes | zringbas 21584, zringcrng 21579
|
| 0, z |
slashed zero (empty set) | df-nul 4288 |
∅ | Yes |
n0i 4294, vn0 4299; snnz 4743, prnz 4744 |
(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.) |
