| Description:
The following gives conventions used in the Metamath Proof Explorer
(MPE, set.mm) regarding labels.
For other conventions, see conventions 28177 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 3147"rgen.1 $e |- ( x e. A -> ph ) $."
or letters corresponding to the (main) class variable used in the
hypothesis, e.g. for mdet0 21210: "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 2747 and stirling 42448.
- 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 1838, and the restricted quantifier version of Theorem 21 from
Section 19 of [Margaris] p. 90 is labeled r19.21 3214.
- 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... 15232. 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 3932, and thus its syntax label fragment is "dif". Similarly, the
subclass relation 𝐴 ⊆ 𝐵 has syntax label fragment "ss"
because it is defined in df-ss 3945. 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 4101. There are many other syntax label fragments, e.g.,
singleton construct {𝐴} has syntax label fragment "sn" (because it
is defined in df-sn 4561), and the pair construct {𝐴, 𝐵} has
fragment "pr" ( from df-pr 4563). 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 4712. An "n" is often used for negation (¬), e.g.,
nan 827.
- 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 10536) and "re" represents real numbers ℝ ( definition df-r 10540).
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 10541), 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 11766.
- 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 15498 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 labeld "NAMEcl".
E.g., for cosine (df-cos 15419) we have value cosval 15471 and closure
coscl 15475.
- 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 28180 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 2206. This
often permits to prove the result using fewer axioms, and/or to
eliminate a nonfreeness hypothesis (such as Ⅎ𝑥𝜑 in 19.21 2206).
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 2660 derived from eu6 2658. 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 5335.
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 2429 (cbval 2415 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 3552.
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 586), commutes
(e.g., biimpac 481)
- 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 479, rexlimiva 3280 |
| abl | Abelian group | df-abl 18904 |
Abel | Yes | ablgrp 18906, zringabl 20616 |
| abs | absorption | | | No |
ressabs 16558 |
| abs | absolute value (of a complex number) |
df-abs 14590 | (abs‘𝐴) | Yes |
absval 14592, absneg 14632, abs1 14652 |
| ad | adding | |
| No | adantr 483, ad2antlr 725 |
| add | add (see "p") | df-add 10541 |
(𝐴 + 𝐵) | Yes |
addcl 10612, addcom 10819, addass 10617 |
| al | "for all" | |
∀𝑥𝜑 | No | alim 1810, alex 1825 |
| ALT | alternative/less preferred (suffix) | |
| No | idALT 23 |
| an | and | df-an 399 |
(𝜑 ∧ 𝜓) | Yes |
anor 979, iman 404, imnan 402 |
| ant | antecedent | |
| No | adantr 483 |
| ass | associative | |
| No | biass 388, orass 918, mulass 10618 |
| asym | asymmetric, antisymmetric | |
| No | intasym 5968, asymref 5969, posasymb 17557 |
| ax | axiom | |
| No | ax6dgen 2131, ax1cn 10564 |
| bas, base |
base (set of an extensible structure) | df-base 16484 |
(Base‘𝑆) | Yes |
baseval 16537, ressbas 16549, cnfldbas 20544 |
| b, bi | biconditional ("iff", "if and only if")
| df-bi 209 | (𝜑 ↔ 𝜓) | Yes |
impbid 214, sspwb 5335 |
| br | binary relation | df-br 5060 |
𝐴𝑅𝐵 | Yes | brab1 5107, brun 5110 |
| cbv | change bound variable | | |
No | cbvalivw 2013, cbvrex 3443 |
| cl | closure | | | No |
ifclda 4494, ovrcl 7190, zaddcl 12016 |
| cn | complex numbers | df-c 10536 |
ℂ | Yes | nnsscn 11636, nncn 11639 |
| cnfld | field of complex numbers | df-cnfld 20541 |
ℂfld | Yes | cnfldbas 20544, cnfldinv 20571 |
| cntz | centralizer | df-cntz 18442 |
(Cntz‘𝑀) | Yes |
cntzfval 18445, dprdfcntz 19132 |
| cnv | converse | df-cnv 5556 |
◡𝐴 | Yes | opelcnvg 5744, f1ocnv 6620 |
| co | composition | df-co 5557 |
(𝐴 ∘ 𝐵) | Yes | cnvco 5749, fmptco 6884 |
| com | commutative | |
| No | orcom 866, bicomi 226, eqcomi 2829 |
| con | contradiction, contraposition | |
| No | condan 816, con2d 136 |
| csb | class substitution | df-csb 3877 |
⦋𝐴 / 𝑥⦌𝐵 | Yes |
csbid 3889, csbie2g 3916 |
| cyg | cyclic group | df-cyg 18992 |
CycGrp | Yes |
iscyg 18993, zringcyg 20633 |
| d | deduction form (suffix) | |
| No | idd 24, impbid 214 |
| df | (alternate) definition (prefix) | |
| No | dfrel2 6039, dffn2 6509 |
| di, distr | distributive | |
| No |
andi 1004, imdi 393, ordi 1002, difindi 4251, ndmovdistr 7330 |
| dif | class difference | df-dif 3932 |
(𝐴 ∖ 𝐵) | Yes |
difss 4101, difindi 4251 |
| div | division | df-div 11291 |
(𝐴 / 𝐵) | Yes |
divcl 11297, divval 11293, divmul 11294 |
| dm | domain | df-dm 5558 |
dom 𝐴 | Yes | dmmpt 6087, iswrddm0 13883 |
| e, eq, equ | equals (equ for setvars, eq for
classes) | df-cleq 2813 |
𝐴 = 𝐵 | Yes |
2p2e4 11766, uneqri 4120, equtr 2027 |
| edg | edge | df-edg 26831 |
(Edg‘𝐺) | Yes |
edgopval 26834, usgredgppr 26976 |
| el | element of | |
𝐴 ∈ 𝐵 | Yes |
eldif 3939, eldifsn 4712, elssuni 4861 |
| en | equinumerous | df-en |
𝐴 ≈ 𝐵 | Yes | domen 8515, enfi 8727 |
| eu | "there exists exactly one" | eu6 2658 |
∃!𝑥𝜑 | Yes | euex 2661, euabsn 4655 |
| ex | exists (i.e. is a set) | |
∈ V | No | brrelex1 5598, 0ex 5204 |
| ex, e | "there exists (at least one)" |
df-ex 1780 |
∃𝑥𝜑 | Yes | exim 1833, alex 1825 |
| exp | export | |
| No | expt 179, expcom 416 |
| f | "not free in" (suffix) | |
| No | equs45f 2481, sbf 2270 |
| f | function | df-f 6352 |
𝐹:𝐴⟶𝐵 | Yes | fssxp 6527, opelf 6532 |
| fal | false | df-fal 1549 |
⊥ | Yes | bifal 1552, falantru 1571 |
| fi | finite intersection | df-fi 8868 |
(fi‘𝐵) | Yes | fival 8869, inelfi 8875 |
| fi, fin | finite | df-fin 8506 |
Fin | Yes |
isfi 8526, snfi 8587, onfin 8702 |
| fld | field (Note: there is an alternative
definition Fld of a field, see df-fld 35303) | df-field 19500 |
Field | Yes | isfld 19506, fldidom 20073 |
| fn | function with domain | df-fn 6351 |
𝐴 Fn 𝐵 | Yes | ffn 6507, fndm 6448 |
| frgp | free group | df-frgp 18831 |
(freeGrp‘𝐼) | Yes |
frgpval 18879, frgpadd 18884 |
| fsupp | finitely supported function |
df-fsupp 8827 | 𝑅 finSupp 𝑍 | Yes |
isfsupp 8830, fdmfisuppfi 8835, fsuppco 8858 |
| fun | function | df-fun 6350 |
Fun 𝐹 | Yes | funrel 6365, ffun 6510 |
| fv | function value | df-fv 6356 |
(𝐹‘𝐴) | Yes | fvres 6682, swrdfv 14005 |
| fz | finite set of sequential integers |
df-fz 12890 |
(𝑀...𝑁) | Yes | fzval 12891, eluzfz 12900 |
| fz0 | finite set of sequential nonnegative integers |
|
(0...𝑁) | Yes | nn0fz0 13002, fz0tp 13005 |
| fzo | half-open integer range | df-fzo 13031 |
(𝑀..^𝑁) | Yes |
elfzo 13037, elfzofz 13050 |
| g | more general (suffix); eliminates "is a set"
hypotheses | |
| No | uniexg 7459 |
| gr | graph | |
| No | uhgrf 26845, isumgr 26878, usgrres1 27095 |
| grp | group | df-grp 18101 |
Grp | Yes | isgrp 18104, tgpgrp 22681 |
| gsum | group sum | df-gsum 16711 |
(𝐺 Σg 𝐹) | Yes |
gsumval 17882, gsumwrev 18489 |
| hash | size (of a set) | df-hash 13688 |
(♯‘𝐴) | Yes |
hashgval 13690, hashfz1 13703, hashcl 13714 |
| hb | hypothesis builder (prefix) | |
| No | hbxfrbi 1824, hbald 2174, hbequid 36078 |
| hm | (monoid, group, ring) homomorphism | |
| No | ismhm 17953, isghm 18353, isrhm 19468 |
| i | inference (suffix) | |
| No | eleq1i 2902, tcsni 9178 |
| i | implication (suffix) | |
| No | brwdomi 9025, infeq5i 9092 |
| id | identity | |
| No | biid 263 |
| iedg | indexed edge | df-iedg 26782 |
(iEdg‘𝐺) | Yes |
iedgval0 26823, edgiedgb 26837 |
| idm | idempotent | |
| No | anidm 567, tpidm13 4685 |
| im, imp | implication (label often omitted) |
df-im 14455 | (𝐴 → 𝐵) | Yes |
iman 404, imnan 402, impbidd 212 |
| ima | image | df-ima 5561 |
(𝐴 “ 𝐵) | Yes | resima 5880, imaundi 6001 |
| imp | import | |
| No | biimpa 479, impcom 410 |
| in | intersection | df-in 3936 |
(𝐴 ∩ 𝐵) | Yes | elin 4162, incom 4171 |
| inf | infimum | df-inf 8900 |
inf(ℝ+, ℝ*, < ) | Yes |
fiinfcl 8958, infiso 8965 |
| is... | is (something a) ...? | |
| No | isring 19296 |
| j | joining, disjoining | |
| No | jc 163, jaoi 853 |
| l | left | |
| No | olcd 870, simpl 485 |
| map | mapping operation or set exponentiation |
df-map 8401 | (𝐴 ↑m 𝐵) | Yes |
mapvalg 8409, elmapex 8420 |
| mat | matrix | df-mat 21012 |
(𝑁 Mat 𝑅) | Yes |
matval 21015, matring 21047 |
| mdet | determinant (of a square matrix) |
df-mdet 21189 | (𝑁 maDet 𝑅) | Yes |
mdetleib 21191, mdetrlin 21206 |
| mgm | magma | df-mgm 17847 |
Magma | Yes |
mgmidmo 17865, mgmlrid 17872, ismgm 17848 |
| mgp | multiplicative group | df-mgp 19235 |
(mulGrp‘𝑅) | Yes |
mgpress 19245, ringmgp 19298 |
| mnd | monoid | df-mnd 17907 |
Mnd | Yes | mndass 17915, mndodcong 18665 |
| mo | "there exists at most one" | df-mo 2621 |
∃*𝑥𝜑 | Yes | eumo 2662, moim 2625 |
| mp | modus ponens | ax-mp 5 |
| No | mpd 15, mpi 20 |
| mpo | maps-to notation for an operation |
df-mpo 7154 | (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) | Yes |
mpompt 7259, resmpo 7265 |
| mpt | modus ponendo tollens | |
| No | mptnan 1768, mptxor 1769 |
| mpt | maps-to notation for a function |
df-mpt 5140 | (𝑥 ∈ 𝐴 ↦ 𝐵) | Yes |
fconstmpt 5607, resmpt 5898 |
| mpt2 | maps-to notation for an operation (deprecated).
We are in the process of replacing mpt2 with mpo in labels. |
df-mpo 7154 | (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) | Yes |
mpompt 7259, resmpo 7265 |
| mul | multiplication (see "t") | df-mul 10542 |
(𝐴 · 𝐵) | Yes |
mulcl 10614, divmul 11294, mulcom 10616, mulass 10618 |
| n, not | not | |
¬ 𝜑 | Yes |
nan 827, notnotr 132 |
| ne | not equal | df-ne | 𝐴 ≠ 𝐵 |
Yes | exmidne 3025, neeqtrd 3084 |
| nel | not element of | df-nel | 𝐴 ∉ 𝐵
|
Yes | neli 3124, nnel 3131 |
| ne0 | not equal to zero (see n0) | |
≠ 0 | No |
negne0d 10988, ine0 11068, gt0ne0 11098 |
| nf | "not free in" (prefix) | |
| No | nfnd 1857 |
| ngp | normed group | df-ngp 23188 |
NrmGrp | Yes | isngp 23200, ngptps 23206 |
| nm | norm (on a group or ring) | df-nm 23187 |
(norm‘𝑊) | Yes |
nmval 23194, subgnm 23237 |
| nn | positive integers | df-nn 11632 |
ℕ | Yes | nnsscn 11636, nncn 11639 |
| nn0 | nonnegative integers | df-n0 11892 |
ℕ0 | Yes | nnnn0 11898, nn0cn 11901 |
| n0 | not the empty set (see ne0) | |
≠ ∅ | No | n0i 4292, vn0 4297, ssn0 4347 |
| OLD | old, obsolete (to be removed soon) | |
| No | 19.43OLD 1883 |
| on | ordinal number | df-on 6188 |
𝐴 ∈ On | Yes |
elon 6193, 1on 8102 onelon 6209 |
| op | ordered pair | df-op 4567 |
⟨𝐴, 𝐵⟩ | Yes | dfopif 4793, opth 5361 |
| or | or | df-or 844 |
(𝜑 ∨ 𝜓) | Yes |
orcom 866, anor 979 |
| ot | ordered triple | df-ot 4569 |
⟨𝐴, 𝐵, 𝐶⟩ | Yes |
euotd 5396, fnotovb 7199 |
| ov | operation value | df-ov 7152 |
(𝐴𝐹𝐵) | Yes
| fnotovb 7199, fnovrn 7316 |
| p | plus (see "add"), for all-constant
theorems | df-add 10541 |
(3 + 2) = 5 | Yes |
3p2e5 11782 |
| pfx | prefix | df-pfx 14028 |
(𝑊 prefix 𝐿) | Yes |
pfxlen 14040, ccatpfx 14058 |
| pm | Principia Mathematica | |
| No | pm2.27 42 |
| pm | partial mapping (operation) | df-pm 8402 |
(𝐴 ↑pm 𝐵) | Yes | elpmi 8418, pmsspw 8434 |
| pr | pair | df-pr 4563 |
{𝐴, 𝐵} | Yes |
elpr 4583, prcom 4661, prid1g 4689, prnz 4705 |
| prm, prime | prime (number) | df-prm 16011 |
ℙ | Yes | 1nprm 16018, dvdsprime 16026 |
| pss | proper subset | df-pss 3947 |
𝐴 ⊊ 𝐵 | Yes | pssss 4065, sspsstri 4072 |
| q | rational numbers ("quotients") | df-q 12343 |
ℚ | Yes | elq 12344 |
| r | right | |
| No | orcd 869, simprl 769 |
| rab | restricted class abstraction |
df-rab 3146 | {𝑥 ∈ 𝐴 ∣ 𝜑} | Yes |
rabswap 3485, df-oprab 7153 |
| ral | restricted universal quantification |
df-ral 3142 | ∀𝑥 ∈ 𝐴𝜑 | Yes |
ralnex 3235, ralrnmpo 7282 |
| rcl | reverse closure | |
| No | ndmfvrcl 6694, nnarcl 8235 |
| re | real numbers | df-r 10540 |
ℝ | Yes | recn 10620, 0re 10636 |
| rel | relation | df-rel 5555 | Rel 𝐴 |
Yes | brrelex1 5598, relmpoopab 7782 |
| res | restriction | df-res 5560 |
(𝐴 ↾ 𝐵) | Yes |
opelres 5852, f1ores 6622 |
| reu | restricted existential uniqueness |
df-reu 3144 | ∃!𝑥 ∈ 𝐴𝜑 | Yes |
nfreud 3371, reurex 3428 |
| rex | restricted existential quantification |
df-rex 3143 | ∃𝑥 ∈ 𝐴𝜑 | Yes |
rexnal 3237, rexrnmpo 7283 |
| rmo | restricted "at most one" |
df-rmo 3145 | ∃*𝑥 ∈ 𝐴𝜑 | Yes |
nfrmod 3372, nrexrmo 3432 |
| rn | range | df-rn 5559 | ran 𝐴 |
Yes | elrng 5755, rncnvcnv 5797 |
| rng | (unital) ring | df-ring 19294 |
Ring | Yes |
ringidval 19248, isring 19296, ringgrp 19297 |
| rot | rotation | |
| No | 3anrot 1095, 3orrot 1087 |
| s | eliminates need for syllogism (suffix) |
| | No | ancoms 461 |
| sb | (proper) substitution (of a set) |
df-sb 2069 | [𝑦 / 𝑥]𝜑 | Yes |
spsbe 2087, sbimi 2078 |
| sbc | (proper) substitution of a class |
df-sbc 3769 | [𝐴 / 𝑥]𝜑 | Yes |
sbc2or 3777, sbcth 3783 |
| sca | scalar | df-sca 16576 |
(Scalar‘𝐻) | Yes |
resssca 16645, mgpsca 19241 |
| simp | simple, simplification | |
| No | simpl 485, simp3r3 1278 |
| sn | singleton | df-sn 4561 |
{𝐴} | Yes | eldifsn 4712 |
| sp | specialization | |
| No | spsbe 2087, spei 2411 |
| ss | subset | df-ss 3945 |
𝐴 ⊆ 𝐵 | Yes | difss 4101 |
| struct | structure | df-struct 16480 |
Struct | Yes | brstruct 16487, structfn 16495 |
| sub | subtract | df-sub 10865 |
(𝐴 − 𝐵) | Yes |
subval 10870, subaddi 10966 |
| sup | supremum | df-sup 8899 |
sup(𝐴, 𝐵, < ) | Yes |
fisupcl 8926, supmo 8909 |
| supp | support (of a function) | df-supp 7824 |
(𝐹 supp 𝑍) | Yes |
ressuppfi 8852, mptsuppd 7846 |
| swap | swap (two parts within a theorem) |
| | No | rabswap 3485, 2reuswap 3733 |
| syl | syllogism | syl 17 |
| No | 3syl 18 |
| sym | symmetric | |
| No | df-symdif 4212, cnvsym 5967 |
| symg | symmetric group | df-symg 18491 |
(SymGrp‘𝐴) | Yes |
symghash 18501, pgrpsubgsymg 18532 |
| t |
times (see "mul"), for all-constant theorems |
df-mul 10542 |
(3 · 2) = 6 | Yes |
3t2e6 11797 |
| th, t |
theorem |
|
|
No |
nfth 1801, sbcth 3783, weth 9910, ancomst 467 |
| tp | triple | df-tp 4565 |
{𝐴, 𝐵, 𝐶} | Yes |
eltpi 4618, tpeq1 4671 |
| tr | transitive | |
| No | bitrd 281, biantr 804 |
| tru, t |
true, truth |
df-tru 1539 |
⊤ |
Yes |
bitru 1545, truanfal 1570, biimt 363 |
| un | union | df-un 3934 |
(𝐴 ∪ 𝐵) | Yes |
uneqri 4120, uncom 4122 |
| unit | unit (in a ring) |
df-unit 19387 | (Unit‘𝑅) | Yes |
isunit 19402, nzrunit 20035 |
| v |
setvar (especially for specializations of
theorems when a class is replaced by a setvar variable) |
|
x |
Yes |
cv 1535, vex 3494, velpw 4537, vtoclf 3555 |
| v |
disjoint variable condition used in place of nonfreeness
hypothesis (suffix) |
|
|
No |
spimv 2407 |
| vtx |
vertex |
df-vtx 26781 |
(Vtx‘𝐺) |
Yes |
vtxval0 26822, opvtxov 26788 |
| 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 2133, spnfw 1983 |
| wrd | word |
df-word 13859 | Word 𝑆 | Yes |
iswrdb 13864, wrdfn 13872, ffz0iswrd 13886 |
| xp | cross product (Cartesian product) |
df-xp 5554 | (𝐴 × 𝐵) | Yes |
elxp 5571, opelxpi 5585, xpundi 5613 |
| xr | eXtended reals | df-xr 10672 |
ℝ* | Yes | ressxr 10678, rexr 10680, 0xr 10681 |
| z | integers (from German "Zahlen") |
df-z 11976 | ℤ | Yes |
elz 11977, zcn 11980 |
| zn | ring of integers mod 𝑁 | df-zn 20649 |
(ℤ/nℤ‘𝑁) | Yes |
znval 20677, zncrng 20686, znhash 20700 |
| zring | ring of integers | df-zring 20613 |
ℤring | Yes | zringbas 20618, zringcrng 20614
|
| 0, z |
slashed zero (empty set) | df-nul 4285 |
∅ | Yes |
n0i 4292, vn0 4297; snnz 4704, prnz 4705 |
(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.) |
