MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  conventions-label Structured version   Visualization version   GIF version

Theorem conventions-label 27147

The following explains some of the label conventions in use in the Metamath Proof Explorer (""). For the general conventions, see conventions 27146.

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 2918"rgen.1 $e |- ( x e. A -> ph ) $." or letters corresponding to the (main) class variable used in the hypothesis, e.g. for mdet0 20352: "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 2562 and stirling 39643.
  • 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 1763, and the restricted quantifier version of Theorem 21 from Section 19 of [Margaris] p. 90 is labeled r19.21 2952.
  • 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... 14556. Furthermore, the underscore "_" should not be used.
  • 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 3563, and thus its syntax label fragment is "dif". Similarly, the subclass relation 𝐴𝐵 has syntax label fragment "ss" because it is defined in df-ss 3574. 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 3721. There are many other syntax label fragments, e.g., singleton construct {𝐴} has syntax label fragment "sn" (because it is defined in df-sn 4156), and the pair construct {𝐴, 𝐵} has fragment "pr" ( from df-pr 4158). 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 4294. An "n" is often used for negation (¬), e.g., nan 603.
  • 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 9902) and "re" represents real numbers ( definition df-r 9906). The empty set often uses fragment 0, even though it is defined in df-nul 3898. The syntax construct (𝐴 + 𝐵) usually uses the fragment "add" (which is consistent with df-add 9907), 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 11104.
  • 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 14824 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 labeld "NAMEcl". E.g., for cosine (df-cos 14745) we have value cosval 14797 and closure coscl 14801.
  • 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 27148 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, and searching for it will give you the label.
  • Suffixes. Suffixes are used to indicate the form of a theorem (see above). Additionally, we sometimes suffix with "v" the label of a theorem eliminating a hypothesis such as 𝑥𝜑 in 19.21 2073 via the use of disjoint variable conditions combined with nfv 1840. If two (or three) such hypotheses are eliminated, the suffix "vv" resp. "vvv" is used, e.g. exlimivv 1857. 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 2477 derived from df-eu 2473. 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 4888. 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 2280 (cbval 2270 in deduction form "d" with a not free variable replaced by a disjoint variable condition "v" with a conjunction as antecedent "a"). 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 692), commutes (e.g., biimpac 503)
    • 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)
    • 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
    • OLD : old/obsolete version of a theorem/definition/proof
  • 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 501, rexlimiva 3023
ablAbelian group df-abl 18136 Abel Yes ablgrp 18138, zringabl 19762
absabsorption No ressabs 15879
absabsolute value (of a complex number) df-abs 13926 (abs‘𝐴) Yes absval 13928, absneg 13967, abs1 13987
adadding No adantr 481, ad2antlr 762
addadd (see "p") df-add 9907 (𝐴 + 𝐵) Yes addcl 9978, addcom 10182, addass 9983
al"for all" 𝑥𝜑 No alim 1735, alex 1750
ALTalternative/less preferred (suffix) No idALT 23
anand df-an 386 (𝜑𝜓) Yes anor 510, iman 440, imnan 438
antantecedent No adantr 481
assassociative No biass 374, orass 546, mulass 9984
asymasymmetric, antisymmetric No intasym 5480, asymref 5481, posasymb 16892
axaxiom No ax6dgen 2002, ax1cn 9930
bas, base base (set of an extensible structure) df-base 15805 (Base‘𝑆) Yes baseval 15858, ressbas 15870, cnfldbas 19690
b, bibiconditional ("iff", "if and only if") df-bi 197 (𝜑𝜓) Yes impbid 202, sspwb 4888
brbinary relation df-br 4624 𝐴𝑅𝐵 Yes brab1 4670, brun 4673
cbvchange bound variable No cbvalivw 1931, cbvrex 3160
clclosure No ifclda 4098, ovrcl 6651, zaddcl 11377
cncomplex numbers df-c 9902 Yes nnsscn 10985, nncn 10988
cnfldfield of complex numbers df-cnfld 19687 fld Yes cnfldbas 19690, cnfldinv 19717
cntzcentralizer df-cntz 17690 (Cntz‘𝑀) Yes cntzfval 17693, dprdfcntz 18354
cnvconverse df-cnv 5092 𝐴 Yes opelcnvg 5272, f1ocnv 6116
cocomposition df-co 5093 (𝐴𝐵) Yes cnvco 5278, fmptco 6362
comcommutative No orcom 402, bicomi 214, eqcomi 2630
concontradiction, contraposition No condan 834, con2d 129
csbclass substitution df-csb 3520 𝐴 / 𝑥𝐵 Yes csbid 3527, csbie2g 3550
cygcyclic group df-cyg 18220 CycGrp Yes iscyg 18221, zringcyg 19779
ddeduction form (suffix) No idd 24, impbid 202
df(alternate) definition (prefix) No dfrel2 5552, dffn2 6014
di, distrdistributive No andi 910, imdi 378, ordi 907, difindi 3863, ndmovdistr 6788
difclass difference df-dif 3563 (𝐴𝐵) Yes difss 3721, difindi 3863
divdivision df-div 10645 (𝐴 / 𝐵) Yes divcl 10651, divval 10647, divmul 10648
dmdomain df-dm 5094 dom 𝐴 Yes dmmpt 5599, iswrddm0 13284
e, eq, equequals df-cleq 2614 𝐴 = 𝐵 Yes 2p2e4 11104, uneqri 3739, equtr 1945
edgedge df-edg 25874 (Edg‘𝐺) Yes edgopval 25876, usgredgppr 26015
elelement of 𝐴𝐵 Yes eldif 3570, eldifsn 4294, elssuni 4440
eu"there exists exactly one" df-eu 2473 ∃!𝑥𝜑 Yes euex 2493, euabsn 4238
exexists (i.e. is a set) No brrelex 5126, 0ex 4760
ex"there exists (at least one)" df-ex 1702 𝑥𝜑 Yes exim 1758, alex 1750
expexport No expt 168, expcom 451
f"not free in" (suffix) No equs45f 2349, sbf 2379
ffunction df-f 5861 𝐹:𝐴𝐵 Yes fssxp 6027, opelf 6032
falfalse df-fal 1486 Yes bifal 1494, falantru 1505
fifinite intersection df-fi 8277 (fi‘𝐵) Yes fival 8278, inelfi 8284
fi, finfinite df-fin 7919 Fin Yes isfi 7939, snfi 7998, onfin 8111
fldfield (Note: there is an alternative definition Fld of a field, see df-fld 33462) df-field 18690 Field Yes isfld 18696, fldidom 19245
fnfunction with domain df-fn 5860 𝐴 Fn 𝐵 Yes ffn 6012, fndm 5958
frgpfree group df-frgp 18063 (freeGrp‘𝐼) Yes frgpval 18111, frgpadd 18116
fsuppfinitely supported function df-fsupp 8236 𝑅 finSupp 𝑍 Yes isfsupp 8239, fdmfisuppfi 8244, fsuppco 8267
funfunction df-fun 5859 Fun 𝐹 Yes funrel 5874, ffun 6015
fvfunction value df-fv 5865 (𝐹𝐴) Yes fvres 6174, swrdfv 13378
fzfinite set of sequential integers df-fz 12285 (𝑀...𝑁) Yes fzval 12286, eluzfz 12295
fz0finite set of sequential nonnegative integers (0...𝑁) Yes nn0fz0 12394, fz0tp 12397
fzohalf-open integer range df-fzo 12423 (𝑀..^𝑁) Yes elfzo 12429, elfzofz 12442
gmore general (suffix); eliminates "is a set" hypothsis No uniexg 6920
grgraph No uhgrf 25887, isumgr 25919, usgrres1 26129
grpgroup df-grp 17365 Grp Yes isgrp 17368, tgpgrp 21822
gsumgroup sum df-gsum 16043 (𝐺 Σg 𝐹) Yes gsumval 17211, gsumwrev 17736
hashsize (of a set) df-hash 13074 (#‘𝐴) Yes hashgval 13076, hashfz1 13090, hashcl 13103
hbhypothesis builder (prefix) No hbxfrbi 1749, hbald 2038, hbequid 33713
hm(monoid, group, ring) homomorphism No ismhm 17277, isghm 17600, isrhm 18661
iinference (suffix) No eleq1i 2689, tcsni 8579
iimplication (suffix) No brwdomi 8433, infeq5i 8493
ididentity No biid 251
iedgindexed edge df-iedg 25811 (iEdg‘𝐺) Yes iedgval0 25866, edgiedgb 25879
idmidempotent No anidm 675, tpidm13 4268
im, impimplication (label often omitted) df-im 13791 (𝐴𝐵) Yes iman 440, imnan 438, impbidd 200
imaimage df-ima 5097 (𝐴𝐵) Yes resima 5400, imaundi 5514
impimport No biimpa 501, impcom 446
inintersection df-in 3567 (𝐴𝐵) Yes elin 3780, incom 3789
infinfimum df-inf 8309 inf(ℝ+, ℝ*, < ) Yes fiinfcl 8367, infiso 8373 (something a) ...? No isring 18491
jjoining, disjoining No jc 159, jaoi 394
lleft No olcd 408, simpl 473
mapmapping operation or set exponentiation df-map 7819 (𝐴𝑚 𝐵) Yes mapvalg 7827, elmapex 7838
matmatrix df-mat 20154 (𝑁 Mat 𝑅) Yes matval 20157, matring 20189
mdetdeterminant (of a square matrix) df-mdet 20331 (𝑁 maDet 𝑅) Yes mdetleib 20333, mdetrlin 20348
mgmmagma df-mgm 17182 Magma Yes mgmidmo 17199, mgmlrid 17206, ismgm 17183
mgpmultiplicative group df-mgp 18430 (mulGrp‘𝑅) Yes mgpress 18440, ringmgp 18493
mndmonoid df-mnd 17235 Mnd Yes mndass 17242, mndodcong 17901
mo"there exists at most one" df-mo 2474 ∃*𝑥𝜑 Yes eumo 2498, moim 2518
mpmodus ponens ax-mp 5 No mpd 15, mpi 20
mptmodus ponendo tollens No mptnan 1690, mptxor 1691
mptmaps-to notation for a function df-mpt 4685 (𝑥𝐴𝐵) Yes fconstmpt 5133, resmpt 5418
mpt2maps-to notation for an operation df-mpt2 6620 (𝑥𝐴, 𝑦𝐵𝐶) Yes mpt2mpt 6717, resmpt2 6723
mulmultiplication (see "t") df-mul 9908 (𝐴 · 𝐵) Yes mulcl 9980, divmul 10648, mulcom 9982, mulass 9984
n, notnot ¬ 𝜑 Yes nan 603, notnotr 125
nenot equaldf-ne 𝐴𝐵 Yes exmidne 2800, neeqtrd 2859
nelnot element ofdf-nel 𝐴𝐵 Yes neli 2895, nnel 2902
ne0not equal to zero (see n0) ≠ 0 No negne0d 10350, ine0 10425, gt0ne0 10453
nf "not free in" (prefix) No nfnd 1782
ngpnormed group df-ngp 22328 NrmGrp Yes isngp 22340, ngptps 22346
nmnorm (on a group or ring) df-nm 22327 (norm‘𝑊) Yes nmval 22334, subgnm 22377
nnpositive integers df-nn 10981 Yes nnsscn 10985, nncn 10988
nn0nonnegative integers df-n0 11253 0 Yes nnnn0 11259, nn0cn 11262
n0not the empty set (see ne0) ≠ ∅ No n0i 3902, vn0 3906, ssn0 3954
OLDold, obsolete (to be removed soon) No 19.43OLD 1808
opordered pair df-op 4162 𝐴, 𝐵 Yes dfopif 4374, opth 4915
oror df-or 385 (𝜑𝜓) Yes orcom 402, anor 510
otordered triple df-ot 4164 𝐴, 𝐵, 𝐶 Yes euotd 4945, fnotovb 6659
ovoperation value df-ov 6618 (𝐴𝐹𝐵) Yes fnotovb 6659, fnovrn 6774
pplus (see "add"), for all-constant theorems df-add 9907 (3 + 2) = 5 Yes 3p2e5 11120
pfxprefix df-pfx 40711 (𝑊 prefix 𝐿) Yes pfxlen 40720, ccatpfx 40738
pmPrincipia Mathematica No pm2.27 42
pmpartial mapping (operation) df-pm 7820 (𝐴pm 𝐵) Yes elpmi 7836, pmsspw 7852
prpair df-pr 4158 {𝐴, 𝐵} Yes elpr 4176, prcom 4244, prid1g 4272, prnz 4287
prm, primeprime (number) df-prm 15329 Yes 1nprm 15335, dvdsprime 15343
pssproper subset df-pss 3576 𝐴𝐵 Yes pssss 3686, sspsstri 3693
q rational numbers ("quotients") df-q 11749 Yes elq 11750
rright No orcd 407, simprl 793
rabrestricted class abstraction df-rab 2917 {𝑥𝐴𝜑} Yes rabswap 3114, df-oprab 6619
ralrestricted universal quantification df-ral 2913 𝑥𝐴𝜑 Yes ralnex 2988, ralrnmpt2 6740
rclreverse closure No ndmfvrcl 6186, nnarcl 7656
rereal numbers df-r 9906 Yes recn 9986, 0re 10000
relrelation df-rel 5091 Rel 𝐴 Yes brrelex 5126, relmpt2opab 7219
resrestriction df-res 5096 (𝐴𝐵) Yes opelres 5371, f1ores 6118
reurestricted existential uniqueness df-reu 2915 ∃!𝑥𝐴𝜑 Yes nfreud 3106, reurex 3153
rexrestricted existential quantification df-rex 2914 𝑥𝐴𝜑 Yes rexnal 2991, rexrnmpt2 6741
rmorestricted "at most one" df-rmo 2916 ∃*𝑥𝐴𝜑 Yes nfrmod 3107, nrexrmo 3156
rnrange df-rn 5095 ran 𝐴 Yes elrng 5284, rncnvcnv 5319
rng(unital) ring df-ring 18489 Ring Yes ringidval 18443, isring 18491, ringgrp 18492
rotrotation No 3anrot 1041, 3orrot 1042
seliminates need for syllogism (suffix) No ancoms 469
sb(proper) substitution (of a set) df-sb 1878 [𝑦 / 𝑥]𝜑 Yes spsbe 1881, sbimi 1883
sbc(proper) substitution of a class df-sbc 3423 [𝐴 / 𝑥]𝜑 Yes sbc2or 3431, sbcth 3437
scascalar df-sca 15897 (Scalar‘𝐻) Yes resssca 15971, mgpsca 18436
simpsimple, simplification No simpl 473, simp3r3 1169
snsingleton df-sn 4156 {𝐴} Yes eldifsn 4294
spspecialization No spsbe 1881, spei 2260
sssubset df-ss 3574 𝐴𝐵 Yes difss 3721
structstructure df-struct 15802 Struct Yes brstruct 15808, structfn 15816
subsubtract df-sub 10228 (𝐴𝐵) Yes subval 10232, subaddi 10328
supsupremum df-sup 8308 sup(𝐴, 𝐵, < ) Yes fisupcl 8335, supmo 8318
suppsupport (of a function) df-supp 7256 (𝐹 supp 𝑍) Yes ressuppfi 8261, mptsuppd 7278
swapswap (two parts within a theorem) No rabswap 3114, 2reuswap 3397
sylsyllogism syl 17 No 3syl 18
symsymmetric No df-symdif 3828, cnvsym 5479
symgsymmetric group df-symg 17738 (SymGrp‘𝐴) Yes symghash 17745, pgrpsubgsymg 17768
t times (see "mul"), for all-constant theorems df-mul 9908 (3 · 2) = 6 Yes 3t2e6 11139
ththeorem No nfth 1724, sbcth 3437, weth 9277
tptriple df-tp 4160 {𝐴, 𝐵, 𝐶} Yes eltpi 4207, tpeq1 4254
trtransitive No bitrd 268, biantr 971
trutrue df-tru 1483 Yes bitru 1493, truanfal 1504
ununion df-un 3565 (𝐴𝐵) Yes uneqri 3739, uncom 3741
unitunit (in a ring) df-unit 18582 (Unit‘𝑅) Yes isunit 18597, nzrunit 19207
vdisjoint variable conditions used when a not-free hypothesis (suffix) No spimv 2256
vtxvertex df-vtx 25810 (Vtx‘𝐺) Yes vtxval0 25865, opvtxov 25819
vv2 disjoint variables (in a not-free hypothesis) (suffix) No 19.23vv 1900
wweak (version of a theorem) (suffix) No ax11w 2004, spnfw 1925
wrdword df-word 13254 Word 𝑆 Yes iswrdb 13266, wrdfn 13274, ffz0iswrd 13287
xpcross product (Cartesian product) df-xp 5090 (𝐴 × 𝐵) Yes elxp 5101, opelxpi 5118, xpundi 5142
xreXtended reals df-xr 10038 * Yes ressxr 10043, rexr 10045, 0xr 10046
z integers (from German "Zahlen") df-z 11338 Yes elz 11339, zcn 11342
zn ring of integers mod 𝑛 df-zn 19795 (ℤ/nℤ‘𝑁) Yes znval 19823, zncrng 19833, znhash 19847
zringring of integers df-zring 19759 ring Yes zringbas 19764, zringcrng 19760
0, z slashed zero (empty set) (see n0) df-nul 3898 Yes n0i 3902, vn0 3906; snnz 4286, prnz 4287

(Contributed by DAW, 27-Dec-2016.) (New usage is discouraged.)

Ref Expression
conventions-label.1 𝜑
Ref Expression
conventions-label 𝜑

Proof of Theorem conventions-label
StepHypRef Expression
1 conventions-label.1 1 𝜑
Colors of variables: wff setvar class
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator