MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  conventions-labels Structured version   Visualization version   GIF version

Theorem conventions-labels 30198
Description:

The following gives conventions used in the Metamath Proof Explorer (MPE, set.mm) regarding labels. For other conventions, see conventions 30197 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 3058"rgen.1 $e |- ( x e. A -> ph ) $." or letters corresponding to the (main) class variable used in the hypothesis, e.g., for mdet0 22495: "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 2653 and stirling 45400.
  • 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 1834, and the restricted quantifier version of Theorem 21 from Section 19 of [Margaris] p. 90 is labeled r19.21 3246.
  • 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... 15851. 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 3947, and thus its syntax label fragment is "dif". Similarly, the subclass relation 𝐴 βŠ† 𝐡 has syntax label fragment "ss" because it is defined in df-ss 3961. 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 4127. There are many other syntax label fragments, e.g., singleton construct {𝐴} has syntax label fragment "sn" (because it is defined in df-sn 4625), and the pair construct {𝐴, 𝐡} has fragment "pr" ( from df-pr 4627). 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 4786. 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 11136) and "re" represents real numbers ℝ (Definition df-r 11140). The empty set βˆ… often uses fragment 0, even though it is defined in df-nul 4319. The syntax construct (𝐴 + 𝐡) usually uses the fragment "add" (which is consistent with df-add 11141), 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 12369.
  • 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 16118 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 16038) we have value cosval 16091 and closure coscl 16095.
  • 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 30200 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 1935 versus 19.21 2193. This often permits to prove the result using fewer axioms, and/or to eliminate a nonfreeness hypothesis (such as β„²π‘₯πœ‘ in 19.21 2193). If no constraint is put on axiom use, then the v-version can be proved from the original theorem using nfv 1910. If two (resp. three) such disjoint variable conditions are added, then the suffix "vv" (resp. "vvv") is used, e.g., exlimivv 1928. 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 2565 derived from eu6 2563. 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 5445. 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 2403 (cbval 2392 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 3542. 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 583), 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.

AbbreviationMnenomicSource ExpressionSyntax?Example(s)
aand (suffix) No biimpa 476, rexlimiva 3142
ablAbelian group df-abl 19729 Abel Yes ablgrp 19731, zringabl 21364
absabsorption No ressabs 17221
absabsolute value (of a complex number) df-abs 15207 (absβ€˜π΄) Yes absval 15209, absneg 15248, abs1 15268
adadding No adantr 480, ad2antlr 726
addadd (see "p") df-add 11141 (𝐴 + 𝐡) Yes addcl 11212, addcom 11422, addass 11217
al"for all" βˆ€π‘₯πœ‘ No alim 1805, alex 1821
ALTalternative/less preferred (suffix) No idALT 23
anand df-an 396 (πœ‘ ∧ πœ“) Yes anor 981, iman 401, imnan 399
antantecedent No adantr 480
assassociative No biass 384, orass 920, mulass 11218
asymasymmetric, antisymmetric No intasym 6115, asymref 6116, posasymb 18302
axaxiom No ax6dgen 2117, ax1cn 11164
bas, base base (set of an extensible structure) df-base 17172 (Baseβ€˜π‘†) Yes baseval 17173, ressbas 17206, cnfldbas 21270
b, bibiconditional ("iff", "if and only if") df-bi 206 (πœ‘ ↔ πœ“) Yes impbid 211, sspwb 5445
brbinary relation df-br 5143 𝐴𝑅𝐡 Yes brab1 5190, brun 5193
ccommutes, commuted (suffix) No biimpac 478
ccontraction (suffix) No sylc 65, syl2anc 583
cbvchange bound variable No cbvalivw 2003, cbvrex 3354
cdmcodomain No ffvelcdm 7085, focdmex 7953
clclosure No ifclda 4559, ovrcl 7455, zaddcl 12624
cncomplex numbers df-c 11136 β„‚ Yes nnsscn 12239, nncn 12242
cnfldfield of complex numbers df-cnfld 21267 β„‚fld Yes cnfldbas 21270, cnfldinv 21317
cntzcentralizer df-cntz 19259 (Cntzβ€˜π‘€) Yes cntzfval 19262, dprdfcntz 19963
cnvconverse df-cnv 5680 ◑𝐴 Yes opelcnvg 5877, f1ocnv 6845
cocomposition df-co 5681 (𝐴 ∘ 𝐡) Yes cnvco 5882, fmptco 7132
comcommutative No orcom 869, bicomi 223, eqcomi 2736
concontradiction, contraposition No condan 817, con2d 134
csbclass substitution df-csb 3890 ⦋𝐴 / π‘₯⦌𝐡 Yes csbid 3902, csbie2g 3932
cygcyclic group df-cyg 19824 CycGrp Yes iscyg 19825, zringcyg 21382
ddeduction form (suffix) No idd 24, impbid 211
df(alternate) definition (prefix) No dfrel2 6187, dffn2 6718
di, distrdistributive No andi 1006, imdi 389, ordi 1004, difindi 4277, ndmovdistr 7604
difclass difference df-dif 3947 (𝐴 βˆ– 𝐡) Yes difss 4127, difindi 4277
divdivision df-div 11894 (𝐴 / 𝐡) Yes divcl 11900, divval 11896, divmul 11897
dmdomain df-dm 5682 dom 𝐴 Yes dmmpt 6238, iswrddm0 14512
e, eq, equequals (equ for setvars, eq for classes) df-cleq 2719 𝐴 = 𝐡 Yes 2p2e4 12369, uneqri 4147, equtr 2017
edgedge df-edg 28848 (Edgβ€˜πΊ) Yes edgopval 28851, usgredgppr 28996
elelement of 𝐴 ∈ 𝐡 Yes eldif 3954, eldifsn 4786, elssuni 4935
enequinumerous df-en 𝐴 β‰ˆ 𝐡 Yes domen 8973, enfi 9206
eu"there exists exactly one" eu6 2563 βˆƒ!π‘₯πœ‘ Yes euex 2566, euabsn 4726
exexists (i.e. is a set) ∈ V No brrelex1 5725, 0ex 5301
ex, e"there exists (at least one)" df-ex 1775 βˆƒπ‘₯πœ‘ Yes exim 1829, alex 1821
expexport No expt 177, expcom 413
f"not free in" (suffix) No equs45f 2453, sbf 2255
ffunction df-f 6546 𝐹:𝐴⟢𝐡 Yes fssxp 6745, opelf 6752
falfalse df-fal 1547 βŠ₯ Yes bifal 1550, falantru 1569
fifinite intersection df-fi 9426 (fiβ€˜π΅) Yes fival 9427, inelfi 9433
fi, finfinite df-fin 8959 Fin Yes isfi 8988, snfi 9060, onfin 9246
fldfield (Note: there is an alternative definition Fld of a field, see df-fld 37400) df-field 20616 Field Yes isfld 20624, fldidom 21245
fnfunction with domain df-fn 6545 𝐴 Fn 𝐡 Yes ffn 6716, fndm 6651
frgpfree group df-frgp 19656 (freeGrpβ€˜πΌ) Yes frgpval 19704, frgpadd 19709
fsuppfinitely supported function df-fsupp 9378 𝑅 finSupp 𝑍 Yes isfsupp 9381, fdmfisuppfi 9389, fsuppco 9417
funfunction df-fun 6544 Fun 𝐹 Yes funrel 6564, ffun 6719
fvfunction value df-fv 6550 (πΉβ€˜π΄) Yes fvres 6910, swrdfv 14622
fzfinite set of sequential integers df-fz 13509 (𝑀...𝑁) Yes fzval 13510, eluzfz 13520
fz0finite set of sequential nonnegative integers (0...𝑁) Yes nn0fz0 13623, fz0tp 13626
fzohalf-open integer range df-fzo 13652 (𝑀..^𝑁) Yes elfzo 13658, elfzofz 13672
gmore general (suffix); eliminates "is a set" hypotheses No uniexg 7739
grgraph No uhgrf 28862, isumgr 28895, usgrres1 29115
grpgroup df-grp 18884 Grp Yes isgrp 18887, tgpgrp 23969
gsumgroup sum df-gsum 17415 (𝐺 Ξ£g 𝐹) Yes gsumval 18628, gsumwrev 19311
hashsize (of a set) df-hash 14314 (β™―β€˜π΄) Yes hashgval 14316, hashfz1 14329, hashcl 14339
hbhypothesis builder (prefix) No hbxfrbi 1820, hbald 2161, hbequid 38318
hm(monoid, group, ring, ...) homomorphism No ismhm 18733, isghm 19161, isrhm 20406
iinference (suffix) No eleq1i 2819, tcsni 9758
iimplication (suffix) No brwdomi 9583, infeq5i 9651
ididentity No biid 261
iedgindexed edge df-iedg 28799 (iEdgβ€˜πΊ) Yes iedgval0 28840, edgiedgb 28854
idmidempotent No anidm 564, tpidm13 4756
im, impimplication (label often omitted) df-im 15072 (𝐴 β†’ 𝐡) Yes iman 401, imnan 399, impbidd 209
im(group, ring, ...) isomorphism No isgim 19207, rimrcl 20410
imaimage df-ima 5685 (𝐴 β€œ 𝐡) Yes resima 6013, imaundi 6148
impimport No biimpa 476, impcom 407
inintersection df-in 3951 (𝐴 ∩ 𝐡) Yes elin 3960, incom 4197
infinfimum df-inf 9458 inf(ℝ+, ℝ*, < ) Yes fiinfcl 9516, infiso 9523
is...is (something a) ...? No isring 20168
jjoining, disjoining No jc 161, jaoi 856
lleft No olcd 873, simpl 482
mapmapping operation or set exponentiation df-map 8838 (𝐴 ↑m 𝐡) Yes mapvalg 8846, elmapex 8858
matmatrix df-mat 22295 (𝑁 Mat 𝑅) Yes matval 22298, matring 22332
mdetdeterminant (of a square matrix) df-mdet 22474 (𝑁 maDet 𝑅) Yes mdetleib 22476, mdetrlin 22491
mgmmagma df-mgm 18591 Magma Yes mgmidmo 18611, mgmlrid 18618, ismgm 18592
mgpmultiplicative group df-mgp 20066 (mulGrpβ€˜π‘…) Yes mgpress 20080, ringmgp 20170
mndmonoid df-mnd 18686 Mnd Yes mndass 18694, mndodcong 19488
mo"there exists at most one" df-mo 2529 βˆƒ*π‘₯πœ‘ Yes eumo 2567, moim 2533
mpmodus ponens ax-mp 5 No mpd 15, mpi 20
mpomaps-to notation for an operation df-mpo 7419 (π‘₯ ∈ 𝐴, 𝑦 ∈ 𝐡 ↦ 𝐢) Yes mpompt 7528, resmpo 7534
mptmodus ponendo tollens No mptnan 1763, mptxor 1764
mptmaps-to notation for a function df-mpt 5226 (π‘₯ ∈ 𝐴 ↦ 𝐡) Yes fconstmpt 5734, resmpt 6035
mpt2maps-to notation for an operation (deprecated). We are in the process of replacing mpt2 with mpo in labels. df-mpo 7419 (π‘₯ ∈ 𝐴, 𝑦 ∈ 𝐡 ↦ 𝐢) Yes mpompt 7528, resmpo 7534
mulmultiplication (see "t") df-mul 11142 (𝐴 Β· 𝐡) Yes mulcl 11214, divmul 11897, mulcom 11216, mulass 11218
n, notnot Β¬ πœ‘ Yes nan 829, notnotr 130
nenot equaldf-ne 𝐴 β‰  𝐡 Yes exmidne 2945, neeqtrd 3005
nelnot element ofdf-nel 𝐴 βˆ‰ 𝐡 Yes neli 3043, nnel 3051
ne0not equal to zero (see n0) β‰  0 No negne0d 11591, ine0 11671, gt0ne0 11701
nf "not free in" (prefix) df-nf 1779 β„²π‘₯πœ‘ Yes nfnd 1854
ngpnormed group df-ngp 24479 NrmGrp Yes isngp 24492, ngptps 24498
nmnorm (on a group or ring) df-nm 24478 (normβ€˜π‘Š) Yes nmval 24485, subgnm 24529
nnpositive integers df-nn 12235 β„• Yes nnsscn 12239, nncn 12242
nn0nonnegative integers df-n0 12495 β„•0 Yes nnnn0 12501, nn0cn 12504
n0not the empty set (see ne0) β‰  βˆ… No n0i 4329, vn0 4334, ssn0 4396
OLDold, obsolete (to be removed soon) No 19.43OLD 1879
onordinal number df-on 6367 𝐴 ∈ On Yes elon 6372, 1on 8492 onelon 6388
opordered pair df-op 4631 ⟨𝐴, 𝐡⟩ Yes dfopif 4866, opth 5472
oror df-or 847 (πœ‘ ∨ πœ“) Yes orcom 869, anor 981
otordered triple df-ot 4633 ⟨𝐴, 𝐡, 𝐢⟩ Yes euotd 5509, fnotovb 7464
ovoperation value df-ov 7417 (𝐴𝐹𝐡) Yes fnotovb 7464, fnovrn 7590
pplus (see "add"), for all-constant theorems df-add 11141 (3 + 2) = 5 Yes 3p2e5 12385
pfxprefix df-pfx 14645 (π‘Š prefix 𝐿) Yes pfxlen 14657, ccatpfx 14675
pmPrincipia Mathematica No pm2.27 42
pmpartial mapping (operation) df-pm 8839 (𝐴 ↑pm 𝐡) Yes elpmi 8856, pmsspw 8887
prpair df-pr 4627 {𝐴, 𝐡} Yes elpr 4647, prcom 4732, prid1g 4760, prnz 4777
prm, primeprime (number) df-prm 16634 β„™ Yes 1nprm 16641, dvdsprime 16649
pssproper subset df-pss 3963 𝐴 ⊊ 𝐡 Yes pssss 4091, sspsstri 4098
q rational numbers ("quotients") df-q 12955 β„š Yes elq 12956
rreversed (suffix) No pm4.71r 558, caovdir 7649
rright No orcd 872, simprl 770
rabrestricted class abstraction df-rab 3428 {π‘₯ ∈ 𝐴 ∣ πœ‘} Yes rabswap 3436, df-oprab 7418
ralrestricted universal quantification df-ral 3057 βˆ€π‘₯ ∈ π΄πœ‘ Yes ralnex 3067, ralrnmpo 7554
rclreverse closure No ndmfvrcl 6927, nnarcl 8630
rereal numbers df-r 11140 ℝ Yes recn 11220, 0re 11238
relrelation df-rel 5679 Rel 𝐴 Yes brrelex1 5725, relmpoopab 8093
resrestriction df-res 5684 (𝐴 β†Ύ 𝐡) Yes opelres 5985, f1ores 6847
reurestricted existential uniqueness df-reu 3372 βˆƒ!π‘₯ ∈ π΄πœ‘ Yes nfreud 3424, reurex 3375
rexrestricted existential quantification df-rex 3066 βˆƒπ‘₯ ∈ π΄πœ‘ Yes rexnal 3095, rexrnmpo 7555
rmorestricted "at most one" df-rmo 3371 βˆƒ*π‘₯ ∈ π΄πœ‘ Yes nfrmod 3423, nrexrmo 3392
rnrange df-rn 5683 ran 𝐴 Yes elrng 5888, rncnvcnv 5930
ring(unital) ring df-ring 20166 Ring Yes ringidval 20114, isring 20168, ringgrp 20169
rngnon-unital ring df-rng 20084 Rng Yes isrng 20085, rngabl 20086, rnglz 20096
rotrotation No 3anrot 1098, 3orrot 1090
seliminates need for syllogism (suffix) No ancoms 458
sb(proper) substitution (of a set) df-sb 2061 [𝑦 / π‘₯]πœ‘ Yes spsbe 2078, sbimi 2070
sbc(proper) substitution of a class df-sbc 3775 [𝐴 / π‘₯]πœ‘ Yes sbc2or 3783, sbcth 3789
scascalar df-sca 17240 (Scalarβ€˜π») Yes resssca 17315, mgpsca 20073
simpsimple, simplification No simpl 482, simp3r3 1281
snsingleton df-sn 4625 {𝐴} Yes eldifsn 4786
spspecialization No spsbe 2078, spei 2388
sssubset df-ss 3961 𝐴 βŠ† 𝐡 Yes difss 4127
structstructure df-struct 17107 Struct Yes brstruct 17108, structfn 17116
subsubtract df-sub 11468 (𝐴 βˆ’ 𝐡) Yes subval 11473, subaddi 11569
supsupremum df-sup 9457 sup(𝐴, 𝐡, < ) Yes fisupcl 9484, supmo 9467
suppsupport (of a function) df-supp 8160 (𝐹 supp 𝑍) Yes ressuppfi 9410, mptsuppd 8185
swapswap (two parts within a theorem) No rabswap 3436, 2reuswap 3739
sylsyllogism syl 17 No 3syl 18
symsymmetric No df-symdif 4238, cnvsym 6112
symgsymmetric group df-symg 19313 (SymGrpβ€˜π΄) Yes symghash 19323, pgrpsubgsymg 19355
t times (see "mul"), for all-constant theorems df-mul 11142 (3 Β· 2) = 6 Yes 3t2e6 12400
th, t theorem No nfth 1796, sbcth 3789, weth 10510, ancomst 464
tptriple df-tp 4629 {𝐴, 𝐡, 𝐢} Yes eltpi 4687, tpeq1 4742
trtransitive No bitrd 279, biantr 805
tru, t true, truth df-tru 1537 ⊀ Yes bitru 1543, truanfal 1568, biimt 360
ununion df-un 3949 (𝐴 βˆͺ 𝐡) Yes uneqri 4147, uncom 4149
unitunit (in a ring) df-unit 20286 (Unitβ€˜π‘…) Yes isunit 20301, nzrunit 20450
v setvar (especially for specializations of theorems when a class is replaced by a setvar variable) x Yes cv 1533, vex 3473, velpw 4603, vtoclf 3547
v disjoint variable condition used in place of nonfreeness hypothesis (suffix) No spimv 2384
vtx vertex df-vtx 28798 (Vtxβ€˜πΊ) Yes vtxval0 28839, opvtxov 28805
vv two disjoint variable conditions used in place of nonfreeness hypotheses (suffix) No 19.23vv 1939
wweak (version of a theorem) (suffix) No ax11w 2119, spnfw 1976
wrdword df-word 14489 Word 𝑆 Yes iswrdb 14494, wrdfn 14502, ffz0iswrd 14515
xpcross product (Cartesian product) df-xp 5678 (𝐴 Γ— 𝐡) Yes elxp 5695, opelxpi 5709, xpundi 5740
xreXtended reals df-xr 11274 ℝ* Yes ressxr 11280, rexr 11282, 0xr 11283
z integers (from German "Zahlen") df-z 12581 β„€ Yes elz 12582, zcn 12585
zn ring of integers mod 𝑁 df-zn 21419 (β„€/nβ„€β€˜π‘) Yes znval 21452, zncrng 21465, znhash 21479
zringring of integers df-zring 21360 β„€ring Yes zringbas 21366, zringcrng 21361
0, z slashed zero (empty set) df-nul 4319 βˆ… Yes n0i 4329, vn0 4334; snnz 4776, prnz 4777

(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.)

Hypothesis
Ref Expression
conventions-labels.1 πœ‘
Assertion
Ref Expression
conventions-labels πœ‘

Proof of Theorem conventions-labels
StepHypRef Expression
1 conventions-labels.1 1 πœ‘
Colors of variables: wff setvar class
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator