| Description:
The following gives conventions used in the Metamath Proof Explorer
(MPE, set.mm) regarding labels.
For other conventions, see conventions 30495 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 3056"rgen.1 $e |- ( x e. A -> ph ) $."
or letters corresponding to the (main) class variable used in the
hypothesis, e.g., for mdet0 22596: "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 2667 and stirling 46539.
- 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 1846, and the restricted quantifier version of Theorem 21 from
Section 19 of [Margaris] p. 90 is labeled r19.21 3235.
- 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... 15844. 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 3893, and thus its syntax label fragment is "dif". Similarly, the
subclass relation 𝐴 ⊆ 𝐵 has syntax label fragment "ss"
because it is defined in df-ss 3907. 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 4073. There are many other syntax label fragments, e.g.,
singleton construct {𝐴} has syntax label fragment "sn" (because it
is defined in df-sn 4563), and the pair construct {𝐴, 𝐵} has
fragment "pr" ( from df-pr 4565). 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 4726. An "n" is often used for negation (¬), e.g.,
nan 835.
- 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 11042) and "re" represents real numbers ℝ (Definition df-r 11046).
The empty set ∅ often uses fragment 0, even though it is defined
in df-nul 4269. The syntax construct (𝐴 + 𝐵) usually uses the
fragment "add" (which is consistent with df-add 11047), 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 12309.
- 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 16115 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 16033) we have value cosval 16088 and
closure coscl 16092.
- 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 30498 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 1946 versus 19.21 2219. This
often permits to prove the result using fewer axioms, and/or to
eliminate a nonfreeness hypothesis (such as Ⅎ𝑥𝜑 in 19.21 2219).
If no constraint is put on axiom use, then the v-version can be proved
from the original theorem using nfv 1921. If two (resp. three) such
disjoint variable conditions are added, then the suffix "vv" (resp.
"vvv") is used, e.g., exlimivv 1939.
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 2580 derived from eu6 2578. 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 5395.
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 2417 (cbval 2406 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 3508.
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 590), commutes
(e.g., biimpac 479)
- 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 477, rexlimiva 3133 |
| abl | Abelian group | df-abl 19756 |
Abel | Yes | ablgrp 19758, zringabl 21433 |
| abs | absorption | | | No |
ressabs 17216 |
| abs | absolute value (of a complex number) |
df-abs 15196 | (abs‘𝐴) | Yes |
absval 15198, absneg 15237, abs1 15257 |
| ad | adding | |
| No | adantr 481, ad2antlr 733 |
| add | add (see "p") | df-add 11047 |
(𝐴 + 𝐵) | Yes |
addcl 11118, addcom 11330, addass 11123 |
| al | "for all" | |
∀𝑥𝜑 | No | alim 1817, alex 1833 |
| ALT | alternative/less preferred (suffix) | |
| No | idALT 23 |
| an | and | df-an 397 |
(𝜑 ∧ 𝜓) | Yes |
anor 990, iman 402, imnan 400 |
| ant | antecedent | |
| No | adantr 481 |
| ass | associative | |
| No | biass 385, orass 927, mulass 11124 |
| asym | asymmetric, antisymmetric | |
| No | intasym 6072, asymref 6073, posasymb 18283 |
| ax | axiom | |
| No | ax6dgen 2139, ax1cn 11070 |
| bas, base |
base (set of an extensible structure) | df-base 17178 |
(Base‘𝑆) | Yes |
baseval 17179, ressbas 17204, cnfldbas 21358 |
| b, bi | biconditional ("iff", "if and only if")
| df-bi 208 | (𝜑 ↔ 𝜓) | Yes |
impbid 213, sspwb 5395 |
| br | binary relation | df-br 5080 |
𝐴𝑅𝐵 | Yes | brab1 5127, brun 5130 |
| c | commutes, commuted (suffix) | | |
No | biimpac 479 |
| c | contraction (suffix) | | |
No | sylc 65, syl2anc 590 |
| cbv | change bound variable | | |
No | cbvalivw 2014, cbvrex 3328 |
| cdm | codomain | |
| No | ffvelcdm 7029, focdmex 7905 |
| cl | closure | | | No |
ifclda 4497, ovrcl 7404, zaddcl 12565 |
| cn | complex numbers | df-c 11042 |
ℂ | Yes | nnsscn 12177, nncn 12180 |
| cnfld | field of complex numbers | df-cnfld 21355 |
ℂfld | Yes | cnfldbas 21358, cnfldinv 21385 |
| cntz | centralizer | df-cntz 19290 |
(Cntz‘𝑀) | Yes |
cntzfval 19293, dprdfcntz 19990 |
| cnv | converse | df-cnv 5633 |
◡𝐴 | Yes | opelcnvg 5829, f1ocnv 6786 |
| co | composition | df-co 5634 |
(𝐴 ∘ 𝐵) | Yes | cnvco 5834, fmptco 7078 |
| com | commutative | |
| No | orcom 876, bicomi 225, eqcomi 2749 |
| con | contradiction, contraposition | |
| No | condan 823, con2d 134 |
| csb | class substitution | df-csb 3839 |
⦋𝐴 / 𝑥⦌𝐵 | Yes |
csbid 3851, csbie2g 3878 |
| cyg | cyclic group | df-cyg 19851 |
CycGrp | Yes |
iscyg 19852, zringcyg 21451 |
| d | deduction form (suffix) | |
| No | idd 24, impbid 213 |
| df | (alternate) definition (prefix) | |
| No | dfrel2 6147, dffn2 6664 |
| di, distr | distributive | |
| No |
andi 1015, imdi 390, ordi 1013, difindi 4227, ndmovdistr 7552 |
| dif | class difference | df-dif 3893 |
(𝐴 ∖ 𝐵) | Yes |
difss 4073, difindi 4227 |
| div | division | df-div 11806 |
(𝐴 / 𝐵) | Yes |
divcl 11813, divval 11809, divmul 11810 |
| dm | domain | df-dm 5635 |
dom 𝐴 | Yes | dmmpt 6198, iswrddm0 14498 |
| e, eq, equ | equals (equ for setvars, eq for
classes) | df-cleq 2732 |
𝐴 = 𝐵 | Yes |
2p2e4 12309, uneqri 4093, equtr 2028 |
| edg | edge | df-edg 29142 |
(Edg‘𝐺) | Yes |
edgopval 29145, usgredgppr 29290 |
| el | element of | |
𝐴 ∈ 𝐵 | Yes |
eldif 3900, eldifsn 4726, elssuni 4876 |
| en | equinumerous | df-en |
𝐴 ≈ 𝐵 | Yes | domen 8905, enfi 9118 |
| eu | "there exists exactly one" | eu6 2578 |
∃!𝑥𝜑 | Yes | euex 2581, euabsn 4665 |
| ex | exists (i.e. is a set) | |
∈ V | No | brrelex1 5678, 0ex 5236 |
| ex, e | "there exists (at least one)" |
df-ex 1787 |
∃𝑥𝜑 | Yes | exim 1841, alex 1833 |
| exp | export | |
| No | expt 177, expcom 414 |
| f | "not free in" (suffix) | |
| No | equs45f 2467, sbf 2282 |
| f | function | df-f 6496 |
𝐹:𝐴⟶𝐵 | Yes | fssxp 6689, opelf 6695 |
| fal | false | df-fal 1560 |
⊥ | Yes | bifal 1563, falantru 1582 |
| fi | finite intersection | df-fi 9321 |
(fi‘𝐵) | Yes | fival 9322, inelfi 9328 |
| fi, fin | finite | df-fin 8894 |
Fin | Yes |
isfi 8919, snfi 8987, onfin 9146 |
| fld | field (Note: there is an alternative
definition Fld of a field, see df-fld 38366) | df-field 20711 |
Field | Yes | isfld 20719, fldidom 20750 |
| fn | function with domain | df-fn 6495 |
𝐴 Fn 𝐵 | Yes | ffn 6662, fndm 6595 |
| frgp | free group | df-frgp 19683 |
(freeGrp‘𝐼) | Yes |
frgpval 19731, frgpadd 19736 |
| fsupp | finitely supported function |
df-fsupp 9272 | 𝑅 finSupp 𝑍 | Yes |
isfsupp 9275, fdmfisuppfi 9284, fsuppco 9312 |
| fun | function | df-fun 6494 |
Fun 𝐹 | Yes | funrel 6509, ffun 6665 |
| fv | function value | df-fv 6500 |
(𝐹‘𝐴) | Yes | fvres 6853, swrdfv 14609 |
| fz | finite set of sequential integers |
df-fz 13460 |
(𝑀...𝑁) | Yes | fzval 13461, eluzfz 13471 |
| fz0 | finite set of sequential nonnegative integers |
|
(0...𝑁) | Yes | nn0fz0 13577, fz0tp 13580 |
| fzo | half-open integer range | df-fzo 13607 |
(𝑀..^𝑁) | Yes |
elfzo 13613, elfzofz 13628 |
| g | more general (suffix); eliminates "is a set"
hypotheses | |
| No | uniexg 7690 |
| gr | graph | |
| No | uhgrf 29156, isumgr 29189, usgrres1 29409 |
| grp | group | df-grp 18910 |
Grp | Yes | isgrp 18913, tgpgrp 24068 |
| gsum | group sum | df-gsum 17403 |
(𝐺 Σg 𝐹) | Yes |
gsumval 18643, gsumwrev 19339 |
| hash | size (of a set) | df-hash 14291 |
(♯‘𝐴) | Yes |
hashgval 14293, hashfz1 14306, hashcl 14316 |
| hb | hypothesis builder (prefix) | |
| No | hbxfrbi 1832, hbald 2179, hbequid 39408 |
| hm | (monoid, group, ring, ...) homomorphism |
| | No |
ismhm 18751, isghm 19188, isrhm 20456 |
| i | inference (suffix) | |
| No | eleq1i 2831, tcsni 9660 |
| i | implication (suffix) | |
| No | brwdomi 9480, infeq5i 9555 |
| id | identity | |
| No | biid 262 |
| iedg | indexed edge | df-iedg 29093 |
(iEdg‘𝐺) | Yes |
iedgval0 29134, edgiedgb 29148 |
| idm | idempotent | |
| No | anidm 569, tpidm13 4695 |
| im, imp | implication (label often omitted) |
df-im 15061 | (𝐴 → 𝐵) | Yes |
iman 402, imnan 400, impbidd 211 |
| im | (group, ring, ...) isomorphism | |
| No | isgim 19235, rimrcl 20459 |
| ima | image | df-ima 5638 |
(𝐴 “ 𝐵) | Yes | resima 5974, imaundi 6107 |
| imp | import | |
| No | biimpa 477, impcom 408 |
| in | intersection | df-in 3897 |
(𝐴 ∩ 𝐵) | Yes | elin 3906, incom 4145 |
| inf | infimum | df-inf 9353 |
inf(ℝ+, ℝ*, < ) | Yes |
fiinfcl 9413, infiso 9420 |
| is... | is (something a) ...? | |
| No | isring 20216 |
| j | joining, disjoining | |
| No | jc 161, jaoi 863 |
| l | left | |
| No | olcd 880, simpl 483 |
| map | mapping operation or set exponentiation |
df-map 8772 | (𝐴 ↑m 𝐵) | Yes |
mapvalg 8780, elmapex 8792 |
| mat | matrix | df-mat 22398 |
(𝑁 Mat 𝑅) | Yes |
matval 22401, matring 22433 |
| mdet | determinant (of a square matrix) |
df-mdet 22575 | (𝑁 maDet 𝑅) | Yes |
mdetleib 22577, mdetrlin 22592 |
| mgm | magma | df-mgm 18606 |
Magma | Yes |
mgmidmo 18626, mgmlrid 18633, ismgm 18607 |
| mgp | multiplicative group | df-mgp 20120 |
(mulGrp‘𝑅) | Yes |
mgpress 20129, ringmgp 20218 |
| mnd | monoid | df-mnd 18701 |
Mnd | Yes | mndass 18709, mndodcong 19515 |
| mo | "there exists at most one" | df-mo 2543 |
∃*𝑥𝜑 | Yes | eumo 2582, moim 2548 |
| mp | modus ponens | ax-mp 5 |
| No | mpd 15, mpi 20 |
| mpo | maps-to notation for an operation |
df-mpo 7368 | (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) | Yes |
mpompt 7477, resmpo 7483 |
| mpt | modus ponendo tollens | |
| No | mptnan 1775, mptxor 1776 |
| mpt | maps-to notation for a function |
df-mpt 5161 | (𝑥 ∈ 𝐴 ↦ 𝐵) | Yes |
fconstmpt 5687, resmpt 5996 |
| mul | multiplication (see "t") | df-mul 11048 |
(𝐴 · 𝐵) | Yes |
mulcl 11120, divmul 11810, mulcom 11122, mulass 11124 |
| n, not | not | |
¬ 𝜑 | Yes |
nan 835, notnotr 130 |
| ne | not equal | df-ne | 𝐴 ≠ 𝐵 |
Yes | exmidne 2945, neeqtrd 3004 |
| nel | not element of | df-nel | 𝐴 ∉ 𝐵
|
Yes | neli 3041, nnel 3049 |
| ne0 | not equal to zero (see n0) | |
≠ 0 | No |
negne0d 11501, ine0 11583, gt0ne0 11613 |
| nf | "not free in" (prefix) | df-nf 1791 |
Ⅎ𝑥𝜑 | Yes | nfnd 1865 |
| ngp | normed group | df-ngp 24573 |
NrmGrp | Yes | isngp 24586, ngptps 24592 |
| nm | norm (on a group or ring) | df-nm 24572 |
(norm‘𝑊) | Yes |
nmval 24579, subgnm 24623 |
| nn | positive integers | df-nn 12173 |
ℕ | Yes | nnsscn 12177, nncn 12180 |
| nn0 | nonnegative integers | df-n0 12436 |
ℕ0 | Yes | nnnn0 12442, nn0cn 12445 |
| n0 | not the empty set (see ne0) | |
≠ ∅ | No | n0i 4275, vn0 4280, ssn0 4339 |
| OLD | old, obsolete (to be removed soon) | |
| No | 19.43OLD 1890 |
| on | ordinal number | df-on 6321 |
𝐴 ∈ On | Yes |
elon 6326, 1on 8414 onelon 6342 |
| op | ordered pair | df-op 4569 |
⟨𝐴, 𝐵⟩ | Yes | dfopif 4808, opth 5423 |
| or | or | df-or 854 |
(𝜑 ∨ 𝜓) | Yes |
orcom 876, anor 990 |
| ot | ordered triple | df-ot 4571 |
⟨𝐴, 𝐵, 𝐶⟩ | Yes |
euotd 5461, fnotovb 7415 |
| ov | operation value | df-ov 7366 |
(𝐴𝐹𝐵) | Yes
| fnotovb 7415, fnovrn 7538 |
| p | plus (see "add"), for all-constant
theorems | df-add 11047 |
(3 + 2) = 5 | Yes |
3p2e5 12325 |
| pfx | prefix | df-pfx 14632 |
(𝑊 prefix 𝐿) | Yes |
pfxlen 14644, ccatpfx 14661 |
| pm | Principia Mathematica | |
| No | pm2.27 42 |
| pm | partial mapping (operation) | df-pm 8773 |
(𝐴 ↑pm 𝐵) | Yes | elpmi 8790, pmsspw 8822 |
| pr | pair | df-pr 4565 |
{𝐴, 𝐵} | Yes |
elpr 4587, prcom 4671, prid1g 4699, prnz 4716 |
| prm, prime | prime (number) | df-prm 16639 |
ℙ | Yes | 1nprm 16646, dvdsprime 16654 |
| pss | proper subset | df-pss 3910 |
𝐴 ⊊ 𝐵 | Yes | pssss 4036, sspsstri 4043 |
| q | rational numbers ("quotients") | df-q 12897 |
ℚ | Yes | elq 12898 |
| r | reversed (suffix) | |
| No | pm4.71r 563, caovdir 7597 |
| r | right | |
| No | orcd 879, simprl 776 |
| rab | restricted class abstraction |
df-rab 3393 | {𝑥 ∈ 𝐴 ∣ 𝜑} | Yes |
rabswap 3401, df-oprab 7367 |
| ral | restricted universal quantification |
df-ral 3055 | ∀𝑥 ∈ 𝐴𝜑 | Yes |
ralnex 3066, ralrnmpo 7502 |
| rcl | reverse closure | |
| No | ndmfvrcl 6867, nnarcl 8549 |
| re | real numbers | df-r 11046 |
ℝ | Yes | recn 11126, 0re 11144 |
| rel | relation | df-rel 5632 | Rel 𝐴 |
Yes | brrelex1 5678, relmpoopab 8040 |
| res | restriction | df-res 5637 |
(𝐴 ↾ 𝐵) | Yes |
opelres 5944, f1ores 6788 |
| reu | restricted existential uniqueness |
df-reu 3346 | ∃!𝑥 ∈ 𝐴𝜑 | Yes |
nfreud 3389, reurex 3349 |
| rex | restricted existential quantification |
df-rex 3065 | ∃𝑥 ∈ 𝐴𝜑 | Yes |
rexnal 3092, rexrnmpo 7503 |
| rmo | restricted "at most one" |
df-rmo 3345 | ∃*𝑥 ∈ 𝐴𝜑 | Yes |
nfrmod 3388, nrexrmo 3364 |
| rn | range | df-rn 5636 | ran 𝐴 |
Yes | elrng 5840, rncnvcnv 5883 |
| ring | (unital) ring | df-ring 20214 |
Ring | Yes |
ringidval 20162, isring 20216, ringgrp 20217 |
| rng | non-unital ring | df-rng 20132 |
Rng | Yes |
isrng 20133, rngabl 20134, rnglz 20144 |
| rot | rotation | |
| No | 3anrot 1105, 3orrot 1097 |
| s | eliminates need for syllogism (suffix) |
| | No | ancoms 459 |
| sb | (proper) substitution (of a set) |
df-sb 2074 | [𝑦 / 𝑥]𝜑 | Yes |
spsbe 2093, sbimi 2085 |
| sbc | (proper) substitution of a class |
df-sbc 3731 | [𝐴 / 𝑥]𝜑 | Yes |
sbc2or 3739, sbcth 3745 |
| sca | scalar | df-sca 17234 |
(Scalar‘𝐻) | Yes |
resssca 17304, mgpsca 20125 |
| simp | simple, simplification | |
| No | simpl 483, simp3r3 1290 |
| sn | singleton | df-sn 4563 |
{𝐴} | Yes | eldifsn 4726 |
| sp | specialization | |
| No | spsbe 2093, spei 2402 |
| ss | subset | df-ss 3907 |
𝐴 ⊆ 𝐵 | Yes | difss 4073 |
| struct | structure | df-struct 17115 |
Struct | Yes | brstruct 17116, structfn 17124 |
| sub | subtract | df-sub 11377 |
(𝐴 − 𝐵) | Yes |
subval 11382, subaddi 11479 |
| sup | supremum | df-sup 9352 |
sup(𝐴, 𝐵, < ) | Yes |
fisupcl 9380, supmo 9362 |
| supp | support (of a function) | df-supp 8108 |
(𝐹 supp 𝑍) | Yes |
ressuppfi 9305, mptsuppd 8134 |
| swap | swap (two parts within a theorem) |
| | No | rabswap 3401, 2reuswap 3694 |
| syl | syllogism | syl 17 |
| No | 3syl 18 |
| sym | symmetric | |
| No | df-symdif 4188, cnvsym 6071 |
| symg | symmetric group | df-symg 19343 |
(SymGrp‘𝐴) | Yes |
symghash 19351, pgrpsubgsymg 19382 |
| t |
times (see "mul"), for all-constant theorems |
df-mul 11048 |
(3 · 2) = 6 | Yes |
3t2e6 12340 |
| th, t |
theorem |
|
|
No |
nfth 1808, sbcth 3745, weth 10415, ancomst 465 |
| tp | triple | df-tp 4567 |
{𝐴, 𝐵, 𝐶} | Yes |
eltpi 4627, tpeq1 4681 |
| tr | transitive | |
| No | bitrd 280, biantr 811 |
| tru, t |
true, truth |
df-tru 1550 |
⊤ |
Yes |
bitru 1556, truanfal 1581, biimt 361 |
| un | union | df-un 3895 |
(𝐴 ∪ 𝐵) | Yes |
uneqri 4093, uncom 4095 |
| unit | unit (in a ring) |
df-unit 20336 | (Unit‘𝑅) | Yes |
isunit 20351, nzrunit 20503 |
| v |
setvar (especially for specializations of
theorems when a class is replaced by a setvar variable) |
|
x |
Yes |
cv 1546, vex 3436, velpw 4541, vtoclf 3512 |
| v |
disjoint variable condition used in place of nonfreeness
hypothesis (suffix) |
|
|
No |
spimv 2398 |
| vtx |
vertex |
df-vtx 29092 |
(Vtx‘𝐺) |
Yes |
vtxval0 29133, opvtxov 29099 |
| vv |
two disjoint variable conditions used in place of nonfreeness
hypotheses (suffix) |
|
|
No |
19.23vv 1950 |
| w | weak (version of a theorem) (suffix) | |
| No | ax11w 2141, spnfw 1986 |
| wrd | word |
df-word 14474 | Word 𝑆 | Yes |
iswrdb 14480, wrdfn 14488, ffz0iswrd 14501 |
| xp | cross product (Cartesian product) |
df-xp 5631 | (𝐴 × 𝐵) | Yes |
elxp 5648, opelxpi 5662, xpundi 5694 |
| xr | eXtended reals | df-xr 11181 |
ℝ* | Yes | ressxr 11187, rexr 11189, 0xr 11190 |
| z | integers (from German "Zahlen") |
df-z 12523 | ℤ | Yes |
elz 12524, zcn 12527 |
| zn | ring of integers mod 𝑁 | df-zn 21488 |
(ℤ/nℤ‘𝑁) | Yes |
znval 21517, zncrng 21526, znhash 21540 |
| zring | ring of integers | df-zring 21429 |
ℤring | Yes | zringbas 21435, zringcrng 21430
|
| 0, z |
slashed zero (empty set) | df-nul 4269 |
∅ | Yes |
n0i 4275, vn0 4280; snnz 4715, prnz 4716 |
(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.) |
