Metamath Proof Explorer Most Recent Proofs 

Mirrors > Home > MPE Home > Th. List > Recent  Other > MM 100 
The original proofs of theorems with recently shortened proofs can often be found by appending "OLD" to the theorem name, for example 19.43OLD for 19.43.
Other links Email: Norm Megill. Mailing list: Metamath Google Group Updated 6Mar2018 . Syndication: RSS feed (courtesy of Dan Getz). Related wikis: Wikiproofs (JHilbert) (Recent Changes); Ghilbert site; Ghilbert Google Group.
Recent news items (28Feb2018) Filip Cernatescu's Milpgame is now stored on the Metamath site, with source code maintained on GitHub. See the link for instructions and other information.
(27Feb2018) Bill Hale has released an app for the Apple iPad and desktop computer that allows you to browse Metamath theorems and their proofs.
(17Jan2018) Dylan Houlihan has kindly provided a new mirror site. He has also provided an rsync server; type "rsync uk.metamath.org::" in a bash shell to check its status (it should return "metamath metamath").
(15Jan2018) The metamath program, version 0.157, has been updated to implement the file inclusion conventions described in the 21Dec2017 entry of mmnotes.txt.
(11Dec2017) I added a paragraph, suggested by Gérard Lang, to the distinct variable description here.
(10Dec2017) Per FL's request, his mathbox will be removed from set.mm. If you wish to export any of his theorems, today's version (master commit 1024a3a) is the last one that will contain it.
(11Nov2017) Alan Sare updated his completeusersproof program.
(3Oct2017) Sean B. Palmer created a web page that runs the metamath program under emulated Linux in JavaScript. He also wrote some programs to work with our shortest known proofs of the PM propositional calculus theorems.
(28Sep2017) Ivan Kuckir wrote a tutorial blog entry, Introduction to Metamath, that summarizes the language syntax. (It may have been written some time ago, but I was not aware of it before.)
(26Sep2017) The default directory for the Metamath Proof Explorer (MPE) has been changed from the GIF version (mpegif) to the Unicode version (mpeuni) throughout the site. Please let me know if you find broken links or other issues.
(24Sep2017) Saveliy Skresanov added a new proof to the 100 theorem list, Ceva's Theorem cevath, bringing the Metamath total to 67.
(3Sep2017) Brendan Leahy added a new proof to the 100 theorem list, Area of a Circle areacirc, bringing the Metamath total to 66.
(7Aug2017) Mario Carneiro added a new proof to the 100 theorem list, Principle of Inclusion/Exclusion incexc, bringing the Metamath total to 65.
(1Jul2017) Glauco Siliprandi added a new proof to the 100 theorem list, Stirling's Formula stirling, bringing the Metamath total to 64. Related theorems include 2 versions of Wallis' formula for π (wallispi and wallispi2).
(7May2017) Thierry Arnoux added a new proof to the 100 theorem list, Betrand's Ballot Problem ballotth, bringing the Metamath total to 63.
(20Apr2017) Glauco Siliprandi added a new proof in the supplementary list on the 100 theorem list, StoneWeierstrass Theorem stowei.
(28Feb2017) David Moews added a new proof to the 100 theorem list, Product of Segments of Chords chordthm, bringing the Metamath total to 62. Older news...
Color key:  Metamath Proof Explorer  Hilbert Space Explorer  User Mathboxes 
Date  Label  Description 

Theorem  
6Mar2018  a16g 2012  Generalization of ax16 2092. (Contributed by NM, 25Jul2015.) (Proof shortened by Wolf Lammen, 6Mar2018.) 
6Mar2018  ax10 1991  Derive set.mm's original ax10 2188 from others. (Contributed by NM, 25Jul2015.) (Revised by NM, 7Nov2015.) (Proof shortened by Wolf Lammen, 6Mar2018.) 
6Mar2018  spime 1960 
Existential introduction, using implicit substitution. Compare Lemma 14
of [Tarski] p. 70. (Contributed by NM,
7Aug1994.) (Revised by Mario
Carneiro, 3Oct2016.) (Proof shortened by Wolf Lammen, 6Mar2018.)

4Mar2018  ismblfin 25968  Measurability in terms of inner and outer measure. Proposition 7 of [Viaclovsky] p. 3. (Contributed by Brendan Leahy, 4Mar2018.) 
4Mar2018  dral1 2022  Formulabuilding lemma for use with the Distinctor Reduction Theorem. Part of Theorem 9.4 of [Megill] p. 448 (p. 16 of preprint). (Contributed by NM, 24Nov1994.) (Proof shortened by Wolf Lammen, 4Mar2018.) 
4Mar2018  dral2 2020  Formulabuilding lemma for use with the Distinctor Reduction Theorem. Part of Theorem 9.4 of [Megill] p. 448 (p. 16 of preprint). (Contributed by NM, 27Feb2005.) (Revised by Wolf Lammen, 4Mar2018.) 
4Mar2018  dvelimh 2015  Version of dvelim 2064 without any variable restrictions. (Contributed by NM, 1Oct2002.) (Proof shortened by Wolf Lammen, 4Mar2018.) 
3Mar2018  dvelimhw 1872  Proof of dvelimh 2015 without using ax12 1946 but with additional distinct variable conditions. (Contributed by Andrew Salmon, 21Jul2011.) (Revised by NM, 1Aug2017.) (Proof shortened by Wolf Lammen, 3Mar2018.) 
3Mar2018  hbnt 1795  Closed theorem version of boundvariable hypothesis builder hbn 1797. (Contributed by NM, 5Aug1993.) (Proof shortened by Wolf Lammen, 3Mar2018.) 
3Mar2018  19.9ht 1788  A closed version of 19.9 1793. (Contributed by NM, 5Aug1993.) (Proof shortened by Wolf Lammen, 3Mar2018.) 
28Feb2018  hbn1fw 1715  Weak version of ax6 1740 from which we can prove any ax6 1740 instance not involving wff variables or bundling. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 19Apr2017.) (Proof shortened by Wolf Lammen, 28Feb2018.) 
28Feb2018  cbvalvw 1711  Change bound variable. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 9Apr2017.) (Proof shortened by Wolf Lammen, 28Feb2018.) 
27Feb2018  dveeq1 1987  Quantifier introduction when one pair of variables is distinct. Revised to be independent of dvelimv 2017. (Contributed by NM, 2Jan2002.) (Revised by Wolf Lammen, 27Feb2018.) 
27Feb2018  spw 1702  Weak version of specialization scheme sp 1759. Lemma 9 of [KalishMontague] p. 87. While it appears that sp 1759 in its general form does not follow from Tarski's FOL axiom schemes, from this theorem we can prove any instance of sp 1759 having no wff metavariables and mutually distinct set variables (see ax11wdemo 1734 for an example of the procedure to eliminate the hypothesis). Other approximations of sp 1759 are spfw 1699 (minimal distinct variable requirements), spnfw 1678 (when is not free in ), spvw 1674 (when does not appear in ), sptruw 1679 (when is true), and spfalw 1680 (when is false). (Contributed by NM, 9Apr2017.) (Proof shortened by Wolf Lammen, 27Feb2018.) 
26Feb2018  ax12b 1697  Two equivalent ways of expressing ax12 1946. See the comment for ax12 1946. (Contributed by NM, 2May2017.) (Proof shortened by Wolf Lammen, 26Feb2018.) 
25Feb2018  dvelimv 2017  Similar to dvelim 2064 with first hypothesis replaced by distinct variable condition. (Contributed by NM, 25Jul2015.) (Proof shortened by Wolf Lammen, 25Feb2018.) 
25Feb2018  a9e 1948  At least one individual exists. This is not a theorem of free logic, which is sound in empty domains. For such a logic, we would add this theorem as an axiom of set theory (Axiom 0 of [Kunen] p. 10). In the system consisting of ax5 1563 through ax14 1725 and ax17 1623, all axioms other than ax9 1949 are believed to be theorems of free logic, although the system without ax9 1949 is probably not complete in free logic. (Contributed by NM, 5Aug1993.) (Revised by Wolf Lammen, 25Feb2018.) 
25Feb2018  sbequ2 1657  An equality theorem for substitution. (Contributed by NM, 5Aug1993.) (Proof shortened by Wolf Lammen, 25Feb2018.) 
24Feb2018  spimt 1953  Closed theorem form of spim 1955. (Contributed by NM, 15Jan2008.) (Revised by Mario Carneiro, 17Oct2016.) (Proof shortened by Wolf Lammen, 24Feb2018.) 
23Feb2018  spei 1964  Inference from existential specialization, using implicit substitution. Revised to remove a distinct variable constraint. (Contributed by NM, 19Aug1993.) (Revised by Wolf Lammen, 23Feb2018.) 
21Feb2018  mblfinlem 25967  Lemma for ismblfin 25968, effectively one direction of the same fact for open sets, made necessary by Viaclovsky's slightly different defintion of outer measure. Note that unlike the main theorem, this holds for sets of infinite measure. (Contributed by Brendan Leahy, 21Feb2018.) 
19Feb2018  spimed 1958  Deduction version of spime 1960. (Contributed by NM, 5Aug1993.) (Revised by Mario Carneiro, 3Oct2016.) (Proof shortened by Wolf Lammen, 19Feb2018.) 
18Feb2018  spim 1955  Specialization, using implicit substitution. Compare Lemma 14 of [Tarski] p. 70. The spim 1955 series of theorems requires that only one direction of the substitution hypothesis hold. (Contributed by NM, 5Aug1993.) (Revised by Mario Carneiro, 3Oct2016.) (Proof shortened by Wolf Lammen, 18Feb2018.) 
17Feb2018  aevlem1 2010  Lemma for ax10 1991. Change free and bound variables. (Contributed by NM, 22Jul2015.) (Proof shortened by Wolf Lammen, 17Feb2018.) 
17Feb2018  ax10lem2 1989  Lemma for ax10 1991. Change bound variable. (Contributed by NM, 8Jul2016.) (Proof shortened by Wolf Lammen, 17Feb2018.) 
8Feb2018  ax12olem4 1975  Lemma for ax12o 1976. (Contributed by Wolf Lammen, 8Feb2018.) 
8Feb2018  ax12olem2 1973  Lemma for ax12o 1976. (Contributed by Wolf Lammen, 8Feb2018.) 
8Feb2018  ax12olem1 1972  Lemma for ax12o 1976. The proof of ax12o 1976 bases on ideas from NM, 24Dec2015. (Contributed by Wolf Lammen, 8Feb2018.) 
6Feb2018  equsex 1969  A useful equivalence related to substitution. (Contributed by NM, 5Aug1993.) (Revised by Mario Carneiro, 3Oct2016.) (Proof shortened by Wolf Lammen, 6Feb2018.) 
5Feb2018  equsal 1966  A useful equivalence related to substitution. (Contributed by NM, 5Aug1993.) (Proof shortened by Andrew Salmon, 12Aug2011.) (Revised by Mario Carneiro, 3Oct2016.) (Proof shortened by Wolf Lammen, 5Feb2018.) 
5Feb2018  equs4 1951  Lemma used in proofs of substitution properties. (Contributed by NM, 5Aug1993.) (Proof shortened by Mario Carneiro, 20May2014.) (Proof shortened by Wolf Lammen, 5Feb2018.) 
5Feb2018  equid 1684  Identity law for equality. Lemma 2 of [KalishMontague] p. 85. See also Lemma 6 of [Tarski] p. 68. (Contributed by NM, 1Apr2005.) (Revised by NM, 9Apr2017.) (Proof shortened by WolfLammen, 5Feb2018.) 
4Feb2018  ax9 1949 
Theorem showing that ax9 1662 follows from the weaker version ax9v 1663.
(Even though this theorem depends on ax9 1662,
all references of ax9 1662
are made via ax9v 1663. An earlier version stated ax9v 1663
as a separate
axiom, but having two axioms caused some confusion.)
This theorem should be referenced in place of ax9 1662 so that all proofs can be traced back to ax9v 1663. (Contributed by NM, 12Nov2013.) (Revised by NM, 25Jul2015.) (Proof shortened by Wolf Lammen, 4Feb2018.) 
3Feb2018  eximii 1584  Inference associated with eximi 1582. (Contributed by BJ, 3Feb2018.) 
31Jan2018  ax12 1985  Derive ax12 1946 from ax12v 1947 via ax12o 1976. This shows that the weakening in ax12v 1947 is still sufficient for a complete system. (Contributed by NM, 21Dec2015.) (Proof shortened by Wolf Lammen, 31Jan2018.) 
30Jan2018  ax12o 1976  Derive set.mm's original ax12o 2190 from the shorter ax12 1946. (Contributed by NM, 29Nov2015.) (Revised by NM, 24Dec2015.) (Revised by Wolf Lammen, 30Jan2018.) 
30Jan2018  ax12olem3 1974  Lemma for ax12o 1976. (Contributed by Wolf Lammen, 30Jan2018.) 
28Jan2018  qqhucn 24189  The QQHom homomorphism is uniformly continuous. (Contributed by Thierry Arnoux, 28Jan2018.) 
ℂ_{fld} ↾_{s} UnifSt metUnif Mod NrmRing NrmMod chr QQHom Cn_{u}  
26Jan2018  metucn 18504  Uniform continuity in metric spaces. Compare the order of the quantifiers with metcn 18477. (Contributed by Thierry Arnoux, 26Jan2018.) 
metUnif metUnif Cn_{u}  
26Jan2018  elbl4 18497  Membership in a ball, alternative definition. (Contributed by Thierry Arnoux, 26Jan2018.) 
26Jan2018  isucn2 18244  The predicate " is a uniformly continuous function from uniform space to uniform space ." , expressed with filter bases for the entourages. (Contributed by Thierry Arnoux, 26Jan2018.) 
UnifOn UnifOn Cn_{u}  
25Jan2018  ucnextcn 18269  Extension by continuity. Theorem 2 of [BourbakiTop1] p. II.20. Given an uniform space on a set , a subset dense in , and a function uniformly continuous from to , that function can be extended by continuity to the whole , and its extension is uniformly continuous. (Contributed by Thierry Arnoux, 25Jan2018.) 
UnifSt UnifSt ↾_{s} UnifSt UnifSp CUnifSp Cn_{u} CnExt  
25Jan2018  tustps 18238  A constructed uniform space is a topological space. (Contributed by Thierry Arnoux, 25Jan2018.) 
toUnifSp UnifOn  
25Jan2018  ssrel2 4920  A subclass relationship depends only on a relation's ordered pairs. This version of ssrel 4918 is restricted to the relation's domain. (Contributed by Thierry Arnoux, 25Jan2018.) 
24Jan2018  metuel2 18499  Elementhood in the uniform structure generated by a metric (Contributed by Thierry Arnoux, 24Jan2018.) 
metUnif  
24Jan2018  neipcfilu 18261  In an uniform space, a neighboring filter is a Cauchy filter base. (Contributed by Thierry Arnoux, 24Jan2018.) 
UnifSt UnifSp CauFil_{u}  
24Jan2018  cfiluweak 18260  A Cauchy filter base is also a Cauchy filter base on any coarser uniform structure. (Contributed by Thierry Arnoux, 24Jan2018.) 
UnifOn CauFil_{u} ↾_{t} CauFil_{u}  
24Jan2018  trcfilu 18259  Condition for the trace of a Cauchy filter base to be a Cauchy filter base for the restricted uniform structure. (Contributed by Thierry Arnoux, 24Jan2018.) 
UnifOn CauFil_{u} ↾_{t} ↾_{t} CauFil_{u} ↾_{t}  
24Jan2018  cfilufg 18258  The filter generated by a Cauchy filter base is still a Cauchy filter base. (Contributed by Thierry Arnoux, 24Jan2018.) 
UnifOn CauFil_{u} CauFil_{u}  
23Jan2018  ftp 5870  A function with a domain of three elements. (Contributed by Stefan O'Rear, 17Oct2014.) (Proof shortened by Alexander van der Vekens, 23Jan2018.) 
23Jan2018  ax12olem2OLD 1978  Obsolete proof of ax12oOLD 1984 as of 30Jan2018. Lemma for ax12oOLD 1984. Negate the equalities in ax12 1946, shown as the hypothesis. (Contributed by NM, 24Dec2015.) (Proof shortened by Wolf Lammen, 23Jan2018.) (New usage is discouraged.) (Proof modification is discouraged.) 
22Jan2018  ressust 18229  The uniform structure of a restricted space. (Contributed by Thierry Arnoux, 22Jan2018.) 
UnifSt ↾_{s} UnifSp UnifOn  
22Jan2018  pm11.07 2162  (Probably not) Axiom *11.07 in [WhiteheadRussell] p. 159. The original confusingly reads: *11.07 "Whatever possible argument may be, is true whatever possible argument may be" implies the corresponding statement with and interchanged except in " ". This theorem will be deleted after 22Feb2018 if no one is able to determine the correct interpretation. See https://groups.google.com/d/msg/metamath/iS0fOvSemC8/YzrRyX70AgAJ. (Contributed by Andrew Salmon, 17Jun2011.) (Proof shortened by Jim Kingdon, 22Jan2018.) (New usage is discouraged.) 
21Jan2018  fallfacfwd 25133  The forward difference of a falling factorial. (Contributed by Scott Fenton, 21Jan2018.) 
FallFac FallFac FallFac  
21Jan2018  reofld 24110  The real numbers form an ordered field. (Contributed by Thierry Arnoux, 21Jan2018.) 
ℂ_{fld} ↾_{s} oField  
21Jan2018  retos 24108  The real numbers are a totally ordered set. (Contributed by Thierry Arnoux, 21Jan2018.) 
ℂ_{fld} ↾_{s} Toset  
21Jan2018  relt 24106  The ordering relation of the field of reals. (Contributed by Thierry Arnoux, 21Jan2018.) 
ℂ_{fld} ↾_{s}  
21Jan2018  rele2 24105  The ordering relation of the field of reals. (Contributed by Thierry Arnoux, 21Jan2018.) 
ℂ_{fld} ↾_{s}  
21Jan2018  replusg 24101  The addition operation of the field of reals. (Contributed by Thierry Arnoux, 21Jan2018.) 
ℂ_{fld} ↾_{s}  
21Jan2018  subofld 24085  Every subfield of an ordered field is also an ordered field. (Contributed by Thierry Arnoux, 21Jan2018.) 
oField ↾_{s} Field ↾_{s} oField  
21Jan2018  ofldchr 24084  The characteristic of an ordered field is zero. (Contributed by Thierry Arnoux, 21Jan2018.) 
oField chr  
21Jan2018  ofldlt1 24083  In an ordered field, the ring unit is strictly positive. (Contributed by Thierry Arnoux, 21Jan2018.) 
oField  
21Jan2018  ofld0le1 24082  In an ordered field, the ring unit is positive. (Contributed by Thierry Arnoux, 21Jan2018.) 
oField  
21Jan2018  vdgrfiun 21535  The degree of a vertex in the union of two graphs (of finite size) on the same vertex set is the sum of the degrees of the vertex in each graph. (Contributed by Mario Carneiro, 12Mar2015.) (Revised by Alexander van der Vekens, 21Jan2018.) 
UMGrph UMGrph VDeg VDeg VDeg  
21Jan2018  vdgrfival 21530  The value of the vertex degree function (for graphs of finite size). (Contributed by Mario Carneiro, 12Mar2015.) (Revised by Alexander van der Vekens, 21Jan2018.) 
VDeg  
20Jan2018  ofldaddlt 24081  In an ordered field, the ordering is compatible with group addition. (Contributed by Thierry Arnoux, 20Jan2018.) 
oField  
20Jan2018  ofldsqr 24080  In an ordered field, all squares are positive. (Contributed by Thierry Arnoux, 20Jan2018.) 
oField  
20Jan2018  ofldmul 24079  In an ordered field, the ordering is compatible with the ring multiplication operation. (Contributed by Thierry Arnoux, 20Jan2018.) 
oField  
20Jan2018  ofldadd 24078  In an ordered field, the ordering is compatible with group addition. (Contributed by Thierry Arnoux, 20Jan2018.) 
oField  
20Jan2018  ofldtos 24077  An ordered field is a totally ordered set. (Contributed by Thierry Arnoux, 20Jan2018.) 
oField Toset  
20Jan2018  ofldfld 24076  An ordered field is a field. (Contributed by Thierry Arnoux, 20Jan2018.) 
oField Field  
20Jan2018  resstos 24041  The restriction of a Toset is a Toset. (Contributed by Thierry Arnoux, 20Jan2018.) 
Toset ↾_{s} Toset  
20Jan2018  resspos 24040  The restriction of a Poset is a Poset. (Contributed by Thierry Arnoux, 20Jan2018.) 
↾_{s}  
20Jan2018  tospos 24039  A Toset is a Poset. (Contributed by Thierry Arnoux, 20Jan2018.) 
Toset  
20Jan2018  ax12olem1OLD 1977  Obsolete proof of ax12oOLD 1984 as of 30Jan2018. Lemma for ax12oOLD 1984. Similar to equvin 2049 but with a negated equality. (Contributed by NM, 24Dec2015.) (Proof shortened by Wolf Lammen, 20Jan2018.) (New usage is discouraged.) (Proof modification is discouraged.) 
20Jan2018  eeeanv 1934  Rearrange existential quantifiers. Revised to loosen distinct variable restrictions. (Contributed by NM, 26Jul1995.) (Proof shortened by Andrew Salmon, 25May2011.) (Revised by Wolf Lammen, 20Jan2018.) 
20Jan2018  4exdistr 1930  Distribution of existential quantifiers. (Contributed by NM, 9Mar1995.) (Proof shortened by Wolf Lammen, 20Jan2018.) 
18Jan2018  isofld 24075  An ordered field is a field with a total ordering compatible with the operations. (Contributed by Thierry Arnoux, 18Jan2018.) 
oField Field Toset  
18Jan2018  dfofld 24074  Define class of all ordered fields. An ordered field is a field with a total ordering compatible with the operations. (Contributed by Thierry Arnoux, 18Jan2018.) 
oField Field Toset  
18Jan2018  cusgrauvtxb 21385  An undirected simple graph is complete if and only if each vertex is a universal vertex. (Contributed by Alexander van der Vekens, 14Oct2017.) (Revised by Alexander van der Vekens, 18Jan2018.) 
USGrph ComplUSGrph UnivVertex  
18Jan2018  hashgt0elexb 11612  The size of a set is greater than zero if and only if the set contains at least one element. (Contributed by Alexander van der Vekens, 18Jan2018.) 
18Jan2018  hashnfinnn0 11584  The size of an infinite set is not a nonnegative integer. (Contributed by Alexander van der Vekens, 21Dec2017.) (Proof shortened by Alexander van der Vekens, 18Jan2018.) 
18Jan2018  prsspwg 3912  An unordered pair belongs to the power class of a class iff each member belongs to the class. (Contributed by Thierry Arnoux, 3Oct2016.) (Revised by NM, 18Jan2018.) 
18Jan2018  nnel 2662  Negation of negated membership, analogous to nne 2568. (Contributed by Alexander van der Vekens, 18Jan2018.) 
17Jan2018  fallrisefac 25123  A relationship between falling and rising factorials. (Contributed by Scott Fenton, 17Jan2018.) 
FallFac RiseFac  
17Jan2018  m1expevenALT 24698  Exponentiation of negative one to an even power. (Contributed by Scott Fenton, 17Jan2018.) 
17Jan2018  rrhcn 24193  If the topology of is Hausdorff, and is a complete uniform space, then the canonical homomorphism from the real numbers to is continuous. (Contributed by Thierry Arnoux, 17Jan2018.) 
NrmRing Mod NrmMod chr CUnifSp UnifSt metUnif RRHom  
17Jan2018  utop3cls 18216  Relation between a topological closure and a symmetric entourage in an uniform space. Second part of proposition 2 of [BourbakiTop1] p. II.4. (Contributed by Thierry Arnoux, 17Jan2018.) 
unifTop UnifOn  
17Jan2018  cnextfres 18034  and its extension by continuity agree on the domain of . (Contributed by Thierry Arnoux, 17Jan2018.) 
↾_{t} ↾_{t} CnExt  
17Jan2018  neitr 17180  The neighborhood of a trace is the trace of the neighborhood. (Contributed by Thierry Arnoux, 17Jan2018.) 
↾_{t} ↾_{t}  
17Jan2018  hashprb 11609  The size of an unordered pair is 2 if and only if its elements are different sets. (Contributed by Alexander van der Vekens, 17Jan2018.) 
17Jan2018  elfznelfzob 11134  A value in a finite set of sequential integers is a border value if and only if it is not contained in the halfopen integer range contained in the finite set of sequential integerss. (Contributed by Alexander van der Vekens, 17Jan2018.) 
..^  
17Jan2018  nn0n0n1ge2b 10227  A nonnegative integer is neither 0 nor 1 if and only if it is is greater than or equal to 2. (Contributed by Alexander van der Vekens, 17Jan2018.) 
16Jan2018  utopreg 18217  All Hausdorff uniform spaces are regular. Proposition 3 of [BourbakiTop1] p. II.5. (Contributed by Thierry Arnoux, 16Jan2018.) 
unifTop UnifOn  
16Jan2018  ustex3sym 18182  In an uniform structure, for any entourage , there exists a symmetrical entourage smaller than a third of . (Contributed by Thierry Arnoux, 16Jan2018.) 
UnifOn  
16Jan2018  ustex2sym 18181  In an uniform structure, for any entourage , there exists a symmetrical entourage smaller than half . (Contributed by Thierry Arnoux, 16Jan2018.) 
UnifOn  
16Jan2018  prnebg 3935  A (proper) pair is not equal to another (maybe inproper) pair if and only if an element of the first pair is not contained in the second pair. (Contributed by Alexander van der Vekens, 16Jan2018.) 
15Jan2018  risefallfac 25122  A relationship between rising and falling factorials. (Contributed by Scott Fenton, 15Jan2018.) 
RiseFac FallFac  
15Jan2018  fallfacval2 25110  Onebased value of falling factorial. (Contributed by Scott Fenton, 15Jan2018.) 
FallFac  
15Jan2018  risefacval2 25109  Onebased value of rising factorial. (Contributed by Scott Fenton, 15Jan2018.) 
RiseFac  
15Jan2018  fprodn0 25096  A finite product of nonzero terms is nonzero. (Contributed by Scott Fenton, 15Jan2018.) 
15Jan2018  fproddiv 25078  The quotient of two finite products. (Contributed by Scott Fenton, 15Jan2018.) 
15Jan2018  prodfdiv 25017  The quotient of two infinite products. (Contributed by Scott Fenton, 15Jan2018.) 
15Jan2018  prodfrec 25016  The reciprocal of an infinite product. (Contributed by Scott Fenton, 15Jan2018.) 
15Jan2018  tppreqb 3896  An unordered triple is an unordered pair if and only if one of its elements is a proper class or is identical with one of the another elements. (Contributed by Alexander van der Vekens, 15Jan2018.) 
15Jan2018  sb8e 2140  Substitution of variable in existential quantifier. (Contributed by NM, 12Aug1993.) (Revised by Mario Carneiro, 6Oct2016.) (Proof shortened by Jim Kingdon, 15Jan2018.) 
15Jan2018  sb8 2139  Substitution of variable in universal quantifier. (Contributed by NM, 5Aug1993.) (Revised by Mario Carneiro, 6Oct2016.) (Proof shortened by Jim Kingdon, 15Jan2018.) 
15Jan2018  equs5e 1906  A property related to substitution that unlike equs5 2047 doesn't require a distinctor antecedent. (Contributed by NM, 2Feb2007.) (Proof shortened by Wolf Lammen, 15Jan2018.) 
14Jan2018  prodfn0 25015  No term of a nonzero infinite product is zero. (Contributed by Scott Fenton, 14Jan2018.) 
14Jan2018  utop2nei 18215  For any symmetrical entourage and any relation , build a neighborhood of . First part of proposition 2 of [BourbakiTop1] p. II.4. (Contributed by Thierry Arnoux, 14Jan2018.) 
unifTop UnifOn  
14Jan2018  imasncls 17659  If a relation graph is closed, then an image set of a singleton is also closed. Corollary of proposition 4 of [BourbakiTop1] p. I.26. (Contributed by Thierry Arnoux, 14Jan2018.) 
14Jan2018  imasncld 17658  If a relation graph is closed, then an image set of a singleton is also closed. Corollary of proposition 4 of [BourbakiTop1] p. I.26. (Contributed by Thierry Arnoux, 14Jan2018.) 
14Jan2018  imasnopn 17657  If a relation graph is opened, then an image set of a singleton is also opened. Corollary of proposition 4 of [BourbakiTop1] p. I.26. (Contributed by Thierry Arnoux, 14Jan2018.) 
14Jan2018  hash2prb 11630  A set of size two is an unordered pair if and only if it contains two different elements. (Contributed by Alexander van der Vekens, 14Jan2018.) 
14Jan2018  xpcoid 5369  Composition of two square cross products. (Contributed by Thierry Arnoux, 14Jan2018.) 
14Jan2018  xpimasn 5270  The image of a singleton by a cross product. (Contributed by Thierry Arnoux, 14Jan2018.) 
14Jan2018  brcogw 4995  Ordered pair membership in a composition. (Contributed by Thierry Arnoux, 14Jan2018.) 
13Jan2018  usgramaxsize 21376  The maximum size of an undirected simple graph with vertices ( ) is . (Contributed by Alexander van der Vekens, 13Jan2018.) 
USGrph  
13Jan2018  sizeusglecusg 21375  The size of an undirected simple graph with vertices is at most the size of a complete simple graph with vertices ( may be infinite). (Contributed by Alexander van der Vekens, 13Jan2018.) 
USGrph ComplUSGrph  
13Jan2018  sizeusglecusglem2 21374  Lemma 2 for sizeusglecusg 21375. (Contributed by Alexander van der Vekens, 13Jan2018.) 
USGrph ComplUSGrph  
13Jan2018  cusgrafi 21371  If the size of a complete simple graph is finite, then also its order is finite. (Contributed by Alexander van der Vekens, 13Jan2018.) 
ComplUSGrph  
13Jan2018  cusgrafilem3 21370  Lemma 2 for cusgrafi 21371. (Contributed by Alexander van der Vekens, 13Jan2018.) 
13Jan2018  cusgrafilem2 21369  Lemma 2 for cusgrafi 21371. (Contributed by Alexander van der Vekens, 13Jan2018.) 
13Jan2018  cusgrafilem1 21368  Lemma 1 for cusgrafi 21371. (Contributed by Alexander van der Vekens, 13Jan2018.) 
ComplUSGrph  
13Jan2018  utopsnnei 18214  Images of singletons by entourages are neighborhoods of those singletons. (Contributed by Thierry Arnoux, 13Jan2018.) 
unifTop UnifOn  
13Jan2018  utopsnneip 18213  The neighborhoods of a point for the topology induced by an uniform space . (Contributed by Thierry Arnoux, 13Jan2018.) 
unifTop UnifOn  
13Jan2018  neitx 17574  The cross product of two neighborhoods is a neighborhood in the product topology. (Contributed by Thierry Arnoux, 13Jan2018.) 
13Jan2018  exan 1899  Place a conjunct in the scope of an existential quantifier. (Contributed by NM, 18Aug1993.) (Proof shortened by Andrew Salmon, 25May2011.) (Proof shortened by Wolf Lammen, 13Jan2018.) 
13Jan2018  nfan 1842  If is not free in and , it is not free in . (Contributed by Mario Carneiro, 11Aug2016.) (Proof shortened by Wolf Lammen, 13Jan2018.) 
13Jan2018  sp 1759 
Specialization. A universally quantified wff implies the wff without a
quantifier Axiom scheme B5 of [Tarski]
p. 67 (under his system S2,
defined in the last paragraph on p. 77). Also appears as Axiom scheme
C5' in [Megill] p. 448 (p. 16 of the
preprint).
For the axiom of specialization presented in many logic textbooks, see theorem stdpc4 2071. This theorem shows that our obsolete axiom ax4 2183 can be derived from the others. The proof uses ideas from the proof of Lemma 21 of [Monk2] p. 114. It appears that this scheme cannot be derived directly from Tarski's axioms without auxilliary axiom scheme ax11 1757. It is thought the best we can do using only Tarski's axioms is spw 1702. (Contributed by NM, 21May2008.) (Proof shortened by Scott Fenton, 24Jan2011.) (Proof shortened by Wolf Lammen, 13Jan2018.) 
13Jan2018  19.8a 1758  If a wff is true, it is true for at least one instance. Special case of Theorem 19.8 of [Margaris] p. 89. (Contributed by NM, 5Aug1993.) (Revised by Wolf Lammen, 13Jan2018.) 
12Jan2018  fprodconst 25095  The product of constant terms ( is not free in .) (Contributed by Scott Fenton, 12Jan2018.) 
12Jan2018  sizeusglecusglem1 21373  Lemma 1 for sizeusglecusg 21375. (Contributed by Alexander van der Vekens, 12Jan2018.) 
USGrph ComplUSGrph  
12Jan2018  cusgraexg 21358  For each set there is an edge function so that the set together with this edge function is a complete graph. (Contributed by Alexander van der Vekens, 12Jan2018.) 
ComplUSGrph  
12Jan2018  cusgraexi 21357  For each set the identity function restricted to the set of pairs of elements from the given set is an edge function, so that the given set together with this edge function is a complete graph. (Contributed by Alexander van der Vekens, 12Jan2018.) 
ComplUSGrph  
12Jan2018  cusgraexilem2 21356  Lemma 2 for cusgraexi 21357. (Contributed by Alexander van der Vekens, 12Jan2018.) 
USGrph  
12Jan2018  cusgraexilem1 21355  Lemma 1 for cusgraexi 21357. (Contributed by Alexander van der Vekens, 12Jan2018.) 
12Jan2018  cusgrarn 21348  In a complete simple graph, the range of the edge function consists of all the pairs with different vertices. (Contributed by Alexander van der Vekens, 12Jan2018.) 
ComplUSGrph  
12Jan2018  hashf1rn 11577  The size of a finite set which is a onetoone function is equal to the size of the function's range. (Contributed by Alexander van der Vekens, 12Jan2018.) 
12Jan2018  nfielex 7287  If a class is not finite, it contains at least one element. (Contributed by Alexander van der Vekens, 12Jan2018.) 
12Jan2018  19.41 1896  Theorem 19.41 of [Margaris] p. 90. (Contributed by NM, 5Aug1993.) (Proof shortened by Andrew Salmon, 25May2011.) (Proof shortened by Wolf Lammen, 12Jan2018.) 
12Jan2018  exlimd 1820  Deduction from Theorem 19.9 of [Margaris] p. 89. (Contributed by Mario Carneiro, 24Sep2016.) (Proof shortened by Wolf Lammen, 12Jan2018.) 
11Jan2018  usgrasscusgra 21372  An undirected simple graph is a subgraph of a complete simple graph. (Contributed by Alexander van der Vekens, 11Jan2018.) 
USGrph ComplUSGrph  
11Jan2018  cusgrasize 21367  The size of a finite complete simple graph with vertices ( ) is (" choose 2") resp. . (Contributed by Alexander van der Vekens, 11Jan2018.) 
ComplUSGrph  
11Jan2018  cusgrasize2inds 21366  Induction step in cusgrasize 21367. If the size of the complete graph with vertices reduced by one vertex is " choose 2", the size of the complete graph with vertices is " choose 2". (Contributed by Alexander van der Vekens, 11Jan2018.) 
ComplUSGrph  
11Jan2018  cusgrasizeinds 21365  Part 1 of induction step in cusgrasize 21367. The size of a complete simple graph with vertices is plus the size of the complete graph reduced by one vertex. (Contributed by Alexander van der Vekens, 11Jan2018.) 
ComplUSGrph  
11Jan2018  cusgrasizeindslem3 21364  Lemma 3 for cusgrasizeinds 21365. (Contributed by Alexander van der Vekens, 11Jan2018.) 
ComplUSGrph  
11Jan2018  cusgrasizeindslem2 21363  Lemma 2 for cusgrasizeinds 21365. (Contributed by Alexander van der Vekens, 11Jan2018.) 
11Jan2018  utopsnneiplem 18212  The neighborhoods of a point for the topology induced by an uniform space . (Contributed by Thierry Arnoux, 11Jan2018.) 
unifTop UnifOn  
11Jan2018  ustuqtop 18211  For a given uniform structure on a set , there is a unique topology such that the set is the filter of the neighbourhoods of for that topology. Proposition 1 of [BourbakiTop1] p. II.3. (Contributed by Thierry Arnoux, 11Jan2018.) 
UnifOn TopOn  
11Jan2018  ustuqtop5 18210  Lemma for ustuqtop 18211 (Contributed by Thierry Arnoux, 11Jan2018.) 
UnifOn  
11Jan2018  ustuqtop4 18209  Lemma for ustuqtop 18211 (Contributed by Thierry Arnoux, 11Jan2018.) 
UnifOn  
11Jan2018  ustuqtop3 18208  Lemma for ustuqtop 18211, similar to elnei 17112 (Contributed by Thierry Arnoux, 11Jan2018.) 
UnifOn  
11Jan2018  ustuqtop2 18207  Lemma for ustuqtop 18211 (Contributed by Thierry Arnoux, 11Jan2018.) 
UnifOn  
11Jan2018  ustuqtop1 18206  Lemma for ustuqtop 18211, similar to ssnei2 17117 (Contributed by Thierry Arnoux, 11Jan2018.) 
UnifOn  
11Jan2018  ustuqtop0 18205  Lemma for ustuqtop 18211 (Contributed by Thierry Arnoux, 11Jan2018.) 
UnifOn  
11Jan2018  ustuqtoplem 18204  Lemma for ustuqtop 18211 (Contributed by Thierry Arnoux, 11Jan2018.) 
UnifOn  
9Jan2018  rprisefaccl 25121  Closure law for rising factorial. (Contributed by Scott Fenton, 9Jan2018.) 
RiseFac  
9Jan2018  hashnn0n0nn 11605  If a nonnegative integer is the size of a set which contains at least one element, this integer is a positive integer. (Contributed by Alexander van der Vekens, 9Jan2018.) 
8Jan2018  bcn2p1 11557  Compute the binomial coefficient " choose 2 " from " choose 2 ": N + ( N 2 ) = ( (N+1) 2 ) (Contributed by Alexander van der Vekens, 8Jan2018.) 
8Jan2018  excomim 1753  One direction of Theorem 19.11 of [Margaris] p. 89. Revised to remove dependency on ax11 1757, ax6 1740, ax9 1662, ax8 1683 and ax17 1623. (Contributed by NM, 5Aug1993.) (Revised by Mario Carneiro, 24Sep2016.) (Revised by Wolf Lammen, 8Jan2018.) 
8Jan2018  excom 1752  Theorem 19.11 of [Margaris] p. 89. Revised to remove dependency on ax11 1757, ax6 1740, ax9 1662, ax8 1683 and ax17 1623. (Contributed by NM, 5Aug1993.) (Revised by Wolf Lammen, 8Jan2018.) 
7Jan2018  neiptopnei 17133  Lemma for neiptopreu 17134 (Contributed by Thierry Arnoux, 7Jan2018.) 
7Jan2018  neiptoptop 17132  Lemma for neiptopreu 17134 (Contributed by Thierry Arnoux, 7Jan2018.) 
7Jan2018  brfi1ind 11657  Properties of a binary relation with a finite first component, proven by finite induction on the size of the first component. This theorem can be applied for graphs (as binary relation between the set of vertices and an edge function) with a finite number of vertices, e.g. usgrafis 21309. (Contributed by Alexander van der Vekens, 7Jan2018.) 
7Jan2018  brfi1uzind 11656  Properties of a binary relation with a finite first component with at least L elements, proven by finite induction on the size of the first component. This theorem can be applied for graphs (as binary relation between the set of vertices and an edge function) with a finite number of vertices, usually with (see brfi1ind 11657) or . (Contributed by Alexander van der Vekens, 7Jan2018.) 
7Jan2018  brfi1indlem 11655  Lemma for brfi1ind 11657: The size of a set is the size of this set with one element removed, increased by 1. (Contributed by Alexander van der Vekens, 7Jan2018.) 
7Jan2018  bcn2m1 11556  Compute the binomial coefficient " choose 2 " from " choose 2 ": (N1) + ( (N1) 2 ) = ( N 2 ) (Contributed by Alexander van der Vekens, 7Jan2018.) 
6Jan2018  usgrafis 21309  A simple undirected graph with a finite number of vertices has also only a finite number of edges. (Contributed by Alexander van der Vekens, 6Jan2018.) 
USGrph  
6Jan2018  neiptopreu 17134  If, to each element of a set , we associate a set fulfilling the properties V_{i}, V_{ii}, V_{iii} and property V_{iv} of [BourbakiTop1] p. I.2. , corresponding to ssnei 17111, innei 17126, elnei 17112 and neissex 17128, then there is a unique topology such that for any point , is the set of neighborhoods of . Proposition 2 of [BourbakiTop1] p. I.3. This can be used to build a topology from a set of neighborhoods. Note that the additional condition that is a neighborhood of all points was added. (Contributed by Thierry Arnoux, 6Jan2018.) 
TopOn  
6Jan2018  neiptopuni 17131  Lemma for neiptopreu 17134 (Contributed by Thierry Arnoux, 6Jan2018.) 
6Jan2018  neipeltop 17130  Lemma for neiptopreu 17134 (Contributed by Thierry Arnoux, 6Jan2018.) 
6Jan2018  hashdifsn 11620  The size of the difference of a finite set and a singleton subset is the set's size minus 1. (Contributed by Alexander van der Vekens, 6Jan2018.) 
6Jan2018  hashgt0elex 11611  If the size of a set is greater than zero, the set must contain at least one element. (Contributed by Alexander van der Vekens, 6Jan2018.) 
6Jan2018  hashle00 11610  If the size of a set is less than or equal to zero, the set must be empty. (Contributed by Alexander van der Vekens, 6Jan2018.) 
6Jan2018  nn0pnfge0 10674  If a number is a nonnegative integer or positive infinity, it is greater than or equal to 0. (Contributed by Alexander van der Vekens, 6Jan2018.) 
6Jan2018  nfald 1867  If is not free in , it is not free in . (Contributed by Mario Carneiro, 24Sep2016.) (Proof shortened by Wolf Lammen, 6Jan2018.) 
5Jan2018  fallfacfac 25132  Relate falling factorial to factorial. (Contributed by Scott Fenton, 5Jan2018.) 
FallFac  
5Jan2018  risefacfac 25131  Relate rising factorial to factorial. (Contributed by Scott Fenton, 5Jan2018.) 
RiseFac  
5Jan2018  fallfac1 25130  The value of falling factorial at one. (Contributed by Scott Fenton, 5Jan2018.) 
FallFac  
5Jan2018  risefac1 25129  The value of rising factorial at one. (Contributed by Scott Fenton, 5Jan2018.) 
RiseFac  
5Jan2018  fallfacp1 25128  The value of the falling factorial at a successor. (Contributed by Scott Fenton, 5Jan2018.) 
FallFac FallFac  
5Jan2018  risefacp1 25127  The value of the rising factorial at a successor. (Contributed by Scott Fenton, 5Jan2018.) 
RiseFac RiseFac  
5Jan2018  fallfac0 25126  The value of the falling factorial when . (Contributed by Scott Fenton, 5Jan2018.) 
FallFac  
5Jan2018  risefac0 25125  The value of the rising factorial when . (Contributed by Scott Fenton, 5Jan2018.) 
RiseFac  
5Jan2018  risefall0lem 25124  Lemma for risefac0 25125 and fallfac0 25126. Show a particular set of finite integers is empty. (Contributed by Scott Fenton, 5Jan2018.) 
5Jan2018  nn0risefaccl 25120  Closure law for rising factorial. (Contributed by Scott Fenton, 5Jan2018.) 
RiseFac  
5Jan2018  zfallfaccl 25119  Closure law for falling factorial. (Contributed by Scott Fenton, 5Jan2018.) 
FallFac  
5Jan2018  zrisefaccl 25118  Closure law for rising factorial. (Contributed by Scott Fenton, 5Jan2018.) 
RiseFac  
5Jan2018  nnrisefaccl 25117  Closure law for rising factorial. (Contributed by Scott Fenton, 5Jan2018.) 
RiseFac  
5Jan2018  refallfaccl 25116  Closure law for falling factorial. (Contributed by Scott Fenton, 5Jan2018.) 
FallFac  
5Jan2018  rerisefaccl 25115  Closure law for rising factorial. (Contributed by Scott Fenton, 5Jan2018.) 
RiseFac  
5Jan2018  fallfaccl 25114  Closure law for falling factorial. (Contributed by Scott Fenton, 5Jan2018.) 
FallFac  
5Jan2018  risefaccl 25113  Closure law for rising factorial. (Contributed by Scott Fenton, 5Jan2018.) 
RiseFac  
5Jan2018  fallfaccllem 25112  Lemma for falling factorial closure laws. (Contributed by Scott Fenton, 5Jan2018.) 
FallFac  
5Jan2018  risefaccllem 25111  Lemma for rising factorial closure laws. (Contributed by Scott Fenton, 5Jan2018.) 
RiseFac  
5Jan2018  fallfacval 25108  The value of the falling factorial function. (Contributed by Scott Fenton, 5Jan2018.) 
FallFac  
5Jan2018  risefacval 25107  The value of the rising factorial function. (Contributed by Scott Fenton, 5Jan2018.) 
RiseFac  
5Jan2018  dffallfac 25106  Define the falling factorial function. This is the function for complex and nonnegative integers . (Contributed by Scott Fenton, 5Jan2018.) 
FallFac  
5Jan2018  dfrisefac 25105  Define the rising factorial function. This is the function for complex and nonnegative integers . (Contributed by Scott Fenton, 5Jan2018.) 
RiseFac  
5Jan2018  fprodrev 25094  Reversal of a finite product. (Contributed by Scott Fenton, 5Jan2018.) 
5Jan2018  fprodshft 25093  Shift the index of a finite product. (Contributed by Scott Fenton, 5Jan2018.) 
5Jan2018  climlec3 25007  Comparison of a constant to the limit of a sequence. (Contributed by Scott Fenton, 5Jan2018.) 
5Jan2018  usgrafisbase 21308  Induction base for usgrafis 21309. Main work is done in usgrafisindb0 21302. (Contributed by Alexander van der Vekens, 5Jan2018.) 
USGrph  
5Jan2018  usgrafisinds 21307  In a graph with a finite number of vertices, the number of edges is finite if the number of edges not containing one of the vertices is finite. Used for the step of the induction in usgrafis 21309. (Contributed by Alexander van der Vekens, 5Jan2018.) 
USGrph  
5Jan2018  usgrafisindb1 21303  The size of a finite simple graph with 1 vertex is 0. (Contributed by Alexander van der Vekens, 5Jan2018.) 
USGrph  
5Jan2018  usgrafisindb0 21302  The size of a finite simple graph with 0 vertices is 0. Used for the base case of the induction in usgrafis 21309. (Contributed by Alexander van der Vekens, 5Jan2018.) 
USGrph  
5Jan2018  utoptopon 18201  Topology induced by a uniform structure with its base set. (Contributed by Thierry Arnoux, 5Jan2018.) 
UnifOn unifTop TopOn  
5Jan2018  ustssco 18179  In an uniform structure, any entourage is a subset of its composition with itself. (Contributed by Thierry Arnoux, 5Jan2018.) 
UnifOn  
5Jan2018  19.9h 1790  A wff may be existentially quantified with a variable not free in it. Theorem 19.9 of [Margaris] p. 89. (Contributed by FL, 24Mar2007.) (Proof shortened by Wolf Lammen, 5Jan2018.) 
4Jan2018  cusgrasizeindslem1 21362  Lemma 1 for cusgrasizeinds 21365. The domain of the edge function is the union of the arguments/indices of all edges containing a specific vertex and the arguments/indices of all edges not containing this vertex. (Contributed by Alexander van der Vekens, 4Jan2018.) 
4Jan2018  usgrafilem2 21306  In a graph with a finite number of vertices, the number of edges is finite if and only if the number of edges not containing one of the vertices is finite. (Contributed by Alexander van der Vekens, 4Jan2018.) 
USGrph  
4Jan2018  usgrafilem1 21305  The domain of the edge function is the union of the arguments/indices of all edges containing a specific vertex and the arguments/indices of all edges not containing this vertex. (Contributed by Alexander van der Vekens, 4Jan2018.) 
4Jan2018  fiusgraedgfi 21301  In a finite graph the number of edges which contain a given vertex is also finite. (Contributed by Alexander van der Vekens, 4Jan2018.) 
USGrph  
4Jan2018  usgraedgleord 21293  In a graph the number of edges which contain a given vertex is not greater than the number of vertices. (Contributed by Alexander van der Vekens, 4Jan2018.) 
USGrph  
4Jan2018  usgraidx2v 21292  The mapping of indices of edges containing a given vertex into the set of vertices is 11. The index is mapped to the other vertex of the edge containing the vertex N. (Contributed by Alexander van der Vekens, 4Jan2018.) 
USGrph  
4Jan2018  usgraidx2vlem2 21291  Lemma 2 for usgraidx2v 21292. (Contributed by Alexander van der Vekens, 4Jan2018.) 
USGrph  
4Jan2018  usgraidx2vlem1 21290  Lemma 1 for usgraidx2v 21292. (Contributed by Alexander van der Vekens, 4Jan2018.) 
USGrph  
4Jan2018  usgraedgreu 21287  The value of the "edge function" of a graph is a uniquely determined set containing two elements (the endvertices of the corresponding edge). Concretising usgraedg4 21286. (Contributed by Alexander van der Vekens, 4Jan2018.) 
USGrph  
4Jan2018  uspreg 18239  If a uniform space is Hausdorff, it is regular. Proposition 3 of [BourbakiTop1] p. II.5. (Contributed by Thierry Arnoux, 4Jan2018.) 
UnifSp  
4Jan2018  ustexsym 18180  In an uniform structure, for any entourage , there exists a smaller symmetrical entourage. (Contributed by Thierry Arnoux, 4Jan2018.) 
UnifOn  
3Jan2018  cnnei 17282  Continuity in terms of neighborhoods. (Contributed by Thierry Arnoux, 3Jan2018.) 
3Jan2018  finresfin 7284  The restriction of a finite set is finite. (Contributed by Alexander van der Vekens, 3Jan2018.) 
3Jan2018  raldifb 3444  Restricted universal quantification on a class difference in terms of an implication. (Contributed by Alexander van der Vekens, 3Jan2018.) 
3Jan2018  19.12 1865  Theorem 19.12 of [Margaris] p. 89. Assuming the converse is a mistake sometimes made by beginners! But sometimes the converse does hold, as in 19.12vv 1917 and r19.12sn 3829. (Contributed by NM, 5Aug1993.) (Proof shortened by Wolf Lammen, 3Jan2018.) 
3Jan2018  hbimd 1830  Deduction form of boundvariable hypothesis builder hbim 1832. (Contributed by NM, 1Jan2002.) (Proof shortened by Wolf Lammen, 3Jan2018.) 
3Jan2018  19.21t 1809  Closed form of Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 27May1997.) (Revised by Mario Carneiro, 24Sep2016.) (Proof shortened by Wolf Lammen, 3Jan2018.) 
2Jan2018  volsupnfl 25972  volsup 19331 is incompatible with the FefermanLevy model. (Contributed by Brendan Leahy, 2Jan2018.) 
2Jan2018  cusgrares 21361  Restricting a complete simple graph. (Contributed by Alexander van der Vekens, 2Jan2018.) 
ComplUSGrph ComplUSGrph  
2Jan2018  cusgrasizeindb1 21360  Base case of the induction in cusgrasize 21367. The size of a complete simple graph with 1 vertex is 0=((11)*1)/2. (Contributed by Alexander van der Vekens, 2Jan2018.) 
ComplUSGrph  
2Jan2018  cusgrasizeindb0 21359  Base case of the induction in cusgrasize 21367. The size of a complete simple graph with 0 vertices is 0=((01)*0)/2. (Contributed by Alexander van der Vekens, 2Jan2018.) 
ComplUSGrph  
2Jan2018  usgrares1 21304  Restricting an undirected simple graph. (Contributed by Alexander van der Vekens, 2Jan2018.) 
USGrph USGrph  
2Jan2018  nfbi 1852  If is not free in and , it is not free in . (Contributed by Mario Carneiro, 11Aug2016.) (Proof shortened by Wolf Lammen, 2Jan2018.) 
2Jan2018  hb3an 1848  If is not free in , , and , it is not free in . (Contributed by NM, 14Sep2003.) (Proof shortened by Wolf Lammen, 2Jan2018.) 
2Jan2018  hban 1846  If is not free in and , it is not free in . (Contributed by NM, 5Aug1993.) (Proof shortened by Wolf Lammen, 2Jan2018.) 
2Jan2018  nfnan 1843  If is not free in and , then it is not free in . (Contributed by Scott Fenton, 2Jan2018.) 
2Jan2018  nfim 1828  If is not free in and , it is not free in . (Contributed by Mario Carneiro, 11Aug2016.) (Proof shortened by Wolf Lammen, 2Jan2018.) 
2Jan2018  nfim1 1826  A closed form of nfim 1828. (Contributed by NM, 5Aug1993.) (Revised by Mario Carneiro, 24Sep2016.) (Proof shortened by Wolf Lammen, 2Jan2018.) 
2Jan2018  19.23t 1814  Closed form of Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 7Nov2005.) (Proof shortened by Wolf Lammen, 2Jan2018.) 
2Jan2018  19.38 1808  Theorem 19.38 of [Margaris] p. 90. (Contributed by NM, 5Aug1993.) (Revised by Wolf Lammen, 2Jan2018.) 
2Jan2018  nanbi12d 1309  Join two logical equivalences with anticonjunction. (Contributed by Scott Fenton, 2Jan2018.) 
2Jan2018  nanbi2d 1308  Introduce a left anticonjunct to both sides of a logical equivalence. (Contributed by SF, 2Jan2018.) 
2Jan2018  nanbi1d 1307  Introduce a right anticonjunct to both sides of a logical equivalence. (Contributed by SF, 2Jan2018.) 
2Jan2018  nanbi12i 1306  Join two logical equivalences with anticonjunction. (Contributed by SF, 2Jan2018.) 
2Jan2018  nanbi2i 1305  Introduce a left anticonjunct to both sides of a logical equivalence. (Contributed by SF, 2Jan2018.) 
2Jan2018  nanbi1i 1304  Introduce a right anticonjunct to both sides of a logical equivalence. (Contributed by SF, 2Jan2018.) 
2Jan2018  nanbi12 1303  Join two logical equivalences with anticonjunction. (Contributed by SF, 2Jan2018.) 
2Jan2018  nanbi2 1302  Introduce a left anticonjunct to both sides of a logical equivalence. (Contributed by SF, 2Jan2018.) 
2Jan2018  nanbi1 1301  Introduce a right anticonjunct to both sides of a logical equivalence. (Contributed by SF, 2Jan2018.) 
1Jan2018  frgraregorufr 27821  For each nonnegative integer K there are either no edges having degree K, or all vertices have degree K in a friendship graph, unless there is a universal friend. This corresponds to the second claim in the proof of the friendship theorem in [Huneke] p. 2: "Suppose there is a vertex of degree k > 1. ... all vertices have degree k, unless there is a universal friend. ... It follows that G is kregular, i.e., the degree of every vertex is k". (Contributed by Alexander van der Vekens, 1Jan2018.) 
FriendGrph VDeg VDeg  
1Jan2018  frgraregorufr0 27820  For each nonnegative integer K there are either no edges having degree K, or all vertices have degree K in a friendship graph, unless there is a universal friend. This corresponds to the second claim in the proof of the friendship theorem in [Huneke] p. 2: "... all vertices have degree k, unless there is a universal friend." (Contributed by Alexander van der Vekens, 1Jan2018.) 
FriendGrph VDeg VDeg  
1Jan2018  frgrawopreg2 27819  According to the proof of the friendship theorem in [Huneke] p. 2: "If ... B is a singleton, then that singleton is a universal friend". (Contributed by Alexander van der Vekens, 1Jan2018.) 
VDeg FriendGrph  
1Jan2018  frgrawopreg1 27818  According to the proof of the friendship theorem in [Huneke] p. 2: "If A ... is a singleton, then that singleton is a universal friend". (Contributed by Alexander van der Vekens, 1Jan2018.) 
VDeg FriendGrph  
1Jan2018  cnextcn 18033  Extension by continuity. Theorem 1 of [BourbakiTop1] p. I.57. Given a topology on , a subset dense in , this states a condition for from to a regular space to be extensible by continuity (Contributed by Thierry Arnoux, 1Jan2018.) 
↾_{t} CnExt  
1Jan2018  bc0k 11543  The binomial coefficient " 0 choose " is 0 for a positive integer K. Note that (see bcn0 11542). (Contributed by Alexander van der Vekens, 1Jan2018.) 
1Jan2018  exsnrex 3805  There is a set being the element of a singleton if and only if there is an element of the singleton. (Contributed by Alexander van der Vekens, 1Jan2018.) 
1Jan2018  hbim 1832  If is not free in and , it is not free in . (Contributed by NM, 5Aug1993.) (Proof shortened by O'Cat, 3Mar2008.) (Proof shortened by Wolf Lammen, 1Jan2018.) 
1Jan2018  exlimih 1818  Inference from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 5Aug1993.) (Proof shortened by Andrew Salmon, 13May2011.) (Proof shortened by Wolf Lammen, 1Jan2018.) 
1Jan2018  19.23h 1816  Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 5Aug1993.) (Revised by Mario Carneiro, 24Sep2016.) (Proof shortened by Wolf Lammen, 1Jan2018.) 
1Jan2018  stdpc5 1812  An axiom scheme of standard predicate calculus that emulates Axiom 5 of [Mendelson] p. 69. The hypothesis can be thought of as emulating " is not free in ." With this definition, the meaning of "not free" is less restrictive than the usual textbook definition; for example would not (for us) be free in by nfequid 1686. This theorem scheme can be proved as a metatheorem of Mendelson's axiom system, even though it is slightly stronger than his Axiom 5. (Contributed by NM, 22Sep1993.) (Revised by Mario Carneiro, 12Oct2016.) (Proof shortened by Wolf Lammen, 1Jan2018.) 
1Jan2018  19.21h 1811  Theorem 19.21 of [Margaris] p. 90. The hypothesis can be thought of as " is not free in ." (Contributed by NM, 1Aug2017.) (Proof shortened by Wolf Lammen, 1Jan2018.) 
31Dec2017  frgrawopreg 27817  In a friendship graph there are either no vertices or exactly one vertex having degree K, or all or all except one vertices have degree K. (Contributed by Alexander van der Vekens, 31Dec2017.) 
VDeg FriendGrph  
31Dec2017  frgrawopreglem5 27816  Lemma 5 for frgrawopreg 27817. If A as well as B contain at least two vertices in a friendship graph, there is a 4cycle in the graph. This corresponds to the observation in the proof of [Huneke] p. 2: "... otherwise, there are two different vertices in A, and they have two common neighbors in B, ...". (Contributed by Alexander van der Vekens, 31Dec2017.) 
VDeg FriendGrph  
31Dec2017  frgrawopreglem1 27812  Lemma 1 for frgrawopreg 27817. In a friendship graph, the classes A and B are sets. (Contributed by Alexander van der Vekens, 31Dec2017.) 
VDeg FriendGrph  
31Dec2017  difrab0eq 3645  If the difference between the restricting class of a restricted class abstraction and the restricted class abstraction is empty, the restricting class is equal to this restricted class abstraction. (Contributed by Alexander van der Vekens, 31Dec2017.) 
31Dec2017  ssrabeq 3386  If the restricting class of a restricted class abstraction is a subset of this restricted class abstraction, it is equal to this restricted class abstraction. (Contributed by Alexander van der Vekens, 31Dec2017.) 
31Dec2017  elrabi 3047  Implication for the membership in a restricted class abstraction. (Contributed by Alexander van der Vekens, 31Dec2017.) 
31Dec2017  axi12 2381 
Axiom of Quantifier Introduction (intuitionistic logic axiom axi12).
In classical logic, this is mostly a restatement of ax12o 1976 (with one additional quantifier). But in intuitionistic logic, changing the negations and implications to disjunctions makes it stronger. (Contributed by Jim Kingdon, 31Dec2017.) 
31Dec2017  axi11e 2380  Axiom of Variable Substitution for Existence (intuitionistic logic axiom axi11e). This can be derived from ax11 1757 in a classical context but a separate axiom is needed for intuitionistic predicate calculus. (Contributed by Jim Kingdon, 31Dec2017.) 
31Dec2017  axi10 2379  Axiom of Quantifier Substitution (intuitionistic logic axiom ax10). This is just ax10 1991 by another name. (Contributed by Jim Kingdon, 31Dec2017.) 
31Dec2017  axi9 2378  Axiom of existence (intuitionistic logic axiom axi9). In classical logic, this is equivalent to ax9 1662 but in intuitionistic logic it needs to be stated using the existential quantifier. (Contributed by Jim Kingdon, 31Dec2017.) 
31Dec2017  axie2 2377  A key property of existential quantification (intuitionistic logic axiom axie2). (Contributed by Jim Kingdon, 31Dec2017.) 
31Dec2017  axie1 2376  is bound in (intuitionistic logic axiom axie1). (Contributed by Jim Kingdon, 31Dec2017.) 
31Dec2017  axial 2375  is not free in (intuitionistic logic axiom axial). (Contributed by Jim Kingdon, 31Dec2017.) 
31Dec2017  axi5r 2374  Converse of ax5o (intuitionistic logic axiom axi5r). (Contributed by Jim Kingdon, 31Dec2017.) 
31Dec2017  axi4 2373  Specialization (intuitionistic logic axiom ax4). This is just sp 1759 by another name. (Contributed by Jim Kingdon, 31Dec2017.) 
30Dec2017  frgrawopreglem4 27815  Lemma 4 for frgrawopreg 27817. In a friendship graph each vertex with degree K is connected with a vertex with degree other than K. This corresponds to the observation in the proof of [Huneke] p. 2: "By the first claim, every vertex in A is adjacent to every vertex in B." (Contributed by Alexander van der Vekens, 30Dec2017.) 
VDeg FriendGrph  
30Dec2017  frgrawopreglem3 27814  Lemma 3 for frgrawopreg 27817. The vertices in the sets A and B have different degrees. (Contributed by Alexander van der Vekens, 30Dec2017.) 
VDeg VDeg VDeg  
30Dec2017  frgrawopreglem2 27813  Lemma 2 for frgrawopreg 27817. In a friendship graph with at least 2 vertices, the degree of a vertex must be at least 2. (Contributed by Alexander van der Vekens, 30Dec2017.) 
VDeg FriendGrph  
30Dec2017  vdgrnn0pnf 21542  The degree of a vertex is either a nonnegative integer or positive infinity. (Contributed by Alexander van der Vekens, 30Dec2017.) 
USGrph VDeg  
30Dec2017  nfnf 1863  If is not free in , it is not free in . (Contributed by Mario Carneiro, 11Aug2016.) (Proof shortened by Wolf Lammen, 30Dec2017.) 
30Dec2017  nfex 1861  If is not free in , it is not free in . (Contributed by Mario Carneiro, 11Aug2016.) (Proof shortened by Wolf Lammen, 30Dec2017.) 
30Dec2017  nfimd 1823  If in a context is not free in and , it is not free in . (Contributed by Mario Carneiro, 24Sep2016.) (Proof shortened by Wolf Lammen, 30Dec2017.) 
30Dec2017  19.9 1793  A wff may be existentially quantified with a variable not free in it. Theorem 19.9 of [Margaris] p. 89. (Contributed by FL, 24Mar2007.) (Revised by Mario Carneiro, 24Sep2016.) (Proof shortened by Wolf Lammen, 30Dec2017.) 
29Dec2017  hashv01gt1 11570  The size of a set is either 0 or 1 or greater than 1. (Contributed by Alexander van der Vekens, 29Dec2017.) 
29Dec2017  cbv3hv 1874  Lemma for ax10 1991. Similar to cbv3h 2036. Requires distinct variables but avoids ax12 1946. (Contributed by NM, 25Jul2015.) (Proof shortened by Wolf Lammen, 29Dec2017.) 
29Dec2017  nfbid 1850  If in a context is not free in and , it is not free in . (Contributed by Mario Carneiro, 24Sep2016.) (Proof shortened by Wolf Lammen, 29Dec2017.) 
28Dec2017  hauseqcn 24111  In a Hausdorff topology, two continuous functions which agree on a dense set agree everywhere. (Contributed by Thierry Arnoux, 28Dec2017.) 
28Dec2017  equsalhw 1856  Weaker version of equsalh 1968 (requiring distinct variables) without using ax12 1946. (Contributed by NM, 29Nov2015.) (Proof shortened by Wolf Lammen, 28Dec2017.) 
28Dec2017  nfnd 1805  If in a context is not free in , it is not free in . (Contributed by Mario Carneiro, 24Sep2016.) (Proof shortened by Wolf Lammen, 28Dec2017.) 
27Dec2017  fprodeq0 25092  Anything finite product containing a zero term is itself zero. (Contributed by Scott Fenton, 27Dec2017.) 
27Dec2017  fprodp1s 25087  Multiply in the last term in a finite product. (Contributed by Scott Fenton, 27Dec2017.) 
27Dec2017  fprodm1s 25086  Separate out the last term in a finite product. (Contributed by Scott Fenton, 27Dec2017.) 
27Dec2017  umisuhgra 21243  An undirected multigraph is an undirected hypergraph. (Contributed by Alexander van der Vekens, 27Dec2017.) 
UMGrph UHGrph  
27Dec2017  uhgraun 21227  If and are hypergraphs, then is a hypergraph (the vertex set stays the same, but the edges from both graphs are kept, maybe resulting in two edges between two vertices), analogous to umgraun 21244. (Contributed by Alexander van der Vekens, 27Dec2017.) 
UHGrph UHGrph UHGrph  
27Dec2017  uhgra0v 21226  The null graph, with no vertices, is a hypergraph if and only if the edge function is empty. (Contributed by Alexander van der Vekens, 27Dec2017.) 
UHGrph  
27Dec2017  uhgra0 21225  The empty graph, with vertices but no edges, is a hypergraph, analogous to umgra0 21241. (Contributed by Alexander van der Vekens, 27Dec2017.) 
UHGrph  
27Dec2017  uhgrares 21224  A subgraph of a hypergraph (formed by removing some edges from the original graph) is a hypergraph, analogous to umgrares 21240. (Contributed by Alexander van der Vekens, 27Dec2017.) 
UHGrph UHGrph  
26Dec2017  fprodefsum 25091  Move the exponential function from inside a finite product to outside a finite sum. (Contributed by Scott Fenton, 26Dec2017.) 
26Dec2017  uhgraeq12d 21223  Equality of hypergraphs. (Contributed by Alexander van der Vekens, 26Dec2017.) 
UHGrph UHGrph  
26Dec2017  uhgrass 21222  An edge is a subset of vertices, analogous to umgrass 21235. (Contributed by Alexander van der Vekens, 26Dec2017.) 
UHGrph  
26Dec2017  uhgrafun 21221  The edge function of an undirected hypergraph is a function. (Contributed by Alexander van der Vekens, 26Dec2017.) 
UHGrph  
26Dec2017  uhgraf 21220  The edge function of an undirected hypergraph is a function into the power set of the set of vertices. (Contributed by Alexander van der Vekens, 26Dec2017.) 
UHGrph  
26Dec2017  isuhgra 21219  The property of being an undirected hypergraph. (Contributed by Alexander van der Vekens, 26Dec2017.) 
UHGrph  
26Dec2017  uhgrav 21218  The classes of vertices and edges of an undirected hypergraph are sets. (Contributed by Alexander van der Vekens, 26Dec2017.) 
UHGrph  
26Dec2017  reluhgra 21217  The class of all undirected hypergraphs is a relation. (Contributed by Alexander van der Vekens, 26Dec2017.) 
UHGrph  
26Dec2017  dfuhgra 21216  Define the class of all undirected hypergraphs. An undirected hypergraph is a pair of a set and a function into the powerset of this set (the empty set excluded). (Contributed by Alexander van der Vekens, 26Dec2017.) 
UHGrph  
25Dec2017  fprodabs 25090  The absolute value of a finite product. (Contributed by Scott Fenton, 25Dec2017.) 
25Dec2017  prodsns 25088  A product of the singleton is the term. (Contributed by Scott Fenton, 25Dec2017.) 
25Dec2017  cnextf 18032  Extension by continuity. The extension by continuity is a function. (Contributed by Thierry Arnoux, 25Dec2017.) 
↾_{t} CnExt  
25Dec2017  hasheqf1oi 11576  The size of two sets is equal if there is a bijection mapping one of the sets onto the other. (Contributed by Alexander van der Vekens, 25Dec2017.) 
25Dec2017  fiinfnf1o 11575  There is no bijection between a finite set and an infinite set. (Contributed by Alexander van der Vekens, 25Dec2017.) 
25Dec2017  spfalw 1680  Version of sp 1759 when is false. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 23Apr1017.) (Proof shortened by Wolf Lammen, 25Dec2017.) 
24Dec2017  frgrancvvdeqlem9 27809  Lemma 9 for frgrancvvdeq 27810. (Contributed by Alexander van der Vekens, 24Dec2017.) 
FriendGrph Neighbors Neighbors Neighbors  
24Dec2017  frgrancvvdeqlem8 27808  Lemma 8 for frgrancvvdeq 27810. (Contributed by Alexander van der Vekens, 24Dec2017.) 
Neighbors Neighbors FriendGrph  
24Dec2017  frgrancvvdeqlemC 27807  Lemma C for frgrancvvdeq 27810. This corresponds to the following observation in [Huneke] p. 1: "By symmetry the map is onto". (Contributed by Alexander van der Vekens, 24Dec2017.) 
Neighbors Neighbors FriendGrph  
24Dec2017  fprodp1 25085  Multiply in the last term in a finite product. (Contributed by Scott Fenton, 24Dec2017.) 
24Dec2017  fprod1p 25084  Separate out the first term in a finite product. (Contributed by Scott Fenton, 24Dec2017.) 
23Dec2017  frgrancvvdeqlemB 27806  Lemma B for frgrancvvdeq 27810. This corresponds to the following observation in [Huneke] p. 1: "The map is onetoone since z in N(x) is uniquely determined as the common neighbor of x and a(x)". (Contributed by Alexander van der Vekens, 23Dec2017.) 
Neighbors Neighbors FriendGrph  
23Dec2017  frgrancvvdeqlemA 27805  Lemma A for frgrancvvdeq 27810. This corresponds to the following observation in [Huneke] p. 1: "This common neighbor cannot be x, as x and y are not adjacent.". (Contributed by Alexander van der Vekens, 23Dec2017.) 
Neighbors Neighbors FriendGrph 