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

The following gives conventions used in the Metamath Proof Explorer (MPE, set.mm) regarding labels. For other conventions, see conventions 28900 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 3064"rgen.1 $e |- ( x e. A -> ph ) $." or letters corresponding to the (main) class variable used in the hypothesis, e.g., for mdet0 21838: "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 43880.
  • 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 3234.
  • 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... 15672. 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 3900, and thus its syntax label fragment is "dif". Similarly, the subclass relation 𝐴𝐵 has syntax label fragment "ss" because it is defined in df-ss 3914. 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 4077. There are many other syntax label fragments, e.g., singleton construct {𝐴} has syntax label fragment "sn" (because it is defined in df-sn 4572), and the pair construct {𝐴, 𝐵} has fragment "pr" ( from df-pr 4574). 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 4732. An "n" is often used for negation (¬), e.g., nan 827.
  • 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 10957) and "re" represents real numbers (Definition df-r 10961). The empty set often uses fragment 0, even though it is defined in df-nul 4268. The syntax construct (𝐴 + 𝐵) usually uses the fragment "add" (which is consistent with df-add 10962), 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 12188.
  • 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 15938 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 15859) we have value cosval 15911 and closure coscl 15915.
  • 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 28903 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 2199. This often permits to prove the result using fewer axioms, and/or to eliminate a nonfreeness hypothesis (such as 𝑥𝜑 in 19.21 2199). 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 2575 derived from eu6 2573. 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 5384. 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 2408 (cbval 2397 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 3502. 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 479)
    • d : theorem in deduction form
    • f : theorem with a hypothesis such as 𝑥𝜑
    • g : theorem in closed form having an "is a set" antecedent
    • i : theorem in inference form
    • l : theorem concerning something at the left
    • r : theorem concerning something at the right
    • r : theorem with something reversed (e.g., a biconditional)
    • s : inference that manipulates an antecedent ("s" refers to an application of syl 17 that is eliminated)
    • t : theorem in closed form (not having an "is a set" antecedent)
    • v : theorem with one (main) disjoint variable condition
    • vv : theorem with two (main) disjoint variable conditions
    • w : weak(er) form of a theorem
    • ALT : alternate proof of a theorem
    • ALTV : alternate version of a theorem or definition (mathbox only)
    • OLD : old/obsolete version of a theorem (or proof) or definition
  • Reuse. When creating a new theorem or axiom, try to reuse abbreviations used elsewhere. A comment should explain the first use of an abbreviation.

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

AbbreviationMnenomicSource ExpressionSyntax?Example(s)
aand (suffix) No biimpa 477, rexlimiva 3141
ablAbelian group df-abl 19464 Abel Yes ablgrp 19466, zringabl 20757
absabsorption No ressabs 17036
absabsolute value (of a complex number) df-abs 15026 (abs‘𝐴) Yes absval 15028, absneg 15068, abs1 15088
adadding No adantr 481, ad2antlr 724
addadd (see "p") df-add 10962 (𝐴 + 𝐵) Yes addcl 11033, addcom 11241, addass 11038
al"for all" 𝑥𝜑 No alim 1811, alex 1827
ALTalternative/less preferred (suffix) No idALT 23
anand df-an 397 (𝜑𝜓) Yes anor 980, iman 402, imnan 400
antantecedent No adantr 481
assassociative No biass 385, orass 919, mulass 11039
asymasymmetric, antisymmetric No intasym 6043, asymref 6044, posasymb 18114
axaxiom No ax6dgen 2123, ax1cn 10985
bas, base base (set of an extensible structure) df-base 16990 (Base‘𝑆) Yes baseval 16991, ressbas 17024, cnfldbas 20684
b, bibiconditional ("iff", "if and only if") df-bi 206 (𝜑𝜓) Yes impbid 211, sspwb 5384
brbinary relation df-br 5088 𝐴𝑅𝐵 Yes brab1 5135, brun 5138
cbvchange bound variable No cbvalivw 2009, cbvrex 3333
cdmcodomain No ffvelcdm 6999, focdmex 7845
clclosure No ifclda 4506, ovrcl 7358, zaddcl 12440
cncomplex numbers df-c 10957 Yes nnsscn 12058, nncn 12061
cnfldfield of complex numbers df-cnfld 20681 fld Yes cnfldbas 20684, cnfldinv 20712
cntzcentralizer df-cntz 18999 (Cntz‘𝑀) Yes cntzfval 19002, dprdfcntz 19693
cnvconverse df-cnv 5616 𝐴 Yes opelcnvg 5810, f1ocnv 6766
cocomposition df-co 5617 (𝐴𝐵) Yes cnvco 5815, fmptco 7041
comcommutative No orcom 867, bicomi 223, eqcomi 2746
concontradiction, contraposition No condan 815, con2d 134
csbclass substitution df-csb 3843 𝐴 / 𝑥𝐵 Yes csbid 3855, csbie2g 3885
cygcyclic group df-cyg 19553 CycGrp Yes iscyg 19554, zringcyg 20774
ddeduction form (suffix) No idd 24, impbid 211
df(alternate) definition (prefix) No dfrel2 6115, dffn2 6640
di, distrdistributive No andi 1005, imdi 390, ordi 1003, difindi 4226, ndmovdistr 7503
difclass difference df-dif 3900 (𝐴𝐵) Yes difss 4077, difindi 4226
divdivision df-div 11713 (𝐴 / 𝐵) Yes divcl 11719, divval 11715, divmul 11716
dmdomain df-dm 5618 dom 𝐴 Yes dmmpt 6166, iswrddm0 14320
e, eq, equequals (equ for setvars, eq for classes) df-cleq 2729 𝐴 = 𝐵 Yes 2p2e4 12188, uneqri 4096, equtr 2023
edgedge df-edg 27554 (Edg‘𝐺) Yes edgopval 27557, usgredgppr 27699
elelement of 𝐴𝐵 Yes eldif 3907, eldifsn 4732, elssuni 4883
enequinumerous df-en 𝐴𝐵 Yes domen 8801, enfi 9034
eu"there exists exactly one" eu6 2573 ∃!𝑥𝜑 Yes euex 2576, euabsn 4672
exexists (i.e. is a set) ∈ V No brrelex1 5659, 0ex 5246
ex, e"there exists (at least one)" df-ex 1781 𝑥𝜑 Yes exim 1835, alex 1827
expexport No expt 177, expcom 414
f"not free in" (suffix) No equs45f 2458, sbf 2262
ffunction df-f 6470 𝐹:𝐴𝐵 Yes fssxp 6666, opelf 6673
falfalse df-fal 1553 Yes bifal 1556, falantru 1575
fifinite intersection df-fi 9247 (fi‘𝐵) Yes fival 9248, inelfi 9254
fi, finfinite df-fin 8787 Fin Yes isfi 8816, snfi 8888, onfin 9074
fldfield (Note: there is an alternative definition Fld of a field, see df-fld 36222) df-field 20073 Field Yes isfld 20081, fldidom 20659
fnfunction with domain df-fn 6469 𝐴 Fn 𝐵 Yes ffn 6638, fndm 6575
frgpfree group df-frgp 19391 (freeGrp‘𝐼) Yes frgpval 19439, frgpadd 19444
fsuppfinitely supported function df-fsupp 9206 𝑅 finSupp 𝑍 Yes isfsupp 9209, fdmfisuppfi 9214, fsuppco 9238
funfunction df-fun 6468 Fun 𝐹 Yes funrel 6488, ffun 6641
fvfunction value df-fv 6474 (𝐹𝐴) Yes fvres 6831, swrdfv 14440
fzfinite set of sequential integers df-fz 13320 (𝑀...𝑁) Yes fzval 13321, eluzfz 13331
fz0finite set of sequential nonnegative integers (0...𝑁) Yes nn0fz0 13434, fz0tp 13437
fzohalf-open integer range df-fzo 13463 (𝑀..^𝑁) Yes elfzo 13469, elfzofz 13483
gmore general (suffix); eliminates "is a set" hypotheses No uniexg 7635
grgraph No uhgrf 27568, isumgr 27601, usgrres1 27818
grpgroup df-grp 18656 Grp Yes isgrp 18659, tgpgrp 23312
gsumgroup sum df-gsum 17230 (𝐺 Σg 𝐹) Yes gsumval 18438, gsumwrev 19049
hashsize (of a set) df-hash 14125 (♯‘𝐴) Yes hashgval 14127, hashfz1 14140, hashcl 14150
hbhypothesis builder (prefix) No hbxfrbi 1826, hbald 2167, hbequid 37143
hm(monoid, group, ring) homomorphism No ismhm 18509, isghm 18910, isrhm 20040
iinference (suffix) No eleq1i 2828, tcsni 9579
iimplication (suffix) No brwdomi 9404, infeq5i 9472
ididentity No biid 260
iedgindexed edge df-iedg 27505 (iEdg‘𝐺) Yes iedgval0 27546, edgiedgb 27560
idmidempotent No anidm 565, tpidm13 4702
im, impimplication (label often omitted) df-im 14891 (𝐴𝐵) Yes iman 402, imnan 400, impbidd 209
imaimage df-ima 5621 (𝐴𝐵) Yes resima 5945, imaundi 6076
impimport No biimpa 477, impcom 408
inintersection df-in 3904 (𝐴𝐵) Yes elin 3913, incom 4146
infinfimum df-inf 9279 inf(ℝ+, ℝ*, < ) Yes fiinfcl 9337, infiso 9344
is...is (something a) ...? No isring 19862
jjoining, disjoining No jc 161, jaoi 854
lleft No olcd 871, simpl 483
mapmapping operation or set exponentiation df-map 8667 (𝐴m 𝐵) Yes mapvalg 8675, elmapex 8686
matmatrix df-mat 21638 (𝑁 Mat 𝑅) Yes matval 21641, matring 21675
mdetdeterminant (of a square matrix) df-mdet 21817 (𝑁 maDet 𝑅) Yes mdetleib 21819, mdetrlin 21834
mgmmagma df-mgm 18403 Magma Yes mgmidmo 18421, mgmlrid 18428, ismgm 18404
mgpmultiplicative group df-mgp 19796 (mulGrp‘𝑅) Yes mgpress 19810, ringmgp 19864
mndmonoid df-mnd 18463 Mnd Yes mndass 18471, mndodcong 19226
mo"there exists at most one" df-mo 2539 ∃*𝑥𝜑 Yes eumo 2577, moim 2543
mpmodus ponens ax-mp 5 No mpd 15, mpi 20
mpomaps-to notation for an operation df-mpo 7322 (𝑥𝐴, 𝑦𝐵𝐶) Yes mpompt 7430, resmpo 7436
mptmodus ponendo tollens No mptnan 1769, mptxor 1770
mptmaps-to notation for a function df-mpt 5171 (𝑥𝐴𝐵) Yes fconstmpt 5668, resmpt 5965
mpt2maps-to notation for an operation (deprecated). We are in the process of replacing mpt2 with mpo in labels. df-mpo 7322 (𝑥𝐴, 𝑦𝐵𝐶) Yes mpompt 7430, resmpo 7436
mulmultiplication (see "t") df-mul 10963 (𝐴 · 𝐵) Yes mulcl 11035, divmul 11716, mulcom 11037, mulass 11039
n, notnot ¬ 𝜑 Yes nan 827, notnotr 130
nenot equaldf-ne 𝐴𝐵 Yes exmidne 2951, neeqtrd 3011
nelnot element ofdf-nel 𝐴𝐵 Yes neli 3049, nnel 3056
ne0not equal to zero (see n0) ≠ 0 No negne0d 11410, ine0 11490, gt0ne0 11520
nf "not free in" (prefix) No nfnd 1860
ngpnormed group df-ngp 23822 NrmGrp Yes isngp 23835, ngptps 23841
nmnorm (on a group or ring) df-nm 23821 (norm‘𝑊) Yes nmval 23828, subgnm 23872
nnpositive integers df-nn 12054 Yes nnsscn 12058, nncn 12061
nn0nonnegative integers df-n0 12314 0 Yes nnnn0 12320, nn0cn 12323
n0not the empty set (see ne0) ≠ ∅ No n0i 4278, vn0 4283, ssn0 4345
OLDold, obsolete (to be removed soon) No 19.43OLD 1885
onordinal number df-on 6293 𝐴 ∈ On Yes elon 6298, 1on 8358 onelon 6314
opordered pair df-op 4578 𝐴, 𝐵 Yes dfopif 4812, opth 5410
oror df-or 845 (𝜑𝜓) Yes orcom 867, anor 980
otordered triple df-ot 4580 𝐴, 𝐵, 𝐶 Yes euotd 5446, fnotovb 7367
ovoperation value df-ov 7320 (𝐴𝐹𝐵) Yes fnotovb 7367, fnovrn 7489
pplus (see "add"), for all-constant theorems df-add 10962 (3 + 2) = 5 Yes 3p2e5 12204
pfxprefix df-pfx 14463 (𝑊 prefix 𝐿) Yes pfxlen 14475, ccatpfx 14493
pmPrincipia Mathematica No pm2.27 42
pmpartial mapping (operation) df-pm 8668 (𝐴pm 𝐵) Yes elpmi 8684, pmsspw 8715
prpair df-pr 4574 {𝐴, 𝐵} Yes elpr 4594, prcom 4678, prid1g 4706, prnz 4723
prm, primeprime (number) df-prm 16454 Yes 1nprm 16461, dvdsprime 16469
pssproper subset df-pss 3916 𝐴𝐵 Yes pssss 4041, sspsstri 4048
q rational numbers ("quotients") df-q 12769 Yes elq 12770
rright No orcd 870, simprl 768
rabrestricted class abstraction df-rab 3405 {𝑥𝐴𝜑} Yes rabswap 3413, df-oprab 7321
ralrestricted universal quantification df-ral 3063 𝑥𝐴𝜑 Yes ralnex 3073, ralrnmpo 7454
rclreverse closure No ndmfvrcl 6845, nnarcl 8497
rereal numbers df-r 10961 Yes recn 11041, 0re 11057
relrelation df-rel 5615 Rel 𝐴 Yes brrelex1 5659, relmpoopab 7981
resrestriction df-res 5620 (𝐴𝐵) Yes opelres 5917, f1ores 6768
reurestricted existential uniqueness df-reu 3351 ∃!𝑥𝐴𝜑 Yes nfreud 3401, reurex 3354
rexrestricted existential quantification df-rex 3072 𝑥𝐴𝜑 Yes rexnal 3100, rexrnmpo 7455
rmorestricted "at most one" df-rmo 3350 ∃*𝑥𝐴𝜑 Yes nfrmod 3400, nrexrmo 3371
rnrange df-rn 5619 ran 𝐴 Yes elrng 5821, rncnvcnv 5863
rng(unital) ring df-ring 19860 Ring Yes ringidval 19814, isring 19862, ringgrp 19863
rotrotation No 3anrot 1099, 3orrot 1091
seliminates need for syllogism (suffix) No ancoms 459
sb(proper) substitution (of a set) df-sb 2067 [𝑦 / 𝑥]𝜑 Yes spsbe 2084, sbimi 2076
sbc(proper) substitution of a class df-sbc 3727 [𝐴 / 𝑥]𝜑 Yes sbc2or 3735, sbcth 3741
scascalar df-sca 17055 (Scalar‘𝐻) Yes resssca 17130, mgpsca 19803
simpsimple, simplification No simpl 483, simp3r3 1282
snsingleton df-sn 4572 {𝐴} Yes eldifsn 4732
spspecialization No spsbe 2084, spei 2393
sssubset df-ss 3914 𝐴𝐵 Yes difss 4077
structstructure df-struct 16925 Struct Yes brstruct 16926, structfn 16934
subsubtract df-sub 11287 (𝐴𝐵) Yes subval 11292, subaddi 11388
supsupremum df-sup 9278 sup(𝐴, 𝐵, < ) Yes fisupcl 9305, supmo 9288
suppsupport (of a function) df-supp 8027 (𝐹 supp 𝑍) Yes ressuppfi 9231, mptsuppd 8052
swapswap (two parts within a theorem) No rabswap 3413, 2reuswap 3691
sylsyllogism syl 17 No 3syl 18
symsymmetric No df-symdif 4187, cnvsym 6040
symgsymmetric group df-symg 19051 (SymGrp‘𝐴) Yes symghash 19061, pgrpsubgsymg 19093
t times (see "mul"), for all-constant theorems df-mul 10963 (3 · 2) = 6 Yes 3t2e6 12219
th, t theorem No nfth 1802, sbcth 3741, weth 10331, ancomst 465
tptriple df-tp 4576 {𝐴, 𝐵, 𝐶} Yes eltpi 4633, tpeq1 4688
trtransitive No bitrd 278, biantr 803
tru, t true, truth df-tru 1543 Yes bitru 1549, truanfal 1574, biimt 360
ununion df-un 3902 (𝐴𝐵) Yes uneqri 4096, uncom 4098
unitunit (in a ring) df-unit 19959 (Unit‘𝑅) Yes isunit 19974, nzrunit 20621
v setvar (especially for specializations of theorems when a class is replaced by a setvar variable) x Yes cv 1539, vex 3445, velpw 4550, vtoclf 3506
v disjoint variable condition used in place of nonfreeness hypothesis (suffix) No spimv 2389
vtx vertex df-vtx 27504 (Vtx‘𝐺) Yes vtxval0 27545, opvtxov 27511
vv two disjoint variable conditions used in place of nonfreeness hypotheses (suffix) No 19.23vv 1945
wweak (version of a theorem) (suffix) No ax11w 2125, spnfw 1982
wrdword df-word 14297 Word 𝑆 Yes iswrdb 14302, wrdfn 14310, ffz0iswrd 14323
xpcross product (Cartesian product) df-xp 5614 (𝐴 × 𝐵) Yes elxp 5631, opelxpi 5645, xpundi 5674
xreXtended reals df-xr 11093 * Yes ressxr 11099, rexr 11101, 0xr 11102
z integers (from German "Zahlen") df-z 12400 Yes elz 12401, zcn 12404
zn ring of integers mod 𝑁 df-zn 20791 (ℤ/nℤ‘𝑁) Yes znval 20822, zncrng 20835, znhash 20849
zringring of integers df-zring 20754 ring Yes zringbas 20759, zringcrng 20755
0, z slashed zero (empty set) df-nul 4268 Yes n0i 4278, vn0 4283; snnz 4722, prnz 4723

(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