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

The following gives conventions used in the Metamath Proof Explorer (MPE, set.mm) regarding labels. For other conventions, see conventions 29386 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 3067"rgen.1 $e |- ( x e. A -> ph ) $." or letters corresponding to the (main) class variable used in the hypothesis, e.g., for mdet0 21971: "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 44404.
  • 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 1842, and the restricted quantifier version of Theorem 21 from Section 19 of [Margaris] p. 90 is labeled r19.21 3240.
  • 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... 15773. 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 3918, and thus its syntax label fragment is "dif". Similarly, the subclass relation 𝐴 βŠ† 𝐡 has syntax label fragment "ss" because it is defined in df-ss 3932. 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 4096. There are many other syntax label fragments, e.g., singleton construct {𝐴} has syntax label fragment "sn" (because it is defined in df-sn 4592), and the pair construct {𝐴, 𝐡} has fragment "pr" ( from df-pr 4594). 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 4752. An "n" is often used for negation (Β¬), e.g., nan 829.
  • 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 11064) and "re" represents real numbers ℝ (Definition df-r 11068). The empty set βˆ… often uses fragment 0, even though it is defined in df-nul 4288. The syntax construct (𝐴 + 𝐡) usually uses the fragment "add" (which is consistent with df-add 11069), 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 12295.
  • 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 16039 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 15960) we have value cosval 16012 and closure coscl 16016.
  • 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 29389 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 1943 versus 19.21 2201. This often permits to prove the result using fewer axioms, and/or to eliminate a nonfreeness hypothesis (such as β„²π‘₯πœ‘ in 19.21 2201). If no constraint is put on axiom use, then the v-version can be proved from the original theorem using nfv 1918. If two (resp. three) such disjoint variable conditions are added, then the suffix "vv" (resp. "vvv") is used, e.g., exlimivv 1936. 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 5411. 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 3513. 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 585), commutes (e.g., biimpac 480)
    • 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 478, rexlimiva 3145
ablAbelian group df-abl 19572 Abel Yes ablgrp 19574, zringabl 20889
absabsorption No ressabs 17137
absabsolute value (of a complex number) df-abs 15128 (absβ€˜π΄) Yes absval 15130, absneg 15169, abs1 15189
adadding No adantr 482, ad2antlr 726
addadd (see "p") df-add 11069 (𝐴 + 𝐡) Yes addcl 11140, addcom 11348, addass 11145
al"for all" βˆ€π‘₯πœ‘ No alim 1813, alex 1829
ALTalternative/less preferred (suffix) No idALT 23
anand df-an 398 (πœ‘ ∧ πœ“) Yes anor 982, iman 403, imnan 401
antantecedent No adantr 482
assassociative No biass 386, orass 921, mulass 11146
asymasymmetric, antisymmetric No intasym 6074, asymref 6075, posasymb 18215
axaxiom No ax6dgen 2125, ax1cn 11092
bas, base base (set of an extensible structure) df-base 17091 (Baseβ€˜π‘†) Yes baseval 17092, ressbas 17125, cnfldbas 20816
b, bibiconditional ("iff", "if and only if") df-bi 206 (πœ‘ ↔ πœ“) Yes impbid 211, sspwb 5411
brbinary relation df-br 5111 𝐴𝑅𝐡 Yes brab1 5158, brun 5161
cbvchange bound variable No cbvalivw 2011, cbvrex 3339
cdmcodomain No ffvelcdm 7037, focdmex 7893
clclosure No ifclda 4526, ovrcl 7403, zaddcl 12550
cncomplex numbers df-c 11064 β„‚ Yes nnsscn 12165, nncn 12168
cnfldfield of complex numbers df-cnfld 20813 β„‚fld Yes cnfldbas 20816, cnfldinv 20844
cntzcentralizer df-cntz 19104 (Cntzβ€˜π‘€) Yes cntzfval 19107, dprdfcntz 19801
cnvconverse df-cnv 5646 ◑𝐴 Yes opelcnvg 5841, f1ocnv 6801
cocomposition df-co 5647 (𝐴 ∘ 𝐡) Yes cnvco 5846, fmptco 7080
comcommutative No orcom 869, bicomi 223, eqcomi 2746
concontradiction, contraposition No condan 817, con2d 134
csbclass substitution df-csb 3861 ⦋𝐴 / π‘₯⦌𝐡 Yes csbid 3873, csbie2g 3903
cygcyclic group df-cyg 19662 CycGrp Yes iscyg 19663, zringcyg 20906
ddeduction form (suffix) No idd 24, impbid 211
df(alternate) definition (prefix) No dfrel2 6146, dffn2 6675
di, distrdistributive No andi 1007, imdi 391, ordi 1005, difindi 4246, ndmovdistr 7548
difclass difference df-dif 3918 (𝐴 βˆ– 𝐡) Yes difss 4096, difindi 4246
divdivision df-div 11820 (𝐴 / 𝐡) Yes divcl 11826, divval 11822, divmul 11823
dmdomain df-dm 5648 dom 𝐴 Yes dmmpt 6197, iswrddm0 14433
e, eq, equequals (equ for setvars, eq for classes) df-cleq 2729 𝐴 = 𝐡 Yes 2p2e4 12295, uneqri 4116, equtr 2025
edgedge df-edg 28041 (Edgβ€˜πΊ) Yes edgopval 28044, usgredgppr 28186
elelement of 𝐴 ∈ 𝐡 Yes eldif 3925, eldifsn 4752, elssuni 4903
enequinumerous df-en 𝐴 β‰ˆ 𝐡 Yes domen 8908, enfi 9141
eu"there exists exactly one" eu6 2573 βˆƒ!π‘₯πœ‘ Yes euex 2576, euabsn 4692
exexists (i.e. is a set) ∈ V No brrelex1 5690, 0ex 5269
ex, e"there exists (at least one)" df-ex 1783 βˆƒπ‘₯πœ‘ Yes exim 1837, alex 1829
expexport No expt 177, expcom 415
f"not free in" (suffix) No equs45f 2458, sbf 2263
ffunction df-f 6505 𝐹:𝐴⟢𝐡 Yes fssxp 6701, opelf 6708
falfalse df-fal 1555 βŠ₯ Yes bifal 1558, falantru 1577
fifinite intersection df-fi 9354 (fiβ€˜π΅) Yes fival 9355, inelfi 9361
fi, finfinite df-fin 8894 Fin Yes isfi 8923, snfi 8995, onfin 9181
fldfield (Note: there is an alternative definition Fld of a field, see df-fld 36480) df-field 20202 Field Yes isfld 20210, fldidom 20791
fnfunction with domain df-fn 6504 𝐴 Fn 𝐡 Yes ffn 6673, fndm 6610
frgpfree group df-frgp 19499 (freeGrpβ€˜πΌ) Yes frgpval 19547, frgpadd 19552
fsuppfinitely supported function df-fsupp 9313 𝑅 finSupp 𝑍 Yes isfsupp 9316, fdmfisuppfi 9321, fsuppco 9345
funfunction df-fun 6503 Fun 𝐹 Yes funrel 6523, ffun 6676
fvfunction value df-fv 6509 (πΉβ€˜π΄) Yes fvres 6866, swrdfv 14543
fzfinite set of sequential integers df-fz 13432 (𝑀...𝑁) Yes fzval 13433, eluzfz 13443
fz0finite set of sequential nonnegative integers (0...𝑁) Yes nn0fz0 13546, fz0tp 13549
fzohalf-open integer range df-fzo 13575 (𝑀..^𝑁) Yes elfzo 13581, elfzofz 13595
gmore general (suffix); eliminates "is a set" hypotheses No uniexg 7682
grgraph No uhgrf 28055, isumgr 28088, usgrres1 28305
grpgroup df-grp 18758 Grp Yes isgrp 18761, tgpgrp 23445
gsumgroup sum df-gsum 17331 (𝐺 Ξ£g 𝐹) Yes gsumval 18539, gsumwrev 19154
hashsize (of a set) df-hash 14238 (β™―β€˜π΄) Yes hashgval 14240, hashfz1 14253, hashcl 14263
hbhypothesis builder (prefix) No hbxfrbi 1828, hbald 2169, hbequid 37400
hm(monoid, group, ring) homomorphism No ismhm 18610, isghm 19015, isrhm 20161
iinference (suffix) No eleq1i 2829, tcsni 9686
iimplication (suffix) No brwdomi 9511, infeq5i 9579
ididentity No biid 261
iedgindexed edge df-iedg 27992 (iEdgβ€˜πΊ) Yes iedgval0 28033, edgiedgb 28047
idmidempotent No anidm 566, tpidm13 4722
im, impimplication (label often omitted) df-im 14993 (𝐴 β†’ 𝐡) Yes iman 403, imnan 401, impbidd 209
imaimage df-ima 5651 (𝐴 β€œ 𝐡) Yes resima 5976, imaundi 6107
impimport No biimpa 478, impcom 409
inintersection df-in 3922 (𝐴 ∩ 𝐡) Yes elin 3931, incom 4166
infinfimum df-inf 9386 inf(ℝ+, ℝ*, < ) Yes fiinfcl 9444, infiso 9451
is...is (something a) ...? No isring 19975
jjoining, disjoining No jc 161, jaoi 856
lleft No olcd 873, simpl 484
mapmapping operation or set exponentiation df-map 8774 (𝐴 ↑m 𝐡) Yes mapvalg 8782, elmapex 8793
matmatrix df-mat 21771 (𝑁 Mat 𝑅) Yes matval 21774, matring 21808
mdetdeterminant (of a square matrix) df-mdet 21950 (𝑁 maDet 𝑅) Yes mdetleib 21952, mdetrlin 21967
mgmmagma df-mgm 18504 Magma Yes mgmidmo 18522, mgmlrid 18529, ismgm 18505
mgpmultiplicative group df-mgp 19904 (mulGrpβ€˜π‘…) Yes mgpress 19918, ringmgp 19977
mndmonoid df-mnd 18564 Mnd Yes mndass 18572, mndodcong 19331
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 7367 (π‘₯ ∈ 𝐴, 𝑦 ∈ 𝐡 ↦ 𝐢) Yes mpompt 7475, resmpo 7481
mptmodus ponendo tollens No mptnan 1771, mptxor 1772
mptmaps-to notation for a function df-mpt 5194 (π‘₯ ∈ 𝐴 ↦ 𝐡) Yes fconstmpt 5699, resmpt 5996
mpt2maps-to notation for an operation (deprecated). We are in the process of replacing mpt2 with mpo in labels. df-mpo 7367 (π‘₯ ∈ 𝐴, 𝑦 ∈ 𝐡 ↦ 𝐢) Yes mpompt 7475, resmpo 7481
mulmultiplication (see "t") df-mul 11070 (𝐴 Β· 𝐡) Yes mulcl 11142, divmul 11823, mulcom 11144, mulass 11146
n, notnot Β¬ πœ‘ Yes nan 829, notnotr 130
nenot equaldf-ne 𝐴 β‰  𝐡 Yes exmidne 2954, neeqtrd 3014
nelnot element ofdf-nel 𝐴 βˆ‰ 𝐡 Yes neli 3052, nnel 3059
ne0not equal to zero (see n0) β‰  0 No negne0d 11517, ine0 11597, gt0ne0 11627
nf "not free in" (prefix) No nfnd 1862
ngpnormed group df-ngp 23955 NrmGrp Yes isngp 23968, ngptps 23974
nmnorm (on a group or ring) df-nm 23954 (normβ€˜π‘Š) Yes nmval 23961, subgnm 24005
nnpositive integers df-nn 12161 β„• Yes nnsscn 12165, nncn 12168
nn0nonnegative integers df-n0 12421 β„•0 Yes nnnn0 12427, nn0cn 12430
n0not the empty set (see ne0) β‰  βˆ… No n0i 4298, vn0 4303, ssn0 4365
OLDold, obsolete (to be removed soon) No 19.43OLD 1887
onordinal number df-on 6326 𝐴 ∈ On Yes elon 6331, 1on 8429 onelon 6347
opordered pair df-op 4598 ⟨𝐴, 𝐡⟩ Yes dfopif 4832, opth 5438
oror df-or 847 (πœ‘ ∨ πœ“) Yes orcom 869, anor 982
otordered triple df-ot 4600 ⟨𝐴, 𝐡, 𝐢⟩ Yes euotd 5475, fnotovb 7412
ovoperation value df-ov 7365 (𝐴𝐹𝐡) Yes fnotovb 7412, fnovrn 7534
pplus (see "add"), for all-constant theorems df-add 11069 (3 + 2) = 5 Yes 3p2e5 12311
pfxprefix df-pfx 14566 (π‘Š prefix 𝐿) Yes pfxlen 14578, ccatpfx 14596
pmPrincipia Mathematica No pm2.27 42
pmpartial mapping (operation) df-pm 8775 (𝐴 ↑pm 𝐡) Yes elpmi 8791, pmsspw 8822
prpair df-pr 4594 {𝐴, 𝐡} Yes elpr 4614, prcom 4698, prid1g 4726, prnz 4743
prm, primeprime (number) df-prm 16555 β„™ Yes 1nprm 16562, dvdsprime 16570
pssproper subset df-pss 3934 𝐴 ⊊ 𝐡 Yes pssss 4060, sspsstri 4067
q rational numbers ("quotients") df-q 12881 β„š Yes elq 12882
rright No orcd 872, simprl 770
rabrestricted class abstraction df-rab 3411 {π‘₯ ∈ 𝐴 ∣ πœ‘} Yes rabswap 3419, df-oprab 7366
ralrestricted universal quantification df-ral 3066 βˆ€π‘₯ ∈ π΄πœ‘ Yes ralnex 3076, ralrnmpo 7499
rclreverse closure No ndmfvrcl 6883, nnarcl 8568
rereal numbers df-r 11068 ℝ Yes recn 11148, 0re 11164
relrelation df-rel 5645 Rel 𝐴 Yes brrelex1 5690, relmpoopab 8031
resrestriction df-res 5650 (𝐴 β†Ύ 𝐡) Yes opelres 5948, f1ores 6803
reurestricted existential uniqueness df-reu 3357 βˆƒ!π‘₯ ∈ π΄πœ‘ Yes nfreud 3407, reurex 3360
rexrestricted existential quantification df-rex 3075 βˆƒπ‘₯ ∈ π΄πœ‘ Yes rexnal 3104, rexrnmpo 7500
rmorestricted "at most one" df-rmo 3356 βˆƒ*π‘₯ ∈ π΄πœ‘ Yes nfrmod 3406, nrexrmo 3377
rnrange df-rn 5649 ran 𝐴 Yes elrng 5852, rncnvcnv 5894
ring(unital) ring df-ring 19973 Ring Yes ringidval 19922, isring 19975, ringgrp 19976
rngnon-unital ring df-rng 46247 Rng Yes isrng 46248, rngabl 46249, rnglz 46256
rotrotation No 3anrot 1101, 3orrot 1093
seliminates need for syllogism (suffix) No ancoms 460
sb(proper) substitution (of a set) df-sb 2069 [𝑦 / π‘₯]πœ‘ Yes spsbe 2086, sbimi 2078
sbc(proper) substitution of a class df-sbc 3745 [𝐴 / π‘₯]πœ‘ Yes sbc2or 3753, sbcth 3759
scascalar df-sca 17156 (Scalarβ€˜π») Yes resssca 17231, mgpsca 19911
simpsimple, simplification No simpl 484, simp3r3 1284
snsingleton df-sn 4592 {𝐴} Yes eldifsn 4752
spspecialization No spsbe 2086, spei 2393
sssubset df-ss 3932 𝐴 βŠ† 𝐡 Yes difss 4096
structstructure df-struct 17026 Struct Yes brstruct 17027, structfn 17035
subsubtract df-sub 11394 (𝐴 βˆ’ 𝐡) Yes subval 11399, subaddi 11495
supsupremum df-sup 9385 sup(𝐴, 𝐡, < ) Yes fisupcl 9412, supmo 9395
suppsupport (of a function) df-supp 8098 (𝐹 supp 𝑍) Yes ressuppfi 9338, mptsuppd 8123
swapswap (two parts within a theorem) No rabswap 3419, 2reuswap 3709
sylsyllogism syl 17 No 3syl 18
symsymmetric No df-symdif 4207, cnvsym 6071
symgsymmetric group df-symg 19156 (SymGrpβ€˜π΄) Yes symghash 19166, pgrpsubgsymg 19198
t times (see "mul"), for all-constant theorems df-mul 11070 (3 Β· 2) = 6 Yes 3t2e6 12326
th, t theorem No nfth 1804, sbcth 3759, weth 10438, ancomst 466
tptriple df-tp 4596 {𝐴, 𝐡, 𝐢} Yes eltpi 4653, tpeq1 4708
trtransitive No bitrd 279, biantr 805
tru, t true, truth df-tru 1545 ⊀ Yes bitru 1551, truanfal 1576, biimt 361
ununion df-un 3920 (𝐴 βˆͺ 𝐡) Yes uneqri 4116, uncom 4118
unitunit (in a ring) df-unit 20078 (Unitβ€˜π‘…) Yes isunit 20093, nzrunit 20753
v setvar (especially for specializations of theorems when a class is replaced by a setvar variable) x Yes cv 1541, vex 3452, velpw 4570, vtoclf 3519
v disjoint variable condition used in place of nonfreeness hypothesis (suffix) No spimv 2389
vtx vertex df-vtx 27991 (Vtxβ€˜πΊ) Yes vtxval0 28032, opvtxov 27998
vv two disjoint variable conditions used in place of nonfreeness hypotheses (suffix) No 19.23vv 1947
wweak (version of a theorem) (suffix) No ax11w 2127, spnfw 1984
wrdword df-word 14410 Word 𝑆 Yes iswrdb 14415, wrdfn 14423, ffz0iswrd 14436
xpcross product (Cartesian product) df-xp 5644 (𝐴 Γ— 𝐡) Yes elxp 5661, opelxpi 5675, xpundi 5705
xreXtended reals df-xr 11200 ℝ* Yes ressxr 11206, rexr 11208, 0xr 11209
z integers (from German "Zahlen") df-z 12507 β„€ Yes elz 12508, zcn 12511
zn ring of integers mod 𝑁 df-zn 20923 (β„€/nβ„€β€˜π‘) Yes znval 20954, zncrng 20967, znhash 20981
zringring of integers df-zring 20886 β„€ring Yes zringbas 20891, zringcrng 20887
0, z slashed zero (empty set) df-nul 4288 βˆ… Yes n0i 4298, vn0 4303; snnz 4742, prnz 4743

(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