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 30420
Description:

The following gives conventions used in the Metamath Proof Explorer (MPE, set.mm) regarding labels. For other conventions, see conventions 30419 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 3063"rgen.1 $e |- ( x e. A -> ph ) $." or letters corresponding to the (main) class variable used in the hypothesis, e.g., for mdet0 22612: "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 2663 and stirling 46104.
  • 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 1839, and the restricted quantifier version of Theorem 21 from Section 19 of [Margaris] p. 90 is labeled r19.21 3254.
  • 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... 15917. 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 3954, and thus its syntax label fragment is "dif". Similarly, the subclass relation 𝐴𝐵 has syntax label fragment "ss" because it is defined in df-ss 3968. 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 4136. There are many other syntax label fragments, e.g., singleton construct {𝐴} has syntax label fragment "sn" (because it is defined in df-sn 4627), and the pair construct {𝐴, 𝐵} has fragment "pr" ( from df-pr 4629). 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 830.
  • 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 11161) and "re" represents real numbers (Definition df-r 11165). The empty set often uses fragment 0, even though it is defined in df-nul 4334. The syntax construct (𝐴 + 𝐵) usually uses the fragment "add" (which is consistent with df-add 11166), 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 12401.
  • 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 16186 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 16106) we have value cosval 16159 and closure coscl 16163.
  • 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 30422 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 1939 versus 19.21 2207. This often permits to prove the result using fewer axioms, and/or to eliminate a nonfreeness hypothesis (such as 𝑥𝜑 in 19.21 2207). If no constraint is put on axiom use, then the v-version can be proved from the original theorem using nfv 1914. If two (resp. three) such disjoint variable conditions are added, then the suffix "vv" (resp. "vvv") is used, e.g., exlimivv 1932. 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 2576 derived from eu6 2574. 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 5454. 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 2414 (cbval 2403 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 3560. Here is a non-exhaustive list of common suffixes:
    • a : theorem having a conjunction as antecedent
    • b : theorem expressing a logical equivalence
    • c : contraction (e.g., sylc 65, syl2anc 584), commutes (e.g., biimpac 478)
    • d : theorem in deduction form
    • f : theorem with a hypothesis such as 𝑥𝜑
    • g : theorem in closed form having an "is a set" antecedent
    • i : theorem in inference form
    • l : theorem concerning something at the left
    • r : theorem concerning something at the right
    • r : theorem with something reversed (e.g., a biconditional)
    • s : inference that manipulates an antecedent ("s" refers to an application of syl 17 that is eliminated)
    • t : theorem in closed form (not having an "is a set" antecedent)
    • v : theorem with one (main) disjoint variable condition
    • vv : theorem with two (main) disjoint variable conditions
    • w : weak(er) form of a theorem
    • ALT : alternate proof of a theorem
    • ALTV : alternate version of a theorem or definition (mathbox only)
    • OLD : old/obsolete version of a theorem (or proof) or definition
  • Reuse. When creating a new theorem or axiom, try to reuse abbreviations used elsewhere. A comment should explain the first use of an abbreviation.

The following table shows some commonly used abbreviations in labels, in alphabetical order. For each abbreviation we provide a mnenomic, the source theorem or the assumption defining it, an expression showing what it looks like, whether or not it is a "syntax fragment" (an abbreviation that indicates a particular kind of syntax), and hyperlinks to label examples that use the abbreviation. The abbreviation is bolded if there is a df-NAME definition but the label fragment is not NAME. This is not a complete list of abbreviations, though we do want this to eventually be a complete list of exceptions.

AbbreviationMnenomicSource ExpressionSyntax?Example(s)
aand (suffix) No biimpa 476, rexlimiva 3147
ablAbelian group df-abl 19801 Abel Yes ablgrp 19803, zringabl 21462
absabsorption No ressabs 17294
absabsolute value (of a complex number) df-abs 15275 (abs‘𝐴) Yes absval 15277, absneg 15316, abs1 15336
adadding No adantr 480, ad2antlr 727
addadd (see "p") df-add 11166 (𝐴 + 𝐵) Yes addcl 11237, addcom 11447, addass 11242
al"for all" 𝑥𝜑 No alim 1810, alex 1826
ALTalternative/less preferred (suffix) No idALT 23
anand df-an 396 (𝜑𝜓) Yes anor 985, iman 401, imnan 399
antantecedent No adantr 480
assassociative No biass 384, orass 922, mulass 11243
asymasymmetric, antisymmetric No intasym 6135, asymref 6136, posasymb 18365
axaxiom No ax6dgen 2128, ax1cn 11189
bas, base base (set of an extensible structure) df-base 17248 (Base‘𝑆) Yes baseval 17249, ressbas 17280, cnfldbas 21368
b, bibiconditional ("iff", "if and only if") df-bi 207 (𝜑𝜓) Yes impbid 212, sspwb 5454
brbinary relation df-br 5144 𝐴𝑅𝐵 Yes brab1 5191, brun 5194
ccommutes, commuted (suffix) No biimpac 478
ccontraction (suffix) No sylc 65, syl2anc 584
cbvchange bound variable No cbvalivw 2006, cbvrex 3363
cdmcodomain No ffvelcdm 7101, focdmex 7980
clclosure No ifclda 4561, ovrcl 7472, zaddcl 12657
cncomplex numbers df-c 11161 Yes nnsscn 12271, nncn 12274
cnfldfield of complex numbers df-cnfld 21365 fld Yes cnfldbas 21368, cnfldinv 21415
cntzcentralizer df-cntz 19335 (Cntz‘𝑀) Yes cntzfval 19338, dprdfcntz 20035
cnvconverse df-cnv 5693 𝐴 Yes opelcnvg 5891, f1ocnv 6860
cocomposition df-co 5694 (𝐴𝐵) Yes cnvco 5896, fmptco 7149
comcommutative No orcom 871, bicomi 224, eqcomi 2746
concontradiction, contraposition No condan 818, con2d 134
csbclass substitution df-csb 3900 𝐴 / 𝑥𝐵 Yes csbid 3912, csbie2g 3939
cygcyclic group df-cyg 19896 CycGrp Yes iscyg 19897, zringcyg 21480
ddeduction form (suffix) No idd 24, impbid 212
df(alternate) definition (prefix) No dfrel2 6209, dffn2 6738
di, distrdistributive No andi 1010, imdi 389, ordi 1008, difindi 4292, ndmovdistr 7622
difclass difference df-dif 3954 (𝐴𝐵) Yes difss 4136, difindi 4292
divdivision df-div 11921 (𝐴 / 𝐵) Yes divcl 11928, divval 11924, divmul 11925
dmdomain df-dm 5695 dom 𝐴 Yes dmmpt 6260, iswrddm0 14576
e, eq, equequals (equ for setvars, eq for classes) df-cleq 2729 𝐴 = 𝐵 Yes 2p2e4 12401, uneqri 4156, equtr 2020
edgedge df-edg 29065 (Edg‘𝐺) Yes edgopval 29068, usgredgppr 29213
elelement of 𝐴𝐵 Yes eldif 3961, eldifsn 4786, elssuni 4937
enequinumerous df-en 𝐴𝐵 Yes domen 9002, enfi 9227
eu"there exists exactly one" eu6 2574 ∃!𝑥𝜑 Yes euex 2577, euabsn 4726
exexists (i.e. is a set) ∈ V No brrelex1 5738, 0ex 5307
ex, e"there exists (at least one)" df-ex 1780 𝑥𝜑 Yes exim 1834, alex 1826
expexport No expt 177, expcom 413
f"not free in" (suffix) No equs45f 2464, sbf 2271
ffunction df-f 6565 𝐹:𝐴𝐵 Yes fssxp 6763, opelf 6769
falfalse df-fal 1553 Yes bifal 1556, falantru 1575
fifinite intersection df-fi 9451 (fi‘𝐵) Yes fival 9452, inelfi 9458
fi, finfinite df-fin 8989 Fin Yes isfi 9016, snfi 9083, onfin 9267
fldfield (Note: there is an alternative definition Fld of a field, see df-fld 37999) df-field 20732 Field Yes isfld 20740, fldidom 20771
fnfunction with domain df-fn 6564 𝐴 Fn 𝐵 Yes ffn 6736, fndm 6671
frgpfree group df-frgp 19728 (freeGrp‘𝐼) Yes frgpval 19776, frgpadd 19781
fsuppfinitely supported function df-fsupp 9402 𝑅 finSupp 𝑍 Yes isfsupp 9405, fdmfisuppfi 9414, fsuppco 9442
funfunction df-fun 6563 Fun 𝐹 Yes funrel 6583, ffun 6739
fvfunction value df-fv 6569 (𝐹𝐴) Yes fvres 6925, swrdfv 14686
fzfinite set of sequential integers df-fz 13548 (𝑀...𝑁) Yes fzval 13549, eluzfz 13559
fz0finite set of sequential nonnegative integers (0...𝑁) Yes nn0fz0 13665, fz0tp 13668
fzohalf-open integer range df-fzo 13695 (𝑀..^𝑁) Yes elfzo 13701, elfzofz 13715
gmore general (suffix); eliminates "is a set" hypotheses No uniexg 7760
grgraph No uhgrf 29079, isumgr 29112, usgrres1 29332
grpgroup df-grp 18954 Grp Yes isgrp 18957, tgpgrp 24086
gsumgroup sum df-gsum 17487 (𝐺 Σg 𝐹) Yes gsumval 18690, gsumwrev 19385
hashsize (of a set) df-hash 14370 (♯‘𝐴) Yes hashgval 14372, hashfz1 14385, hashcl 14395
hbhypothesis builder (prefix) No hbxfrbi 1825, hbald 2168, hbequid 38910
hm(monoid, group, ring, ...) homomorphism No ismhm 18798, isghm 19233, isrhm 20478
iinference (suffix) No eleq1i 2832, tcsni 9783
iimplication (suffix) No brwdomi 9608, infeq5i 9676
ididentity No biid 261
iedgindexed edge df-iedg 29016 (iEdg‘𝐺) Yes iedgval0 29057, edgiedgb 29071
idmidempotent No anidm 564, tpidm13 4756
im, impimplication (label often omitted) df-im 15140 (𝐴𝐵) Yes iman 401, imnan 399, impbidd 210
im(group, ring, ...) isomorphism No isgim 19280, rimrcl 20482
imaimage df-ima 5698 (𝐴𝐵) Yes resima 6033, imaundi 6169
impimport No biimpa 476, impcom 407
inintersection df-in 3958 (𝐴𝐵) Yes elin 3967, incom 4209
infinfimum df-inf 9483 inf(ℝ+, ℝ*, < ) Yes fiinfcl 9541, infiso 9548
is...is (something a) ...? No isring 20234
jjoining, disjoining No jc 161, jaoi 858
lleft No olcd 875, simpl 482
mapmapping operation or set exponentiation df-map 8868 (𝐴m 𝐵) Yes mapvalg 8876, elmapex 8888
matmatrix df-mat 22412 (𝑁 Mat 𝑅) Yes matval 22415, matring 22449
mdetdeterminant (of a square matrix) df-mdet 22591 (𝑁 maDet 𝑅) Yes mdetleib 22593, mdetrlin 22608
mgmmagma df-mgm 18653 Magma Yes mgmidmo 18673, mgmlrid 18680, ismgm 18654
mgpmultiplicative group df-mgp 20138 (mulGrp‘𝑅) Yes mgpress 20147, ringmgp 20236
mndmonoid df-mnd 18748 Mnd Yes mndass 18756, mndodcong 19560
mo"there exists at most one" df-mo 2540 ∃*𝑥𝜑 Yes eumo 2578, moim 2544
mpmodus ponens ax-mp 5 No mpd 15, mpi 20
mpomaps-to notation for an operation df-mpo 7436 (𝑥𝐴, 𝑦𝐵𝐶) Yes mpompt 7547, resmpo 7553
mptmodus ponendo tollens No mptnan 1768, mptxor 1769
mptmaps-to notation for a function df-mpt 5226 (𝑥𝐴𝐵) Yes fconstmpt 5747, resmpt 6055
mulmultiplication (see "t") df-mul 11167 (𝐴 · 𝐵) Yes mulcl 11239, divmul 11925, mulcom 11241, mulass 11243
n, notnot ¬ 𝜑 Yes nan 830, notnotr 130
nenot equaldf-ne 𝐴𝐵 Yes exmidne 2950, neeqtrd 3010
nelnot element ofdf-nel 𝐴𝐵 Yes neli 3048, nnel 3056
ne0not equal to zero (see n0) ≠ 0 No negne0d 11618, ine0 11698, gt0ne0 11728
nf "not free in" (prefix) df-nf 1784 𝑥𝜑 Yes nfnd 1858
ngpnormed group df-ngp 24596 NrmGrp Yes isngp 24609, ngptps 24615
nmnorm (on a group or ring) df-nm 24595 (norm‘𝑊) Yes nmval 24602, subgnm 24646
nnpositive integers df-nn 12267 Yes nnsscn 12271, nncn 12274
nn0nonnegative integers df-n0 12527 0 Yes nnnn0 12533, nn0cn 12536
n0not the empty set (see ne0) ≠ ∅ No n0i 4340, vn0 4345, ssn0 4404
OLDold, obsolete (to be removed soon) No 19.43OLD 1883
onordinal number df-on 6388 𝐴 ∈ On Yes elon 6393, 1on 8518 onelon 6409
opordered pair df-op 4633 𝐴, 𝐵 Yes dfopif 4870, opth 5481
oror df-or 849 (𝜑𝜓) Yes orcom 871, anor 985
otordered triple df-ot 4635 𝐴, 𝐵, 𝐶 Yes euotd 5518, fnotovb 7483
ovoperation value df-ov 7434 (𝐴𝐹𝐵) Yes fnotovb 7483, fnovrn 7608
pplus (see "add"), for all-constant theorems df-add 11166 (3 + 2) = 5 Yes 3p2e5 12417
pfxprefix df-pfx 14709 (𝑊 prefix 𝐿) Yes pfxlen 14721, ccatpfx 14739
pmPrincipia Mathematica No pm2.27 42
pmpartial mapping (operation) df-pm 8869 (𝐴pm 𝐵) Yes elpmi 8886, pmsspw 8917
prpair df-pr 4629 {𝐴, 𝐵} Yes elpr 4650, prcom 4732, prid1g 4760, prnz 4777
prm, primeprime (number) df-prm 16709 Yes 1nprm 16716, dvdsprime 16724
pssproper subset df-pss 3971 𝐴𝐵 Yes pssss 4098, sspsstri 4105
q rational numbers ("quotients") df-q 12991 Yes elq 12992
rreversed (suffix) No pm4.71r 558, caovdir 7667
rright No orcd 874, simprl 771
rabrestricted class abstraction df-rab 3437 {𝑥𝐴𝜑} Yes rabswap 3446, df-oprab 7435
ralrestricted universal quantification df-ral 3062 𝑥𝐴𝜑 Yes ralnex 3072, ralrnmpo 7572
rclreverse closure No ndmfvrcl 6942, nnarcl 8654
rereal numbers df-r 11165 Yes recn 11245, 0re 11263
relrelation df-rel 5692 Rel 𝐴 Yes brrelex1 5738, relmpoopab 8119
resrestriction df-res 5697 (𝐴𝐵) Yes opelres 6003, f1ores 6862
reurestricted existential uniqueness df-reu 3381 ∃!𝑥𝐴𝜑 Yes nfreud 3433, reurex 3384
rexrestricted existential quantification df-rex 3071 𝑥𝐴𝜑 Yes rexnal 3100, rexrnmpo 7573
rmorestricted "at most one" df-rmo 3380 ∃*𝑥𝐴𝜑 Yes nfrmod 3432, nrexrmo 3401
rnrange df-rn 5696 ran 𝐴 Yes elrng 5902, rncnvcnv 5945
ring(unital) ring df-ring 20232 Ring Yes ringidval 20180, isring 20234, ringgrp 20235
rngnon-unital ring df-rng 20150 Rng Yes isrng 20151, rngabl 20152, rnglz 20162
rotrotation No 3anrot 1100, 3orrot 1092
seliminates need for syllogism (suffix) No ancoms 458
sb(proper) substitution (of a set) df-sb 2065 [𝑦 / 𝑥]𝜑 Yes spsbe 2082, sbimi 2074
sbc(proper) substitution of a class df-sbc 3789 [𝐴 / 𝑥]𝜑 Yes sbc2or 3797, sbcth 3803
scascalar df-sca 17313 (Scalar‘𝐻) Yes resssca 17387, mgpsca 20143
simpsimple, simplification No simpl 482, simp3r3 1284
snsingleton df-sn 4627 {𝐴} Yes eldifsn 4786
spspecialization No spsbe 2082, spei 2399
sssubset df-ss 3968 𝐴𝐵 Yes difss 4136
structstructure df-struct 17184 Struct Yes brstruct 17185, structfn 17193
subsubtract df-sub 11494 (𝐴𝐵) Yes subval 11499, subaddi 11596
supsupremum df-sup 9482 sup(𝐴, 𝐵, < ) Yes fisupcl 9509, supmo 9492
suppsupport (of a function) df-supp 8186 (𝐹 supp 𝑍) Yes ressuppfi 9435, mptsuppd 8212
swapswap (two parts within a theorem) No rabswap 3446, 2reuswap 3752
sylsyllogism syl 17 No 3syl 18
symsymmetric No df-symdif 4253, cnvsym 6132
symgsymmetric group df-symg 19387 (SymGrp‘𝐴) Yes symghash 19395, pgrpsubgsymg 19427
t times (see "mul"), for all-constant theorems df-mul 11167 (3 · 2) = 6 Yes 3t2e6 12432
th, t theorem No nfth 1801, sbcth 3803, weth 10535, ancomst 464
tptriple df-tp 4631 {𝐴, 𝐵, 𝐶} Yes eltpi 4688, tpeq1 4742
trtransitive No bitrd 279, biantr 806
tru, t true, truth df-tru 1543 Yes bitru 1549, truanfal 1574, biimt 360
ununion df-un 3956 (𝐴𝐵) Yes uneqri 4156, uncom 4158
unitunit (in a ring) df-unit 20358 (Unit‘𝑅) Yes isunit 20373, nzrunit 20524
v setvar (especially for specializations of theorems when a class is replaced by a setvar variable) x Yes cv 1539, vex 3484, velpw 4605, vtoclf 3564
v disjoint variable condition used in place of nonfreeness hypothesis (suffix) No spimv 2395
vtx vertex df-vtx 29015 (Vtx‘𝐺) Yes vtxval0 29056, opvtxov 29022
vv two disjoint variable conditions used in place of nonfreeness hypotheses (suffix) No 19.23vv 1943
wweak (version of a theorem) (suffix) No ax11w 2130, spnfw 1979
wrdword df-word 14553 Word 𝑆 Yes iswrdb 14558, wrdfn 14566, ffz0iswrd 14579
xpcross product (Cartesian product) df-xp 5691 (𝐴 × 𝐵) Yes elxp 5708, opelxpi 5722, xpundi 5754
xreXtended reals df-xr 11299 * Yes ressxr 11305, rexr 11307, 0xr 11308
z integers (from German "Zahlen") df-z 12614 Yes elz 12615, zcn 12618
zn ring of integers mod 𝑁 df-zn 21517 (ℤ/nℤ‘𝑁) Yes znval 21550, zncrng 21563, znhash 21577
zringring of integers df-zring 21458 ring Yes zringbas 21464, zringcrng 21459
0, z slashed zero (empty set) df-nul 4334 Yes n0i 4340, vn0 4345; 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