| Description:
The following gives conventions used in the Metamath Proof Explorer
(MPE, set.mm) regarding labels.
For other conventions, see conventions 30348 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 3046"rgen.1 $e |- ( x e. A -> ph ) $."
or letters corresponding to the (main) class variable used in the
hypothesis, e.g., for mdet0 22491: "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 2656 and stirling 46090.
- 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 3224.
- 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... 15788. 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 3906, and thus its syntax label fragment is "dif". Similarly, the
subclass relation 𝐴 ⊆ 𝐵 has syntax label fragment "ss"
because it is defined in df-ss 3920. 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 4087. There are many other syntax label fragments, e.g.,
singleton construct {𝐴} has syntax label fragment "sn" (because it
is defined in df-sn 4578), and the pair construct {𝐴, 𝐵} has
fragment "pr" ( from df-pr 4580). 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 4737. An "n" is often used for negation (¬), e.g.,
nan 829.
- 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 11015) and "re" represents real numbers ℝ (Definition df-r 11019).
The empty set ∅ often uses fragment 0, even though it is defined
in df-nul 4285. The syntax construct (𝐴 + 𝐵) usually uses the
fragment "add" (which is consistent with df-add 11020), 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 12258.
- 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 16059 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 15977) we have value cosval 16032 and
closure coscl 16036.
- 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 30351 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 2208. This
often permits to prove the result using fewer axioms, and/or to
eliminate a nonfreeness hypothesis (such as Ⅎ𝑥𝜑 in 19.21 2208).
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 2569 derived from eu6 2567. 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 5392.
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 2407 (cbval 2396 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 3515.
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 3122 |
| abl | Abelian group | df-abl 19662 |
Abel | Yes | ablgrp 19664, zringabl 21358 |
| abs | absorption | | | No |
ressabs 17159 |
| abs | absolute value (of a complex number) |
df-abs 15143 | (abs‘𝐴) | Yes |
absval 15145, absneg 15184, abs1 15204 |
| ad | adding | |
| No | adantr 480, ad2antlr 727 |
| add | add (see "p") | df-add 11020 |
(𝐴 + 𝐵) | Yes |
addcl 11091, addcom 11302, addass 11096 |
| al | "for all" | |
∀𝑥𝜑 | No | alim 1810, alex 1826 |
| ALT | alternative/less preferred (suffix) | |
| No | idALT 23 |
| an | and | df-an 396 |
(𝜑 ∧ 𝜓) | Yes |
anor 984, iman 401, imnan 399 |
| ant | antecedent | |
| No | adantr 480 |
| ass | associative | |
| No | biass 384, orass 921, mulass 11097 |
| asym | asymmetric, antisymmetric | |
| No | intasym 6064, asymref 6065, posasymb 18225 |
| ax | axiom | |
| No | ax6dgen 2129, ax1cn 11043 |
| bas, base |
base (set of an extensible structure) | df-base 17121 |
(Base‘𝑆) | Yes |
baseval 17122, ressbas 17147, cnfldbas 21265 |
| b, bi | biconditional ("iff", "if and only if")
| df-bi 207 | (𝜑 ↔ 𝜓) | Yes |
impbid 212, sspwb 5392 |
| br | binary relation | df-br 5093 |
𝐴𝑅𝐵 | Yes | brab1 5140, brun 5143 |
| c | commutes, commuted (suffix) | | |
No | biimpac 478 |
| c | contraction (suffix) | | |
No | sylc 65, syl2anc 584 |
| cbv | change bound variable | | |
No | cbvalivw 2007, cbvrex 3326 |
| cdm | codomain | |
| No | ffvelcdm 7015, focdmex 7891 |
| cl | closure | | | No |
ifclda 4512, ovrcl 7390, zaddcl 12515 |
| cn | complex numbers | df-c 11015 |
ℂ | Yes | nnsscn 12133, nncn 12136 |
| cnfld | field of complex numbers | df-cnfld 21262 |
ℂfld | Yes | cnfldbas 21265, cnfldinv 21309 |
| cntz | centralizer | df-cntz 19196 |
(Cntz‘𝑀) | Yes |
cntzfval 19199, dprdfcntz 19896 |
| cnv | converse | df-cnv 5627 |
◡𝐴 | Yes | opelcnvg 5823, f1ocnv 6776 |
| co | composition | df-co 5628 |
(𝐴 ∘ 𝐵) | Yes | cnvco 5828, fmptco 7063 |
| com | commutative | |
| No | orcom 870, bicomi 224, eqcomi 2738 |
| con | contradiction, contraposition | |
| No | condan 817, con2d 134 |
| csb | class substitution | df-csb 3852 |
⦋𝐴 / 𝑥⦌𝐵 | Yes |
csbid 3864, csbie2g 3891 |
| cyg | cyclic group | df-cyg 19757 |
CycGrp | Yes |
iscyg 19758, zringcyg 21376 |
| d | deduction form (suffix) | |
| No | idd 24, impbid 212 |
| df | (alternate) definition (prefix) | |
| No | dfrel2 6138, dffn2 6654 |
| di, distr | distributive | |
| No |
andi 1009, imdi 389, ordi 1007, difindi 4243, ndmovdistr 7538 |
| dif | class difference | df-dif 3906 |
(𝐴 ∖ 𝐵) | Yes |
difss 4087, difindi 4243 |
| div | division | df-div 11778 |
(𝐴 / 𝐵) | Yes |
divcl 11785, divval 11781, divmul 11782 |
| dm | domain | df-dm 5629 |
dom 𝐴 | Yes | dmmpt 6189, iswrddm0 14445 |
| e, eq, equ | equals (equ for setvars, eq for
classes) | df-cleq 2721 |
𝐴 = 𝐵 | Yes |
2p2e4 12258, uneqri 4107, equtr 2021 |
| edg | edge | df-edg 28997 |
(Edg‘𝐺) | Yes |
edgopval 29000, usgredgppr 29145 |
| el | element of | |
𝐴 ∈ 𝐵 | Yes |
eldif 3913, eldifsn 4737, elssuni 4888 |
| en | equinumerous | df-en |
𝐴 ≈ 𝐵 | Yes | domen 8887, enfi 9101 |
| eu | "there exists exactly one" | eu6 2567 |
∃!𝑥𝜑 | Yes | euex 2570, euabsn 4678 |
| ex | exists (i.e. is a set) | |
∈ V | No | brrelex1 5672, 0ex 5246 |
| 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 2457, sbf 2271 |
| f | function | df-f 6486 |
𝐹:𝐴⟶𝐵 | Yes | fssxp 6679, opelf 6685 |
| fal | false | df-fal 1553 |
⊥ | Yes | bifal 1556, falantru 1575 |
| fi | finite intersection | df-fi 9301 |
(fi‘𝐵) | Yes | fival 9302, inelfi 9308 |
| fi, fin | finite | df-fin 8876 |
Fin | Yes |
isfi 8901, snfi 8968, onfin 9129 |
| fld | field (Note: there is an alternative
definition Fld of a field, see df-fld 37992) | df-field 20617 |
Field | Yes | isfld 20625, fldidom 20656 |
| fn | function with domain | df-fn 6485 |
𝐴 Fn 𝐵 | Yes | ffn 6652, fndm 6585 |
| frgp | free group | df-frgp 19589 |
(freeGrp‘𝐼) | Yes |
frgpval 19637, frgpadd 19642 |
| fsupp | finitely supported function |
df-fsupp 9252 | 𝑅 finSupp 𝑍 | Yes |
isfsupp 9255, fdmfisuppfi 9264, fsuppco 9292 |
| fun | function | df-fun 6484 |
Fun 𝐹 | Yes | funrel 6499, ffun 6655 |
| fv | function value | df-fv 6490 |
(𝐹‘𝐴) | Yes | fvres 6841, swrdfv 14555 |
| fz | finite set of sequential integers |
df-fz 13411 |
(𝑀...𝑁) | Yes | fzval 13412, eluzfz 13422 |
| fz0 | finite set of sequential nonnegative integers |
|
(0...𝑁) | Yes | nn0fz0 13528, fz0tp 13531 |
| fzo | half-open integer range | df-fzo 13558 |
(𝑀..^𝑁) | Yes |
elfzo 13564, elfzofz 13578 |
| g | more general (suffix); eliminates "is a set"
hypotheses | |
| No | uniexg 7676 |
| gr | graph | |
| No | uhgrf 29011, isumgr 29044, usgrres1 29264 |
| grp | group | df-grp 18815 |
Grp | Yes | isgrp 18818, tgpgrp 23963 |
| gsum | group sum | df-gsum 17346 |
(𝐺 Σg 𝐹) | Yes |
gsumval 18551, gsumwrev 19245 |
| hash | size (of a set) | df-hash 14238 |
(♯‘𝐴) | Yes |
hashgval 14240, hashfz1 14253, hashcl 14263 |
| hb | hypothesis builder (prefix) | |
| No | hbxfrbi 1825, hbald 2169, hbequid 38908 |
| hm | (monoid, group, ring, ...) homomorphism |
| | No |
ismhm 18659, isghm 19094, isrhm 20363 |
| i | inference (suffix) | |
| No | eleq1i 2819, tcsni 9639 |
| i | implication (suffix) | |
| No | brwdomi 9460, infeq5i 9532 |
| id | identity | |
| No | biid 261 |
| iedg | indexed edge | df-iedg 28948 |
(iEdg‘𝐺) | Yes |
iedgval0 28989, edgiedgb 29003 |
| idm | idempotent | |
| No | anidm 564, tpidm13 4708 |
| im, imp | implication (label often omitted) |
df-im 15008 | (𝐴 → 𝐵) | Yes |
iman 401, imnan 399, impbidd 210 |
| im | (group, ring, ...) isomorphism | |
| No | isgim 19141, rimrcl 20367 |
| ima | image | df-ima 5632 |
(𝐴 “ 𝐵) | Yes | resima 5966, imaundi 6098 |
| imp | import | |
| No | biimpa 476, impcom 407 |
| in | intersection | df-in 3910 |
(𝐴 ∩ 𝐵) | Yes | elin 3919, incom 4160 |
| inf | infimum | df-inf 9333 |
inf(ℝ+, ℝ*, < ) | Yes |
fiinfcl 9393, infiso 9400 |
| is... | is (something a) ...? | |
| No | isring 20122 |
| j | joining, disjoining | |
| No | jc 161, jaoi 857 |
| l | left | |
| No | olcd 874, simpl 482 |
| map | mapping operation or set exponentiation |
df-map 8755 | (𝐴 ↑m 𝐵) | Yes |
mapvalg 8763, elmapex 8775 |
| mat | matrix | df-mat 22293 |
(𝑁 Mat 𝑅) | Yes |
matval 22296, matring 22328 |
| mdet | determinant (of a square matrix) |
df-mdet 22470 | (𝑁 maDet 𝑅) | Yes |
mdetleib 22472, mdetrlin 22487 |
| mgm | magma | df-mgm 18514 |
Magma | Yes |
mgmidmo 18534, mgmlrid 18541, ismgm 18515 |
| mgp | multiplicative group | df-mgp 20026 |
(mulGrp‘𝑅) | Yes |
mgpress 20035, ringmgp 20124 |
| mnd | monoid | df-mnd 18609 |
Mnd | Yes | mndass 18617, mndodcong 19421 |
| mo | "there exists at most one" | df-mo 2533 |
∃*𝑥𝜑 | Yes | eumo 2571, moim 2537 |
| mp | modus ponens | ax-mp 5 |
| No | mpd 15, mpi 20 |
| mpo | maps-to notation for an operation |
df-mpo 7354 | (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) | Yes |
mpompt 7463, resmpo 7469 |
| mpt | modus ponendo tollens | |
| No | mptnan 1768, mptxor 1769 |
| mpt | maps-to notation for a function |
df-mpt 5174 | (𝑥 ∈ 𝐴 ↦ 𝐵) | Yes |
fconstmpt 5681, resmpt 5988 |
| mul | multiplication (see "t") | df-mul 11021 |
(𝐴 · 𝐵) | Yes |
mulcl 11093, divmul 11782, mulcom 11095, mulass 11097 |
| n, not | not | |
¬ 𝜑 | Yes |
nan 829, notnotr 130 |
| ne | not equal | df-ne | 𝐴 ≠ 𝐵 |
Yes | exmidne 2935, neeqtrd 2994 |
| nel | not element of | df-nel | 𝐴 ∉ 𝐵
|
Yes | neli 3031, nnel 3039 |
| ne0 | not equal to zero (see n0) | |
≠ 0 | No |
negne0d 11473, ine0 11555, gt0ne0 11585 |
| nf | "not free in" (prefix) | df-nf 1784 |
Ⅎ𝑥𝜑 | Yes | nfnd 1858 |
| ngp | normed group | df-ngp 24469 |
NrmGrp | Yes | isngp 24482, ngptps 24488 |
| nm | norm (on a group or ring) | df-nm 24468 |
(norm‘𝑊) | Yes |
nmval 24475, subgnm 24519 |
| nn | positive integers | df-nn 12129 |
ℕ | Yes | nnsscn 12133, nncn 12136 |
| nn0 | nonnegative integers | df-n0 12385 |
ℕ0 | Yes | nnnn0 12391, nn0cn 12394 |
| n0 | not the empty set (see ne0) | |
≠ ∅ | No | n0i 4291, vn0 4296, ssn0 4355 |
| OLD | old, obsolete (to be removed soon) | |
| No | 19.43OLD 1883 |
| on | ordinal number | df-on 6311 |
𝐴 ∈ On | Yes |
elon 6316, 1on 8400 onelon 6332 |
| op | ordered pair | df-op 4584 |
⟨𝐴, 𝐵⟩ | Yes | dfopif 4821, opth 5419 |
| or | or | df-or 848 |
(𝜑 ∨ 𝜓) | Yes |
orcom 870, anor 984 |
| ot | ordered triple | df-ot 4586 |
⟨𝐴, 𝐵, 𝐶⟩ | Yes |
euotd 5456, fnotovb 7401 |
| ov | operation value | df-ov 7352 |
(𝐴𝐹𝐵) | Yes
| fnotovb 7401, fnovrn 7524 |
| p | plus (see "add"), for all-constant
theorems | df-add 11020 |
(3 + 2) = 5 | Yes |
3p2e5 12274 |
| pfx | prefix | df-pfx 14578 |
(𝑊 prefix 𝐿) | Yes |
pfxlen 14590, ccatpfx 14607 |
| pm | Principia Mathematica | |
| No | pm2.27 42 |
| pm | partial mapping (operation) | df-pm 8756 |
(𝐴 ↑pm 𝐵) | Yes | elpmi 8773, pmsspw 8804 |
| pr | pair | df-pr 4580 |
{𝐴, 𝐵} | Yes |
elpr 4602, prcom 4684, prid1g 4712, prnz 4729 |
| prm, prime | prime (number) | df-prm 16583 |
ℙ | Yes | 1nprm 16590, dvdsprime 16598 |
| pss | proper subset | df-pss 3923 |
𝐴 ⊊ 𝐵 | Yes | pssss 4049, sspsstri 4056 |
| q | rational numbers ("quotients") | df-q 12850 |
ℚ | Yes | elq 12851 |
| r | reversed (suffix) | |
| No | pm4.71r 558, caovdir 7583 |
| r | right | |
| No | orcd 873, simprl 770 |
| rab | restricted class abstraction |
df-rab 3395 | {𝑥 ∈ 𝐴 ∣ 𝜑} | Yes |
rabswap 3404, df-oprab 7353 |
| ral | restricted universal quantification |
df-ral 3045 | ∀𝑥 ∈ 𝐴𝜑 | Yes |
ralnex 3055, ralrnmpo 7488 |
| rcl | reverse closure | |
| No | ndmfvrcl 6856, nnarcl 8534 |
| re | real numbers | df-r 11019 |
ℝ | Yes | recn 11099, 0re 11117 |
| rel | relation | df-rel 5626 | Rel 𝐴 |
Yes | brrelex1 5672, relmpoopab 8027 |
| res | restriction | df-res 5631 |
(𝐴 ↾ 𝐵) | Yes |
opelres 5936, f1ores 6778 |
| reu | restricted existential uniqueness |
df-reu 3344 | ∃!𝑥 ∈ 𝐴𝜑 | Yes |
nfreud 3391, reurex 3347 |
| rex | restricted existential quantification |
df-rex 3054 | ∃𝑥 ∈ 𝐴𝜑 | Yes |
rexnal 3081, rexrnmpo 7489 |
| rmo | restricted "at most one" |
df-rmo 3343 | ∃*𝑥 ∈ 𝐴𝜑 | Yes |
nfrmod 3390, nrexrmo 3364 |
| rn | range | df-rn 5630 | ran 𝐴 |
Yes | elrng 5834, rncnvcnv 5876 |
| ring | (unital) ring | df-ring 20120 |
Ring | Yes |
ringidval 20068, isring 20122, ringgrp 20123 |
| rng | non-unital ring | df-rng 20038 |
Rng | Yes |
isrng 20039, rngabl 20040, rnglz 20050 |
| rot | rotation | |
| No | 3anrot 1099, 3orrot 1091 |
| s | eliminates need for syllogism (suffix) |
| | No | ancoms 458 |
| sb | (proper) substitution (of a set) |
df-sb 2066 | [𝑦 / 𝑥]𝜑 | Yes |
spsbe 2083, sbimi 2075 |
| sbc | (proper) substitution of a class |
df-sbc 3743 | [𝐴 / 𝑥]𝜑 | Yes |
sbc2or 3751, sbcth 3757 |
| sca | scalar | df-sca 17177 |
(Scalar‘𝐻) | Yes |
resssca 17247, mgpsca 20031 |
| simp | simple, simplification | |
| No | simpl 482, simp3r3 1284 |
| sn | singleton | df-sn 4578 |
{𝐴} | Yes | eldifsn 4737 |
| sp | specialization | |
| No | spsbe 2083, spei 2392 |
| ss | subset | df-ss 3920 |
𝐴 ⊆ 𝐵 | Yes | difss 4087 |
| struct | structure | df-struct 17058 |
Struct | Yes | brstruct 17059, structfn 17067 |
| sub | subtract | df-sub 11349 |
(𝐴 − 𝐵) | Yes |
subval 11354, subaddi 11451 |
| sup | supremum | df-sup 9332 |
sup(𝐴, 𝐵, < ) | Yes |
fisupcl 9360, supmo 9342 |
| supp | support (of a function) | df-supp 8094 |
(𝐹 supp 𝑍) | Yes |
ressuppfi 9285, mptsuppd 8120 |
| swap | swap (two parts within a theorem) |
| | No | rabswap 3404, 2reuswap 3706 |
| syl | syllogism | syl 17 |
| No | 3syl 18 |
| sym | symmetric | |
| No | df-symdif 4204, cnvsym 6063 |
| symg | symmetric group | df-symg 19249 |
(SymGrp‘𝐴) | Yes |
symghash 19257, pgrpsubgsymg 19288 |
| t |
times (see "mul"), for all-constant theorems |
df-mul 11021 |
(3 · 2) = 6 | Yes |
3t2e6 12289 |
| th, t |
theorem |
|
|
No |
nfth 1801, sbcth 3757, weth 10389, ancomst 464 |
| tp | triple | df-tp 4582 |
{𝐴, 𝐵, 𝐶} | Yes |
eltpi 4640, tpeq1 4694 |
| tr | transitive | |
| No | bitrd 279, biantr 805 |
| tru, t |
true, truth |
df-tru 1543 |
⊤ |
Yes |
bitru 1549, truanfal 1574, biimt 360 |
| un | union | df-un 3908 |
(𝐴 ∪ 𝐵) | Yes |
uneqri 4107, uncom 4109 |
| unit | unit (in a ring) |
df-unit 20243 | (Unit‘𝑅) | Yes |
isunit 20258, nzrunit 20409 |
| v |
setvar (especially for specializations of
theorems when a class is replaced by a setvar variable) |
|
x |
Yes |
cv 1539, vex 3440, velpw 4556, vtoclf 3519 |
| v |
disjoint variable condition used in place of nonfreeness
hypothesis (suffix) |
|
|
No |
spimv 2388 |
| vtx |
vertex |
df-vtx 28947 |
(Vtx‘𝐺) |
Yes |
vtxval0 28988, opvtxov 28954 |
| 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 2131, spnfw 1979 |
| wrd | word |
df-word 14421 | Word 𝑆 | Yes |
iswrdb 14427, wrdfn 14435, ffz0iswrd 14448 |
| xp | cross product (Cartesian product) |
df-xp 5625 | (𝐴 × 𝐵) | Yes |
elxp 5642, opelxpi 5656, xpundi 5688 |
| xr | eXtended reals | df-xr 11153 |
ℝ* | Yes | ressxr 11159, rexr 11161, 0xr 11162 |
| z | integers (from German "Zahlen") |
df-z 12472 | ℤ | Yes |
elz 12473, zcn 12476 |
| zn | ring of integers mod 𝑁 | df-zn 21413 |
(ℤ/nℤ‘𝑁) | Yes |
znval 21442, zncrng 21451, znhash 21465 |
| zring | ring of integers | df-zring 21354 |
ℤring | Yes | zringbas 21360, zringcrng 21355
|
| 0, z |
slashed zero (empty set) | df-nul 4285 |
∅ | Yes |
n0i 4291, vn0 4296; snnz 4728, prnz 4729 |
(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.) |
