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

The following gives conventions used in the Metamath Proof Explorer (MPE, set.mm) regarding labels. For other conventions, see conventions 30282 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 3052"rgen.1 $e |- ( x e. A -> ph ) $." or letters corresponding to the (main) class variable used in the hypothesis, e.g., for mdet0 22552: "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 2651 and stirling 45615.
  • 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 1833, and the restricted quantifier version of Theorem 21 from Section 19 of [Margaris] p. 90 is labeled r19.21 3241.
  • 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... 15863. 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 4128. There are many other syntax label fragments, e.g., singleton construct {𝐴} has syntax label fragment "sn" (because it is defined in df-sn 4631), and the pair construct {𝐴, 𝐵} has fragment "pr" ( from df-pr 4633). 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 4792. 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 11146) and "re" represents real numbers (Definition df-r 11150). The empty set often uses fragment 0, even though it is defined in df-nul 4323. The syntax construct (𝐴 + 𝐵) usually uses the fragment "add" (which is consistent with df-add 11151), 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 12380.
  • 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 16130 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 16050) we have value cosval 16103 and closure coscl 16107.
  • 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 30285 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 1934 versus 19.21 2195. This often permits to prove the result using fewer axioms, and/or to eliminate a nonfreeness hypothesis (such as 𝑥𝜑 in 19.21 2195). If no constraint is put on axiom use, then the v-version can be proved from the original theorem using nfv 1909. If two (resp. three) such disjoint variable conditions are added, then the suffix "vv" (resp. "vvv") is used, e.g., exlimivv 1927. 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 2564 derived from eu6 2562. 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 5451. 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 2402 (cbval 2391 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 3537. 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 582), commutes (e.g., biimpac 477)
    • 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 475, rexlimiva 3136
ablAbelian group df-abl 19750 Abel Yes ablgrp 19752, zringabl 21394
absabsorption No ressabs 17233
absabsolute value (of a complex number) df-abs 15219 (abs‘𝐴) Yes absval 15221, absneg 15260, abs1 15280
adadding No adantr 479, ad2antlr 725
addadd (see "p") df-add 11151 (𝐴 + 𝐵) Yes addcl 11222, addcom 11432, addass 11227
al"for all" 𝑥𝜑 No alim 1804, alex 1820
ALTalternative/less preferred (suffix) No idALT 23
anand df-an 395 (𝜑𝜓) Yes anor 980, iman 400, imnan 398
antantecedent No adantr 479
assassociative No biass 383, orass 919, mulass 11228
asymasymmetric, antisymmetric No intasym 6122, asymref 6123, posasymb 18314
axaxiom No ax6dgen 2116, ax1cn 11174
bas, base base (set of an extensible structure) df-base 17184 (Base‘𝑆) Yes baseval 17185, ressbas 17218, cnfldbas 21300
b, bibiconditional ("iff", "if and only if") df-bi 206 (𝜑𝜓) Yes impbid 211, sspwb 5451
brbinary relation df-br 5150 𝐴𝑅𝐵 Yes brab1 5197, brun 5200
ccommutes, commuted (suffix) No biimpac 477
ccontraction (suffix) No sylc 65, syl2anc 582
cbvchange bound variable No cbvalivw 2002, cbvrex 3346
cdmcodomain No ffvelcdm 7090, focdmex 7960
clclosure No ifclda 4565, ovrcl 7460, zaddcl 12635
cncomplex numbers df-c 11146 Yes nnsscn 12250, nncn 12253
cnfldfield of complex numbers df-cnfld 21297 fld Yes cnfldbas 21300, cnfldinv 21347
cntzcentralizer df-cntz 19280 (Cntz‘𝑀) Yes cntzfval 19283, dprdfcntz 19984
cnvconverse df-cnv 5686 𝐴 Yes opelcnvg 5883, f1ocnv 6850
cocomposition df-co 5687 (𝐴𝐵) Yes cnvco 5888, fmptco 7138
comcommutative No orcom 868, bicomi 223, eqcomi 2734
concontradiction, contraposition No condan 816, con2d 134
csbclass substitution df-csb 3890 𝐴 / 𝑥𝐵 Yes csbid 3902, csbie2g 3932
cygcyclic group df-cyg 19845 CycGrp Yes iscyg 19846, zringcyg 21412
ddeduction form (suffix) No idd 24, impbid 211
df(alternate) definition (prefix) No dfrel2 6195, dffn2 6725
di, distrdistributive No andi 1005, imdi 388, ordi 1003, difindi 4280, ndmovdistr 7610
difclass difference df-dif 3947 (𝐴𝐵) Yes difss 4128, difindi 4280
divdivision df-div 11904 (𝐴 / 𝐵) Yes divcl 11911, divval 11907, divmul 11908
dmdomain df-dm 5688 dom 𝐴 Yes dmmpt 6246, iswrddm0 14524
e, eq, equequals (equ for setvars, eq for classes) df-cleq 2717 𝐴 = 𝐵 Yes 2p2e4 12380, uneqri 4148, equtr 2016
edgedge df-edg 28933 (Edg‘𝐺) Yes edgopval 28936, usgredgppr 29081
elelement of 𝐴𝐵 Yes eldif 3954, eldifsn 4792, elssuni 4941
enequinumerous df-en 𝐴𝐵 Yes domen 8982, enfi 9215
eu"there exists exactly one" eu6 2562 ∃!𝑥𝜑 Yes euex 2565, euabsn 4732
exexists (i.e. is a set) ∈ V No brrelex1 5731, 0ex 5308
ex, e"there exists (at least one)" df-ex 1774 𝑥𝜑 Yes exim 1828, alex 1820
expexport No expt 177, expcom 412
f"not free in" (suffix) No equs45f 2452, sbf 2257
ffunction df-f 6553 𝐹:𝐴𝐵 Yes fssxp 6751, opelf 6758
falfalse df-fal 1546 Yes bifal 1549, falantru 1568
fifinite intersection df-fi 9436 (fi‘𝐵) Yes fival 9437, inelfi 9443
fi, finfinite df-fin 8968 Fin Yes isfi 8997, snfi 9069, onfin 9255
fldfield (Note: there is an alternative definition Fld of a field, see df-fld 37596) df-field 20639 Field Yes isfld 20647, fldidom 21275
fnfunction with domain df-fn 6552 𝐴 Fn 𝐵 Yes ffn 6723, fndm 6658
frgpfree group df-frgp 19677 (freeGrp‘𝐼) Yes frgpval 19725, frgpadd 19730
fsuppfinitely supported function df-fsupp 9388 𝑅 finSupp 𝑍 Yes isfsupp 9391, fdmfisuppfi 9399, fsuppco 9427
funfunction df-fun 6551 Fun 𝐹 Yes funrel 6571, ffun 6726
fvfunction value df-fv 6557 (𝐹𝐴) Yes fvres 6915, swrdfv 14634
fzfinite set of sequential integers df-fz 13520 (𝑀...𝑁) Yes fzval 13521, eluzfz 13531
fz0finite set of sequential nonnegative integers (0...𝑁) Yes nn0fz0 13634, fz0tp 13637
fzohalf-open integer range df-fzo 13663 (𝑀..^𝑁) Yes elfzo 13669, elfzofz 13683
gmore general (suffix); eliminates "is a set" hypotheses No uniexg 7746
grgraph No uhgrf 28947, isumgr 28980, usgrres1 29200
grpgroup df-grp 18901 Grp Yes isgrp 18904, tgpgrp 24026
gsumgroup sum df-gsum 17427 (𝐺 Σg 𝐹) Yes gsumval 18640, gsumwrev 19332
hashsize (of a set) df-hash 14326 (♯‘𝐴) Yes hashgval 14328, hashfz1 14341, hashcl 14351
hbhypothesis builder (prefix) No hbxfrbi 1819, hbald 2157, hbequid 38511
hm(monoid, group, ring, ...) homomorphism No ismhm 18745, isghm 19178, isrhm 20429
iinference (suffix) No eleq1i 2816, tcsni 9768
iimplication (suffix) No brwdomi 9593, infeq5i 9661
ididentity No biid 260
iedgindexed edge df-iedg 28884 (iEdg‘𝐺) Yes iedgval0 28925, edgiedgb 28939
idmidempotent No anidm 563, tpidm13 4762
im, impimplication (label often omitted) df-im 15084 (𝐴𝐵) Yes iman 400, imnan 398, impbidd 209
im(group, ring, ...) isomorphism No isgim 19225, rimrcl 20433
imaimage df-ima 5691 (𝐴𝐵) Yes resima 6020, imaundi 6156
impimport No biimpa 475, impcom 406
inintersection df-in 3951 (𝐴𝐵) Yes elin 3960, incom 4199
infinfimum df-inf 9468 inf(ℝ+, ℝ*, < ) Yes fiinfcl 9526, infiso 9533
is...is (something a) ...? No isring 20189
jjoining, disjoining No jc 161, jaoi 855
lleft No olcd 872, simpl 481
mapmapping operation or set exponentiation df-map 8847 (𝐴m 𝐵) Yes mapvalg 8855, elmapex 8867
matmatrix df-mat 22352 (𝑁 Mat 𝑅) Yes matval 22355, matring 22389
mdetdeterminant (of a square matrix) df-mdet 22531 (𝑁 maDet 𝑅) Yes mdetleib 22533, mdetrlin 22548
mgmmagma df-mgm 18603 Magma Yes mgmidmo 18623, mgmlrid 18630, ismgm 18604
mgpmultiplicative group df-mgp 20087 (mulGrp‘𝑅) Yes mgpress 20101, ringmgp 20191
mndmonoid df-mnd 18698 Mnd Yes mndass 18706, mndodcong 19509
mo"there exists at most one" df-mo 2528 ∃*𝑥𝜑 Yes eumo 2566, moim 2532
mpmodus ponens ax-mp 5 No mpd 15, mpi 20
mpomaps-to notation for an operation df-mpo 7424 (𝑥𝐴, 𝑦𝐵𝐶) Yes mpompt 7534, resmpo 7540
mptmodus ponendo tollens No mptnan 1762, mptxor 1763
mptmaps-to notation for a function df-mpt 5233 (𝑥𝐴𝐵) Yes fconstmpt 5740, resmpt 6042
mpt2maps-to notation for an operation (deprecated). We are in the process of replacing mpt2 with mpo in labels. df-mpo 7424 (𝑥𝐴, 𝑦𝐵𝐶) Yes mpompt 7534, resmpo 7540
mulmultiplication (see "t") df-mul 11152 (𝐴 · 𝐵) Yes mulcl 11224, divmul 11908, mulcom 11226, mulass 11228
n, notnot ¬ 𝜑 Yes nan 828, notnotr 130
nenot equaldf-ne 𝐴𝐵 Yes exmidne 2939, neeqtrd 2999
nelnot element ofdf-nel 𝐴𝐵 Yes neli 3037, nnel 3045
ne0not equal to zero (see n0) ≠ 0 No negne0d 11601, ine0 11681, gt0ne0 11711
nf "not free in" (prefix) df-nf 1778 𝑥𝜑 Yes nfnd 1853
ngpnormed group df-ngp 24536 NrmGrp Yes isngp 24549, ngptps 24555
nmnorm (on a group or ring) df-nm 24535 (norm‘𝑊) Yes nmval 24542, subgnm 24586
nnpositive integers df-nn 12246 Yes nnsscn 12250, nncn 12253
nn0nonnegative integers df-n0 12506 0 Yes nnnn0 12512, nn0cn 12515
n0not the empty set (see ne0) ≠ ∅ No n0i 4333, vn0 4338, ssn0 4402
OLDold, obsolete (to be removed soon) No 19.43OLD 1878
onordinal number df-on 6375 𝐴 ∈ On Yes elon 6380, 1on 8499 onelon 6396
opordered pair df-op 4637 𝐴, 𝐵 Yes dfopif 4872, opth 5478
oror df-or 846 (𝜑𝜓) Yes orcom 868, anor 980
otordered triple df-ot 4639 𝐴, 𝐵, 𝐶 Yes euotd 5515, fnotovb 7470
ovoperation value df-ov 7422 (𝐴𝐹𝐵) Yes fnotovb 7470, fnovrn 7596
pplus (see "add"), for all-constant theorems df-add 11151 (3 + 2) = 5 Yes 3p2e5 12396
pfxprefix df-pfx 14657 (𝑊 prefix 𝐿) Yes pfxlen 14669, ccatpfx 14687
pmPrincipia Mathematica No pm2.27 42
pmpartial mapping (operation) df-pm 8848 (𝐴pm 𝐵) Yes elpmi 8865, pmsspw 8896
prpair df-pr 4633 {𝐴, 𝐵} Yes elpr 4654, prcom 4738, prid1g 4766, prnz 4783
prm, primeprime (number) df-prm 16646 Yes 1nprm 16653, dvdsprime 16661
pssproper subset df-pss 3964 𝐴𝐵 Yes pssss 4091, sspsstri 4098
q rational numbers ("quotients") df-q 12966 Yes elq 12967
rreversed (suffix) No pm4.71r 557, caovdir 7655
rright No orcd 871, simprl 769
rabrestricted class abstraction df-rab 3419 {𝑥𝐴𝜑} Yes rabswap 3428, df-oprab 7423
ralrestricted universal quantification df-ral 3051 𝑥𝐴𝜑 Yes ralnex 3061, ralrnmpo 7560
rclreverse closure No ndmfvrcl 6932, nnarcl 8637
rereal numbers df-r 11150 Yes recn 11230, 0re 11248
relrelation df-rel 5685 Rel 𝐴 Yes brrelex1 5731, relmpoopab 8099
resrestriction df-res 5690 (𝐴𝐵) Yes opelres 5991, f1ores 6852
reurestricted existential uniqueness df-reu 3364 ∃!𝑥𝐴𝜑 Yes nfreud 3415, reurex 3367
rexrestricted existential quantification df-rex 3060 𝑥𝐴𝜑 Yes rexnal 3089, rexrnmpo 7561
rmorestricted "at most one" df-rmo 3363 ∃*𝑥𝐴𝜑 Yes nfrmod 3414, nrexrmo 3384
rnrange df-rn 5689 ran 𝐴 Yes elrng 5894, rncnvcnv 5936
ring(unital) ring df-ring 20187 Ring Yes ringidval 20135, isring 20189, ringgrp 20190
rngnon-unital ring df-rng 20105 Rng Yes isrng 20106, rngabl 20107, rnglz 20117
rotrotation No 3anrot 1097, 3orrot 1089
seliminates need for syllogism (suffix) No ancoms 457
sb(proper) substitution (of a set) df-sb 2060 [𝑦 / 𝑥]𝜑 Yes spsbe 2077, sbimi 2069
sbc(proper) substitution of a class df-sbc 3774 [𝐴 / 𝑥]𝜑 Yes sbc2or 3782, sbcth 3788
scascalar df-sca 17252 (Scalar‘𝐻) Yes resssca 17327, mgpsca 20094
simpsimple, simplification No simpl 481, simp3r3 1280
snsingleton df-sn 4631 {𝐴} Yes eldifsn 4792
spspecialization No spsbe 2077, spei 2387
sssubset df-ss 3961 𝐴𝐵 Yes difss 4128
structstructure df-struct 17119 Struct Yes brstruct 17120, structfn 17128
subsubtract df-sub 11478 (𝐴𝐵) Yes subval 11483, subaddi 11579
supsupremum df-sup 9467 sup(𝐴, 𝐵, < ) Yes fisupcl 9494, supmo 9477
suppsupport (of a function) df-supp 8166 (𝐹 supp 𝑍) Yes ressuppfi 9420, mptsuppd 8192
swapswap (two parts within a theorem) No rabswap 3428, 2reuswap 3738
sylsyllogism syl 17 No 3syl 18
symsymmetric No df-symdif 4241, cnvsym 6119
symgsymmetric group df-symg 19334 (SymGrp‘𝐴) Yes symghash 19344, pgrpsubgsymg 19376
t times (see "mul"), for all-constant theorems df-mul 11152 (3 · 2) = 6 Yes 3t2e6 12411
th, t theorem No nfth 1795, sbcth 3788, weth 10520, ancomst 463
tptriple df-tp 4635 {𝐴, 𝐵, 𝐶} Yes eltpi 4693, tpeq1 4748
trtransitive No bitrd 278, biantr 804
tru, t true, truth df-tru 1536 Yes bitru 1542, truanfal 1567, biimt 359
ununion df-un 3949 (𝐴𝐵) Yes uneqri 4148, uncom 4150
unitunit (in a ring) df-unit 20309 (Unit‘𝑅) Yes isunit 20324, nzrunit 20473
v setvar (especially for specializations of theorems when a class is replaced by a setvar variable) x Yes cv 1532, vex 3465, velpw 4609, vtoclf 3542
v disjoint variable condition used in place of nonfreeness hypothesis (suffix) No spimv 2383
vtx vertex df-vtx 28883 (Vtx‘𝐺) Yes vtxval0 28924, opvtxov 28890
vv two disjoint variable conditions used in place of nonfreeness hypotheses (suffix) No 19.23vv 1938
wweak (version of a theorem) (suffix) No ax11w 2118, spnfw 1975
wrdword df-word 14501 Word 𝑆 Yes iswrdb 14506, wrdfn 14514, ffz0iswrd 14527
xpcross product (Cartesian product) df-xp 5684 (𝐴 × 𝐵) Yes elxp 5701, opelxpi 5715, xpundi 5746
xreXtended reals df-xr 11284 * Yes ressxr 11290, rexr 11292, 0xr 11293
z integers (from German "Zahlen") df-z 12592 Yes elz 12593, zcn 12596
zn ring of integers mod 𝑁 df-zn 21449 (ℤ/nℤ‘𝑁) Yes znval 21482, zncrng 21495, znhash 21509
zringring of integers df-zring 21390 ring Yes zringbas 21396, zringcrng 21391
0, z slashed zero (empty set) df-nul 4323 Yes n0i 4333, vn0 4338; snnz 4782, prnz 4783

(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