| Description:
The following gives conventions used in the Metamath Proof Explorer
(MPE, set.mm) regarding labels.
For other conventions, see conventions 30382 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 3050"rgen.1 $e |- ( x e. A -> ph ) $."
or letters corresponding to the (main) class variable used in the
hypothesis, e.g., for mdet0 22522: "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 2660 and stirling 46211.
- 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 1840, and the restricted quantifier version of Theorem 21 from
Section 19 of [Margaris] p. 90 is labeled r19.21 3228.
- 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... 15790. 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 3901, and thus its syntax label fragment is "dif". Similarly, the
subclass relation 𝐴 ⊆ 𝐵 has syntax label fragment "ss"
because it is defined in df-ss 3915. 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 4085. There are many other syntax label fragments, e.g.,
singleton construct {𝐴} has syntax label fragment "sn" (because it
is defined in df-sn 4576), and the pair construct {𝐴, 𝐵} has
fragment "pr" ( from df-pr 4578). 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 11019) and "re" represents real numbers ℝ (Definition df-r 11023).
The empty set ∅ often uses fragment 0, even though it is defined
in df-nul 4283. The syntax construct (𝐴 + 𝐵) usually uses the
fragment "add" (which is consistent with df-add 11024), 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 12262.
- 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 16061 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 15979) we have value cosval 16034 and
closure coscl 16038.
- 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 30385 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 1940 versus 19.21 2212. This
often permits to prove the result using fewer axioms, and/or to
eliminate a nonfreeness hypothesis (such as Ⅎ𝑥𝜑 in 19.21 2212).
If no constraint is put on axiom use, then the v-version can be proved
from the original theorem using nfv 1915. If two (resp. three) such
disjoint variable conditions are added, then the suffix "vv" (resp.
"vvv") is used, e.g., exlimivv 1933.
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 2573 derived from eu6 2571. 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 2411 (cbval 2400 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 3514.
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 3126 |
| abl | Abelian group | df-abl 19697 |
Abel | Yes | ablgrp 19699, zringabl 21390 |
| abs | absorption | | | No |
ressabs 17161 |
| abs | absolute value (of a complex number) |
df-abs 15145 | (abs‘𝐴) | Yes |
absval 15147, absneg 15186, abs1 15206 |
| ad | adding | |
| No | adantr 480, ad2antlr 727 |
| add | add (see "p") | df-add 11024 |
(𝐴 + 𝐵) | Yes |
addcl 11095, addcom 11306, addass 11100 |
| al | "for all" | |
∀𝑥𝜑 | No | alim 1811, alex 1827 |
| 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 11101 |
| asym | asymmetric, antisymmetric | |
| No | intasym 6066, asymref 6067, posasymb 18227 |
| ax | axiom | |
| No | ax6dgen 2133, ax1cn 11047 |
| bas, base |
base (set of an extensible structure) | df-base 17123 |
(Base‘𝑆) | Yes |
baseval 17124, ressbas 17149, cnfldbas 21297 |
| b, bi | biconditional ("iff", "if and only if")
| df-bi 207 | (𝜑 ↔ 𝜓) | Yes |
impbid 212, sspwb 5392 |
| br | binary relation | df-br 5094 |
𝐴𝑅𝐵 | Yes | brab1 5141, brun 5144 |
| c | commutes, commuted (suffix) | | |
No | biimpac 478 |
| c | contraction (suffix) | | |
No | sylc 65, syl2anc 584 |
| cbv | change bound variable | | |
No | cbvalivw 2008, cbvrex 3330 |
| cdm | codomain | |
| No | ffvelcdm 7020, focdmex 7894 |
| cl | closure | | | No |
ifclda 4510, ovrcl 7393, zaddcl 12518 |
| cn | complex numbers | df-c 11019 |
ℂ | Yes | nnsscn 12137, nncn 12140 |
| cnfld | field of complex numbers | df-cnfld 21294 |
ℂfld | Yes | cnfldbas 21297, cnfldinv 21341 |
| cntz | centralizer | df-cntz 19231 |
(Cntz‘𝑀) | Yes |
cntzfval 19234, dprdfcntz 19931 |
| cnv | converse | df-cnv 5627 |
◡𝐴 | Yes | opelcnvg 5824, f1ocnv 6780 |
| co | composition | df-co 5628 |
(𝐴 ∘ 𝐵) | Yes | cnvco 5829, fmptco 7068 |
| com | commutative | |
| No | orcom 870, bicomi 224, eqcomi 2742 |
| con | contradiction, contraposition | |
| No | condan 817, con2d 134 |
| csb | class substitution | df-csb 3847 |
⦋𝐴 / 𝑥⦌𝐵 | Yes |
csbid 3859, csbie2g 3886 |
| cyg | cyclic group | df-cyg 19792 |
CycGrp | Yes |
iscyg 19793, zringcyg 21408 |
| d | deduction form (suffix) | |
| No | idd 24, impbid 212 |
| df | (alternate) definition (prefix) | |
| No | dfrel2 6141, dffn2 6658 |
| di, distr | distributive | |
| No |
andi 1009, imdi 389, ordi 1007, difindi 4241, ndmovdistr 7541 |
| dif | class difference | df-dif 3901 |
(𝐴 ∖ 𝐵) | Yes |
difss 4085, difindi 4241 |
| div | division | df-div 11782 |
(𝐴 / 𝐵) | Yes |
divcl 11789, divval 11785, divmul 11786 |
| dm | domain | df-dm 5629 |
dom 𝐴 | Yes | dmmpt 6192, iswrddm0 14447 |
| e, eq, equ | equals (equ for setvars, eq for
classes) | df-cleq 2725 |
𝐴 = 𝐵 | Yes |
2p2e4 12262, uneqri 4105, equtr 2022 |
| edg | edge | df-edg 29028 |
(Edg‘𝐺) | Yes |
edgopval 29031, usgredgppr 29176 |
| el | element of | |
𝐴 ∈ 𝐵 | Yes |
eldif 3908, eldifsn 4737, elssuni 4889 |
| en | equinumerous | df-en |
𝐴 ≈ 𝐵 | Yes | domen 8890, enfi 9103 |
| eu | "there exists exactly one" | eu6 2571 |
∃!𝑥𝜑 | Yes | euex 2574, euabsn 4678 |
| ex | exists (i.e. is a set) | |
∈ V | No | brrelex1 5672, 0ex 5247 |
| ex, e | "there exists (at least one)" |
df-ex 1781 |
∃𝑥𝜑 | Yes | exim 1835, alex 1827 |
| exp | export | |
| No | expt 177, expcom 413 |
| f | "not free in" (suffix) | |
| No | equs45f 2461, sbf 2275 |
| f | function | df-f 6490 |
𝐹:𝐴⟶𝐵 | Yes | fssxp 6683, opelf 6689 |
| fal | false | df-fal 1554 |
⊥ | Yes | bifal 1557, falantru 1576 |
| fi | finite intersection | df-fi 9302 |
(fi‘𝐵) | Yes | fival 9303, inelfi 9309 |
| fi, fin | finite | df-fin 8879 |
Fin | Yes |
isfi 8904, snfi 8972, onfin 9131 |
| fld | field (Note: there is an alternative
definition Fld of a field, see df-fld 38052) | df-field 20649 |
Field | Yes | isfld 20657, fldidom 20688 |
| fn | function with domain | df-fn 6489 |
𝐴 Fn 𝐵 | Yes | ffn 6656, fndm 6589 |
| frgp | free group | df-frgp 19624 |
(freeGrp‘𝐼) | Yes |
frgpval 19672, frgpadd 19677 |
| fsupp | finitely supported function |
df-fsupp 9253 | 𝑅 finSupp 𝑍 | Yes |
isfsupp 9256, fdmfisuppfi 9265, fsuppco 9293 |
| fun | function | df-fun 6488 |
Fun 𝐹 | Yes | funrel 6503, ffun 6659 |
| fv | function value | df-fv 6494 |
(𝐹‘𝐴) | Yes | fvres 6847, swrdfv 14558 |
| fz | finite set of sequential integers |
df-fz 13410 |
(𝑀...𝑁) | Yes | fzval 13411, eluzfz 13421 |
| fz0 | finite set of sequential nonnegative integers |
|
(0...𝑁) | Yes | nn0fz0 13527, fz0tp 13530 |
| fzo | half-open integer range | df-fzo 13557 |
(𝑀..^𝑁) | Yes |
elfzo 13563, elfzofz 13577 |
| g | more general (suffix); eliminates "is a set"
hypotheses | |
| No | uniexg 7679 |
| gr | graph | |
| No | uhgrf 29042, isumgr 29075, usgrres1 29295 |
| grp | group | df-grp 18851 |
Grp | Yes | isgrp 18854, tgpgrp 23994 |
| gsum | group sum | df-gsum 17348 |
(𝐺 Σg 𝐹) | Yes |
gsumval 18587, gsumwrev 19280 |
| hash | size (of a set) | df-hash 14240 |
(♯‘𝐴) | Yes |
hashgval 14242, hashfz1 14255, hashcl 14265 |
| hb | hypothesis builder (prefix) | |
| No | hbxfrbi 1826, hbald 2173, hbequid 39028 |
| hm | (monoid, group, ring, ...) homomorphism |
| | No |
ismhm 18695, isghm 19129, isrhm 20398 |
| i | inference (suffix) | |
| No | eleq1i 2824, tcsni 9638 |
| i | implication (suffix) | |
| No | brwdomi 9461, infeq5i 9533 |
| id | identity | |
| No | biid 261 |
| iedg | indexed edge | df-iedg 28979 |
(iEdg‘𝐺) | Yes |
iedgval0 29020, edgiedgb 29034 |
| idm | idempotent | |
| No | anidm 564, tpidm13 4708 |
| im, imp | implication (label often omitted) |
df-im 15010 | (𝐴 → 𝐵) | Yes |
iman 401, imnan 399, impbidd 210 |
| im | (group, ring, ...) isomorphism | |
| No | isgim 19176, rimrcl 20401 |
| ima | image | df-ima 5632 |
(𝐴 “ 𝐵) | Yes | resima 5968, imaundi 6101 |
| imp | import | |
| No | biimpa 476, impcom 407 |
| in | intersection | df-in 3905 |
(𝐴 ∩ 𝐵) | Yes | elin 3914, incom 4158 |
| inf | infimum | df-inf 9334 |
inf(ℝ+, ℝ*, < ) | Yes |
fiinfcl 9394, infiso 9401 |
| is... | is (something a) ...? | |
| No | isring 20157 |
| j | joining, disjoining | |
| No | jc 161, jaoi 857 |
| l | left | |
| No | olcd 874, simpl 482 |
| map | mapping operation or set exponentiation |
df-map 8758 | (𝐴 ↑m 𝐵) | Yes |
mapvalg 8766, elmapex 8778 |
| mat | matrix | df-mat 22324 |
(𝑁 Mat 𝑅) | Yes |
matval 22327, matring 22359 |
| mdet | determinant (of a square matrix) |
df-mdet 22501 | (𝑁 maDet 𝑅) | Yes |
mdetleib 22503, mdetrlin 22518 |
| mgm | magma | df-mgm 18550 |
Magma | Yes |
mgmidmo 18570, mgmlrid 18577, ismgm 18551 |
| mgp | multiplicative group | df-mgp 20061 |
(mulGrp‘𝑅) | Yes |
mgpress 20070, ringmgp 20159 |
| mnd | monoid | df-mnd 18645 |
Mnd | Yes | mndass 18653, mndodcong 19456 |
| mo | "there exists at most one" | df-mo 2537 |
∃*𝑥𝜑 | Yes | eumo 2575, moim 2541 |
| mp | modus ponens | ax-mp 5 |
| No | mpd 15, mpi 20 |
| mpo | maps-to notation for an operation |
df-mpo 7357 | (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) | Yes |
mpompt 7466, resmpo 7472 |
| mpt | modus ponendo tollens | |
| No | mptnan 1769, mptxor 1770 |
| mpt | maps-to notation for a function |
df-mpt 5175 | (𝑥 ∈ 𝐴 ↦ 𝐵) | Yes |
fconstmpt 5681, resmpt 5990 |
| mul | multiplication (see "t") | df-mul 11025 |
(𝐴 · 𝐵) | Yes |
mulcl 11097, divmul 11786, mulcom 11099, mulass 11101 |
| n, not | not | |
¬ 𝜑 | Yes |
nan 829, notnotr 130 |
| ne | not equal | df-ne | 𝐴 ≠ 𝐵 |
Yes | exmidne 2939, neeqtrd 2998 |
| nel | not element of | df-nel | 𝐴 ∉ 𝐵
|
Yes | neli 3035, nnel 3043 |
| ne0 | not equal to zero (see n0) | |
≠ 0 | No |
negne0d 11477, ine0 11559, gt0ne0 11589 |
| nf | "not free in" (prefix) | df-nf 1785 |
Ⅎ𝑥𝜑 | Yes | nfnd 1859 |
| ngp | normed group | df-ngp 24499 |
NrmGrp | Yes | isngp 24512, ngptps 24518 |
| nm | norm (on a group or ring) | df-nm 24498 |
(norm‘𝑊) | Yes |
nmval 24505, subgnm 24549 |
| nn | positive integers | df-nn 12133 |
ℕ | Yes | nnsscn 12137, nncn 12140 |
| nn0 | nonnegative integers | df-n0 12389 |
ℕ0 | Yes | nnnn0 12395, nn0cn 12398 |
| n0 | not the empty set (see ne0) | |
≠ ∅ | No | n0i 4289, vn0 4294, ssn0 4353 |
| OLD | old, obsolete (to be removed soon) | |
| No | 19.43OLD 1884 |
| on | ordinal number | df-on 6315 |
𝐴 ∈ On | Yes |
elon 6320, 1on 8403 onelon 6336 |
| op | ordered pair | df-op 4582 |
⟨𝐴, 𝐵⟩ | Yes | dfopif 4821, opth 5419 |
| or | or | df-or 848 |
(𝜑 ∨ 𝜓) | Yes |
orcom 870, anor 984 |
| ot | ordered triple | df-ot 4584 |
⟨𝐴, 𝐵, 𝐶⟩ | Yes |
euotd 5456, fnotovb 7404 |
| ov | operation value | df-ov 7355 |
(𝐴𝐹𝐵) | Yes
| fnotovb 7404, fnovrn 7527 |
| p | plus (see "add"), for all-constant
theorems | df-add 11024 |
(3 + 2) = 5 | Yes |
3p2e5 12278 |
| pfx | prefix | df-pfx 14581 |
(𝑊 prefix 𝐿) | Yes |
pfxlen 14593, ccatpfx 14610 |
| pm | Principia Mathematica | |
| No | pm2.27 42 |
| pm | partial mapping (operation) | df-pm 8759 |
(𝐴 ↑pm 𝐵) | Yes | elpmi 8776, pmsspw 8807 |
| pr | pair | df-pr 4578 |
{𝐴, 𝐵} | Yes |
elpr 4600, prcom 4684, prid1g 4712, prnz 4729 |
| prm, prime | prime (number) | df-prm 16585 |
ℙ | Yes | 1nprm 16592, dvdsprime 16600 |
| pss | proper subset | df-pss 3918 |
𝐴 ⊊ 𝐵 | Yes | pssss 4047, sspsstri 4054 |
| q | rational numbers ("quotients") | df-q 12849 |
ℚ | Yes | elq 12850 |
| r | reversed (suffix) | |
| No | pm4.71r 558, caovdir 7586 |
| r | right | |
| No | orcd 873, simprl 770 |
| rab | restricted class abstraction |
df-rab 3397 | {𝑥 ∈ 𝐴 ∣ 𝜑} | Yes |
rabswap 3405, df-oprab 7356 |
| ral | restricted universal quantification |
df-ral 3049 | ∀𝑥 ∈ 𝐴𝜑 | Yes |
ralnex 3059, ralrnmpo 7491 |
| rcl | reverse closure | |
| No | ndmfvrcl 6861, nnarcl 8537 |
| re | real numbers | df-r 11023 |
ℝ | Yes | recn 11103, 0re 11121 |
| rel | relation | df-rel 5626 | Rel 𝐴 |
Yes | brrelex1 5672, relmpoopab 8030 |
| res | restriction | df-res 5631 |
(𝐴 ↾ 𝐵) | Yes |
opelres 5938, f1ores 6782 |
| reu | restricted existential uniqueness |
df-reu 3348 | ∃!𝑥 ∈ 𝐴𝜑 | Yes |
nfreud 3393, reurex 3351 |
| rex | restricted existential quantification |
df-rex 3058 | ∃𝑥 ∈ 𝐴𝜑 | Yes |
rexnal 3085, rexrnmpo 7492 |
| rmo | restricted "at most one" |
df-rmo 3347 | ∃*𝑥 ∈ 𝐴𝜑 | Yes |
nfrmod 3392, nrexrmo 3366 |
| rn | range | df-rn 5630 | ran 𝐴 |
Yes | elrng 5835, rncnvcnv 5878 |
| ring | (unital) ring | df-ring 20155 |
Ring | Yes |
ringidval 20103, isring 20157, ringgrp 20158 |
| rng | non-unital ring | df-rng 20073 |
Rng | Yes |
isrng 20074, rngabl 20075, rnglz 20085 |
| rot | rotation | |
| No | 3anrot 1099, 3orrot 1091 |
| s | eliminates need for syllogism (suffix) |
| | No | ancoms 458 |
| sb | (proper) substitution (of a set) |
df-sb 2068 | [𝑦 / 𝑥]𝜑 | Yes |
spsbe 2087, sbimi 2079 |
| sbc | (proper) substitution of a class |
df-sbc 3738 | [𝐴 / 𝑥]𝜑 | Yes |
sbc2or 3746, sbcth 3752 |
| sca | scalar | df-sca 17179 |
(Scalar‘𝐻) | Yes |
resssca 17249, mgpsca 20066 |
| simp | simple, simplification | |
| No | simpl 482, simp3r3 1284 |
| sn | singleton | df-sn 4576 |
{𝐴} | Yes | eldifsn 4737 |
| sp | specialization | |
| No | spsbe 2087, spei 2396 |
| ss | subset | df-ss 3915 |
𝐴 ⊆ 𝐵 | Yes | difss 4085 |
| struct | structure | df-struct 17060 |
Struct | Yes | brstruct 17061, structfn 17069 |
| sub | subtract | df-sub 11353 |
(𝐴 − 𝐵) | Yes |
subval 11358, subaddi 11455 |
| sup | supremum | df-sup 9333 |
sup(𝐴, 𝐵, < ) | Yes |
fisupcl 9361, supmo 9343 |
| supp | support (of a function) | df-supp 8097 |
(𝐹 supp 𝑍) | Yes |
ressuppfi 9286, mptsuppd 8123 |
| swap | swap (two parts within a theorem) |
| | No | rabswap 3405, 2reuswap 3701 |
| syl | syllogism | syl 17 |
| No | 3syl 18 |
| sym | symmetric | |
| No | df-symdif 4202, cnvsym 6065 |
| symg | symmetric group | df-symg 19284 |
(SymGrp‘𝐴) | Yes |
symghash 19292, pgrpsubgsymg 19323 |
| t |
times (see "mul"), for all-constant theorems |
df-mul 11025 |
(3 · 2) = 6 | Yes |
3t2e6 12293 |
| th, t |
theorem |
|
|
No |
nfth 1802, sbcth 3752, weth 10393, ancomst 464 |
| tp | triple | df-tp 4580 |
{𝐴, 𝐵, 𝐶} | Yes |
eltpi 4640, tpeq1 4694 |
| tr | transitive | |
| No | bitrd 279, biantr 805 |
| tru, t |
true, truth |
df-tru 1544 |
⊤ |
Yes |
bitru 1550, truanfal 1575, biimt 360 |
| un | union | df-un 3903 |
(𝐴 ∪ 𝐵) | Yes |
uneqri 4105, uncom 4107 |
| unit | unit (in a ring) |
df-unit 20278 | (Unit‘𝑅) | Yes |
isunit 20293, nzrunit 20441 |
| v |
setvar (especially for specializations of
theorems when a class is replaced by a setvar variable) |
|
x |
Yes |
cv 1540, vex 3441, velpw 4554, vtoclf 3518 |
| v |
disjoint variable condition used in place of nonfreeness
hypothesis (suffix) |
|
|
No |
spimv 2392 |
| vtx |
vertex |
df-vtx 28978 |
(Vtx‘𝐺) |
Yes |
vtxval0 29019, opvtxov 28985 |
| vv |
two disjoint variable conditions used in place of nonfreeness
hypotheses (suffix) |
|
|
No |
19.23vv 1944 |
| w | weak (version of a theorem) (suffix) | |
| No | ax11w 2135, spnfw 1980 |
| wrd | word |
df-word 14423 | Word 𝑆 | Yes |
iswrdb 14429, wrdfn 14437, ffz0iswrd 14450 |
| xp | cross product (Cartesian product) |
df-xp 5625 | (𝐴 × 𝐵) | Yes |
elxp 5642, opelxpi 5656, xpundi 5688 |
| xr | eXtended reals | df-xr 11157 |
ℝ* | Yes | ressxr 11163, rexr 11165, 0xr 11166 |
| z | integers (from German "Zahlen") |
df-z 12476 | ℤ | Yes |
elz 12477, zcn 12480 |
| zn | ring of integers mod 𝑁 | df-zn 21445 |
(ℤ/nℤ‘𝑁) | Yes |
znval 21474, zncrng 21483, znhash 21497 |
| zring | ring of integers | df-zring 21386 |
ℤring | Yes | zringbas 21392, zringcrng 21387
|
| 0, z |
slashed zero (empty set) | df-nul 4283 |
∅ | Yes |
n0i 4289, vn0 4294; 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.) |
