| Description:
The following gives conventions used in the Metamath Proof Explorer
(MPE, set.mm) regarding labels.
For other conventions, see conventions 31047 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 3082"rgen.1 $e |- ( x e. A -> ph ) $."
or letters corresponding to the (main) class variable used in the
hypothesis, e.g., for mdet0 22965: "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 47366.
- 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 1872, and the restricted quantifier version of Theorem 21 from
Section 19 of [Margaris] p. 90 is labeled r19.21 3261.
- 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... 16091. 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 4050, and thus its syntax label fragment is "dif". Similarly, the
subclass relation 𝐴 ⊆ 𝐵 has syntax label fragment "ss"
because it is defined in df-ss 3901. 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 4075. There are many other syntax label fragments, e.g.,
singleton construct {𝐴} has syntax label fragment "sn" (because it
is defined in df-sn 4589), and the pair construct {𝐴, 𝐵} has
fragment "pr" ( from df-pr 4591). 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 4748. An "n" is often used for negation (¬), e.g.,
nan 843.
- 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 11243) and "re" represents real numbers ℝ (Definition df-r 11247).
The empty set ∅ often uses fragment 0, even though it is defined
in df-nul 4282. The syntax construct (𝐴 + 𝐵) usually uses the
fragment "add" (which is consistent with df-add 11248), 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 12515.
- 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 16359 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 16277) we have value cosval 16332 and
closure coscl 16336.
- 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 31050 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 1974 versus 19.21 2247. This
often permits to prove the result using fewer axioms, and/or to
eliminate a nonfreeness hypothesis (such as Ⅎ𝑥𝜑 in 19.21 2247).
If no constraint is put on axiom use, then the v-version can be proved
from the original theorem using nfv 1949. If two (resp. three) such
disjoint variable conditions are added, then the suffix "vv" (resp.
"vvv") is used, e.g., exlimivv 1967.
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 5422.
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 3525.
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 596), commutes
(e.g., biimpac 484)
- 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 482, rexlimiva 3159 |
| abl | Abelian group | df-abl 20039 |
Abel | Yes | ablgrp 20041, zringabl 21801 |
| abs | absorption | | | No |
ressabs 17467 |
| abs | absolute value (of a complex number) |
df-abs 15444 | (abs‘𝐴) | Yes |
absval 15446, absneg 15485, abs1 15505 |
| ad | adding | |
| No | adantr 486, ad2antlr 740 |
| add | add (see "p") | df-add 11248 |
(𝐴 + 𝐵) | Yes |
addcl 11319, addcom 11533, addass 11324 |
| al | "for all" | |
∀𝑥𝜑 | No | alim 1843, alex 1859 |
| ALT | alternative/less preferred (suffix) | |
| No | idALT 24 |
| an | and | df-an 402 |
(𝜑 ∧ 𝜓) | Yes |
anor 998, iman 407, imnan 405 |
| ant | antecedent | |
| No | adantr 486 |
| ass | associative | |
| No | biass 388, orass 935, mulass 11325 |
| asym | asymmetric, antisymmetric | |
| No | intasym 6125, asymref 6126, posasymb 18534 |
| ax | axiom | |
| No | ax6dgen 2167, ax1cn 11271 |
| bas, base |
base (set of an extensible structure) | df-base 17429 |
(Base‘𝑆) | Yes |
baseval 17430, ressbas 17455, cnfldbas 21724 |
| b, bi | biconditional ("iff", "if and only if")
| df-bi 210 | (𝜑 ↔ 𝜓) | Yes |
impbid 215, sspwb 5422 |
| br | binary relation | df-br 5107 |
𝐴𝑅𝐵 | Yes | brab1 5157, brun 5160 |
| c | commutes, commuted (suffix) | | |
No | biimpac 484 |
| c | contraction (suffix) | | |
No | sylc 66, syl2anc 596 |
| cbv | change bound variable | | |
No | cbvalivw 2042, cbvrex 3352 |
| cdm | codomain | |
| No | ffvelcdm 7111, focdmex 8000 |
| cl | closure | | | No |
ifclda 4521, ovrcl 7490, zaddcl 12774 |
| cn | complex numbers | df-c 11243 |
ℂ | Yes | nnsscn 12378, nncn 12381 |
| cnfld | field of complex numbers | df-cnfld 21721 |
ℂfld | Yes | cnfldbas 21724, cnfldinv 21751 |
| cntz | centralizer | df-cntz 19573 |
(Cntz‘𝑀) | Yes |
cntzfval 19576, dprdfcntz 20273 |
| cnv | converse | df-cnv 5664 |
◡𝐴 | Yes | opelcnvg 5868, f1ocnv 6865 |
| co | composition | df-co 5665 |
(𝐴 ∘ 𝐵) | Yes | cnvco 5877, fmptco 7160 |
| com | commutative | |
| No | orcom 884, bicomi 227, eqcomi 2772 |
| con | contradiction, contraposition | |
| No | condan 830, con2d 135 |
| csb | class substitution | df-csb 3852 |
⦋𝐴 / 𝑥⦌𝐵 | Yes |
csbid 3864, csbie2g 3891 |
| cyg | cyclic group | df-cyg 20134 |
CycGrp | Yes |
iscyg 20135, zringcyg 21819 |
| d | deduction form (suffix) | |
| No | idd 25, impbid 215 |
| df | (alternate) definition (prefix) | |
| No | dfrel2 6197, dffn2 6739 |
| di, distr | distributive | |
| No |
andi 1025, imdi 394, ordi 1023, difindi 4240, ndmovdistr 7640 |
| dif | class difference | df-dif 4050 |
(𝐴 ∖ 𝐵) | Yes |
difss 4075, difindi 4240 |
| div | division | df-div 12012 |
(𝐴 / 𝐵) | Yes |
divcl 12018, divval 12014, divmul 12015 |
| dm | domain | df-dm 5666 |
dom 𝐴 | Yes | dmmpt 6258, iswrddm0 14722 |
| e, eq, equ | equals (equ for setvars, eq for
classes) | df-cleq 2755 |
𝐴 = 𝐵 | Yes |
2p2e4 12515, uneqri 4158, equtr 2056 |
| edg | edge | df-edg 29672 |
(Edg‘𝐺) | Yes |
edgopval 29675, usgredgppr 29823 |
| el | element of | |
𝐴 ∈ 𝐵 | Yes |
eldif 4052, eldifsn 4748, elssuni 4902 |
| en | equinumerous | df-en |
𝐴 ≈ 𝐵 | Yes | domen 9024, enfi 9238 |
| eu | "there exists exactly one" | eu6 2602 |
∃!𝑥𝜑 | Yes | euex 2605, euabsn 4687 |
| ex | exists (i.e. is a set) | |
∈ V | No | brrelex1 5709, 0ex 5265 |
| ex, e | "there exists (at least one)" |
df-ex 1813 |
∃𝑥𝜑 | Yes | exim 1867, alex 1859 |
| exp | export | |
| No | expt 178, expcom 419 |
| f | "not free in" (suffix) | |
| No | equs45f 2491, sbf 2308 |
| f | function | df-f 6568 |
𝐹:𝐴⟶𝐵 | Yes | fssxp 6765, opelf 6771 |
| fal | false | df-fal 1583 |
⊥ | Yes | bifal 1586, falantru 1605 |
| fi | finite intersection | df-fi 9438 |
(fi‘𝐵) | Yes | fival 9439, inelfi 9445 |
| fi, fin | finite | df-fin 9013 |
Fin | Yes |
isfi 9038, snfi 9107, onfin 9266 |
| fld | field (Note: there is an alternative
definition Fld of a field, see df-fld 39185) | df-field 21025 |
Field | Yes | isfld 21035, fldidom 21071 |
| fn | function with domain | df-fn 6567 |
𝐴 Fn 𝐵 | Yes | ffn 6737, fndm 6670 |
| frgp | free group | df-frgp 19966 |
(freeGrp‘𝐼) | Yes |
frgpval 20014, frgpadd 20019 |
| fsupp | finitely supported function |
df-fsupp 9390 | 𝑅 finSupp 𝑍 | Yes |
isfsupp 9393, fdmfisuppfi 9401, fsuppco 9429 |
| fun | function | df-fun 6566 |
Fun 𝐹 | Yes | funrel 6582, ffun 6740 |
| fv | function value | df-fv 6572 |
(𝐹‘𝐴) | Yes | fvres 6933, swrdfv 14836 |
| fz | finite set of sequential integers |
df-fz 13678 |
(𝑀...𝑁) | Yes | fzval 13679, eluzfz 13689 |
| fz0 | finite set of sequential nonnegative integers |
|
(0...𝑁) | Yes | nn0fz0 13797, fz0tp 13800 |
| fzo | half-open integer range | df-fzo 13827 |
(𝑀..^𝑁) | Yes |
elfzo 13833, elfzofz 13848 |
| g | more general (suffix); eliminates "is a set"
hypotheses | |
| No | uniexg 7787 |
| gr | graph | |
| No | uhgrf 29686, isumgr 29719, usgrres1 29942 |
| grp | group | df-grp 19188 |
Grp | Yes | isgrp 19191, tgpgrp 24441 |
| gsum | group sum | df-gsum 17654 |
(𝐺 Σg 𝐹) | Yes |
gsumval 18907, gsumwrev 19622 |
| hash | size (of a set) | df-hash 14514 |
(♯‘𝐴) | Yes |
hashgval 14516, hashfz1 14529, hashcl 14539 |
| hb | hypothesis builder (prefix) | |
| No | hbxfrbi 1858, hbald 2208, hbequid 40225 |
| hm | (monoid, group, ring, ...) homomorphism |
| | No |
ismhm 19021, isghm 19471, isrhm 20751 |
| i | inference (suffix) | |
| No | eleq1i 2855, tcsni 9777 |
| i | implication (suffix) | |
| No | brwdomi 9597, infeq5i 9672 |
| id | identity | |
| No | biid 264 |
| iedg | indexed edge | df-iedg 29623 |
(iEdg‘𝐺) | Yes |
iedgval0 29664, edgiedgb 29678 |
| idm | idempotent | |
| No | anidm 575, tpidm13 4717 |
| im, imp | implication (label often omitted) |
df-im 15309 | (𝐴 → 𝐵) | Yes |
iman 407, imnan 405, impbidd 213 |
| im | (group, ring, ...) isomorphism | |
| No | isgim 19517, rimrcl 20754 |
| ima | image | df-ima 5669 |
(𝐴 “ 𝐵) | Yes | resima 6072, imaundi 6157 |
| imp | import | |
| No | biimpa 482, impcom 413 |
| in | intersection | df-in 4094 |
(𝐴 ∩ 𝐵) | Yes | elin 4096, incom 4109 |
| inf | infimum | df-inf 9470 |
inf(ℝ+, ℝ*, < ) | Yes |
fiinfcl 9530, infiso 9537 |
| is... | is (something a) ...? | |
| No | isring 20505 |
| j | joining, disjoining | |
| No | jc 162, jaoi 871 |
| l | left | |
| No | olcd 888, simpl 488 |
| map | mapping operation or set exponentiation |
df-map 8885 | (𝐴 ↑m 𝐵) | Yes |
mapvalg 8892, elmapex 8904 |
| mat | matrix | df-mat 22767 |
(𝑁 Mat 𝑅) | Yes |
matval 22770, matring 22802 |
| mdet | determinant (of a square matrix) |
df-mdet 22944 | (𝑁 maDet 𝑅) | Yes |
mdetleib 22946, mdetrlin 22961 |
| mgm | magma | df-mgm 18857 |
Magma | Yes |
mgmidmo 18879, mgmlrid 18888, ismgm 18858 |
| mgp | multiplicative group | df-mgp 20403 |
(mulGrp‘𝑅) | Yes |
mgpress 20412, ringmgp 20507 |
| mnd | monoid | df-mnd 18965 |
Mnd | Yes | mndass 18973, mndodcong 19798 |
| 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 7454 | (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) | Yes |
mpompt 7563, resmpo 7569 |
| mpt | modus ponendo tollens | |
| No | mptnan 1801, mptxor 1802 |
| mpt | maps-to notation for a function |
df-mpt 5191 | (𝑥 ∈ 𝐴 ↦ 𝐵) | Yes |
fconstmpt 5718, resmpt 6045 |
| mul | multiplication (see "t") | df-mul 11249 |
(𝐴 · 𝐵) | Yes |
mulcl 11321, divmul 12015, mulcom 11323, mulass 11325 |
| n, not | not | |
¬ 𝜑 | Yes |
nan 843, notnotr 131 |
| ne | not equal | df-ne | 𝐴 ≠ 𝐵 |
Yes | exmidne 2969, neeqtrd 3028 |
| nel | not element of | df-nel | 𝐴 ∉ 𝐵
|
Yes | neli 3067, nnel 3075 |
| ne0 | not equal to zero (see n0) | |
≠ 0 | No |
negne0d 11704, ine0 11788, gt0ne0 11819 |
| nf | "not free in" (prefix) | df-nf 1817 |
Ⅎ𝑥𝜑 | Yes | nfnd 1891 |
| ngp | normed group | df-ngp 24946 |
NrmGrp | Yes | isngp 24959, ngptps 24965 |
| nm | norm (on a group or ring) | df-nm 24945 |
(norm‘𝑊) | Yes |
nmval 24952, subgnm 24996 |
| nn | positive integers | df-nn 12374 |
ℕ | Yes | nnsscn 12378, nncn 12381 |
| nn0 | nonnegative integers | df-n0 12645 |
ℕ0 | Yes | nnnn0 12651, nn0cn 12654 |
| n0 | not the empty set (see ne0) | |
≠ ∅ | No | n0i 4289, vn0 4294, ssn0 4358 |
| OLD | old, obsolete (to be removed soon) | |
| No | 19.43OLD 1918 |
| on | ordinal number | df-on 6390 |
𝐴 ∈ On | Yes |
elon 6395, 1on 8525 onelon 6411 |
| op | ordered pair | df-op 4839 |
⟨𝐴, 𝐵⟩ | Yes | dfopif 4840, opth 5450 |
| or | or | df-or 862 |
(𝜑 ∨ 𝜓) | Yes |
orcom 884, anor 998 |
| ot | ordered triple | df-ot 4862 |
⟨𝐴, 𝐵, 𝐶⟩ | Yes |
euotd 5491, fnotovb 7501 |
| ov | operation value | df-ov 7452 |
(𝐴𝐹𝐵) | Yes
| fnotovb 7501, fnovrn 7626 |
| p | plus (see "add"), for all-constant
theorems | df-add 11248 |
(3 + 2) = 5 | Yes |
3p2e5 12531 |
| pfx | prefix | df-pfx 14861 |
(𝑊 prefix 𝐿) | Yes |
pfxlen 14873, ccatpfx 14890 |
| pm | Principia Mathematica | |
| No | pm2.27 43 |
| pm | partial mapping (operation) | df-pm 8886 |
(𝐴 ↑pm 𝐵) | Yes | elpmi 8902, pmsspw 8941 |
| pr | pair | df-pr 4591 |
{𝐴, 𝐵} | Yes |
elpr 4609, prcom 4693, prid1g 4721, prnz 4738 |
| prm, prime | prime (number) | df-prm 16888 |
ℙ | Yes | 1nprm 16895, dvdsprime 16903 |
| pss | proper subset | df-pss 4017 |
𝐴 ⊊ 𝐵 | Yes | pssss 4028, sspsstri 4036 |
| q | rational numbers ("quotients") | df-q 13114 |
ℚ | Yes | elq 13115 |
| r | reversed (suffix) | |
| No | pm4.71r 568, caovdir 7685 |
| r | right | |
| No | orcd 887, simprl 783 |
| rab | restricted class abstraction |
df-rab 3417 | {𝑥 ∈ 𝐴 ∣ 𝜑} | Yes |
rabswap 3425, df-oprab 7453 |
| ral | restricted universal quantification |
df-ral 3081 | ∀𝑥 ∈ 𝐴𝜑 | Yes |
ralnex 3092, ralrnmpo 7589 |
| rcl | reverse closure | |
| No | ndmfvrcl 6947, nnarcl 8661 |
| re | real numbers | df-r 11247 |
ℝ | Yes | recn 11327, 0re 11347 |
| rel | relation | df-rel 5663 | Rel 𝐴 |
Yes | brrelex1 5709, relmpoopab 8139 |
| res | restriction | df-res 5668 |
(𝐴 ↾ 𝐵) | Yes |
opelres 5990, f1ores 6867 |
| reu | restricted existential uniqueness |
df-reu 3370 | ∃!𝑥 ∈ 𝐴𝜑 | Yes |
nfreud 3413, reurex 3373 |
| rex | restricted existential quantification |
df-rex 3091 | ∃𝑥 ∈ 𝐴𝜑 | Yes |
rexnal 3118, rexrnmpo 7590 |
| rmo | restricted "at most one" |
df-rmo 3369 | ∃*𝑥 ∈ 𝐴𝜑 | Yes |
nfrmod 3412, nrexrmo 3388 |
| rn | range | df-rn 5667 | ran 𝐴 |
Yes | elrng 5883, rncnvcnv 5926 |
| ring | (unital) ring | df-ring 20503 |
Ring | Yes |
ringidval 20451, isring 20505, ringgrp 20506 |
| rng | non-unital ring | df-rng 20417 |
Rng | Yes |
isrng 20418, rngabl 20419, rnglz 20429 |
| rot | rotation | |
| No | 3anrot 1117, 3orrot 1108 |
| s | eliminates need for syllogism (suffix) |
| | No | ancoms 464 |
| sb | (proper) substitution (of a set) |
df-sb 2102 | [𝑦 / 𝑥]𝜑 | Yes |
spsbe 2121, sbimi 2113 |
| sbc | (proper) substitution of a class |
df-sbc 3743 | [𝐴 / 𝑥]𝜑 | Yes |
sbc2or 3751, sbcth 3757 |
| sca | scalar | df-sca 17485 |
(Scalar‘𝐻) | Yes |
resssca 17555, mgpsca 20408 |
| simp | simple, simplification | |
| No | simpl 488, simp3r3 1302 |
| sn | singleton | df-sn 4589 |
{𝐴} | Yes | eldifsn 4748 |
| sp | specialization | |
| No | spsbe 2121, spei 2426 |
| ss | subset | df-ss 3901 |
𝐴 ⊆ 𝐵 | Yes | difss 4075 |
| struct | structure | df-struct 17366 |
Struct | Yes | brstruct 17367, structfn 17375 |
| sub | subtract | df-sub 11580 |
(𝐴 − 𝐵) | Yes |
subval 11585, subaddi 11682 |
| sup | supremum | df-sup 9469 |
sup(𝐴, 𝐵, < ) | Yes |
fisupcl 9497, supmo 9479 |
| supp | support (of a function) | df-supp 8213 |
(𝐹 supp 𝑍) | Yes |
ressuppfi 9422, mptsuppd 8240 |
| swap | swap (two parts within a theorem) |
| | No | rabswap 3425, 2reuswap 3707 |
| syl | syllogism | syl 18 |
| No | 3syl 19 |
| sym | symmetric | |
| No | df-symdif 4201, cnvsym 6124 |
| symg | symmetric group | df-symg 19626 |
(SymGrp‘𝐴) | Yes |
symghash 19634, pgrpsubgsymg 19665 |
| t |
times (see "mul"), for all-constant theorems |
df-mul 11249 |
(3 · 2) = 6 | Yes |
3t2e6 12546 |
| th, t |
theorem |
|
|
No |
nfth 1834, sbcth 3757, weth 10610, ancomst 470 |
| tp | triple | df-tp 4593 |
{𝐴, 𝐵, 𝐶} | Yes |
eltpi 4649, tpeq1 4703 |
| tr | transitive | |
| No | bitrd 282, biantr 818 |
| tru, t |
true, truth |
df-tru 1573 |
⊤ |
Yes |
bitru 1579, truanfal 1604, biimt 363 |
| un | union | df-un 4154 |
(𝐴 ∪ 𝐵) | Yes |
uneqri 4158, uncom 4160 |
| unit | unit (in a ring) |
df-unit 20630 | (Unit‘𝑅) | Yes |
isunit 20645, nzrunit 20817 |
| v |
setvar (especially for specializations of
theorems when a class is replaced by a setvar variable) |
|
x |
Yes |
cv 1569, vex 3458, velpw 4565, vtoclf 3529 |
| v |
disjoint variable condition used in place of nonfreeness
hypothesis (suffix) |
|
|
No |
spimv 2422 |
| vtx |
vertex |
df-vtx 29622 |
(Vtx‘𝐺) |
Yes |
vtxval0 29663, opvtxov 29629 |
| vv |
two disjoint variable conditions used in place of nonfreeness
hypotheses (suffix) |
|
|
No |
19.23vv 1978 |
| w | weak (version of a theorem) (suffix) | |
| No | ax11w 2169, spnfw 2014 |
| wrd | word |
df-word 14698 | Word 𝑆 | Yes |
iswrdb 14704, wrdfn 14712, ffz0iswrd 14725 |
| xp | cross product (Cartesian product) |
df-xp 5662 | (𝐴 × 𝐵) | Yes |
elxp 5679, opelxpi 5693, xpundi 5725 |
| xr | eXtended reals | df-xr 11384 |
ℝ* | Yes | ressxr 11390, rexr 11392, 0xr 11393 |
| z | integers (from German "Zahlen") |
df-z 12732 | ℤ | Yes |
elz 12733, zcn 12736 |
| zn | ring of integers mod 𝑁 | df-zn 21856 |
(ℤ/nℤ‘𝑁) | Yes |
znval 21885, zncrng 21894, znhash 21908 |
| zring | ring of integers | df-zring 21797 |
ℤring | Yes | zringbas 21803, zringcrng 21798
|
| 0, z |
slashed zero (empty set) | df-nul 4282 |
∅ | Yes |
n0i 4289, vn0 4294; snnz 4737, prnz 4738 |
(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.) |
