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

The following gives conventions used in the Metamath Proof Explorer (MPE, set.mm) regarding labels. For other conventions, see conventions 29344 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 3066"rgen.1 $e |- ( x e. A -> ph ) $." or letters corresponding to the (main) class variable used in the hypothesis, e.g., for mdet0 21955: "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 2662 and stirling 44320.
  • 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 1841, and the restricted quantifier version of Theorem 21 from Section 19 of [Margaris] p. 90 is labeled r19.21 3237.
  • 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... 15766. 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 3913, and thus its syntax label fragment is "dif". Similarly, the subclass relation 𝐴𝐵 has syntax label fragment "ss" because it is defined in df-ss 3927. 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 4091. There are many other syntax label fragments, e.g., singleton construct {𝐴} has syntax label fragment "sn" (because it is defined in df-sn 4587), and the pair construct {𝐴, 𝐵} has fragment "pr" ( from df-pr 4589). 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 4747. 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 11057) and "re" represents real numbers (Definition df-r 11061). The empty set often uses fragment 0, even though it is defined in df-nul 4283. The syntax construct (𝐴 + 𝐵) usually uses the fragment "add" (which is consistent with df-add 11062), 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 12288.
  • 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 16032 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 15953) we have value cosval 16005 and closure coscl 16009.
  • 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 29347 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 1942 versus 19.21 2200. This often permits to prove the result using fewer axioms, and/or to eliminate a nonfreeness hypothesis (such as 𝑥𝜑 in 19.21 2200). If no constraint is put on axiom use, then the v-version can be proved from the original theorem using nfv 1917. If two (resp. three) such disjoint variable conditions are added, then the suffix "vv" (resp. "vvv") is used, e.g., exlimivv 1935. 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 2574 derived from eu6 2572. 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 5406. 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 2407 (cbval 2396 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 3510. 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 3144
ablAbelian group df-abl 19565 Abel Yes ablgrp 19567, zringabl 20873
absabsorption No ressabs 17130
absabsolute value (of a complex number) df-abs 15121 (abs‘𝐴) Yes absval 15123, absneg 15162, abs1 15182
adadding No adantr 481, ad2antlr 725
addadd (see "p") df-add 11062 (𝐴 + 𝐵) Yes addcl 11133, addcom 11341, addass 11138
al"for all" 𝑥𝜑 No alim 1812, alex 1828
ALTalternative/less preferred (suffix) No idALT 23
anand df-an 397 (𝜑𝜓) Yes anor 981, iman 402, imnan 400
antantecedent No adantr 481
assassociative No biass 385, orass 920, mulass 11139
asymasymmetric, antisymmetric No intasym 6069, asymref 6070, posasymb 18208
axaxiom No ax6dgen 2124, ax1cn 11085
bas, base base (set of an extensible structure) df-base 17084 (Base‘𝑆) Yes baseval 17085, ressbas 17118, cnfldbas 20800
b, bibiconditional ("iff", "if and only if") df-bi 206 (𝜑𝜓) Yes impbid 211, sspwb 5406
brbinary relation df-br 5106 𝐴𝑅𝐵 Yes brab1 5153, brun 5156
cbvchange bound variable No cbvalivw 2010, cbvrex 3336
cdmcodomain No ffvelcdm 7032, focdmex 7888
clclosure No ifclda 4521, ovrcl 7398, zaddcl 12543
cncomplex numbers df-c 11057 Yes nnsscn 12158, nncn 12161
cnfldfield of complex numbers df-cnfld 20797 fld Yes cnfldbas 20800, cnfldinv 20828
cntzcentralizer df-cntz 19097 (Cntz‘𝑀) Yes cntzfval 19100, dprdfcntz 19794
cnvconverse df-cnv 5641 𝐴 Yes opelcnvg 5836, f1ocnv 6796
cocomposition df-co 5642 (𝐴𝐵) Yes cnvco 5841, fmptco 7075
comcommutative No orcom 868, bicomi 223, eqcomi 2745
concontradiction, contraposition No condan 816, con2d 134
csbclass substitution df-csb 3856 𝐴 / 𝑥𝐵 Yes csbid 3868, csbie2g 3898
cygcyclic group df-cyg 19655 CycGrp Yes iscyg 19656, zringcyg 20890
ddeduction form (suffix) No idd 24, impbid 211
df(alternate) definition (prefix) No dfrel2 6141, dffn2 6670
di, distrdistributive No andi 1006, imdi 390, ordi 1004, difindi 4241, ndmovdistr 7543
difclass difference df-dif 3913 (𝐴𝐵) Yes difss 4091, difindi 4241
divdivision df-div 11813 (𝐴 / 𝐵) Yes divcl 11819, divval 11815, divmul 11816
dmdomain df-dm 5643 dom 𝐴 Yes dmmpt 6192, iswrddm0 14426
e, eq, equequals (equ for setvars, eq for classes) df-cleq 2728 𝐴 = 𝐵 Yes 2p2e4 12288, uneqri 4111, equtr 2024
edgedge df-edg 27999 (Edg‘𝐺) Yes edgopval 28002, usgredgppr 28144
elelement of 𝐴𝐵 Yes eldif 3920, eldifsn 4747, elssuni 4898
enequinumerous df-en 𝐴𝐵 Yes domen 8901, enfi 9134
eu"there exists exactly one" eu6 2572 ∃!𝑥𝜑 Yes euex 2575, euabsn 4687
exexists (i.e. is a set) ∈ V No brrelex1 5685, 0ex 5264
ex, e"there exists (at least one)" df-ex 1782 𝑥𝜑 Yes exim 1836, alex 1828
expexport No expt 177, expcom 414
f"not free in" (suffix) No equs45f 2457, sbf 2262
ffunction df-f 6500 𝐹:𝐴𝐵 Yes fssxp 6696, opelf 6703
falfalse df-fal 1554 Yes bifal 1557, falantru 1576
fifinite intersection df-fi 9347 (fi‘𝐵) Yes fival 9348, inelfi 9354
fi, finfinite df-fin 8887 Fin Yes isfi 8916, snfi 8988, onfin 9174
fldfield (Note: there is an alternative definition Fld of a field, see df-fld 36451) df-field 20188 Field Yes isfld 20196, fldidom 20775
fnfunction with domain df-fn 6499 𝐴 Fn 𝐵 Yes ffn 6668, fndm 6605
frgpfree group df-frgp 19492 (freeGrp‘𝐼) Yes frgpval 19540, frgpadd 19545
fsuppfinitely supported function df-fsupp 9306 𝑅 finSupp 𝑍 Yes isfsupp 9309, fdmfisuppfi 9314, fsuppco 9338
funfunction df-fun 6498 Fun 𝐹 Yes funrel 6518, ffun 6671
fvfunction value df-fv 6504 (𝐹𝐴) Yes fvres 6861, swrdfv 14536
fzfinite set of sequential integers df-fz 13425 (𝑀...𝑁) Yes fzval 13426, eluzfz 13436
fz0finite set of sequential nonnegative integers (0...𝑁) Yes nn0fz0 13539, fz0tp 13542
fzohalf-open integer range df-fzo 13568 (𝑀..^𝑁) Yes elfzo 13574, elfzofz 13588
gmore general (suffix); eliminates "is a set" hypotheses No uniexg 7677
grgraph No uhgrf 28013, isumgr 28046, usgrres1 28263
grpgroup df-grp 18751 Grp Yes isgrp 18754, tgpgrp 23429
gsumgroup sum df-gsum 17324 (𝐺 Σg 𝐹) Yes gsumval 18532, gsumwrev 19147
hashsize (of a set) df-hash 14231 (♯‘𝐴) Yes hashgval 14233, hashfz1 14246, hashcl 14256
hbhypothesis builder (prefix) No hbxfrbi 1827, hbald 2168, hbequid 37371
hm(monoid, group, ring) homomorphism No ismhm 18603, isghm 19008, isrhm 20152
iinference (suffix) No eleq1i 2828, tcsni 9679
iimplication (suffix) No brwdomi 9504, infeq5i 9572
ididentity No biid 260
iedgindexed edge df-iedg 27950 (iEdg‘𝐺) Yes iedgval0 27991, edgiedgb 28005
idmidempotent No anidm 565, tpidm13 4717
im, impimplication (label often omitted) df-im 14986 (𝐴𝐵) Yes iman 402, imnan 400, impbidd 209
imaimage df-ima 5646 (𝐴𝐵) Yes resima 5971, imaundi 6102
impimport No biimpa 477, impcom 408
inintersection df-in 3917 (𝐴𝐵) Yes elin 3926, incom 4161
infinfimum df-inf 9379 inf(ℝ+, ℝ*, < ) Yes fiinfcl 9437, infiso 9444
is...is (something a) ...? No isring 19968
jjoining, disjoining No jc 161, jaoi 855
lleft No olcd 872, simpl 483
mapmapping operation or set exponentiation df-map 8767 (𝐴m 𝐵) Yes mapvalg 8775, elmapex 8786
matmatrix df-mat 21755 (𝑁 Mat 𝑅) Yes matval 21758, matring 21792
mdetdeterminant (of a square matrix) df-mdet 21934 (𝑁 maDet 𝑅) Yes mdetleib 21936, mdetrlin 21951
mgmmagma df-mgm 18497 Magma Yes mgmidmo 18515, mgmlrid 18522, ismgm 18498
mgpmultiplicative group df-mgp 19897 (mulGrp‘𝑅) Yes mgpress 19911, ringmgp 19970
mndmonoid df-mnd 18557 Mnd Yes mndass 18565, mndodcong 19324
mo"there exists at most one" df-mo 2538 ∃*𝑥𝜑 Yes eumo 2576, moim 2542
mpmodus ponens ax-mp 5 No mpd 15, mpi 20
mpomaps-to notation for an operation df-mpo 7362 (𝑥𝐴, 𝑦𝐵𝐶) Yes mpompt 7470, resmpo 7476
mptmodus ponendo tollens No mptnan 1770, mptxor 1771
mptmaps-to notation for a function df-mpt 5189 (𝑥𝐴𝐵) Yes fconstmpt 5694, resmpt 5991
mpt2maps-to notation for an operation (deprecated). We are in the process of replacing mpt2 with mpo in labels. df-mpo 7362 (𝑥𝐴, 𝑦𝐵𝐶) Yes mpompt 7470, resmpo 7476
mulmultiplication (see "t") df-mul 11063 (𝐴 · 𝐵) Yes mulcl 11135, divmul 11816, mulcom 11137, mulass 11139
n, notnot ¬ 𝜑 Yes nan 828, notnotr 130
nenot equaldf-ne 𝐴𝐵 Yes exmidne 2953, neeqtrd 3013
nelnot element ofdf-nel 𝐴𝐵 Yes neli 3051, nnel 3058
ne0not equal to zero (see n0) ≠ 0 No negne0d 11510, ine0 11590, gt0ne0 11620
nf "not free in" (prefix) No nfnd 1861
ngpnormed group df-ngp 23939 NrmGrp Yes isngp 23952, ngptps 23958
nmnorm (on a group or ring) df-nm 23938 (norm‘𝑊) Yes nmval 23945, subgnm 23989
nnpositive integers df-nn 12154 Yes nnsscn 12158, nncn 12161
nn0nonnegative integers df-n0 12414 0 Yes nnnn0 12420, nn0cn 12423
n0not the empty set (see ne0) ≠ ∅ No n0i 4293, vn0 4298, ssn0 4360
OLDold, obsolete (to be removed soon) No 19.43OLD 1886
onordinal number df-on 6321 𝐴 ∈ On Yes elon 6326, 1on 8424 onelon 6342
opordered pair df-op 4593 𝐴, 𝐵 Yes dfopif 4827, opth 5433
oror df-or 846 (𝜑𝜓) Yes orcom 868, anor 981
otordered triple df-ot 4595 𝐴, 𝐵, 𝐶 Yes euotd 5470, fnotovb 7407
ovoperation value df-ov 7360 (𝐴𝐹𝐵) Yes fnotovb 7407, fnovrn 7529
pplus (see "add"), for all-constant theorems df-add 11062 (3 + 2) = 5 Yes 3p2e5 12304
pfxprefix df-pfx 14559 (𝑊 prefix 𝐿) Yes pfxlen 14571, ccatpfx 14589
pmPrincipia Mathematica No pm2.27 42
pmpartial mapping (operation) df-pm 8768 (𝐴pm 𝐵) Yes elpmi 8784, pmsspw 8815
prpair df-pr 4589 {𝐴, 𝐵} Yes elpr 4609, prcom 4693, prid1g 4721, prnz 4738
prm, primeprime (number) df-prm 16548 Yes 1nprm 16555, dvdsprime 16563
pssproper subset df-pss 3929 𝐴𝐵 Yes pssss 4055, sspsstri 4062
q rational numbers ("quotients") df-q 12874 Yes elq 12875
rright No orcd 871, simprl 769
rabrestricted class abstraction df-rab 3408 {𝑥𝐴𝜑} Yes rabswap 3416, df-oprab 7361
ralrestricted universal quantification df-ral 3065 𝑥𝐴𝜑 Yes ralnex 3075, ralrnmpo 7494
rclreverse closure No ndmfvrcl 6878, nnarcl 8563
rereal numbers df-r 11061 Yes recn 11141, 0re 11157
relrelation df-rel 5640 Rel 𝐴 Yes brrelex1 5685, relmpoopab 8026
resrestriction df-res 5645 (𝐴𝐵) Yes opelres 5943, f1ores 6798
reurestricted existential uniqueness df-reu 3354 ∃!𝑥𝐴𝜑 Yes nfreud 3404, reurex 3357
rexrestricted existential quantification df-rex 3074 𝑥𝐴𝜑 Yes rexnal 3103, rexrnmpo 7495
rmorestricted "at most one" df-rmo 3353 ∃*𝑥𝐴𝜑 Yes nfrmod 3403, nrexrmo 3374
rnrange df-rn 5644 ran 𝐴 Yes elrng 5847, rncnvcnv 5889
ring(unital) ring df-ring 19966 Ring Yes ringidval 19915, isring 19968, ringgrp 19969
rngnon-unital ring df-rng 46163 Rng Yes isrng 46164, rngabl 46165, rnglz 46172
rotrotation No 3anrot 1100, 3orrot 1092
seliminates need for syllogism (suffix) No ancoms 459
sb(proper) substitution (of a set) df-sb 2068 [𝑦 / 𝑥]𝜑 Yes spsbe 2085, sbimi 2077
sbc(proper) substitution of a class df-sbc 3740 [𝐴 / 𝑥]𝜑 Yes sbc2or 3748, sbcth 3754
scascalar df-sca 17149 (Scalar‘𝐻) Yes resssca 17224, mgpsca 19904
simpsimple, simplification No simpl 483, simp3r3 1283
snsingleton df-sn 4587 {𝐴} Yes eldifsn 4747
spspecialization No spsbe 2085, spei 2392
sssubset df-ss 3927 𝐴𝐵 Yes difss 4091
structstructure df-struct 17019 Struct Yes brstruct 17020, structfn 17028
subsubtract df-sub 11387 (𝐴𝐵) Yes subval 11392, subaddi 11488
supsupremum df-sup 9378 sup(𝐴, 𝐵, < ) Yes fisupcl 9405, supmo 9388
suppsupport (of a function) df-supp 8093 (𝐹 supp 𝑍) Yes ressuppfi 9331, mptsuppd 8118
swapswap (two parts within a theorem) No rabswap 3416, 2reuswap 3704
sylsyllogism syl 17 No 3syl 18
symsymmetric No df-symdif 4202, cnvsym 6066
symgsymmetric group df-symg 19149 (SymGrp‘𝐴) Yes symghash 19159, pgrpsubgsymg 19191
t times (see "mul"), for all-constant theorems df-mul 11063 (3 · 2) = 6 Yes 3t2e6 12319
th, t theorem No nfth 1803, sbcth 3754, weth 10431, ancomst 465
tptriple df-tp 4591 {𝐴, 𝐵, 𝐶} Yes eltpi 4648, tpeq1 4703
trtransitive No bitrd 278, biantr 804
tru, t true, truth df-tru 1544 Yes bitru 1550, truanfal 1575, biimt 360
ununion df-un 3915 (𝐴𝐵) Yes uneqri 4111, uncom 4113
unitunit (in a ring) df-unit 20071 (Unit‘𝑅) Yes isunit 20086, nzrunit 20737
v setvar (especially for specializations of theorems when a class is replaced by a setvar variable) x Yes cv 1540, vex 3449, velpw 4565, vtoclf 3516
v disjoint variable condition used in place of nonfreeness hypothesis (suffix) No spimv 2388
vtx vertex df-vtx 27949 (Vtx‘𝐺) Yes vtxval0 27990, opvtxov 27956
vv two disjoint variable conditions used in place of nonfreeness hypotheses (suffix) No 19.23vv 1946
wweak (version of a theorem) (suffix) No ax11w 2126, spnfw 1983
wrdword df-word 14403 Word 𝑆 Yes iswrdb 14408, wrdfn 14416, ffz0iswrd 14429
xpcross product (Cartesian product) df-xp 5639 (𝐴 × 𝐵) Yes elxp 5656, opelxpi 5670, xpundi 5700
xreXtended reals df-xr 11193 * Yes ressxr 11199, rexr 11201, 0xr 11202
z integers (from German "Zahlen") df-z 12500 Yes elz 12501, zcn 12504
zn ring of integers mod 𝑁 df-zn 20907 (ℤ/nℤ‘𝑁) Yes znval 20938, zncrng 20951, znhash 20965
zringring of integers df-zring 20870 ring Yes zringbas 20875, zringcrng 20871
0, z slashed zero (empty set) df-nul 4283 Yes n0i 4293, vn0 4298; snnz 4737, prnz 4738

(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