| Description:
The following explains some of the label conventions in use
in the Metamath Proof Explorer ("set.mm").
For the general conventions, see conventions 26650.
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 2906"rgen.1 $e |- ( x e. A -> ph ) $."
or letters corresponding to the (main) class variable used in the
hypothesis, e.g. for mdet0 20231: "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 2551 and stirling 38982.
- 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 41.
- 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 1757, and the restricted quantifier version of Theorem 21 from
Section 19 of [Margaris] p. 90 is labeled r19.21 2939.
- 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... 14451. Furthermore, the underscore "_" should not be used.
- 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 3543, and thus its syntax label fragment is "dif". Similarly, the
subclass relation 𝐴 ⊆ 𝐵 has syntax label fragment "ss"
because it is defined in df-ss 3554. 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 3699. There are many other syntax label fragments, e.g.,
singleton construct {𝐴} has syntax label fragment "sn" (because it
is defined in df-sn 4126), and the pair construct {𝐴, 𝐵} has
fragment "pr" ( from df-pr 4128). 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 4260. An "n" is often used for negation (¬), e.g.,
nan 602.
- 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 9821) and "re" represents real numbers ℝ ( definition df-r 9825).
The empty set ∅ often uses fragment 0, even though it is defined
in df-nul 3875. The syntax construct (𝐴 + 𝐵) usually uses the
fragment "add" (which is consistent with df-add 9826), 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 11021.
- 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 14719 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 14640) we have value cosval 14692 and closure
coscl 14696.
- 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 26652 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 (see above).
Additionally, we sometimes suffix with "v" the label of a theorem
eliminating a hypothesis such as Ⅎ𝑥𝜑 in 19.21 2062 via the use of
disjoint variable conditions combined with nfv 1830. If two (or three)
such hypotheses are eliminated, the suffix "vv" resp. "vvv" is used,
e.g. exlimivv 1847.
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 2466 derived from df-eu 2462. 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 4844.
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 2269 (cbval 2259 in deduction form "d" with a not free
variable replaced by a disjoint variable condition "v" with a
conjunction as antecedent "a").
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 63, syl2anc 691), commutes
(e.g., biimpac 502)
- 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)
- 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
- OLD : old/obsolete version of a theorem/definition/proof
- 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 500, rexlimiva 3010 |
| abl | Abelian group | df-abl 18019 |
Abel | Yes | ablgrp 18021, zringabl 19641 |
| abs | absorption | | | No |
ressabs 15766 |
| abs | absolute value (of a complex number) |
df-abs 13824 | (abs‘𝐴) | Yes |
absval 13826, absneg 13865, abs1 13885 |
| ad | adding | |
| No | adantr 480, ad2antlr 759 |
| add | add (see "p") | df-add 9826 |
(𝐴 + 𝐵) | Yes |
addcl 9897, addcom 10101, addass 9902 |
| al | "for all" | |
∀𝑥𝜑 | No | alim 1729, alex 1743 |
| ALT | alternative/less preferred (suffix) | |
| No | idALT 23 |
| an | and | df-an 385 |
(𝜑 ∧ 𝜓) | Yes |
anor 509, iman 439, imnan 437 |
| ant | antecedent | |
| No | adantr 480 |
| ass | associative | |
| No | biass 373, orass 545, mulass 9903 |
| asym | asymmetric, antisymmetric | |
| No | intasym 5430, asymref 5431, posasymb 16775 |
| ax | axiom | |
| No | ax6dgen 1992, ax1cn 9849 |
| bas, base |
base (set of an extensible structure) | df-base 15700 |
(Base‘𝑆) | Yes |
baseval 15746, ressbas 15757, cnfldbas 19571 |
| b, bi | biconditional ("iff", "if and only if")
| df-bi 196 | (𝜑 ↔ 𝜓) | Yes |
impbid 201, sspwb 4844 |
| br | binary relation | df-br 4584 |
𝐴𝑅𝐵 | Yes | brab1 4630, brun 4633 |
| cbv | change bound variable | | |
No | cbvalivw 1921, cbvrex 3144 |
| cl | closure | | | No |
ifclda 4070, ovrcl 6584, zaddcl 11294 |
| cn | complex numbers | df-c 9821 |
ℂ | Yes | nnsscn 10902, nncn 10905 |
| cnfld | field of complex numbers | df-cnfld 19568 |
ℂfld | Yes | cnfldbas 19571, cnfldinv 19596 |
| cntz | centralizer | df-cntz 17573 |
(Cntz‘𝑀) | Yes |
cntzfval 17576, dprdfcntz 18237 |
| cnv | converse | df-cnv 5046 |
◡𝐴 | Yes | opelcnvg 5224, f1ocnv 6062 |
| co | composition | df-co 5047 |
(𝐴 ∘ 𝐵) | Yes | cnvco 5230, fmptco 6303 |
| com | commutative | |
| No | orcom 401, bicomi 213, eqcomi 2619 |
| con | contradiction, contraposition | |
| No | condan 831, con2d 128 |
| csb | class substitution | df-csb 3500 |
⦋𝐴 / 𝑥⦌𝐵 | Yes |
csbid 3507, csbie2g 3530 |
| cyg | cyclic group | df-cyg 18103 |
CycGrp | Yes |
iscyg 18104, zringcyg 19658 |
| d | deduction form (suffix) | |
| No | idd 24, impbid 201 |
| df | (alternate) definition (prefix) | |
| No | dfrel2 5502, dffn2 5960 |
| di, distr | distributive | |
| No |
andi 907, imdi 377, ordi 904, difindi 3840, ndmovdistr 6721 |
| dif | class difference | df-dif 3543 |
(𝐴 ∖ 𝐵) | Yes |
difss 3699, difindi 3840 |
| div | division | df-div 10564 |
(𝐴 / 𝐵) | Yes |
divcl 10570, divval 10566, divmul 10567 |
| dm | domain | df-dm 5048 |
dom 𝐴 | Yes | dmmpt 5547, iswrddm0 13184 |
| e, eq, equ | equals | df-cleq 2603 |
𝐴 = 𝐵 | Yes |
2p2e4 11021, uneqri 3717, equtr 1935 |
| el | element of | |
𝐴 ∈ 𝐵 | Yes |
eldif 3550, eldifsn 4260, elssuni 4403 |
| eu | "there exists exactly one" | df-eu 2462 |
∃!𝑥𝜑 | Yes | euex 2482, euabsn 4205 |
| ex | exists (i.e. is a set) | |
| No | brrelex 5080, 0ex 4718 |
| ex | "there exists (at least one)" | df-ex 1696 |
∃𝑥𝜑 | Yes | exim 1751, alex 1743 |
| exp | export | |
| No | expt 167, expcom 450 |
| f | "not free in" (suffix) | |
| No | equs45f 2338, sbf 2368 |
| f | function | df-f 5808 |
𝐹:𝐴⟶𝐵 | Yes | fssxp 5973, opelf 5978 |
| fal | false | df-fal 1481 |
⊥ | Yes | bifal 1488, falantru 1499 |
| fi | finite intersection | df-fi 8200 |
(fi‘𝐵) | Yes | fival 8201, inelfi 8207 |
| fi, fin | finite | df-fin 7845 |
Fin | Yes |
isfi 7865, snfi 7923, onfin 8036 |
| fld | field (Note: there is an alternative
definition Fld of a field, see df-fld 32961) | df-field 18573 |
Field | Yes | isfld 18579, fldidom 19126 |
| fn | function with domain | df-fn 5807 |
𝐴 Fn 𝐵 | Yes | ffn 5958, fndm 5904 |
| frgp | free group | df-frgp 17946 |
(freeGrp‘𝐼) | Yes |
frgpval 17994, frgpadd 17999 |
| fsupp | finitely supported function |
df-fsupp 8159 | 𝑅 finSupp 𝑍 | Yes |
isfsupp 8162, fdmfisuppfi 8167, fsuppco 8190 |
| fun | function | df-fun 5806 |
Fun 𝐹 | Yes | funrel 5821, ffun 5961 |
| fv | function value | df-fv 5812 |
(𝐹‘𝐴) | Yes | fvres 6117, swrdfv 13276 |
| fz | finite set of sequential integers |
df-fz 12198 |
(𝑀...𝑁) | Yes | fzval 12199, eluzfz 12208 |
| fz0 | finite set of sequential nonnegative integers |
|
(0...𝑁) | Yes | nn0fz0 12306, fz0tp 12309 |
| fzo | half-open integer range | df-fzo 12335 |
(𝑀..^𝑁) | Yes |
elfzo 12341, elfzofz 12354 |
| g | more general (suffix); eliminates "is a set"
hypothsis | |
| No | uniexg 6853 |
| gra | graph | |
| No | uhgrav 25825, isumgra 25844, usgrares 25898 |
| grp | group | df-grp 17248 |
Grp | Yes | isgrp 17251, tgpgrp 21692 |
| gsum | group sum | df-gsum 15926 |
(𝐺 Σg 𝐹) | Yes |
gsumval 17094, gsumwrev 17619 |
| hash | size (of a set) | df-hash 12980 |
(#‘𝐴) | Yes |
hashgval 12982, hashfz1 12996, hashcl 13009 |
| hb | hypothesis builder (prefix) | |
| No | hbxfrbi 1742, hbald 2028, hbequid 33212 |
| hm | (monoid, group, ring) homomorphism | |
| No | ismhm 17160, isghm 17483, isrhm 18544 |
| i | inference (suffix) | |
| No | eleq1i 2679, tcsni 8502 |
| i | implication (suffix) | |
| No | brwdomi 8356, infeq5i 8416 |
| id | identity | |
| No | biid 250 |
| idm | idempotent | |
| No | anidm 674, tpidm13 4235 |
| im, imp | implication (label often omitted) |
df-im 13689 | (𝐴 → 𝐵) | Yes |
iman 439, imnan 437, impbidd 199 |
| ima | image | df-ima 5051 |
(𝐴 “ 𝐵) | Yes | resima 5351, imaundi 5464 |
| imp | import | |
| No | biimpa 500, impcom 445 |
| in | intersection | df-in 3547 |
(𝐴 ∩ 𝐵) | Yes | elin 3758, incom 3767 |
| inf | infimum | df-inf 8232 |
inf(ℝ+, ℝ*, < ) | Yes |
fiinfcl 8290, infiso 8296 |
| is... | is (something a) ...? | |
| No | isring 18374 |
| j | joining, disjoining | |
| No | jc 158, jaoi 393 |
| l | left | |
| No | olcd 407, simpl 472 |
| map | mapping operation or set exponentiation |
df-map 7746 | (𝐴 ↑𝑚 𝐵) | Yes |
mapvalg 7754, elmapex 7764 |
| mat | matrix | df-mat 20033 |
(𝑁 Mat 𝑅) | Yes |
matval 20036, matring 20068 |
| mdet | determinant (of a square matrix) |
df-mdet 20210 | (𝑁 maDet 𝑅) | Yes |
mdetleib 20212, mdetrlin 20227 |
| mgm | magma | df-mgm 17065 |
Magma | Yes |
mgmidmo 17082, mgmlrid 17089, ismgm 17066 |
| mgp | multiplicative group | df-mgp 18313 |
(mulGrp‘𝑅) | Yes |
mgpress 18323, ringmgp 18376 |
| mnd | monoid | df-mnd 17118 |
Mnd | Yes | mndass 17125, mndodcong 17784 |
| mo | "there exists at most one" | df-mo 2463 |
∃*𝑥𝜑 | Yes | eumo 2487, moim 2507 |
| mp | modus ponens | ax-mp 5 |
| No | mpd 15, mpi 20 |
| mpt | modus ponendo tollens | |
| No | mptnan 1684, mptxor 1685 |
| mpt | maps-to notation for a function |
df-mpt 4645 | (𝑥 ∈ 𝐴 ↦ 𝐵) | Yes |
fconstmpt 5085, resmpt 5369 |
| mpt2 | maps-to notation for an operation |
df-mpt2 6554 | (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) | Yes |
mpt2mpt 6650, resmpt2 6656 |
| mul | multiplication (see "t") | df-mul 9827 |
(𝐴 · 𝐵) | Yes |
mulcl 9899, divmul 10567, mulcom 9901, mulass 9903 |
| n, not | not | |
¬ 𝜑 | Yes |
nan 602, notnotr 124 |
| ne | not equal | df-ne | 𝐴 ≠ 𝐵 |
Yes | exmidne 2792, neeqtrd 2851 |
| nel | not element of | df-nel | 𝐴 ∉ 𝐵
|
Yes | neli 2885, nnel 2892 |
| ne0 | not equal to zero (see n0) | |
≠ 0 | No |
negne0d 10269, ine0 10344, gt0ne0 10372 |
| nf | "not free in" (prefix) | |
| No | nfnd 1769 |
| ngp | normed group | df-ngp 22198 |
NrmGrp | Yes | isngp 22210, ngptps 22216 |
| nm | norm (on a group or ring) | df-nm 22197 |
(norm‘𝑊) | Yes |
nmval 22204, subgnm 22247 |
| nn | positive integers | df-nn 10898 |
ℕ | Yes | nnsscn 10902, nncn 10905 |
| nn0 | nonnegative integers | df-n0 11170 |
ℕ0 | Yes | nnnn0 11176, nn0cn 11179 |
| n0 | not the empty set (see ne0) | |
≠ ∅ | No | n0i 3879, vn0 3883, ssn0 3928 |
| OLD | old, obsolete (to be removed soon) | |
| No | 19.43OLD 1800 |
| op | ordered pair | df-op 4132 |
⟨𝐴, 𝐵⟩ | Yes | dfopif 4337, opth 4871 |
| or | or | df-or 384 |
(𝜑 ∨ 𝜓) | Yes |
orcom 401, anor 509 |
| ot | ordered triple | df-ot 4134 |
⟨𝐴, 𝐵, 𝐶⟩ | Yes |
euotd 4900, fnotovb 6592 |
| ov | operation value | df-ov 6552 |
(𝐴𝐹𝐵) | Yes
| fnotovb 6592, fnovrn 6707 |
| p | plus (see "add"), for all-constant
theorems | df-add 9826 |
(3 + 2) = 5 | Yes |
3p2e5 11037 |
| pfx | prefix | df-pfx 40245 |
(𝑊 prefix 𝐿) | Yes |
pfxlen 40254, ccatpfx 40272 |
| pm | Principia Mathematica | |
| No | pm2.27 41 |
| pm | partial mapping (operation) | df-pm 7747 |
(𝐴 ↑pm 𝐵) | Yes | elpmi 7762, pmsspw 7778 |
| pr | pair | df-pr 4128 |
{𝐴, 𝐵} | Yes |
elpr 4146, prcom 4211, prid1g 4239, prnz 4253 |
| prm, prime | prime (number) | df-prm 15224 |
ℙ | Yes | 1nprm 15230, dvdsprime 15238 |
| pss | proper subset | df-pss 3556 |
𝐴 ⊊ 𝐵 | Yes | pssss 3664, sspsstri 3671 |
| q | rational numbers ("quotients") | df-q 11665 |
ℚ | Yes | elq 11666 |
| r | right | |
| No | orcd 406, simprl 790 |
| rab | restricted class abstraction |
df-rab 2905 | {𝑥 ∈ 𝐴 ∣ 𝜑} | Yes |
rabswap 3098, df-oprab 6553 |
| ral | restricted universal quantification |
df-ral 2901 | ∀𝑥 ∈ 𝐴𝜑 | Yes |
ralnex 2975, ralrnmpt2 6673 |
| rcl | reverse closure | |
| No | ndmfvrcl 6129, nnarcl 7583 |
| re | real numbers | df-r 9825 |
ℝ | Yes | recn 9905, 0re 9919 |
| rel | relation | df-rel 5045 | Rel 𝐴 |
Yes | brrelex 5080, relmpt2opab 7146 |
| res | restriction | df-res 5050 |
(𝐴 ↾ 𝐵) | Yes |
opelres 5322, f1ores 6064 |
| reu | restricted existential uniqueness |
df-reu 2903 | ∃!𝑥 ∈ 𝐴𝜑 | Yes |
nfreud 3091, reurex 3137 |
| rex | restricted existential quantification |
df-rex 2902 | ∃𝑥 ∈ 𝐴𝜑 | Yes |
rexnal 2978, rexrnmpt2 6674 |
| rmo | restricted "at most one" |
df-rmo 2904 | ∃*𝑥 ∈ 𝐴𝜑 | Yes |
nfrmod 3092, nrexrmo 3140 |
| rn | range | df-rn 5049 | ran 𝐴 |
Yes | elrng 5236, rncnvcnv 5270 |
| rng | (unital) ring | df-ring 18372 |
Ring | Yes |
ringidval 18326, isring 18374, ringgrp 18375 |
| rot | rotation | |
| No | 3anrot 1036, 3orrot 1037 |
| s | eliminates need for syllogism (suffix) |
| | No | ancoms 468 |
| sb | (proper) substitution (of a set) |
df-sb 1868 | [𝑦 / 𝑥]𝜑 | Yes |
spsbe 1871, sbimi 1873 |
| sbc | (proper) substitution of a class |
df-sbc 3403 | [𝐴 / 𝑥]𝜑 | Yes |
sbc2or 3411, sbcth 3417 |
| sca | scalar | df-sca 15784 |
(Scalar‘𝐻) | Yes |
resssca 15854, mgpsca 18319 |
| simp | simple, simplification | |
| No | simpl 472, simp3r3 1164 |
| sn | singleton | df-sn 4126 |
{𝐴} | Yes | eldifsn 4260 |
| sp | specialization | |
| No | spsbe 1871, spei 2249 |
| ss | subset | df-ss 3554 |
𝐴 ⊆ 𝐵 | Yes | difss 3699 |
| struct | structure | df-struct 15697 |
Struct | Yes | brstruct 15703, structfn 15708 |
| sub | subtract | df-sub 10147 |
(𝐴 − 𝐵) | Yes |
subval 10151, subaddi 10247 |
| sup | supremum | df-sup 8231 |
sup(𝐴, 𝐵, < ) | Yes |
fisupcl 8258, supmo 8241 |
| supp | support (of a function) | df-supp 7183 |
(𝐹 supp 𝑍) | Yes |
ressuppfi 8184, mptsuppd 7205 |
| swap | swap (two parts within a theorem) |
| | No | rabswap 3098, 2reuswap 3377 |
| syl | syllogism | syl 17 |
| No | 3syl 18 |
| sym | symmetric | |
| No | df-symdif 3806, cnvsym 5429 |
| symg | symmetric group | df-symg 17621 |
(SymGrp‘𝐴) | Yes |
symghash 17628, pgrpsubgsymg 17651 |
| t |
times (see "mul"), for all-constant theorems |
df-mul 9827 |
(3 · 2) = 6 | Yes |
3t2e6 11056 |
| th | theorem | |
| No | nfth 1718, sbcth 3417, weth 9200 |
| tp | triple | df-tp 4130 |
{𝐴, 𝐵, 𝐶} | Yes |
eltpi 4176, tpeq1 4221 |
| tr | transitive | |
| No | bitrd 267, biantr 968 |
| tru | true | df-tru 1478 |
⊤ | Yes | bitru 1487, truanfal 1498 |
| un | union | df-un 3545 |
(𝐴 ∪ 𝐵) | Yes |
uneqri 3717, uncom 3719 |
| unit | unit (in a ring) |
df-unit 18465 | (Unit‘𝑅) | Yes |
isunit 18480, nzrunit 19088 |
| v | disjoint variable conditions used when
a not-free hypothesis (suffix) |
| | No | spimv 2245 |
| vv | 2 disjoint variables (in a not-free hypothesis)
(suffix) | | | No | 19.23vv 1890 |
| w | weak (version of a theorem) (suffix) | |
| No | ax11w 1994, spnfw 1915 |
| wrd | word |
df-word 13154 | Word 𝑆 | Yes |
iswrdb 13166, wrdfn 13174, ffz0iswrd 13187 |
| xp | cross product (Cartesian product) |
df-xp 5044 | (𝐴 × 𝐵) | Yes |
elxp 5055, opelxpi 5072, xpundi 5094 |
| xr | eXtended reals | df-xr 9957 |
ℝ* | Yes | ressxr 9962, rexr 9964, 0xr 9965 |
| z | integers (from German "Zahlen") |
df-z 11255 | ℤ | Yes |
elz 11256, zcn 11259 |
| zn | ring of integers mod 𝑛 | df-zn 19674 |
(ℤ/nℤ‘𝑁) | Yes |
znval 19702, zncrng 19712, znhash 19726 |
| zring | ring of integers | df-zring 19638 |
ℤring | Yes | zringbas 19643, zringcrng 19639
|
| 0, z |
slashed zero (empty set) (see n0) | df-nul 3875 |
∅ | Yes |
n0i 3879, vn0 3883; snnz 4252, prnz 4253 |
(Contributed by DAW, 27-Dec-2016.) (New usage is
discouraged.) |
