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

Theorem conventions-labels 28193
Description:

The following gives conventions used in the Metamath Proof Explorer (MPE, set.mm) regarding labels. For other conventions, see conventions 28192 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 3143"rgen.1 \$e |- ( x e. A -> ph ) \$." or letters corresponding to the (main) class variable used in the hypothesis, e.g. for mdet0 21218: "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 2751 and stirling 42662.
• 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 3209.
• 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... 15237. 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 3922, and thus its syntax label fragment is "dif". Similarly, the subclass relation 𝐴𝐵 has syntax label fragment "ss" because it is defined in df-ss 3936. 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 4094. There are many other syntax label fragments, e.g., singleton construct {𝐴} has syntax label fragment "sn" (because it is defined in df-sn 4551), and the pair construct {𝐴, 𝐵} has fragment "pr" ( from df-pr 4553). 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 4704. An "n" is often used for negation (¬), e.g., nan 828.
• 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 10541) and "re" represents real numbers ( definition df-r 10545). The empty set often uses fragment 0, even though it is defined in df-nul 4277. The syntax construct (𝐴 + 𝐵) usually uses the fragment "add" (which is consistent with df-add 10546), 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 11769.
• 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 15503 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 15424) we have value cosval 15476 and closure coscl 15480.
• 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 28195 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 1941 versus 19.21 2209. This often permits to prove the result using fewer axioms, and/or to eliminate a nonfreeness hypothesis (such as 𝑥𝜑 in 19.21 2209). If no constraint is put on axiom use, then the v-version can be proved from the original theorem using nfv 1916. If two (resp. three) such disjoint variable conditions are added, then the suffix "vv" (resp. "vvv") is used, e.g., exlimivv 1934. 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 2662 derived from eu6 2660. 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 5329. 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 2432 (cbval 2418 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 3541. 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 587), commutes (e.g., biimpac 482)
• 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 480, rexlimiva 3273
ablAbelian group df-abl 18909 Abel Yes ablgrp 18911, zringabl 20174
absabsorption No ressabs 16563
absabsolute value (of a complex number) df-abs 14595 (abs‘𝐴) Yes absval 14597, absneg 14637, abs1 14657
al"for all" 𝑥𝜑 No alim 1812, alex 1827
ALTalternative/less preferred (suffix) No idALT 23
anand df-an 400 (𝜑𝜓) Yes anor 980, iman 405, imnan 403
assassociative No biass 389, orass 919, mulass 10623
asymasymmetric, antisymmetric No intasym 5962, asymref 5963, posasymb 17562
axaxiom No ax6dgen 2133, ax1cn 10569
bas, base base (set of an extensible structure) df-base 16489 (Base‘𝑆) Yes baseval 16542, ressbas 16554, cnfldbas 20102
b, bibiconditional ("iff", "if and only if") df-bi 210 (𝜑𝜓) Yes impbid 215, sspwb 5329
brbinary relation df-br 5053 𝐴𝑅𝐵 Yes brab1 5100, brun 5103
cbvchange bound variable No cbvalivw 2015, cbvrex 3431
clclosure No ifclda 4484, ovrcl 7190, zaddcl 12019
cncomplex numbers df-c 10541 Yes nnsscn 11639, nncn 11642
cnfldfield of complex numbers df-cnfld 20099 fld Yes cnfldbas 20102, cnfldinv 20129
cntzcentralizer df-cntz 18447 (Cntz‘𝑀) Yes cntzfval 18450, dprdfcntz 19137
cnvconverse df-cnv 5550 𝐴 Yes opelcnvg 5738, f1ocnv 6618
cocomposition df-co 5551 (𝐴𝐵) Yes cnvco 5743, fmptco 6882
comcommutative No orcom 867, bicomi 227, eqcomi 2833
concontradiction, contraposition No condan 817, con2d 136
csbclass substitution df-csb 3867 𝐴 / 𝑥𝐵 Yes csbid 3879, csbie2g 3906
cygcyclic group df-cyg 18997 CycGrp Yes iscyg 18998, zringcyg 20191
ddeduction form (suffix) No idd 24, impbid 215
df(alternate) definition (prefix) No dfrel2 6033, dffn2 6505
di, distrdistributive No andi 1005, imdi 394, ordi 1003, difindi 4243, ndmovdistr 7331
difclass difference df-dif 3922 (𝐴𝐵) Yes difss 4094, difindi 4243
divdivision df-div 11296 (𝐴 / 𝐵) Yes divcl 11302, divval 11298, divmul 11299
dmdomain df-dm 5552 dom 𝐴 Yes dmmpt 6081, iswrddm0 13890
e, eq, equequals (equ for setvars, eq for classes) df-cleq 2817 𝐴 = 𝐵 Yes 2p2e4 11769, uneqri 4113, equtr 2029
edgedge df-edg 26848 (Edg‘𝐺) Yes edgopval 26851, usgredgppr 26993
elelement of 𝐴𝐵 Yes eldif 3929, eldifsn 4704, elssuni 4854
enequinumerous df-en 𝐴𝐵 Yes domen 8518, enfi 8731
eu"there exists exactly one" eu6 2660 ∃!𝑥𝜑 Yes euex 2663, euabsn 4647
exexists (i.e. is a set) ∈ V No brrelex1 5592, 0ex 5197
ex, e"there exists (at least one)" df-ex 1782 𝑥𝜑 Yes exim 1835, alex 1827
expexport No expt 180, expcom 417
f"not free in" (suffix) No equs45f 2484, sbf 2273
ffunction df-f 6347 𝐹:𝐴𝐵 Yes fssxp 6524, opelf 6529
falfalse df-fal 1551 Yes bifal 1554, falantru 1573
fifinite intersection df-fi 8872 (fi‘𝐵) Yes fival 8873, inelfi 8879
fi, finfinite df-fin 8509 Fin Yes isfi 8529, snfi 8590, onfin 8707
fldfield (Note: there is an alternative definition Fld of a field, see df-fld 35379) df-field 19505 Field Yes isfld 19511, fldidom 20078
fnfunction with domain df-fn 6346 𝐴 Fn 𝐵 Yes ffn 6503, fndm 6443
frgpfree group df-frgp 18836 (freeGrp‘𝐼) Yes frgpval 18884, frgpadd 18889
fsuppfinitely supported function df-fsupp 8831 𝑅 finSupp 𝑍 Yes isfsupp 8834, fdmfisuppfi 8839, fsuppco 8862
funfunction df-fun 6345 Fun 𝐹 Yes funrel 6360, ffun 6506
fvfunction value df-fv 6351 (𝐹𝐴) Yes fvres 6680, swrdfv 14010
fzfinite set of sequential integers df-fz 12895 (𝑀...𝑁) Yes fzval 12896, eluzfz 12906
fz0finite set of sequential nonnegative integers (0...𝑁) Yes nn0fz0 13009, fz0tp 13012
fzohalf-open integer range df-fzo 13038 (𝑀..^𝑁) Yes elfzo 13044, elfzofz 13057
gmore general (suffix); eliminates "is a set" hypotheses No uniexg 7460
grgraph No uhgrf 26862, isumgr 26895, usgrres1 27112
grpgroup df-grp 18106 Grp Yes isgrp 18109, tgpgrp 22690
gsumgroup sum df-gsum 16716 (𝐺 Σg 𝐹) Yes gsumval 17887, gsumwrev 18494
hashsize (of a set) df-hash 13696 (♯‘𝐴) Yes hashgval 13698, hashfz1 13711, hashcl 13722
hbhypothesis builder (prefix) No hbxfrbi 1826, hbald 2176, hbequid 36154
hm(monoid, group, ring) homomorphism No ismhm 17958, isghm 18358, isrhm 19476
iinference (suffix) No eleq1i 2906, tcsni 9182
iimplication (suffix) No brwdomi 9029, infeq5i 9096
ididentity No biid 264
iedgindexed edge df-iedg 26799 (iEdg‘𝐺) Yes iedgval0 26840, edgiedgb 26854
idmidempotent No anidm 568, tpidm13 4677
im, impimplication (label often omitted) df-im 14460 (𝐴𝐵) Yes iman 405, imnan 403, impbidd 213
imaimage df-ima 5555 (𝐴𝐵) Yes resima 5874, imaundi 5995
impimport No biimpa 480, impcom 411
inintersection df-in 3926 (𝐴𝐵) Yes elin 3935, incom 4163
infinfimum df-inf 8904 inf(ℝ+, ℝ*, < ) Yes fiinfcl 8962, infiso 8969
is...is (something a) ...? No isring 19301
jjoining, disjoining No jc 164, jaoi 854
lleft No olcd 871, simpl 486
mapmapping operation or set exponentiation df-map 8404 (𝐴m 𝐵) Yes mapvalg 8412, elmapex 8423
matmatrix df-mat 21020 (𝑁 Mat 𝑅) Yes matval 21023, matring 21055
mdetdeterminant (of a square matrix) df-mdet 21197 (𝑁 maDet 𝑅) Yes mdetleib 21199, mdetrlin 21214
mgmmagma df-mgm 17852 Magma Yes mgmidmo 17870, mgmlrid 17877, ismgm 17853
mgpmultiplicative group df-mgp 19240 (mulGrp‘𝑅) Yes mgpress 19250, ringmgp 19303
mndmonoid df-mnd 17912 Mnd Yes mndass 17920, mndodcong 18670
mo"there exists at most one" df-mo 2624 ∃*𝑥𝜑 Yes eumo 2664, moim 2628
mpmodus ponens ax-mp 5 No mpd 15, mpi 20
mpomaps-to notation for an operation df-mpo 7154 (𝑥𝐴, 𝑦𝐵𝐶) Yes mpompt 7259, resmpo 7265
mptmodus ponendo tollens No mptnan 1770, mptxor 1771
mptmaps-to notation for a function df-mpt 5133 (𝑥𝐴𝐵) Yes fconstmpt 5601, resmpt 5892
mpt2maps-to notation for an operation (deprecated). We are in the process of replacing mpt2 with mpo in labels. df-mpo 7154 (𝑥𝐴, 𝑦𝐵𝐶) Yes mpompt 7259, resmpo 7265
mulmultiplication (see "t") df-mul 10547 (𝐴 · 𝐵) Yes mulcl 10619, divmul 11299, mulcom 10621, mulass 10623
n, notnot ¬ 𝜑 Yes nan 828, notnotr 132
nenot equaldf-ne 𝐴𝐵 Yes exmidne 3024, neeqtrd 3083
nelnot element ofdf-nel 𝐴𝐵 Yes neli 3120, nnel 3127
ne0not equal to zero (see n0) ≠ 0 No negne0d 10993, ine0 11073, gt0ne0 11103
nf "not free in" (prefix) No nfnd 1859
ngpnormed group df-ngp 23197 NrmGrp Yes isngp 23209, ngptps 23215
nmnorm (on a group or ring) df-nm 23196 (norm‘𝑊) Yes nmval 23203, subgnm 23246
nnpositive integers df-nn 11635 Yes nnsscn 11639, nncn 11642
nn0nonnegative integers df-n0 11895 0 Yes nnnn0 11901, nn0cn 11904
n0not the empty set (see ne0) ≠ ∅ No n0i 4282, vn0 4287, ssn0 4337
OLDold, obsolete (to be removed soon) No 19.43OLD 1885
onordinal number df-on 6182 𝐴 ∈ On Yes elon 6187, 1on 8105 onelon 6203
opordered pair df-op 4557 𝐴, 𝐵 Yes dfopif 4784, opth 5355
oror df-or 845 (𝜑𝜓) Yes orcom 867, anor 980
otordered triple df-ot 4559 𝐴, 𝐵, 𝐶 Yes euotd 5390, fnotovb 7199
ovoperation value df-ov 7152 (𝐴𝐹𝐵) Yes fnotovb 7199, fnovrn 7317
pplus (see "add"), for all-constant theorems df-add 10546 (3 + 2) = 5 Yes 3p2e5 11785
pfxprefix df-pfx 14033 (𝑊 prefix 𝐿) Yes pfxlen 14045, ccatpfx 14063
pmPrincipia Mathematica No pm2.27 42
pmpartial mapping (operation) df-pm 8405 (𝐴pm 𝐵) Yes elpmi 8421, pmsspw 8437
prpair df-pr 4553 {𝐴, 𝐵} Yes elpr 4573, prcom 4653, prid1g 4681, prnz 4697
prm, primeprime (number) df-prm 16014 Yes 1nprm 16021, dvdsprime 16029
pssproper subset df-pss 3938 𝐴𝐵 Yes pssss 4058, sspsstri 4065
q rational numbers ("quotients") df-q 12346 Yes elq 12347
rright No orcd 870, simprl 770
rabrestricted class abstraction df-rab 3142 {𝑥𝐴𝜑} Yes rabswap 3474, df-oprab 7153
ralrestricted universal quantification df-ral 3138 𝑥𝐴𝜑 Yes ralnex 3230, ralrnmpo 7282
rclreverse closure No ndmfvrcl 6692, nnarcl 8238
rereal numbers df-r 10545 Yes recn 10625, 0re 10641
relrelation df-rel 5549 Rel 𝐴 Yes brrelex1 5592, relmpoopab 7785
resrestriction df-res 5554 (𝐴𝐵) Yes opelres 5846, f1ores 6620
reurestricted existential uniqueness df-reu 3140 ∃!𝑥𝐴𝜑 Yes nfreud 3363, reurex 3414
rexrestricted existential quantification df-rex 3139 𝑥𝐴𝜑 Yes rexnal 3232, rexrnmpo 7283
rmorestricted "at most one" df-rmo 3141 ∃*𝑥𝐴𝜑 Yes nfrmod 3364, nrexrmo 3418
rnrange df-rn 5553 ran 𝐴 Yes elrng 5749, rncnvcnv 5791
rng(unital) ring df-ring 19299 Ring Yes ringidval 19253, isring 19301, ringgrp 19302
rotrotation No 3anrot 1097, 3orrot 1089
seliminates need for syllogism (suffix) No ancoms 462
sb(proper) substitution (of a set) df-sb 2071 [𝑦 / 𝑥]𝜑 Yes spsbe 2089, sbimi 2080
sbc(proper) substitution of a class df-sbc 3759 [𝐴 / 𝑥]𝜑 Yes sbc2or 3767, sbcth 3773
scascalar df-sca 16581 (Scalar‘𝐻) Yes resssca 16650, mgpsca 19246
simpsimple, simplification No simpl 486, simp3r3 1280
snsingleton df-sn 4551 {𝐴} Yes eldifsn 4704
spspecialization No spsbe 2089, spei 2414
sssubset df-ss 3936 𝐴𝐵 Yes difss 4094
structstructure df-struct 16485 Struct Yes brstruct 16492, structfn 16500
subsubtract df-sub 10870 (𝐴𝐵) Yes subval 10875, subaddi 10971
supsupremum df-sup 8903 sup(𝐴, 𝐵, < ) Yes fisupcl 8930, supmo 8913
suppsupport (of a function) df-supp 7827 (𝐹 supp 𝑍) Yes ressuppfi 8856, mptsuppd 7849
swapswap (two parts within a theorem) No rabswap 3474, 2reuswap 3723
sylsyllogism syl 17 No 3syl 18
symsymmetric No df-symdif 4204, cnvsym 5961
symgsymmetric group df-symg 18496 (SymGrp‘𝐴) Yes symghash 18506, pgrpsubgsymg 18537
t times (see "mul"), for all-constant theorems df-mul 10547 (3 · 2) = 6 Yes 3t2e6 11800
th, t theorem No nfth 1803, sbcth 3773, weth 9915, ancomst 468
tptriple df-tp 4555 {𝐴, 𝐵, 𝐶} Yes eltpi 4610, tpeq1 4663
trtransitive No bitrd 282, biantr 805
tru, t true, truth df-tru 1541 Yes bitru 1547, truanfal 1572, biimt 364
ununion df-un 3924 (𝐴𝐵) Yes uneqri 4113, uncom 4115
unitunit (in a ring) df-unit 19395 (Unit‘𝑅) Yes isunit 19410, nzrunit 20040
v setvar (especially for specializations of theorems when a class is replaced by a setvar variable) x Yes cv 1537, vex 3483, velpw 4527, vtoclf 3544
v disjoint variable condition used in place of nonfreeness hypothesis (suffix) No spimv 2410
vtx vertex df-vtx 26798 (Vtx‘𝐺) Yes vtxval0 26839, opvtxov 26805
vv two disjoint variable conditions used in place of nonfreeness hypotheses (suffix) No 19.23vv 1945
wweak (version of a theorem) (suffix) No ax11w 2135, spnfw 1985
wrdword df-word 13867 Word 𝑆 Yes iswrdb 13872, wrdfn 13880, ffz0iswrd 13893
xpcross product (Cartesian product) df-xp 5548 (𝐴 × 𝐵) Yes elxp 5565, opelxpi 5579, xpundi 5607
xreXtended reals df-xr 10677 * Yes ressxr 10683, rexr 10685, 0xr 10686
z integers (from German "Zahlen") df-z 11979 Yes elz 11980, zcn 11983
zn ring of integers mod 𝑁 df-zn 20207 (ℤ/nℤ‘𝑁) Yes znval 20234, zncrng 20243, znhash 20257
zringring of integers df-zring 20171 ring Yes zringbas 20176, zringcrng 20172
0, z slashed zero (empty set) df-nul 4277 Yes n0i 4282, vn0 4287; snnz 4696, prnz 4697

(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