Metamath Proof Explorer Home Metamath Proof Explorer
Most Recent Proofs
 
Mirrors  >  Home  >  MPE Home  >  Th. List  >  Recent Other  >  MM 100

Most recent proofs    These are the 10 (GIF, Unicode) or 1000 (GIF, Unicode) most recent proofs in the set.mm database for the Metamath Proof Explorer (and the Hilbert Space Explorer). The set.mm database is maintained on GitHub with master (stable) and develop (development) versions. This page was created from develop commit 3a7be31, also available here: set.mm (30MB) or set.mm.bz2 (compressed, 8MB).

Other links    Email: Norm Megill.    Mailing list: Metamath Google Group Updated 8-Aug-2017 .    Syndication: RSS feed (courtesy of Dan Getz).    Related wikis: Wikiproofs (JHilbert) (Recent Changes); Ghilbert site; Ghilbert Google Group.

Recent news items    (7-Aug-2017) Mario Carneiro added a new proof to the 100 theorem list, Principle of Inclusion/Exclusion incexc, bringing the Metamath total to 65.

(1-Jul-2017) 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).

(7-May-2017) Thierry Arnoux added a new proof to the 100 theorem list, Betrand's Ballot Problem ballotth, bringing the Metamath total to 63.

(20-Apr-2017) Glauco Siliprandi added a new proof in the supplementary list on the 100 theorem list, Stone-Weierstrass Theorem stowei.

(24-Mar-2017) Alan Sare updated his completeusersproof program.

(28-Feb-2017) David Moews added a new proof to the 100 theorem list, Product of Segments of Chords chordthm, bringing the Metamath total to 62.

(18-Feb-2017) Filip Cernatescu announced Milpgame 0.1 (MILP: Math is like a puzzle!).

(1-Jan-2017) Saveliy Skresanov added a new proof to the 100 theorem list, Isosceles triangle theorem isosctr, bringing the Metamath total to 61.

(1-Jan-2017) Mario Carneiro added 2 new proofs to the 100 theorem list, L'Hôpital's Rule lhop and Taylor's Theorem taylth, bringing the Metamath total to 60.

(28-Dec-2016) David A. Wheeler is putting together a page on Metamath (specifically set.mm) conventions. Comments are welcome on the Google Group thread.

(24-Dec-2016) Mario Carneiro introduced the abbreviation "F/ x ph" (symbols: turned F, x, phi) in df-nf to represent the "effectively not free" idiom "A. x ( ph -> A. x ph )". Theorem nf2 shows a version without nested quantifiers.

(22-Dec-2016) Naip Moro has developed a Metamath database for G. Spencer-Brown's Laws of Form. You can follow the Google Group discussion here.

(20-Dec-2016) In metamath program version 0.137, 'verify markup *' now checks that ax-XXX $a matches axXXX $p when the latter exists, per the discussion at https://groups.google.com/d/msg/metamath/Vtz3CKGmXnI/Fxq3j1I_EQAJ.

(24-Nov-2016) Mingl Yuan has kindly provided a mirror site in Beijing, China. He has also provided an rsync server; type "rsync cn.metamath.org::" in a bash shell to check its status (it should return "metamath metamath").

(14-Aug-2016) All HTML pages on this site should now be mobile-friendly and pass the Mobile-Friendly Test. If you find one that does not, let me know.

(14-Aug-2016) Daniel Whalen wrote a paper describing the use of using deep learning to prove 14% of test theorems taken from set.mm: Holophrasm: a neural Automated Theorem Prover for higher-order logic. The associated program is called Holophrasm.

(14-Aug-2016) David A. Wheeler created a video called Metamath Proof Explorer: A Modern Principia Mathematica

(12-Aug-2016) A Gitter chat room has been created for Metamath.

(9-Aug-2016) Mario Carneiro wrote a Metamath proof verifier in the Scala language as part of the ongoing Metamath -> MMT import project

(9-Aug-2016) David A. Wheeler created a GitHub project called metamath-test (last execution run) to check that different verifiers both pass good databases and detect errors in defective ones.

(4-Aug-2016) Mario gave two presentations at CICM 2016.

(17-Jul-2016) Thierry Arnoux has written EMetamath, a Metamath plugin for the Eclipse IDE.

(16-Jul-2016) Mario recovered Chris Capel's collapsible proof demo.

(13-Jul-2016) FL sent me an updated version of PDF (LaTeX source) developed with Lamport's pf2 package. See the 23-Apr-2012 entry below.

(12-Jul-2016) David A. Wheeler produced a new video for mmj2 called "Creating functions in Metamath". It shows a more efficient approach than his previous recent video "Creating functions in Metamath" (old) but it can be of interest to see both approaches.

(10-Jul-2016) Metamath program version 0.132 changes the command 'show restricted' to 'show discouraged' and adds a new command, 'set discouragement'. See the mmnotes.txt entry of 11-May-2016 (updated 10-Jul-2016).

(12-Jun-2016) Dan Getz has written Metamath.jl, a Metamath proof verifier written in the Julia language.    Older news...

Color key:   Metamath Proof Explorer  Metamath Proof Explorer   Hilbert Space Explorer  Hilbert Space Explorer   User Mathboxes  User Mathboxes  

Last updated on 10-Aug-2017 at 8:35 AM ET.
Recent Additions to the Metamath Proof Explorer   Notes (last updated 14-May-2017 )
DateLabelDescription
Theorem
 
7-Aug-2017incexc2 12291 The inclusion/exclusion principle for counting the elements of a finite union of finite sets. (Contributed by Mario Carneiro, 7-Aug-2017.)
 |-  ( ( A  e.  Fin  /\  A  C_  Fin )  ->  ( # `  U. A )  =  sum_ n  e.  ( 1 ... ( # `
  A ) ) ( ( -u 1 ^ ( n  -  1 ) )  x. 
 sum_ s  e.  { k  e.  ~P A  |  ( # `  k )  =  n }  ( # ` 
 |^| s ) ) )
 
7-Aug-2017incexc 12290 The inclusion/exclusion principle for counting the elements of a finite union of finite sets. (Contributed by Mario Carneiro, 7-Aug-2017.)
 |-  ( ( A  e.  Fin  /\  A  C_  Fin )  ->  ( # `  U. A )  =  sum_ s  e.  ( ~P A  \  { (/) } ) ( ( -u 1 ^ (
 ( # `  s )  -  1 ) )  x.  ( # `  |^| s
 ) ) )
 
7-Aug-2017incexclem 12289 Lemma for incexc 12290. (Contributed by Mario Carneiro, 7-Aug-2017.)
 |-  ( ( A  e.  Fin  /\  B  e.  Fin )  ->  ( ( # `  B )  -  ( # `  ( B  i^i  U. A ) ) )  =  sum_ s  e.  ~P  A ( (
 -u 1 ^ ( # `
  s ) )  x.  ( # `  ( B  i^i  |^| s ) ) ) )
 
7-Aug-2017spimw 1644 Specialization. Lemma 8 of [KalishMontague] p. 87. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 19-Apr-2017.) (Proof shortened by Wolf Lammen, 7-Aug-2017.)
 |-  ( -.  ps  ->  A. x  -.  ps )   &    |-  ( x  =  y  ->  (
 ph  ->  ps ) )   =>    |-  ( A. x ph 
 ->  ps )
 
7-Aug-2017spimfw 1632 Specialization, with additional weakening to allow bundling of  x and  y. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 23-Apr-1017.) (Proof shortened by Wolf Lammen, 7-Aug-2017.)
 |-  ( -.  ps  ->  A. x  -.  ps )   &    |-  ( x  =  y  ->  (
 ph  ->  ps ) )   =>    |-  ( -.  A. x  -.  x  =  y 
 ->  ( A. x ph  ->  ps ) )
 
6-Aug-2017hashun3 11360 The size of the union of finite sets is the sum of their sizes minus the size of the intersection. (Contributed by Mario Carneiro, 6-Aug-2017.)
 |-  ( ( A  e.  Fin  /\  B  e.  Fin )  ->  ( # `  ( A  u.  B ) )  =  ( ( ( # `  A )  +  ( # `  B ) )  -  ( # `  ( A  i^i  B ) ) ) )
 
5-Aug-2017speimfw 1631 Specialization, with additional weakening to allow bundling of  x and  y. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 23-Apr-2017.) (Proof shortened by Wolf Lammen, 5-Aug-2017.)
 |-  ( x  =  y 
 ->  ( ph  ->  ps )
 )   =>    |-  ( -.  A. x  -.  x  =  y  ->  ( A. x ph  ->  E. x ps )
 )
 
4-Aug-2017equequ2 1653 An equivalence law for equality. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 4-Aug-2017.)
 |-  ( x  =  y 
 ->  ( z  =  x  <-> 
 z  =  y ) )
 
3-Aug-2017a9ev 1643 At least one individual exists. Weaker version of a9e 1894. When possible, use of this theorem rather than a9e 1894 is preferred since its derivation from axioms is much shorter. (Contributed by NM, 3-Aug-2017.)
 |- 
 E. x  x  =  y
 
2-Aug-2017ralbinrald 27350 Elemination of a restricted universal quantification under certain conditions. (Contributed by Alexander van der Vekens, 2-Aug-2017.)
 |-  ( ph  ->  X  e.  A )   &    |-  ( x  e.  A  ->  x  =  X )   &    |-  ( x  =  X  ->  ( ps  <->  th ) )   =>    |-  ( ph  ->  (
 A. x  e.  A  ps 
 <-> 
 th ) )
 
2-Aug-201719.2 1675 Theorem 19.2 of [Margaris] p. 89. Note: This proof is very different from Margaris' because we only have Tarski's FOL axiom schemes available at this point. See the later 19.2g 1784 for a more conventional proof. (Contributed by NM, 2-Aug-2017.)
 |-  ( A. x ph  ->  E. x ph )
 
1-Aug-2017dvelimfALT2 1739 Proof of dvelimh 1996 without using ax-12 1869. (Contributed by Andrew Salmon, 21-Jul-2011.) (Revised by NM, 1-Aug-2017.)
 |-  ( ph  ->  A. x ph )   &    |-  ( ps  ->  A. z ps )   &    |-  (
 z  =  y  ->  ( ph  <->  ps ) )   &    |-  ( -.  A. x  x  =  y  ->  ( y  =  z  ->  A. x  y  =  z )
 )   =>    |-  ( -.  A. x  x  =  y  ->  ( ps  ->  A. x ps ) )
 
1-Aug-201719.21h 1735 Theorem 19.21 of [Margaris] p. 90. The hypothesis can be thought of as " x is not free in  ph." (Contributed by NM, 1-Aug-2017.)
 |-  ( ph  ->  A. x ph )   =>    |-  ( A. x (
 ph  ->  ps )  <->  ( ph  ->  A. x ps ) )
 
1-Aug-201719.9v 1667 Special case of Theorem 19.9 of [Margaris] p. 89. (Contributed by NM, 28-May-1995.) (Revised by NM, 1-Aug-2017.)
 |-  ( E. x ph  <->  ph )
 
1-Aug-201719.3v 1666 Special case of Theorem 19.3 of [Margaris] p. 89. (Contributed by NM, 1-Aug-2017.)
 |-  ( A. x ph  <->  ph )
 
1-Aug-201719.8w 1663 Weak version of 19.8a 1722. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 1-Aug-2017.)
 |-  ( ph  ->  A. x ph )   =>    |-  ( ph  ->  E. x ph )
 
1-Aug-2017spnfw 1662 Weak version of ax-4 2078. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 1-Aug-2017.)
 |-  ( -.  ph  ->  A. x  -.  ph )   =>    |-  ( A. x ph  ->  ph )
 
28-Jul-2017tz6.12-afv 27412 Function value (Theorem 6.12(1) of [TakeutiZaring] p. 27, , analogous to tz6.12-1 5504, but it is required for A to be a set. (Contributed by Alexander van der Vekens, 28-Jul-2017.)
 |-  ( A  e.  V  ->  ( ( A F y 
 /\  E! y  A F y )  ->  ( F'
 A )  =  y ) )
 
25-Jul-2017funressnfv 27364 A restriction to a singleton with a function value is a function under certain conditions. (Contributed by Alexander van der Vekens, 25-Jul-2017.)
 |-  (
 ( ( X  e.  dom  (  F  o.  G )  /\  Fun  ( ( F  o.  G )  |`  { X } ) ) 
 /\  ( G  Fn  A  /\  X  e.  A ) )  ->  Fun  ( F  |`  { ( G `
  X ) }
 ) )
 
25-Jul-2017funcoressn 27363 A composition restricted to a singleton is a function under certain conditions. (Contributed by Alexander van der Vekens, 25-Jul-2017.)
 |-  (
 ( ( ( G `
  X )  e. 
 dom  F  /\  Fun  ( F  |`  { ( G `
  X ) }
 ) )  /\  ( G  Fn  A  /\  X  e.  A ) )  ->  Fun  ( ( F  o.  G )  |`  { X } ) )
 
25-Jul-2017fnresfnco 27362 Composition of two functions, similar to fnco 5317. (Contributed by Alexander van der Vekens, 25-Jul-2017.)
 |-  (
 ( ( F  |`  ran  G )  Fn  ran  G  /\  G  Fn  B )  ->  ( F  o.  G )  Fn  B )
 
25-Jul-2017funresfunco 27361 Composition of two functions, generalization of funco 5257. (Contributed by Alexander van der Vekens, 25-Jul-2017.)
 |-  (
 ( Fun  ( F  |` 
 ran  G )  /\  Fun  G )  ->  Fun  ( F  o.  G ) )
 
23-Jul-2017afvco2 27414 Value of a function composition, analogous to fvco2 5555. (Contributed by Alexander van der Vekens, 23-Jul-2017.)
 |-  (
 ( G  Fn  A  /\  X  e.  A ) 
 ->  ( ( F  o.  G )' X )  =  ( F' ( G'
 X ) ) )
 
23-Jul-2017dmfcoafv 27413 Domains of a function composition, analogous to dmfco 5554. (Contributed by Alexander van der Vekens, 23-Jul-2017.)
 |-  (
 ( Fun  G  /\  A  e.  dom  G ) 
 ->  ( A  e.  dom  (  F  o.  G ) 
 <->  ( G' A )  e.  dom  F )
 )
 
23-Jul-2017csbafv12g 27377 Move class substitution in and out of a function value, analogous to csbfv12g 5495, with a direct proof proposed by Mario Carneiro, analogous to csbovg 5850. (Contributed by Alexander van der Vekens, 23-Jul-2017.)
 |-  ( A  e.  V  ->  [_ A  /  x ]_ ( F' B )  =  ( [_ A  /  x ]_ F' [_ A  /  x ]_ B ) )
 
23-Jul-2017sbcfun 27358 Distribute proper substitution through the domain of a class. (Contributed by Alexander van der Vekens, 23-Jul-2017.)
 |-  ( A  e.  V  ->  (
 [. A  /  x ].
 Fun  F  <->  Fun  [_ A  /  x ]_ F ) )
 
23-Jul-2017csbdmg 27353 Distribute proper substitution through the domain of a class. (Contributed by Alexander van der Vekens, 23-Jul-2017.)
 |-  ( A  e.  V  ->  [_ A  /  x ]_ dom  B  =  dom  [_  A  /  x ]_ B )
 
23-Jul-2017sbcrel 27352 Distribute proper substitution through the domain of a class. (Contributed by Alexander van der Vekens, 23-Jul-2017.)
 |-  ( A  e.  V  ->  (
 [. A  /  x ].
 Rel  R  <->  Rel  [_ A  /  x ]_ R ) )
 
23-Jul-2017sbcss 3565 Distribute proper substitution through a subclass relation. (Contributed by Alan Sare, 22-Jul-2012.) (Proof shortened by Alexander van der Vekens, 23-Jul-2017.)
 |-  ( A  e.  B  ->  ( [. A  /  x ]. C  C_  D  <->  [_ A  /  x ]_ C  C_  [_ A  /  x ]_ D ) )
 
22-Jul-2017logbid1 27527 General logarithm when base and arg match (Contributed by David A. Wheeler, 22-Jul-2017.)
 |-  (
 ( A  e.  CC  /\  A  =/=  0  /\  A  =/=  1 )  ->  ( Alogb A )  =  1 )
 
22-Jul-2017logeq0im1 27523 if  ( log `  A )  =  0 then 
A  =  1 (Contributed by David A. Wheeler, 22-Jul-2017.)
 |-  (
 ( A  e.  CC  /\  A  =/=  0  /\  ( log `  A )  =  0 )  ->  A  =  1 )
 
22-Jul-2017eldiftp 27522 Membership in a set with three elements removed. Similar to eldifsn 3750 and eldifpr 27521. (Contributed by David A. Wheeler, 22-Jul-2017.)
 |-  ( A  e.  ( B  \  { C ,  D ,  E } )  <->  ( A  e.  B  /\  ( A  =/=  C 
 /\  A  =/=  D  /\  A  =/=  E ) ) )
 
22-Jul-2017afvres 27411 The value of a restricted function, analogous to fvres 5502. (Contributed by Alexander van der Vekens, 22-Jul-2017.)
 |-  ( A  e.  B  ->  ( ( F  |`  B )'
 A )  =  ( F' A ) )
 
22-Jul-2017afveq2 27375 Equality theorem for function value, analogous to fveq1 5484. (Contributed by Alexander van der Vekens, 22-Jul-2017.)
 |-  ( A  =  B  ->  ( F' A )  =  ( F' B ) )
 
22-Jul-2017afveq1 27374 Equality theorem for function value, analogous to fveq1 5484. (Contributed by Alexander van der Vekens, 22-Jul-2017.)
 |-  ( F  =  G  ->  ( F' A )  =  ( G' A ) )
 
22-Jul-2017dfafv2 27372 Alternative definition of  ( F' A ) using 
( F `  A
) directly. (Contributed by Alexander van der Vekens, 22-Jul-2017.)
 |-  ( F' A )  =  if ( Fdef@  A ,  ( F `
  A ) ,  _V )
 
22-Jul-2017dfdfat2 27369 Alternate definition of the predicate "defined at" not using the  Fun predicate. (Contributed by Alexander van der Vekens, 22-Jul-2017.)
 |-  ( Fdef@  A  <->  ( A  e.  dom 
 F  /\  E! y  A F y ) )
 
18-Jul-2017eldifpr 27521 Membership in a set with two elements removed. Similar to eldifsn 3750 and eldiftp 27522. (Contributed by Mario Carneiro, 18-Jul-2017.)
 |-  ( A  e.  ( B  \  { C ,  D } )  <->  ( A  e.  B  /\  A  =/=  C  /\  A  =/=  D ) )
 
17-Jul-2017logbcl 27526 General logarithm closure. (Contributed by David A. Wheeler, 17-Jul-2017.)
 |-  (
 ( B  e.  ( CC  \  { 0 ,  1 } )  /\  X  e.  ( CC  \  { 0 } )
 )  ->  ( Blogb X )  e.  CC )
 
17-Jul-2017logccne0ALT 27525 log isn't 0 if argument isn't 0 or 1. Unlike logne0 19950, this handles complex numbers. (Contributed by David A. Wheeler, 17-Jul-2017.)
 |-  (
 ( A  e.  CC  /\  A  =/=  0  /\  A  =/=  1 )  ->  ( log `  A )  =/=  0 )
 
17-Jul-2017logccne0 27524 log isn't 0 if argument isn't 0 or 1. Unlike logne0 19950, this handles complex numbers. (Contributed by David A. Wheeler, 17-Jul-2017.)
 |-  (
 ( A  e.  CC  /\  A  =/=  0  /\  A  =/=  1 )  ->  ( log `  A )  =/=  0 )
 
16-Jul-2017logb2aval 27520 Define the value of the logb function, the logarithm generalized to an arbitrary base, when used in the 2-argument form logb <. B ,  X >. (Contributed by David A. Wheeler, 21-Jan-2017.) (Revised by David A. Wheeler, 16-Jul-2017.)
 |-  (
 ( B  e.  ( CC  \  { 0 ,  1 } )  /\  X  e.  ( CC  \  { 0 } )
 )  ->  (logb `  <. B ,  X >. )  =  ( ( log `  X )  /  ( log `  B ) ) )
 
16-Jul-2017logbval 27519 Define the value of the logb function, the logarithm generalized to an arbitrary base, when used as infix. Most Metamath statements select variables in order of their use, but to make the order clearer we use "B" for base and "X" for the other operand here. Proof is similar to modval 10969. (Contributed by David A. Wheeler, 21-Jan-2017.) (Revised by David A. Wheeler, 16-Jul-2017.)
 |-  (
 ( B  e.  ( CC  \  { 0 ,  1 } )  /\  X  e.  ( CC  \  { 0 } )
 )  ->  ( Blogb X )  =  ( ( log `  X )  /  ( log `  B ) ) )
 
16-Jul-2017prmz 12756 A prime number is an integer. (Contributed by Paul Chapman, 22-Jun-2011.) (Proof shortened by Jonathan Yan, 16-Jul-2017.)
 |-  ( P  e.  Prime  ->  P  e.  ZZ )
 
14-Jul-2017df-log_ 27529 Define the log_ operator. This is the logarithm generalized to an arbitrary base. It can be used as  ( (log_ `  B ) `  X ) for "log base B of X". This formulation suggested by Mario Carneiro. (Contributed by David A. Wheeler, 14-Jul-2017.)
 |- log_  =  ( b  e.  ( CC  \  { 0 ,  1 } )  |->  ( x  e.  ( CC  \  { 0 } )  |->  ( ( log `  x )  /  ( log `  b
 ) ) ) )
 
2-Jul-2017eldmressnsn 27357 The element of the domain of a restriction to a singleton is the element of the singleton. (Contributed by Alexander van der Vekens, 2-Jul-2017.)
 |-  ( A  e.  dom  F  ->  A  e.  dom  (  F  |` 
 { A } )
 )
 
2-Jul-2017dmressnsn 27356 The domain of a restriction to a singleton is a singleton. (Contributed by Alexander van der Vekens, 2-Jul-2017.)
 |-  ( A  e.  dom  F  ->  dom  (  F  |`  { A } )  =  { A } )
 
2-Jul-2017eldmressn 27355 Element of the domain of a restriction to a singleton. (Contributed by Alexander van der Vekens, 2-Jul-2017.)
 |-  ( B  e.  dom  (  F  |`  { A } )  ->  B  =  A )
 
2-Jul-20172reu8 27349 Two equivalent expressions for double restricted existential uniqueness, analogous to 2eu8 2231. Curiously, we can put  E! on either of the internal conjuncts but not both. We can also commute  E! x  e.  A E! y  e.  B using 2reu7 27348. (Contributed by Alexander van der Vekens, 2-Jul-2017.)
 |-  ( E! x  e.  A  E! y  e.  B  ( E. x  e.  A  ph 
 /\  E. y  e.  B  ph )  <->  E! x  e.  A  E! y  e.  B  ( E! x  e.  A  ph 
 /\  E. y  e.  B  ph ) )
 
2-Jul-20172reu7 27348 Two equivalent expressions for double restricted existential uniqueness, analogous to 2eu7 2230. (Contributed by Alexander van der Vekens, 2-Jul-2017.)
 |-  (
 ( E! x  e.  A  E. y  e.  B  ph  /\  E! y  e.  B  E. x  e.  A  ph )  <->  E! x  e.  A  E! y  e.  B  ( E. x  e.  A  ph 
 /\  E. y  e.  B  ph ) )
 
2-Jul-2017reuan 27337 Introduction of a conjunct into restricted uniqueness quantifier, analogous to euan 2201. (Contributed by Alexander van der Vekens, 2-Jul-2017.)
 |-  F/ x ph   =>    |-  ( E! x  e.  A  ( ph  /\  ps ) 
 <->  ( ph  /\  E! x  e.  A  ps ) )
 
2-Jul-20172ralbiim 27331 Split a biconditional and distribute 2 quantifiers, analogous to 2albiim 1604 and ralbiim 2681. (Contributed by Alexander van der Vekens, 2-Jul-2017.)
 |-  ( A. x  e.  A  A. y  e.  B  (
 ph 
 <->  ps )  <->  ( A. x  e.  A  A. y  e.  B  ( ph  ->  ps )  /\  A. x  e.  A  A. y  e.  B  ( ps  ->  ph ) ) )
 
2-Jul-2017cbvrex2 27330 Change bound variables of double restricted universal quantification, using implicit substitution, analogous to cbvrex2v 2774. (Contributed by Alexander van der Vekens, 2-Jul-2017.)
 |-  F/ z ph   &    |-  F/ x ch   &    |-  F/ w ch   &    |-  F/ y ps   &    |-  ( x  =  z  ->  ( ph  <->  ch ) )   &    |-  (
 y  =  w  ->  ( ch  <->  ps ) )   =>    |-  ( E. x  e.  A  E. y  e.  B  ph  <->  E. z  e.  A  E. w  e.  B  ps )
 
2-Jul-2017cbvral2 27329 Change bound variables of double restricted universal quantification, using implicit substitution, analogous to cbvral2v 2773. (Contributed by Alexander van der Vekens, 2-Jul-2017.)
 |-  F/ z ph   &    |-  F/ x ch   &    |-  F/ w ch   &    |-  F/ y ps   &    |-  ( x  =  z  ->  ( ph  <->  ch ) )   &    |-  (
 y  =  w  ->  ( ch  <->  ps ) )   =>    |-  ( A. x  e.  A  A. y  e.  B  ph  <->  A. z  e.  A  A. w  e.  B  ps )
 
2-Jul-2017climreeq 27138 If  F is a real function, then  F converges to  A with respect to the standard topology on the reals if and only if it converges to  A with respect to the standard topology on complex numbers. In the theorem,  R is defined to be convergence w.r.t. the standard topology on the reals and then  F R A represents the statement " F converges to  A, with respect to the standard topology on the reals". Notice that there is no need for the hypothesis that  A is a real number. (Contributed by Glauco Siliprandi, 2-Jul-2017.)
 |-  R  =  ( ~~> t `  ( topGen `
  ran  (,) ) )   &    |-  Z  =  ( ZZ>= `  M )   &    |-  ( ph  ->  M  e.  ZZ )   &    |-  ( ph  ->  F : Z --> RR )   =>    |-  ( ph  ->  ( F R A  <->  F  ~~>  A ) )
 
1-Jul-20172reu4 27347 Definition of double restricted existential uniqueness ("exactly one  x and exactly one  y"), analogous to 2eu4 2227. (Contributed by Alexander van der Vekens, 1-Jul-2017.)
 |-  (
 ( E! x  e.  A  E. y  e.  B  ph  /\  E! y  e.  B  E. x  e.  A  ph )  <->  ( E. x  e.  A  E. y  e.  B  ph  /\  E. z  e.  A  E. w  e.  B  A. x  e.  A  A. y  e.  B  ( ph  ->  ( x  =  z  /\  y  =  w )
 ) ) )
 
1-Jul-20172reu4a 27346 Definition of double restricted existential uniqueness ("exactly one  x and exactly one  y"), analogous to 2eu4 2227 with the additional requirement that the restricting classes are not empty (which is not necessary as shown in 2reu4 27347). (Contributed by Alexander van der Vekens, 1-Jul-2017.)
 |-  (
 ( A  =/=  (/)  /\  B  =/= 
 (/) )  ->  (
 ( E! x  e.  A  E. y  e.  B  ph  /\  E! y  e.  B  E. x  e.  A  ph )  <->  ( E. x  e.  A  E. y  e.  B  ph  /\  E. z  e.  A  E. w  e.  B  A. x  e.  A  A. y  e.  B  ( ph  ->  ( x  =  z  /\  y  =  w )
 ) ) ) )
 
1-Jul-20172rexrsb 27328 An equivalent expression for double restricted existence, analogous to 2exsb 2069. (Contributed by Alexander van der Vekens, 1-Jul-2017.)
 |-  ( E. x  e.  A  E. y  e.  B  ph  <->  E. z  e.  A  E. w  e.  B  A. x  e.  A  A. y  e.  B  ( ( x  =  z  /\  y  =  w )  ->  ph )
 )
 
1-Jul-20172rexsb 27327 An equivalent expression for double restricted existence, analogous to rexsb 27325. (Contributed by Alexander van der Vekens, 1-Jul-2017.)
 |-  ( E. x  e.  A  E. y  e.  B  ph  <->  E. z  e.  A  E. w  e.  B  A. x A. y ( ( x  =  z  /\  y  =  w )  ->  ph )
 )
 
1-Jul-2017rexrsb 27326 An equivalent expression for restricted existence, analogous to exsb 2067. (Contributed by Alexander van der Vekens, 1-Jul-2017.)
 |-  ( E. x  e.  A  ph  <->  E. y  e.  A  A. x  e.  A  ( x  =  y  ->  ph ) )
 
1-Jul-2017rexsb 27325 An equivalent expression for restricted existence, analogous to exsb 2067. (Contributed by Alexander van der Vekens, 1-Jul-2017.)
 |-  ( E. x  e.  A  ph  <->  E. y  e.  A  A. x ( x  =  y  ->  ph ) )
 
30-Jun-2017stirlinglem1 27222 A simple limit of fractions is computed. (Contributed by Glauco Siliprandi, 30-Jun-2017.)
 |-  H  =  ( n  e.  NN  |->  ( ( n ^
 2 )  /  ( n  x.  ( ( 2  x.  n )  +  1 ) ) ) )   &    |-  F  =  ( n  e.  NN  |->  ( 1  -  ( 1 
 /  ( ( 2  x.  n )  +  1 ) ) ) )   &    |-  G  =  ( n  e.  NN  |->  ( 1  /  ( ( 2  x.  n )  +  1 ) ) )   &    |-  L  =  ( n  e.  NN  |->  ( 1  /  n ) )   =>    |-  H  ~~>  ( 1  / 
 2 )
 
30-Jun-2017wallispi2lem2 27220 Two expressions are proven to be equal, and this is used to complete the proof of the second version of Wallis' formula for π . (Contributed by Glauco Siliprandi, 30-Jun-2017.)
 |-  ( N  e.  NN  ->  ( 
 seq  1 (  x. 
 ,  ( k  e. 
 NN  |->  ( ( ( 2  x.  k ) ^ 4 )  /  ( ( ( 2  x.  k )  x.  ( ( 2  x.  k )  -  1
 ) ) ^ 2
 ) ) ) ) `
  N )  =  ( ( ( 2 ^ ( 4  x.  N ) )  x.  ( ( ! `  N ) ^ 4
 ) )  /  (
 ( ! `  (
 2  x.  N ) ) ^ 2 ) ) )
 
30-Jun-2017wallispi2lem1 27219 An intermediate step between the first version of the Wallis' formula for π and the second version of Wallis' formula. This second version will then be used to prove Stirling's approximation formula for the factorial. (Contributed by Glauco Siliprandi, 30-Jun-2017.)
 |-  ( N  e.  NN  ->  ( 
 seq  1 (  x. 
 ,  ( k  e. 
 NN  |->  ( ( ( 2  x.  k ) 
 /  ( ( 2  x.  k )  -  1 ) )  x.  ( ( 2  x.  k )  /  (
 ( 2  x.  k
 )  +  1 ) ) ) ) ) `
  N )  =  ( ( 1  /  ( ( 2  x.  N )  +  1 ) )  x.  (  seq  1 (  x.  ,  ( k  e.  NN  |->  ( ( ( 2  x.  k ) ^
 4 )  /  (
 ( ( 2  x.  k )  x.  (
 ( 2  x.  k
 )  -  1 ) ) ^ 2 ) ) ) ) `  N ) ) )
 
30-Jun-2017wallispilem5 27217 The sequence  H converges to 1. (Contributed by Glauco Siliprandi, 30-Jun-2017.)
 |-  F  =  ( k  e.  NN  |->  ( ( ( 2  x.  k )  /  ( ( 2  x.  k )  -  1
 ) )  x.  (
 ( 2  x.  k
 )  /  ( (
 2  x.  k )  +  1 ) ) ) )   &    |-  I  =  ( n  e.  NN0  |->  S. (
 0 (,) pi ) ( ( sin `  x ) ^ n )  _d x )   &    |-  G  =  ( n  e.  NN  |->  ( ( I `  (
 2  x.  n ) )  /  ( I `
  ( ( 2  x.  n )  +  1 ) ) ) )   &    |-  H  =  ( n  e.  NN  |->  ( ( pi  /  2
 )  x.  ( 1 
 /  (  seq  1
 (  x.  ,  F ) `  n ) ) ) )   &    |-  L  =  ( n  e.  NN  |->  ( ( ( 2  x.  n )  +  1 )  /  ( 2  x.  n ) ) )   =>    |-  H  ~~>  1
 
30-Jun-2017wallispilem4 27216  F maps to explicit expression for the ratio of two consecutive values of  I (Contributed by Glauco Siliprandi, 30-Jun-2017.)
 |-  F  =  ( k  e.  NN  |->  ( ( ( 2  x.  k )  /  ( ( 2  x.  k )  -  1
 ) )  x.  (
 ( 2  x.  k
 )  /  ( (
 2  x.  k )  +  1 ) ) ) )   &    |-  I  =  ( n  e.  NN0  |->  S. (
 0 (,) pi ) ( ( sin `  z
 ) ^ n )  _d z )   &    |-  G  =  ( n  e.  NN  |->  ( ( I `  ( 2  x.  n ) )  /  ( I `  ( ( 2  x.  n )  +  1 ) ) ) )   &    |-  H  =  ( n  e.  NN  |->  ( ( pi  /  2
 )  x.  ( 1 
 /  (  seq  1
 (  x.  ,  F ) `  n ) ) ) )   =>    |-  G  =  H
 
30-Jun-2017mulc1cncfg 27120 A version of mulc1cncf 18403 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 30-Jun-2017.)
 |-  F/_ x F   &    |- 
 F/ x ph   &    |-  ( ph  ->  F  e.  ( A -cn-> CC ) )   &    |-  ( ph  ->  B  e.  CC )   =>    |-  ( ph  ->  ( x  e.  A  |->  ( B  x.  ( F `
  x ) ) )  e.  ( A
 -cn-> CC ) )
 
29-Jun-20172reu3 27345 Double restricted existential uniqueness, analogous to 2eu3 2226. (Contributed by Alexander van der Vekens, 29-Jun-2017.)
 |-  ( A. x  e.  A  A. y  e.  B  ( E* x  e.  A ph 
 \/  E* y  e.  B ph )  ->  ( ( E! x  e.  A  E! y  e.  B  ph 
 /\  E! y  e.  B  E! x  e.  A  ph )  <->  ( E! x  e.  A  E. y  e.  B  ph  /\  E! y  e.  B  E. x  e.  A  ph ) ) )
 
29-Jun-20172reu2 27344 Double restricted existential uniqueness, analogous to 2eu2 2225. (Contributed by Alexander van der Vekens, 29-Jun-2017.)
 |-  ( E! y  e.  B  E. x  e.  A  ph 
 ->  ( E! x  e.  A  E! y  e.  B  ph  <->  E! x  e.  A  E. y  e.  B  ph ) )
 
29-Jun-2017raaan2 27332 Rearrange restricted quantifiers with two different restricting classes, analogous to raaan 3562. It is necessary that either both restricting classes are empty or both are not empty. (Contributed by Alexander van der Vekens, 29-Jun-2017.)
 |-  F/ y ph   &    |-  F/ x ps   =>    |-  (
 ( A  =  (/)  <->  B  =  (/) )  ->  ( A. x  e.  A  A. y  e.  B  (
 ph  /\  ps )  <->  (
 A. x  e.  A  ph 
 /\  A. y  e.  B  ps ) ) )
 
29-Jun-2017r19.32 27324 Theorem 19.32 of [Margaris] p. 90 with restricted quantifiers, analogous to r19.32v 2687. (Contributed by Alexander van der Vekens, 29-Jun-2017.)
 |-  F/ x ph   =>    |-  ( A. x  e.  A  ( ph  \/  ps )  <->  ( ph  \/  A. x  e.  A  ps ) )
 
29-Jun-2017stirlingr 27238 Stirling's approximation formula for 
n factorial: here convergence is expressed with respect to the standard topology on the reals. The main theorem stirling 27237 is proven for convergence in the topology of complex numbers. The variable  R is used to denote convergence with respect to the standard topology on the reals. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
 |-  S  =  ( n  e.  NN0  |->  ( ( sqr `  (
 ( 2  x.  pi )  x.  n ) )  x.  ( ( n 
 /  _e ) ^ n ) ) )   &    |-  R  =  ( ~~> t `  ( topGen `  ran  (,) )
 )   =>    |-  ( n  e.  NN  |->  ( ( ! `  n )  /  ( S `  n ) ) ) R 1
 
29-Jun-2017stirling 27237 Stirling's approximation formula for 
n factorial. The proof follows two major steps: first it is proven that  S and  n factorial are asymptotically equivalent, up to an unknown constant. Then, using Wallis' formula for π it is proven that the unknown constant is the square root of π and then the exact Stirling's formula is established. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
 |-  S  =  ( n  e.  NN0  |->  ( ( sqr `  (
 ( 2  x.  pi )  x.  n ) )  x.  ( ( n 
 /  _e ) ^ n ) ) )   =>    |-  ( n  e.  NN  |->  ( ( ! `  n )  /  ( S `  n ) ) )  ~~>  1
 
29-Jun-2017stirlinglem15 27236 The Stirling's formula is proven using a number of local definitions. The main theorem stirling 27237 will use this final lemma, but it will not expose the local definitions. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
 |-  F/ n ph   &    |-  S  =  ( n  e.  NN0  |->  ( ( sqr `  ( (
 2  x.  pi )  x.  n ) )  x.  ( ( n 
 /  _e ) ^ n ) ) )   &    |-  A  =  ( n  e.  NN  |->  ( ( ! `
  n )  /  ( ( sqr `  (
 2  x.  n ) )  x.  ( ( n  /  _e ) ^ n ) ) ) )   &    |-  D  =  ( n  e.  NN  |->  ( A `  ( 2  x.  n ) ) )   &    |-  E  =  ( n  e.  NN  |->  ( ( sqr `  (
 2  x.  n ) )  x.  ( ( n  /  _e ) ^ n ) ) )   &    |-  V  =  ( n  e.  NN  |->  ( ( ( ( 2 ^ ( 4  x.  n ) )  x.  ( ( ! `  n ) ^ 4
 ) )  /  (
 ( ! `  (
 2  x.  n ) ) ^ 2 ) )  /  ( ( 2  x.  n )  +  1 ) ) )   &    |-  F  =  ( n  e.  NN  |->  ( ( ( A `  n ) ^ 4
 )  /  ( ( D `  n ) ^
 2 ) ) )   &    |-  H  =  ( n  e.  NN  |->  ( ( n ^ 2 )  /  ( n  x.  (
 ( 2  x.  n )  +  1 )
 ) ) )   &    |-  ( ph  ->  C  e.  RR+ )   &    |-  ( ph  ->  A  ~~>  C )   =>    |-  ( ph  ->  ( n  e.  NN  |->  ( ( ! `  n ) 
 /  ( S `  n ) ) )  ~~>  1 )
 
29-Jun-2017stirlinglem14 27235 The sequence  A converges to a positive real. This proves that the Stirling's formula converges to the factorial, up to a constant. In another theorem, using Wallis' formula for π& , such constant is exactly determined, thus proving the Stirling's formula. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
 |-  A  =  ( n  e.  NN  |->  ( ( ! `  n )  /  (
 ( sqr `  ( 2  x.  n ) )  x.  ( ( n  /  _e ) ^ n ) ) ) )   &    |-  B  =  ( n  e.  NN  |->  ( log `  ( A `  n ) ) )   =>    |-  E. c  e.  RR+  A  ~~>  c
 
29-Jun-2017stirlinglem13 27234  B is decreasing and has a lower bound, then it converges. Since  B is  log A, in another theorem it is proven that  A converges also. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
 |-  A  =  ( n  e.  NN  |->  ( ( ! `  n )  /  (
 ( sqr `  ( 2  x.  n ) )  x.  ( ( n  /  _e ) ^ n ) ) ) )   &    |-  B  =  ( n  e.  NN  |->  ( log `  ( A `  n ) ) )   =>    |-  E. d  e.  RR  B  ~~>  d
 
29-Jun-2017stirlinglem12 27233 The sequence  B is bounded below. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
 |-  A  =  ( n  e.  NN  |->  ( ( ! `  n )  /  (
 ( sqr `  ( 2  x.  n ) )  x.  ( ( n  /  _e ) ^ n ) ) ) )   &    |-  B  =  ( n  e.  NN  |->  ( log `  ( A `  n ) ) )   &    |-  F  =  ( n  e.  NN  |->  ( 1  /  ( n  x.  ( n  +  1 )
 ) ) )   =>    |-  ( N  e.  NN  ->  ( ( B `
  1 )  -  ( 1  /  4
 ) )  <_  ( B `  N ) )
 
29-Jun-2017stirlinglem11 27232  B is decreasing. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
 |-  A  =  ( n  e.  NN  |->  ( ( ! `  n )  /  (
 ( sqr `  ( 2  x.  n ) )  x.  ( ( n  /  _e ) ^ n ) ) ) )   &    |-  B  =  ( n  e.  NN  |->  ( log `  ( A `  n ) ) )   &    |-  K  =  ( k  e.  NN  |->  ( ( 1 
 /  ( ( 2  x.  k )  +  1 ) )  x.  ( ( 1  /  ( ( 2  x.  N )  +  1 ) ) ^ (
 2  x.  k ) ) ) )   =>    |-  ( N  e.  NN  ->  ( B `  ( N  +  1
 ) )  <  ( B `  N ) )
 
29-Jun-2017stirlinglem10 27231 A bound for any B(N)-B(N + 1) that will allow to find a lower bound for the whole  B sequence. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
 |-  A  =  ( n  e.  NN  |->  ( ( ! `  n )  /  (
 ( sqr `  ( 2  x.  n ) )  x.  ( ( n  /  _e ) ^ n ) ) ) )   &    |-  B  =  ( n  e.  NN  |->  ( log `  ( A `  n ) ) )   &    |-  K  =  ( k  e.  NN  |->  ( ( 1 
 /  ( ( 2  x.  k )  +  1 ) )  x.  ( ( 1  /  ( ( 2  x.  N )  +  1 ) ) ^ (
 2  x.  k ) ) ) )   &    |-  L  =  ( k  e.  NN  |->  ( ( 1  /  ( ( ( 2  x.  N )  +  1 ) ^ 2
 ) ) ^ k
 ) )   =>    |-  ( N  e.  NN  ->  ( ( B `  N )  -  ( B `  ( N  +  1 ) ) ) 
 <_  ( ( 1  / 
 4 )  x.  (
 1  /  ( N  x.  ( N  +  1 ) ) ) ) )
 
29-Jun-2017stirlinglem9 27230  ( ( B `  N )  -  ( B `  ( N  +  1
) ) ) is expressed as a limit of a series. This result will be used both to prove that  B is decreasing and to prove that  B is bounded (below). It will follow that  B converges in the reals. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
 |-  A  =  ( n  e.  NN  |->  ( ( ! `  n )  /  (
 ( sqr `  ( 2  x.  n ) )  x.  ( ( n  /  _e ) ^ n ) ) ) )   &    |-  B  =  ( n  e.  NN  |->  ( log `  ( A `  n ) ) )   &    |-  J  =  ( n  e.  NN  |->  ( ( ( ( 1  +  (
 2  x.  n ) )  /  2 )  x.  ( log `  (
 ( n  +  1 )  /  n ) ) )  -  1
 ) )   &    |-  K  =  ( k  e.  NN  |->  ( ( 1  /  (
 ( 2  x.  k
 )  +  1 ) )  x.  ( ( 1  /  ( ( 2  x.  N )  +  1 ) ) ^ ( 2  x.  k ) ) ) )   =>    |-  ( N  e.  NN  ->  seq  1 (  +  ,  K )  ~~>  ( ( B `  N )  -  ( B `  ( N  +  1 ) ) ) )
 
29-Jun-2017stirlinglem8 27229 If  A converges to  C, then  F converges to C^2 . (Contributed by Glauco Siliprandi, 29-Jun-2017.)
 |-  F/ n ph   &    |-  F/_ n A   &    |-  F/_ n D   &    |-  D  =  ( n  e.  NN  |->  ( A `
  ( 2  x.  n ) ) )   &    |-  ( ph  ->  A : NN
 --> RR+ )   &    |-  F  =  ( n  e.  NN  |->  ( ( ( A `  n ) ^ 4
 )  /  ( ( D `  n ) ^
 2 ) ) )   &    |-  L  =  ( n  e.  NN  |->  ( ( A `
  n ) ^
 4 ) )   &    |-  M  =  ( n  e.  NN  |->  ( ( D `  n ) ^ 2
 ) )   &    |-  ( ( ph  /\  n  e.  NN )  ->  ( D `  n )  e.  RR+ )   &    |-  ( ph  ->  C  e.  RR+ )   &    |-  ( ph  ->  A  ~~>  C )   =>    |-  ( ph  ->  F  ~~>  ( C ^ 2 ) )
 
29-Jun-2017stirlinglem7 27228 Algebraic manipulation of the formula for J(n) (Contributed by Glauco Siliprandi, 29-Jun-2017.)
 |-  J  =  ( n  e.  NN  |->  ( ( ( ( 1  +  ( 2  x.  n ) ) 
 /  2 )  x.  ( log `  (
 ( n  +  1 )  /  n ) ) )  -  1
 ) )   &    |-  K  =  ( k  e.  NN  |->  ( ( 1  /  (
 ( 2  x.  k
 )  +  1 ) )  x.  ( ( 1  /  ( ( 2  x.  N )  +  1 ) ) ^ ( 2  x.  k ) ) ) )   &    |-  H  =  ( k  e.  NN0  |->  ( 2  x.  ( ( 1 
 /  ( ( 2  x.  k )  +  1 ) )  x.  ( ( 1  /  ( ( 2  x.  N )  +  1 ) ) ^ (
 ( 2  x.  k
 )  +  1 ) ) ) ) )   =>    |-  ( N  e.  NN  ->  seq  1 (  +  ,  K )  ~~>  ( J `  N ) )
 
29-Jun-2017stirlinglem6 27227 A series that converges to log (N+1)/N (Contributed by Glauco Siliprandi, 29-Jun-2017.)
 |-  H  =  ( j  e.  NN0  |->  ( 2  x.  (
 ( 1  /  (
 ( 2  x.  j
 )  +  1 ) )  x.  ( ( 1  /  ( ( 2  x.  N )  +  1 ) ) ^ ( ( 2  x.  j )  +  1 ) ) ) ) )   =>    |-  ( N  e.  NN  ->  seq  0 (  +  ,  H )  ~~>  ( log `  ( ( N  +  1 )  /  N ) ) )
 
29-Jun-2017stirlinglem5 27226 If  T is between  0 and  1, then a series (without alternating negative and positive terms) is given that converges to log (1+T)/(1-T) . (Contributed by Glauco Siliprandi, 29-Jun-2017.)
 |-  D  =  ( j  e.  NN  |->  ( ( -u 1 ^ ( j  -  1 ) )  x.  ( ( T ^
 j )  /  j
 ) ) )   &    |-  E  =  ( j  e.  NN  |->  ( ( T ^
 j )  /  j
 ) )   &    |-  F  =  ( j  e.  NN  |->  ( ( ( -u 1 ^ ( j  -  1 ) )  x.  ( ( T ^
 j )  /  j
 ) )  +  (
 ( T ^ j
 )  /  j )
 ) )   &    |-  H  =  ( j  e.  NN0  |->  ( 2  x.  ( ( 1 
 /  ( ( 2  x.  j )  +  1 ) )  x.  ( T ^ (
 ( 2  x.  j
 )  +  1 ) ) ) ) )   &    |-  G  =  ( j  e.  NN0  |->  ( ( 2  x.  j )  +  1 ) )   &    |-  ( ph  ->  T  e.  RR+ )   &    |-  ( ph  ->  ( abs `  T )  < 
 1 )   =>    |-  ( ph  ->  seq  0
 (  +  ,  H ) 
 ~~>  ( log `  (
 ( 1  +  T )  /  ( 1  -  T ) ) ) )
 
29-Jun-2017stirlinglem4 27225 Algebraic manipulation of  ( ( B n ) - ( B  ( n  +  1 ) ) ). It will be used in other theorems to show that  B is decreasing. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
 |-  A  =  ( n  e.  NN  |->  ( ( ! `  n )  /  (
 ( sqr `  ( 2  x.  n ) )  x.  ( ( n  /  _e ) ^ n ) ) ) )   &    |-  B  =  ( n  e.  NN  |->  ( log `  ( A `  n ) ) )   &    |-  J  =  ( n  e.  NN  |->  ( ( ( ( 1  +  (
 2  x.  n ) )  /  2 )  x.  ( log `  (
 ( n  +  1 )  /  n ) ) )  -  1
 ) )   =>    |-  ( N  e.  NN  ->  ( ( B `  N )  -  ( B `  ( N  +  1 ) ) )  =  ( J `  N ) )
 
29-Jun-2017stirlinglem3 27224 Long but simple algebraic transformations are applied to show that  V, the Wallis formula for π , can be expressed in terms of  A, the Stirling's approximation formula for the factorial, up to a constant factor. This will allow (in a later theorem) to determine the right constant factor to be put into the  A, in order to get the exact Stirling's formula. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
 |-  A  =  ( n  e.  NN  |->  ( ( ! `  n )  /  (
 ( sqr `  ( 2  x.  n ) )  x.  ( ( n  /  _e ) ^ n ) ) ) )   &    |-  D  =  ( n  e.  NN  |->  ( A `  ( 2  x.  n ) ) )   &    |-  E  =  ( n  e.  NN  |->  ( ( sqr `  (
 2  x.  n ) )  x.  ( ( n  /  _e ) ^ n ) ) )   &    |-  V  =  ( n  e.  NN  |->  ( ( ( ( 2 ^ ( 4  x.  n ) )  x.  ( ( ! `  n ) ^ 4
 ) )  /  (
 ( ! `  (
 2  x.  n ) ) ^ 2 ) )  /  ( ( 2  x.  n )  +  1 ) ) )   =>    |-  V  =  ( n  e.  NN  |->  ( ( ( ( A `  n ) ^ 4
 )  /  ( ( D `  n ) ^
 2 ) )  x.  ( ( n ^
 2 )  /  ( n  x.  ( ( 2  x.  n )  +  1 ) ) ) ) )
 
29-Jun-2017stirlinglem2 27223  A maps to positive reals. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
 |-  A  =  ( n  e.  NN  |->  ( ( ! `  n )  /  (
 ( sqr `  ( 2  x.  n ) )  x.  ( ( n  /  _e ) ^ n ) ) ) )   =>    |-  ( N  e.  NN  ->  ( A `  N )  e.  RR+ )
 
29-Jun-2017wallispi2 27221 An alternative version of Wallis' formula for π ; this second formula uses factorials and it is later used to proof Stirling's approximation formula. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
 |-  V  =  ( n  e.  NN  |->  ( ( ( ( 2 ^ ( 4  x.  n ) )  x.  ( ( ! `
  n ) ^
 4 ) )  /  ( ( ! `  ( 2  x.  n ) ) ^ 2
 ) )  /  (
 ( 2  x.  n )  +  1 )
 ) )   =>    |-  V  ~~>  ( pi  / 
 2 )
 
29-Jun-2017wallispi 27218 Wallis' formula for π : Wallis' product converges to π / 2 . (Contributed by Glauco Siliprandi, 29-Jun-2017.)
 |-  F  =  ( k  e.  NN  |->  ( ( ( 2  x.  k )  /  ( ( 2  x.  k )  -  1
 ) )  x.  (
 ( 2  x.  k
 )  /  ( (
 2  x.  k )  +  1 ) ) ) )   &    |-  W  =  ( n  e.  NN  |->  ( 
 seq  1 (  x. 
 ,  F ) `  n ) )   =>    |-  W  ~~>  ( pi  /  2 )
 
29-Jun-2017wallispilem3 27215 I maps to real values (Contributed by Glauco Siliprandi, 29-Jun-2017.)
 |-  I  =  ( n  e.  NN0  |->  S. ( 0 (,) pi ) ( ( sin `  x ) ^ n )  _d x )   =>    |-  ( N  e.  NN0 
 ->  ( I `  N )  e.  RR+ )
 
29-Jun-2017wallispilem2 27214 A first set of properties for the sequence  I that will be used in the proof of the Wallis product formula (Contributed by Glauco Siliprandi, 29-Jun-2017.)
 |-  I  =  ( n  e.  NN0  |->  S. ( 0 (,) pi ) ( ( sin `  x ) ^ n )  _d x )   =>    |-  ( ( I `
  0 )  =  pi  /\  ( I `
  1 )  =  2  /\  ( N  e.  ( ZZ>= `  2
 )  ->  ( I `  N )  =  ( ( ( N  -  1 )  /  N )  x.  ( I `  ( N  -  2
 ) ) ) ) )
 
29-Jun-2017wallispilem1 27213  I is monotone: increasing the exponent, the integral decreases. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
 |-  I  =  ( n  e.  NN0  |->  S. ( 0 (,) pi ) ( ( sin `  x ) ^ n )  _d x )   &    |-  ( ph  ->  N  e.  NN0 )   =>    |-  ( ph  ->  ( I `  ( N  +  1 ) )  <_  ( I `  N ) )
 
29-Jun-2017itgsinexp 27148 A recursive formula for the integral of sin^N on the interval (0,π) .

(Contributed by Glauco Siliprandi, 29-Jun-2017.)

 |-  I  =  ( n  e.  NN0  |->  S. ( 0 (,) pi ) ( ( sin `  x ) ^ n )  _d x )   &    |-  ( ph  ->  N  e.  ( ZZ>=
 `  2 ) )   =>    |-  ( ph  ->  ( I `  N )  =  ( ( ( N  -  1 )  /  N )  x.  ( I `  ( N  -  2
 ) ) ) )
 
29-Jun-2017itgsinexplem1 27147 Integration by parts is applied to integrate sin^(N+1) (Contributed by Glauco Siliprandi, 29-Jun-2017.)
 |-  F  =  ( x  e.  CC  |->  ( ( sin `  x ) ^ N ) )   &    |-  G  =  ( x  e.  CC  |->  -u ( cos `  x ) )   &    |-  H  =  ( x  e.  CC  |->  ( ( N  x.  (
 ( sin `  x ) ^ ( N  -  1 ) ) )  x.  ( cos `  x ) ) )   &    |-  I  =  ( x  e.  CC  |->  ( ( ( sin `  x ) ^ N )  x.  ( sin `  x ) ) )   &    |-  L  =  ( x  e.  CC  |->  ( ( ( N  x.  ( ( sin `  x ) ^ ( N  -  1 ) ) )  x.  ( cos `  x ) )  x.  -u ( cos `  x ) ) )   &    |-  M  =  ( x  e.  CC  |->  ( ( ( cos `  x ) ^ 2
 )  x.  ( ( sin `  x ) ^ ( N  -  1 ) ) ) )   &    |-  ( ph  ->  N  e.  NN )   =>    |-  ( ph  ->  S. ( 0 (,) pi ) ( ( ( sin `  x ) ^ N )  x.  ( sin `  x ) )  _d x  =  ( N  x.  S. (
 0 (,) pi ) ( ( ( cos `  x ) ^ 2 )  x.  ( ( sin `  x ) ^ ( N  -  1 ) ) )  _d x ) )
 
29-Jun-2017iblioosinexp 27146 sin^n on an open integral is integrable (Contributed by Glauco Siliprandi, 29-Jun-2017.)
 |-  (
 ( A  e.  RR  /\  B  e.  RR  /\  N  e.  NN0 )  ->  ( x  e.  ( A (,) B )  |->  ( ( sin `  x ) ^ N ) )  e.  L ^1 )
 
29-Jun-2017itgsin0pi 27145 Calculation of the integral for sine on the (0,π) interval (Contributed by Glauco Siliprandi, 29-Jun-2017.)
 |-  S. ( 0 (,) pi ) ( sin `  x )  _d x  =  2
 
29-Jun-2017ibliccsinexp 27144 sin^n on a closed interval is integrable. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
 |-  (
 ( A  e.  RR  /\  B  e.  RR  /\  N  e.  NN0 )  ->  ( x  e.  ( A [,] B )  |->  ( ( sin `  x ) ^ N ) )  e.  L ^1 )
 
29-Jun-2017itgsin0pilem1 27143 Calculation of the integral for sine on the (0,π) interval (Contributed by Glauco Siliprandi, 29-Jun-2017.)
 |-  C  =  ( t  e.  (
 0 [,] pi )  |->  -u ( cos `  t )
 )   =>    |- 
 S. ( 0 (,)
 pi ) ( sin `  x )  _d x  =  2
 
29-Jun-2017volioo 27142 The measure of an open interval. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
 |-  (
 ( A  e.  RR  /\  B  e.  RR  /\  A  <_  B )  ->  ( vol `  ( A (,) B ) )  =  ( B  -  A ) )
 
29-Jun-2017ioovolcl 27141 An open real interval has finite volume. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
 |-  (
 ( A  e.  RR  /\  B  e.  RR )  ->  ( vol `  ( A (,) B ) )  e.  RR )
 
29-Jun-2017dvcosre 27140 The real derivative of the cosine (Contributed by Glauco Siliprandi, 29-Jun-2017.)
 |-  ( RR  _D  ( x  e. 
 RR  |->  ( cos `  x ) ) )  =  ( x  e.  RR  |->  -u ( sin `  x ) )
 
29-Jun-2017dvsinexp 27139 The derivative of sin^N . (Contributed by Glauco Siliprandi, 29-Jun-2017.)
 |-  ( ph  ->  N  e.  NN )   =>    |-  ( ph  ->  ( CC  _D  ( x  e. 
 CC  |->  ( ( sin `  x ) ^ N ) ) )  =  ( x  e.  CC  |->  ( ( N  x.  ( ( sin `  x ) ^ ( N  -  1 ) ) )  x.  ( cos `  x ) ) ) )
 
29-Jun-2017climdivf 27137 Limit of the ratio of two converging sequences. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
 |-  F/ k ph   &    |-  F/_ k F   &    |-  F/_ k G   &    |-  F/_ k H   &    |-  Z  =  (
 ZZ>= `  M )   &    |-  ( ph  ->  M  e.  ZZ )   &    |-  ( ph  ->  F  ~~>  A )   &    |-  ( ph  ->  H  e.  X )   &    |-  ( ph  ->  G  ~~>  B )   &    |-  ( ph  ->  B  =/=  0
 )   &    |-  ( ( ph  /\  k  e.  Z )  ->  ( F `  k )  e. 
 CC )   &    |-  ( ( ph  /\  k  e.  Z ) 
 ->  ( G `  k
 )  e.  ( CC  \  { 0 } )
 )   &    |-  ( ( ph  /\  k  e.  Z )  ->  ( H `  k )  =  ( ( F `  k )  /  ( G `  k ) ) )   =>    |-  ( ph  ->  H  ~~>  ( A  /  B ) )
 
29-Jun-2017climinff 27136 A version of climinf 27131 using bound-variable hypotheses instead of distinct variable conditions (Contributed by Glauco Siliprandi, 29-Jun-2017.)
 |-  F/ k ph   &    |-  F/_ k F   &    |-  Z  =  ( ZZ>= `  M )   &    |-  ( ph  ->  M  e.  ZZ )   &    |-  ( ph  ->  F : Z --> RR )   &    |-  (
 ( ph  /\  k  e.  Z )  ->  ( F `  ( k  +  1 ) )  <_  ( F `  k ) )   &    |-  ( ph  ->  E. x  e.  RR  A. k  e.  Z  x  <_  ( F `  k
 ) )   =>    |-  ( ph  ->  F  ~~>  sup ( ran  F ,  RR ,  `'  <  )
 )
 
29-Jun-2017climneg 27135 Complex limit of the negative of a sequence. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
 |-  F/ k ph   &    |-  F/_ k F   &    |-  Z  =  ( ZZ>= `  M )   &    |-  ( ph  ->  M  e.  ZZ )   &    |-  ( ph  ->  F  ~~>  A )   &    |-  ( ( ph  /\  k  e.  Z ) 
 ->  ( F `  k
 )  e.  CC )   =>    |-  ( ph  ->  ( k  e.  Z  |->  -u ( F `  k ) )  ~~>  -u A )
 
29-Jun-2017climrecf 27134 A version of climrec 27128 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
 |-  F/ k ph   &    |-  F/_ k G   &    |-  F/_ k H   &    |-  Z  =  ( ZZ>= `  M )   &    |-  ( ph  ->  M  e.  ZZ )   &    |-  ( ph  ->  G  ~~>  A )   &    |-  ( ph  ->  A  =/=  0
 )   &    |-  ( ( ph  /\  k  e.  Z )  ->  ( G `  k )  e.  ( CC  \  {
 0 } ) )   &    |-  ( ( ph  /\  k  e.  Z )  ->  ( H `  k )  =  ( 1  /  ( G `  k ) ) )   &    |-  ( ph  ->  H  e.  W )   =>    |-  ( ph  ->  H  ~~>  ( 1  /  A ) )
 
29-Jun-2017climsuse 27133 A subsequence  G of a converging sequence  F, converges to the same limit.  I is the strictly increasing and it is used to index the subsequence (Contributed by Glauco Siliprandi, 29-Jun-2017.)
 |-  F/ k ph   &    |-  F/_ k F   &    |-  F/_ k G   &    |-  F/_ k I   &    |-  Z  =  (
 ZZ>= `  M )   &    |-  ( ph  ->  M  e.  ZZ )   &    |-  ( ph  ->  F  e.  X )   &    |-  ( ( ph  /\  k  e.  Z ) 
 ->  ( F `  k
 )  e.  CC )   &    |-  ( ph  ->  F  ~~>  A )   &    |-  ( ph  ->  ( I `  M )  e.  Z )   &    |-  ( ( ph  /\  k  e.  Z )  ->  ( I `  ( k  +  1 ) )  e.  ( ZZ>= `  ( ( I `  k )  +  1 ) ) )   &    |-  ( ph  ->  G  e.  Y )   &    |-  ( ( ph  /\  k  e.  Z ) 
 ->  ( G `  k
 )  =  ( F `
  ( I `  k ) ) )   =>    |-  ( ph  ->  G  ~~>  A )
 
29-Jun-2017climsuselem1 27132 The subsequence index  I has the expected properties: it belongs to the same upper integers as the original index, and it is always larger or equal than the original index. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
 |-  Z  =  ( ZZ>= `  M )   &    |-  ( ph  ->  M  e.  ZZ )   &    |-  ( ph  ->  ( I `  M )  e.  Z )   &    |-  ( ( ph  /\  k  e.  Z ) 
 ->  ( I `  (
 k  +  1 ) )  e.  ( ZZ>= `  ( ( I `  k )  +  1
 ) ) )   =>    |-  ( ( ph  /\  K  e.  Z ) 
 ->  ( I `  K )  e.  ( ZZ>= `  K ) )
 
29-Jun-2017climinf 27131 A bounded monotonic non increasing sequence converges to the infimum of its range. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
 |-  Z  =  ( ZZ>= `  M )   &    |-  ( ph  ->  M  e.  ZZ )   &    |-  ( ph  ->  F : Z --> RR )   &    |-  (
 ( ph  /\  k  e.  Z )  ->  ( F `  ( k  +  1 ) )  <_  ( F `  k ) )   &    |-  ( ph  ->  E. x  e.  RR  A. k  e.  Z  x  <_  ( F `  k
 ) )   =>    |-  ( ph  ->  F  ~~>  sup ( ran  F ,  RR ,  `'  <  )
 )
 
29-Jun-2017climexp 27130 The limit of natural powers, is the natural power of the limit. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
 |-  F/ k ph   &    |-  F/_ k F   &    |-  F/_ k H   &    |-  Z  =  ( ZZ>= `  M )   &    |-  ( ph  ->  M  e.  ZZ )   &    |-  ( ph  ->  F : Z --> CC )   &    |-  ( ph  ->  F  ~~>  A )   &    |-  ( ph  ->  N  e.  NN0 )   &    |-  ( ph  ->  H  e.  V )   &    |-  (
 ( ph  /\  k  e.  Z )  ->  ( H `  k )  =  ( ( F `  k ) ^ N ) )   =>    |-  ( ph  ->  H  ~~>  ( A ^ N ) )
 
29-Jun-2017climmulf 27129 A version of climmul 12100 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
 |-  F/ k ph   &    |-  F/_ k F   &    |-  F/_ k G   &    |-  F/_ k H   &    |-  Z  =  (
 ZZ>= `  M )   &    |-  ( ph  ->  M  e.  ZZ )   &    |-  ( ph  ->  F  ~~>  A )   &    |-  ( ph  ->  H  e.  X )   &    |-  ( ph  ->  G  ~~>  B )   &    |-  (
 ( ph  /\  k  e.  Z )  ->  ( F `  k )  e. 
 CC )   &    |-  ( ( ph  /\  k  e.  Z ) 
 ->  ( G `  k
 )  e.  CC )   &    |-  (
 ( ph  /\  k  e.  Z )  ->  ( H `  k )  =  ( ( F `  k )  x.  ( G `  k ) ) )   =>    |-  ( ph  ->  H  ~~>  ( A  x.  B ) )
 
29-Jun-2017climrec 27128 Limit of the reciprocal of a converging sequence. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
 |-  Z  =  ( ZZ>= `  M )   &    |-  ( ph  ->  M  e.  ZZ )   &    |-  ( ph  ->  G  ~~>  A )   &    |-  ( ph  ->  A  =/=  0 )   &    |-  (
 ( ph  /\  k  e.  Z )  ->  ( G `  k )  e.  ( CC  \  {
 0 } ) )   &    |-  ( ( ph  /\  k  e.  Z )  ->  ( H `  k )  =  ( 1  /  ( G `  k ) ) )   &    |-  ( ph  ->  H  e.  W )   =>    |-  ( ph  ->  H  ~~>  ( 1  /  A ) )
 
29-Jun-2017isumneg 27127 Negation of a converging sum. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
 |-  Z  =  ( ZZ>= `  M )   &    |-  ( ph  ->  M  e.  ZZ )   &    |-  ( ph  ->  sum_ k  e.  Z  A  e.  CC )   &    |-  ( ( ph  /\  k  e.  Z )  ->  ( F `  k )  =  A )   &    |-  ( ( ph  /\  k  e.  Z ) 
 ->  A  e.  CC )   &    |-  ( ph  ->  seq  M (  +  ,  F )  e.  dom  ~~>  )   =>    |-  ( ph  ->  sum_ k  e.  Z  -u A  =  -u sum_
 k  e.  Z  A )
 
29-Jun-2017clim1fr1 27126 A class of sequences of fractions that converge to 1 (Contributed by Glauco Siliprandi, 29-Jun-2017.)
 |-  F  =  ( n  e.  NN  |->  ( ( ( A  x.  n )  +  B )  /  ( A  x.  n ) ) )   &    |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  A  =/=  0
 )   &    |-  ( ph  ->  B  e.  CC )   =>    |-  ( ph  ->  F  ~~>  1 )
 
29-Jun-2017expcnfg 27125 If  F is a complex continuous function and N is a fixed number, then F^N is continuous too. A generalization of expcncf 27122. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
 |-  F/_ x F   &    |-  ( ph  ->  F  e.  ( A -cn-> CC )
 )   &    |-  ( ph  ->  N  e.  NN0 )   =>    |-  ( ph  ->  ( x  e.  A  |->  ( ( F `  x ) ^ N ) )  e.  ( A -cn-> CC ) )
 
29-Jun-2017m1expeven 27124 Exponentiation of negative one to an even power. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
 |-  ( N  e.  NN0  ->  ( -u 1 ^ ( 2  x.  N ) )  =  1 )
 
29-Jun-2017eluzelcn 27123 A member of a set of upper integers is a complex number. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
 |-  ( N  e.  ( ZZ>= `  M )  ->  N  e.  CC )
 
29-Jun-2017expcncf 27122 The power function on complex numbers, for fixed exponent N, is continuous. Similar to expcn 18370. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
 |-  ( N  e.  NN0  ->  ( x  e.  CC  |->  ( x ^ N ) )  e.  ( CC -cn-> CC ) )
 
29-Jun-2017infrglb 27121 The infimum of a non-empty bounded set of reals is the greatest lower bound. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
 |-  (
 ( ( A  C_  RR  /\  A  =/=  (/)  /\  E. x  e.  RR  A. y  e.  A  x  <_  y
 )  /\  B  e.  RR )  ->  ( sup ( A ,  RR ,  `'  <  )  <  B  <->  E. z  e.  A  z  <  B ) )
 
29-Jun-2017mulcncf 27119 The multiplication of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
 |-  ( ph  ->  ( x  e.  X  |->  A )  e.  ( X -cn-> CC )
 )   &    |-  ( ph  ->  ( x  e.  X  |->  B )  e.  ( X -cn-> CC ) )   =>    |-  ( ph  ->  ( x  e.  X  |->  ( A  x.  B ) )  e.  ( X -cn-> CC ) )
 
29-Jun-2017rrpsscn 27118 The positive reals are a subset of the complex numbers. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
 |-  RR+  C_  CC
 
29-Jun-2017fmptdf 27117 A version of fmptd 5645 using bound-variable hypothesis instead of a distinct variable condition for  ph. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
 |-  F/ x ph   &    |-  ( ( ph  /\  x  e.  A ) 
 ->  B  e.  C )   &    |-  F  =  ( x  e.  A  |->  B )   =>    |-  ( ph  ->  F : A --> C )
 
29-Jun-2017cncfmptss 27116 A continuous complex function restricted to a subset is continuous, using "map to" notation. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
 |-  F/_ x F   &    |-  ( ph  ->  F  e.  ( A -cn-> B ) )   &    |-  ( ph  ->  C 
 C_  A )   =>    |-  ( ph  ->  ( x  e.  C  |->  ( F `  x ) )  e.  ( C
 -cn-> B ) )
 
25-Jun-20172reu1 27343 Double restricted existential uniqueness. This theorem shows a condition under which a "naive" definition matches the correct one, analogous to 2eu1 2224. (Contributed by Alexander van der Vekens, 25-Jun-2017.)
 |-  ( A. x  e.  A  E* y  e.  B ph 
 ->  ( E! x  e.  A  E! y  e.  B  ph  <->  ( E! x  e.  A  E. y  e.  B  ph  /\  E! y  e.  B  E. x  e.  A  ph ) ) )
 
25-Jun-20172rexreu 27342 Double restricted existential uniqueness implies double restricted uniqueness quantification, analogous to 2exeu 2221. (Contributed by Alexander van der Vekens, 25-Jun-2017.)
 |-  (
 ( E! x  e.  A  E. y  e.  B  ph  /\  E! y  e.  B  E. x  e.  A  ph )  ->  E! x  e.  A  E! y  e.  B  ph )
 
25-Jun-20172rmoswap 27341 A condition allowing swap of restricted "at most one" and restricted existential quantifiers, analogous to 2moswap 2219. (Contributed by Alexander van der Vekens, 25-Jun-2017.)
 |-  ( A. x  e.  A  E* y  e.  B ph 
 ->  ( E* x  e.  A E. y  e.  B  ph  ->  E* y  e.  B E. x  e.  A  ph ) )
 
25-Jun-20172reu2rex 27340 Double restricted existential uniqueness, analogous to 2eu2ex 2218. (Contributed by Alexander van der Vekens, 25-Jun-2017.)
 |-  ( E! x  e.  A  E! y  e.  B  ph 
 ->  E. x  e.  A  E. y  e.  B  ph )
 
25-Jun-2017rmoanim 27336 Introduction of a conjunct into restricted "at most one" quantifier, analogous to moanim 2200. (Contributed by Alexander van der Vekens, 25-Jun-2017.)
 |-  F/ x ph   =>    |-  ( E* x  e.  A ( ph  /\  ps ) 
 <->  ( ph  ->  E* x  e.  A ps ) )
 
25-Jun-2017reuimrmo 27335 Restricted uniqueness implies restricted "at most one" through implication, analogous to euimmo 2193. (Contributed by Alexander van der Vekens, 25-Jun-2017.)
 |-  ( A. x  e.  A  ( ph  ->  ps )  ->  ( E! x  e.  A  ps  ->  E* x  e.  A ph ) )
 
24-Jun-20172reurmo 27339 Double restricted quantification with restricted existential uniqueness and restricted "at most one.", analogous to 2eumo 2217. (Contributed by Alexander van der Vekens, 24-Jun-2017.)
 |-  ( E! x  e.  A  E* y  e.  B ph 
 ->  E* x  e.  A E! y  e.  B  ph )
 
24-Jun-20172reurex 27338 Double restricted quantification with existential uniqueness, analogous to 2euex 2216. (Contributed by Alexander van der Vekens, 24-Jun-2017.)
 |-  ( E! x  e.  A  E. y  e.  B  ph 
 ->  E. y  e.  B  E! x  e.  A  ph )
 
17-Jun-20172reu5a 27334 Double restricted existential uniqueness in terms of restricted existence and restricted "at most one." (Contributed by Alexander van der Vekens, 17-Jun-2017.)
 |-  ( E! x  e.  A  E! y  e.  B  ph  <->  ( E. x  e.  A  ( E. y  e.  B  ph 
 /\  E* y  e.  B ph )  /\  E* x  e.  A ( E. y  e.  B  ph  /\  E* y  e.  B ph ) ) )
 
17-Jun-2017rmoimi 27333 Restricted "at most one" is preserved through implication (note wff reversal). (Contributed by Alexander van der Vekens, 17-Jun-2017.)
 |-  ( ph  ->  ps )   =>    |-  ( E* x  e.  A ps  ->  E* x  e.  A ph )
 
17-Jun-2017idomsubgmo 26913 The units of an integral domain have at most one subgroup of any single finite cardinality. (Contributed by Stefan O'Rear, 12-Sep-2015.) (Revised by NM, 17-Jun-2017.)
 |-  G  =  ( (mulGrp `  R )s  (Unit `  R ) )   =>    |-  ( ( R  e. IDomn  /\  N  e.  NN )  ->  E* y  e.  (SubGrp `  G ) ( # `  y )  =  N )
 
17-Jun-2017hilbert1.2 24185 There is at most one line through any two distinct points. Hilbert's axiom I.2 for geometry. (Contributed by Scott Fenton, 29-Oct-2013.) (Revised by NM, 17-Jun-2017.)
 |-  ( P  =/=  Q  ->  E* x  e. LinesEE ( P  e.  x  /\  Q  e.  x ) )
 
17-Jun-2017cvmliftmo 23219 A lift of a continuous function from a connected and locally connected space over a covering map is unique when it exists. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by NM, 17-Jun-2017.)
 |-  B  =  U. C   &    |-  Y  =  U. K   &    |-  ( ph  ->  F  e.  ( C CovMap  J )
 )   &    |-  ( ph  ->  K  e.  Con )   &    |-  ( ph  ->  K  e. 𝑛Locally  Con )   &    |-  ( ph  ->  O  e.  Y )   &    |-  ( ph  ->  G  e.  ( K  Cn  J ) )   &    |-  ( ph  ->  P  e.  B )   &    |-  ( ph  ->  ( F `  P )  =  ( G `  O ) )   =>    |-  ( ph  ->  E* f  e.  ( K  Cn  C ) ( ( F  o.  f
 )  =  G  /\  ( f `  O )  =  P )
 )
 
17-Jun-2017ply1divmo 19515 Uniqueness of a quotient in a polynomial division. For polynomials  F ,  G such that  G  =/=  0 and the leading coefficient of  G is not a zero divisor, there is at most one polynomial  q which satisfies  F  =  ( G  x.  q )  +  r where the degree of  r is less than the degree of  G. (Contributed by Stefan O'Rear, 26-Mar-2015.) (Revised by NM, 17-Jun-2017.)
 |-  P  =  (Poly1 `  R )   &    |-  D  =  ( deg1  `  R )   &    |-  B  =  ( Base `  P )   &    |-  .-  =  ( -g `  P )   &    |-  .0.  =  ( 0g `  P )   &    |-  .xb  =  ( .r `  P )   &    |-  ( ph  ->  R  e.  Ring )   &    |-  ( ph  ->  F  e.  B )   &    |-  ( ph  ->  G  e.  B )   &    |-  ( ph  ->  G  =/=  .0.  )   &    |-  ( ph  ->  ( (coe1 `  G ) `  ( D `  G ) )  e.  E )   &    |-  E  =  (RLReg `  R )   =>    |-  ( ph  ->  E* q  e.  B ( D `  ( F  .-  ( G 
 .xb  q ) ) )  <  ( D `
  G ) )
 
17-Jun-20172ndcdisj2 17177 Any disjoint collection of open sets in a second-countable space is countable. (Contributed by Mario Carneiro, 21-Mar-2015.) (Proof shortened by Mario Carneiro, 9-Apr-2015.) (Revised by NM, 17-Jun-2017.)
 |-  ( ( J  e.  2ndc  /\  A  C_  J  /\  A. y E* x  e.  A y  e.  x )  ->  A  ~<_  om )
 
17-Jun-20172ndcdisj 17176 Any disjoint family of open sets in a second-countable space is countable. (The sets are required to be nonempty because otherwise there could be many empty sets in the family.) (Contributed by Mario Carneiro, 21-Mar-2015.) (Proof shortened by Mario Carneiro, 9-Apr-2015.) (Revised by NM, 17-Jun-2017.)
 |-  ( ( J  e.  2ndc  /\  A. x  e.  A  B  e.  ( J  \  { (/) } )  /\  A. y E* x  e.  A y  e.  B )  ->  A  ~<_  om )
 
17-Jun-2017lspextmo 15807 A linear function is completely determined (or overdetermined) by its values on a spanning subset. (Contributed by Stefan O'Rear, 7-Mar-2015.) (Revised by NM, 17-Jun-2017.)
 |-  B  =  ( Base `  S )   &    |-  K  =  (
 LSpan `  S )   =>    |-  ( ( X 
 C_  B  /\  ( K `  X )  =  B )  ->  E* g  e.  ( S LMHom  T ) ( g  |`  X )  =  F )
 
17-Jun-2017mgmidmo 14364 A two-sided identity element is unique (if it exists) in any magma. (Contributed by Mario Carneiro, 7-Dec-2014.) (Revised by NM, 17-Jun-2017.)
 |- 
 E* u  e.  B A. x  e.  B  ( ( u  .+  x )  =  x  /\  ( x  .+  u )  =  x )
 
17-Jun-2017sqrmo 11731 Uniqueness for the square root function. (Contributed by Mario Carneiro, 9-Jul-2013.) (Revised by NM, 17-Jun-2017.)
 |-  ( A  e.  CC  ->  E* x  e.  CC ( ( x ^
 2 )  =  A  /\  0  <_  ( Re
 `  x )  /\  ( _i  x.  x )  e/  RR+ ) )
 
17-Jun-2017rmorabex 4232 Restricted "at most one" existence implies a restricted class abstraction exists. (Contributed by NM, 17-Jun-2017.)
 |-  ( E* x  e.  A ph  ->  { x  e.  A  |  ph }  e.  _V )
 
17-Jun-2017dfdisj2 3996 Alternate definition for disjoint classes. (Contributed by NM, 17-Jun-2017.)
 |-  (Disj  x  e.  A B 
 <-> 
 A. y E* x ( x  e.  A  /\  y  e.  B ) )
 
17-Jun-2017rmo2i 3078 Condition implying restricted "at most one." (Contributed by NM, 17-Jun-2017.)
 |- 
 F/ y ph   =>    |-  ( E. y  e.  A  A. x  e.  A  ( ph  ->  x  =  y )  ->  E* x  e.  A ph )
 
17-Jun-2017rmo2 3077 Alternate definition of restricted "at most one." Note that  E* x  e.  A ph is not equivalent to  E. y  e.  A A. x  e.  A ( ph  ->  x  =  y ) (in analogy to reu6 2955); to see this, let  A be the empty set. However, one direction of this pattern holds; see rmo2i 3078. (Contributed by NM, 17-Jun-2017.)
 |- 
 F/ y ph   =>    |-  ( E* x  e.  A ph  <->  E. y A. x  e.  A  ( ph  ->  x  =  y ) )
 
17-Jun-20172reu5 2974 Double restricted existential uniqueness in terms of restricted existential quantification and restricted universal quantification, analogous to 2eu5 2228 and reu3 2956. (Contributed by Alexander van der Vekens, 17-Jun-2017.)
 |-  ( ( E! x  e.  A  E! y  e.  B  ph  /\  A. x  e.  A  E* y  e.  B ph )  <->  ( E. x  e.  A  E. y  e.  B  ph  /\  E. z  e.  A  E. w  e.  B  A. x  e.  A  A. y  e.  B  ( ph  ->  ( x  =  z  /\  y  =  w )
 ) ) )
 
17-Jun-20172reu5lem3 2973 Lemma for 2reu5 2974. This lemma is interesting in its own right, showing that existential restriction in the last conjunct (the "at most one" part) is optional; compare rmo2 3077. (Contributed by Alexander van der Vekens, 17-Jun-2017.)
 |-  ( ( E! x  e.  A  E! y  e.  B  ph  /\  A. x  e.  A  E* y  e.  B ph )  <->  ( E. x  e.  A  E. y  e.  B  ph  /\  E. z E. w A. x  e.  A  A. y  e.  B  ( ph  ->  ( x  =  z  /\  y  =  w )
 ) ) )
 
17-Jun-20172reu5lem2 2972 Lemma for 2reu5 2974. (Contributed by Alexander van der Vekens, 17-Jun-2017.)
 |-  ( A. x  e.  A  E* y  e.  B ph  <->  A. x E* y
 ( x  e.  A  /\  y  e.  B  /\  ph ) )
 
17-Jun-20172reu5lem1 2971 Lemma for 2reu5 2974. Note that  E! x  e.  A E! y  e.  B ph does not mean "there is exactly one  x in  A and exactly one  y in  B such that  ph holds;" see comment for 2eu5 2228. (Contributed by Alexander van der Vekens, 17-Jun-2017.)
 |-  ( E! x  e.  A  E! y  e.  B  ph  <->  E! x E! y
 ( x  e.  A  /\  y  e.  B  /\  ph ) )
 
17-Jun-20172rmorex 2970 Double restricted quantification with "at most one," analogous to 2moex 2215. (Contributed by Alexander van der Vekens, 17-Jun-2017.)
 |-  ( E* x  e.  A E. y  e.  B  ph  ->  A. y  e.  B  E* x  e.  A ph )
 
17-Jun-2017rmoimi2 2967 Restricted "at most one" is preserved through implication (note wff reversal). (Contributed by Alexander van der Vekens, 17-Jun-2017.)
 |- 
 A. x ( ( x  e.  A  /\  ph )  ->  ( x  e.  B  /\  ps )
 )   =>    |-  ( E* x  e.  B ps  ->  E* x  e.  A ph )
 
17-Jun-2017rmoimia 2966 Restricted "at most one" is preserved through implication (note wff reversal). (Contributed by Alexander van der Vekens, 17-Jun-2017.)
 |-  ( x  e.  A  ->  ( ph  ->  ps )
 )   =>    |-  ( E* x  e.  A ps  ->  E* x  e.  A ph )
 
17-Jun-2017rmoim 2965 Restricted "at most one" is preserved through implication (note wff reversal). (Contributed by Alexander van der Vekens, 17-Jun-2017.)
 |-  ( A. x  e.  A  ( ph  ->  ps )  ->  ( E* x  e.  A ps  ->  E* x  e.  A ph ) )
 
17-Jun-2017rmov 2805 A uniqueness quantifier restricted to the universe is unrestricted. (Contributed by Alexander van der Vekens, 17-Jun-2017.)
 |-  ( E* x  e. 
 _V ph  <->  E* x ph )
 
17-Jun-2017cbvrmov 2768 Change the bound variable of a restricted uniqueness quantifier using implicit substitution. (Contributed by Alexander van der Vekens, 17-Jun-2017.)
 |-  ( x  =  y 
 ->  ( ph  <->  ps ) )   =>    |-  ( E* x  e.  A ph  <->  E* y  e.  A ps )
 
17-Jun-2017nrexrmo 2758 Nonexistence implies restricted "at most one". (Contributed by NM, 17-Jun-2017.)
 |-  ( -.  E. x  e.  A  ph  ->  E* x  e.  A ph )
 
17-Jun-2017rmoeqd 2748 Equality deduction for restricted uniqueness quantifier. (Contributed by Alexander van der Vekens, 17-Jun-2017.)
 |-  ( A  =  B  ->  ( ph  <->  ps ) )   =>    |-  ( A  =  B  ->  ( E* x  e.  A ph  <->  E* x  e.  B ps ) )
 
17-Jun-2017rmoeq1 2740 Equality theorem for restricted uniqueness quantifier. (Contributed by Alexander van der Vekens, 17-Jun-2017.)
 |-  ( A  =  B  ->  ( E* x  e.  A ph  <->  E* x  e.  B ph ) )
 
17-Jun-2017rmoeq1f 2736 Equality theorem for restricted uniqueness quantifier, with bound-variable hypotheses instead of distinct variable restrictions. (Contributed by Alexander van der Vekens, 17-Jun-2017.)
 |-  F/_ x A   &    |-  F/_ x B   =>    |-  ( A  =  B  ->  ( E* x  e.  A ph  <->  E* x  e.  B ph ) )
 
17-Jun-2017nfrmod 2714 Deduction version of nfrmo 2716. (Contributed by NM, 17-Jun-2017.)
 |- 
 F/ y ph   &    |-  ( ph  ->  F/_ x A )   &    |-  ( ph  ->  F/ x ps )   =>    |-  ( ph  ->  F/ x E* y  e.  A ps )
 
17-Jun-2017sb8mo 2163 Variable substitution in uniqueness quantifier. (Contributed by Alexander van der Vekens, 17-Jun-2017.)
 |- 
 F/ y ph   =>    |-  ( E* x ph  <->  E* y [ y  /  x ] ph )
 
16-Jun-2017spwmo 14329 A poset has at most one supremum. (Contributed by NM, 13-May-2008.) (Revised by NM, 16-Jun-2017.)
 |-  ( ph  <->  ( A. y  e.  A  y R x 
 /\  A. y  e.  X  ( A. z  e.  A  z R y  ->  x R y ) ) )   =>    |-  ( R  e.  PosetRel  ->  E* x  e.  X ph )
 
16-Jun-2017poslubmo 14244 Least upper bounds in a poset are unique if they exist. (Contributed by Stefan O'Rear, 31-Jan-2015.) (Revised by NM, 16-Jun-2017.)
 |- 
 .<_  =  ( le `  K )   &    |-  B  =  ( Base `  K )   =>    |-  ( ( K  e.  Poset  /\  S  C_  B )  ->  E* x  e.  B ( A. y  e.  S  y  .<_  x  /\  A. z  e.  B  ( A. y  e.  S  y  .<_  z  ->  x  .<_  z ) ) )
 
16-Jun-2017brdom7disj 8151 An equivalence to a dominance relation for disjoint sets. (Contributed by NM, 29-Mar-2007.) (Revised by NM, 16-Jun-2017.)
 |-  A  e.  _V   &    |-  B  e.  _V   &    |-  ( A  i^i  B )  =  (/)   =>    |-  ( A  ~<_  B  <->  E. f ( A. x  e.  B  E* y  e.  A { x ,  y }  e.  f  /\  A. x  e.  A  E. y  e.  B  { y ,  x }  e.  f
 ) )
 
16-Jun-2017brdom4 8150 An equivalence to a dominance relation. (Contributed by NM, 28-Mar-2007.) (Revised by NM, 16-Jun-2017.)
 |-  B  e.  _V   =>    |-  ( A  ~<_  B  <->  E. f ( A. x  e.  B  E* y  e.  A x f y  /\  A. x  e.  A  E. y  e.  B  y f x ) )
 
16-Jun-2017iunmapdisj 7645 The union  U_ n  e.  C ( A  ^m  n ) is a disjoint union. (Contributed by Mario Carneiro, 17-May-2015.) (Revised by NM, 16-Jun-2017.)
 |- 
 E* n  e.  C B  e.  ( A  ^m  n )
 
16-Jun-2017moriotass 6329 Restriction of a unique element to a smaller class. (Contributed by NM, 19-Feb-2006.) (Revised by NM, 16-Jun-2017.)
 |-  ( ( A  C_  B  /\  E. x  e.  A  ph  /\  E* x  e.  B ph )  ->  ( iota_ x  e.  A ph )  =  ( iota_ x  e.  B ph )
 )
 
16-Jun-2017dffun9 5248 Alternate definition of a function. (Contributed by NM, 28-Mar-2007.) (Revised by NM, 16-Jun-2017.)
 |-  ( Fun  A  <->  ( Rel  A  /\  A. x  e.  dom  A E* y  e.  ran  A  x A y ) )
 
16-Jun-2017reuxfr2 4557 Transfer existential uniqueness from a variable  x to another variable  y contained in expression  A. (Contributed by NM, 14-Nov-2004.) (Revised by NM, 16-Jun-2017.)
 |-  ( y  e.  B  ->  A  e.  B )   &    |-  ( x  e.  B  ->  E* y  e.  B x  =  A )   =>    |-  ( E! x  e.  B  E. y  e.  B  ( x  =  A  /\  ph )  <->  E! y  e.  B  ph )
 
16-Jun-2017reuxfr2d 4556 Transfer existential uniqueness from a variable  x to another variable  y contained in expression  A. (Contributed by NM, 16-Jan-2012.) (Revised by NM, 16-Jun-2017.)
 |-  ( ( ph  /\  y  e.  B )  ->  A  e.  B )   &    |-  ( ( ph  /\  x  e.  B ) 
 ->  E* y  e.  B x  =  A )   =>    |-  ( ph  ->  ( E! x  e.  B  E. y  e.  B  ( x  =  A  /\  ps )  <->  E! y  e.  B  ps ) )
 
16-Jun-2017somo 4347 A totally ordered set has at most one minimal element. (Contributed by Mario Carneiro, 24-Jun-2015.) (Revised by NM, 16-Jun-2017.)
 |-  ( R  Or  A  ->  E* x  e.  A A. y  e.  A  -.  y R x )
 
16-Jun-2017df-disj 3995 A collection of classes  B ( x ) is disjoint when for each element  y, it is in  B ( x ) for at most one  x. (Contributed by Mario Carneiro, 14-Nov-2016.) (Revised by NM, 16-Jun-2017.)
 |-  (Disj  x  e.  A B 
 <-> 
 A. y E* x  e.  A y  e.  B )
 
16-Jun-2017rmoi 3081 Consequence of "at most one", using implicit substitution. (Contributed by NM, 4-Nov-2012.) (Revised by NM, 16-Jun-2017.)
 |-  ( x  =  B  ->  ( ph  <->  ps ) )   &    |-  ( x  =  C  ->  (
 ph 
 <->  ch ) )   =>    |-  ( ( E* x  e.  A ph  /\  ( B  e.  A  /\  ps )  /\  ( C  e.  A  /\  ch ) )  ->  B  =  C )
 
16-Jun-2017rmob 3080 Consequence of "at most one", using implicit substitution. (Contributed by NM, 2-Jan-2015.) (Revised by NM, 16-Jun-2017.)
 |-  ( x  =  B  ->  ( ph  <->  ps ) )   &    |-  ( x  =  C  ->  (
 ph 
 <->  ch ) )   =>    |-  ( ( E* x  e.  A ph  /\  ( B  e.  A  /\  ps ) )  ->  ( B  =  C  <->  ( C  e.  A  /\  ch ) ) )
 
16-Jun-2017rmo3 3079 Restricted "at most one" using explicit substitution. (Contributed by NM, 4-Nov-2012.) (Revised by NM, 16-Jun-2017.)
 |- 
 F/ y ph   =>    |-  ( E* x  e.  A ph  <->  A. x  e.  A  A. y  e.  A  ( ( ph  /\  [
 y  /  x ] ph )  ->  x  =  y ) )
 
16-Jun-20172reuswap 2968 A condition allowing swap of uniqueness and existential quantifiers. (Contributed by Thierry Arnoux, 7-Apr-2017.) (Revised by NM, 16-Jun-2017.)
 |-  ( A. x  e.  A  E* y  e.  B ph  ->  ( E! x  e.  A  E. y  e.  B  ph 
 ->  E! y  e.  B  E. x  e.  A  ph ) )
 
16-Jun-2017rmoan 2964 Restricted "at most one" still holds when a conjunct is added. (Contributed by NM, 16-Jun-2017.)
 |-  ( E* x  e.  A ph  ->  E* x  e.  A ( ps  /\  ph ) )
 
16-Jun-2017rmo4 2959 Restricted "at most one" using implicit substitution. (Contributed by NM, 24-Oct-2006.) (Revised by NM, 16-Jun-2017.)
 |-  ( x  =  y 
 ->  ( ph  <->  ps ) )   =>    |-  ( E* x  e.  A ph  <->  A. x  e.  A  A. y  e.  A  ( ( ph  /\  ps )  ->  x  =  y ) )
 
16-Jun-2017cbvrmo 2764 Change the bound variable of restricted "at most one" using implicit substitution. (Contributed by NM, 16-Jun-2017.)
 |- 
 F/ y ph   &    |-  F/ x ps   &    |-  ( x  =  y  ->  (
 ph 
 <->  ps ) )   =>    |-  ( E* x  e.  A ph  <->  E* y  e.  A ps )
 
16-Jun-2017rmo5 2757 Restricted "at most one" in term of uniqueness. (Contributed by NM, 16-Jun-2017.)
 |-  ( E* x  e.  A ph  <->  ( E. x  e.  A  ph  ->  E! x  e.  A  ph ) )
 
16-Jun-2017reurmo 2756 Restricted existential uniqueness implies restricted "at most one." (Contributed by NM, 16-Jun-2017.)
 |-  ( E! x  e.  A  ph  ->  E* x  e.  A ph )
 
16-Jun-2017reu5 2754 Restricted uniqueness in terms of "at most one." (Contributed by NM, 23-May-1999.) (Revised by NM, 16-Jun-2017.)
 |-  ( E! x  e.  A  ph  <->  ( E. x  e.  A  ph  /\  E* x  e.  A ph ) )
 
16-Jun-2017mormo 2753 Unrestricted "at most one" implies restricted "at most one". (Contributed by NM, 16-Jun-2017.)
 |-  ( E* x ph  ->  E* x  e.  A ph )
 
16-Jun-2017rmobii 2732 Formula-building rule for restricted existential quantifier (inference rule). (Contributed by NM, 16-Jun-2017.)
 |-  ( ph  <->  ps )   =>    |-  ( E* x  e.  A ph  <->  E* x  e.  A ps )
 
16-Jun-2017rmobiia 2731 Formula-building rule for restricted existential quantifier (inference rule). (Contributed by NM, 16-Jun-2017.)
 |-  ( x  e.  A  ->  ( ph  <->  ps ) )   =>    |-  ( E* x  e.  A ph  <->  E* x  e.  A ps )
 
16-Jun-2017rmobidv 2730 Formula-building rule for restricted existential quantifier (deduction rule). (Contributed by NM, 16-Jun-2017.)
 |-  ( ph  ->  ( ps 
 <->  ch ) )   =>    |-  ( ph  ->  ( E* x  e.  A ps 
 <->  E* x  e.  A ch ) )
 
16-Jun-2017rmobidva 2729 Formula-building rule for restricted existential quantifier (deduction rule). (Contributed by NM, 16-Jun-2017.)
 |-  ( ( ph  /\  x  e.  A )  ->  ( ps 
 <->  ch ) )   =>    |-  ( ph  ->  ( E* x  e.  A ps 
 <->  E* x  e.  A ch ) )
 
16-Jun-2017rmobida 2728 Formula-building rule for restricted existential quantifier (deduction rule). (Contributed by NM, 16-Jun-2017.)
 |- 
 F/ x ph   &    |-  ( ( ph  /\  x  e.  A ) 
 ->  ( ps  <->  ch ) )   =>    |-  ( ph  ->  ( E* x  e.  A ps 
 <->  E* x  e.  A ch ) )
 
16-Jun-2017nfrmo 2716 Bound-variable hypothesis builder for restricted uniqueness. (Contributed by NM, 16-Jun-2017.)
 |-  F/_ x A   &    |-  F/ x ph   =>    |-  F/ x E* y  e.  A ph
 
16-Jun-2017nfrmo1 2712  x is not free in  E* x  e.  A ph. (Contributed by NM, 16-Jun-2017.)
 |- 
 F/ x E* x  e.  A ph
 
16-Jun-2017df-rmo 2552 Define restricted "at most one". (Contributed by NM, 16-Jun-2017.)
 |-  ( E* x  e.  A ph  <->  E* x ( x  e.  A  /\  ph )
 )
 
1-Jun-2017afvelrnb0 27403 A member of a function's range is a value of the function, only one direction of implication of fvelrnb 5531. (Contributed by Alexander van der Vekens, 1-Jun-2017.)
 |-  ( F  Fn  A  ->  ( B  e.  ran  F  ->  E. x  e.  A  ( F' x )  =  B ) )
 
1-Jun-2017dmmpt2g 27354 Domain of a class given by the "maps to" notation, closed form of dmmpt2 6155. (Contributed by Alexander van der Vekens, 1-Jun-2017.)
 |-  F  =  ( x  e.  A ,  y  e.  B  |->  C )   =>    |-  ( C  e.  V  ->  dom  F  =  ( A  X.  B ) )
 
26-May-2017ndmaovdistr 27446 Any operation is distributive outside its domain. In contrast to ndmaovdistr 27446 where it is required that the operation's domain doesn't contain the empty set ( -.  (/)  e.  S), no additional assumption is required. (Contributed by Alexander van der Vekens, 26-May-2017.)
 |-  dom  F  =  ( S  X.  S )   &    |-  dom  G  =  ( S  X.  S )   =>    |-  ( -.  ( A  e.  S  /\  B  e.  S  /\  C  e.  S ) 
 -> (( A G (( B F C)) ))  = (( (( A G B))  F (( A G C)) ))  )
 
26-May-2017ndmaovass 27445 Any operation is associative outside its domain. In contrast to ndmaovass 27445 where it is required that the operation's domain doesn't contain the empty set ( -.  (/)  e.  S), no additional assumption is required. (Contributed by Alexander van der Vekens, 26-May-2017.)
 |-  dom  F  =  ( S  X.  S )   =>    |-  ( -.  ( A  e.  S  /\  B  e.  S  /\  C  e.  S )  -> (( (( A F B))  F C))  = (( A F (( B F C)) ))  )
 
26-May-2017ndmaovcom 27444 Any operation is commutative outside its domain, analogous to ndmovcom 5968. (Contributed by Alexander van der Vekens, 26-May-2017.)
 |-  dom  F  =  ( S  X.  S )   =>    |-  ( -.  ( A  e.  S  /\  B  e.  S )  -> (( A F B))  = (( B F A))  )
 
26-May-2017ndmaovrcl 27443 Reverse closure law, in contrast to ndmovrcl 5967 where it is required that the operation's domain doesn't contain the empty set ( -.  (/)  e.  S), no additional asumption is required. (Contributed by Alexander van der Vekens, 26-May-2017.)
 |-  dom  F  =  ( S  X.  S )   =>    |-  ( (( A F B))  e.  S  ->  ( A  e.  S  /\  B  e.  S ) )
 
26-May-2017ndmaovcl 27442 The "closure" of an operation outside its domain, when the operation's value is a set in contrast to ndmovcl 5966 where it is required that the domain contains the empty set ( (/) 
e.  S). (Contributed by Alexander van der Vekens, 26-May-2017.)
 |-  dom  F  =  ( S  X.  S )   &    |-  ( ( A  e.  S  /\  B  e.  S )  -> (( A F B))  e.  S )   &    |- (( A F B))  e.  _V   =>    |- (( A F B))  e.  S
 
26-May-2017aoprssdm 27441 Domain of closure of an operation. In contrast to oprssdm 5963, no additional property for S (
-.  (/)  e.  S) is required! (Contributed by Alexander van der Vekens, 26-May-2017.)
 |-  (
 ( x  e.  S  /\  y  e.  S )  -> (( x F y))  e.  S )   =>    |-  ( S  X.  S )  C_  dom  F
 
26-May-2017aovmpt4g 27440 Value of a function given by the "maps to" notation, analogous to ovmpt4g 5931. (Contributed by Alexander van der Vekens, 26-May-2017.)
 |-  F  =  ( x  e.  A ,  y  e.  B  |->  C )   =>    |-  ( ( x  e.  A  /\  y  e.  B  /\  C  e.  V )  -> (( x F y))  =  C )
 
26-May-2017faovcl 27439 Closure law for an operation, analogous to fovcl 5910. (Contributed by Alexander van der Vekens, 26-May-2017.)
 |-  F : ( R  X.  S ) --> C   =>    |-  ( ( A  e.  R  /\  B  e.  S )  -> (( A F B))  e.  C )
 
26-May-2017ffnaov 27438 An operation maps to a class to which all values belong, analogous to ffnov 5909. (Contributed by Alexander van der Vekens, 26-May-2017.)
 |-  ( F : ( A  X.  B ) --> C  <->  ( F  Fn  ( A  X.  B ) 
 /\  A. x  e.  A  A. y  e.  B (( x F y))  e.  C ) )
 
26-May-2017fnotaovb 27437 Equivalence of operation value and ordered triple membership, analogous to fnopfvb 5525. (Contributed by Alexander van der Vekens, 26-May-2017.)
 |-  (
 ( F  Fn  ( A  X.  B )  /\  C  e.  A  /\  D  e.  B )  ->  ( (( C F D))  =  R  <->  <. C ,  D ,  R >.  e.  F ) )
 
26-May-2017rspceaov 27436 A frequently used special case of rspc2ev 2893 for operation values, analogous to rspceov 5854. (Contributed by Alexander van der Vekens, 26-May-2017.)
 |-  (
 ( C  e.  A  /\  D  e.  B  /\  S  = (( C F D))  )  ->  E. x  e.  A  E. y  e.  B  S  = (( x F y))  )
 
26-May-2017aovov0bi 27435 The operation's value on an ordered pair is the empty set if and only if the alternative value of the operation on this ordered pair is either the empty set or the universal class. (Contributed by Alexander van der Vekens, 26-May-2017.)
 |-  (
 ( A F B )  =  (/)  <->  ( (( A F B))  =  (/)  \/ (( A F B))  =  _V ) )
 
26-May-2017aov0nbovbi 27434 The operation's value on an ordered pair is an element of a set if and only if the alternative value of the operation on this ordered pair is an element of that set, if the set does not contain the empty set. (Contributed by Alexander van der Vekens, 26-May-2017.)
 |-  ( (/)  e/  C  ->  ( (( A F B))  e.  C  <->  ( A F B )  e.  C ) )
 
26-May-2017aovovn0oveq 27433 If the operation's value at an argument is not the empty set, it equals the value of the alternative operation at this argument. (Contributed by Alexander van der Vekens, 26-May-2017.)
 |-  (
 ( A F B )  =/=  (/)  -> (( A F B))  =  ( A F B ) )
 
26-May-2017aov0ov0 27432 If the alternative value of the operation on an ordered pair is the empty set, the operation's value at this ordered pair is the empty set. (Contributed by Alexander van der Vekens, 26-May-2017.)
 |-  ( (( A F B))  =  (/)  ->  ( A F B )  =  (/) )
 
26-May-2017aovvoveq 27431 The alternative value of the operation on an ordered pair equals the operation's value on this ordered pair. (Contributed by Alexander van der Vekens, 26-May-2017.)
 |-  ( (( A F B))  e.  C  -> (( A F B))  =  ( A F B ) )
 
26-May-2017aovnuoveq 27430 The alternative value of the operation on an ordered pair equals the operation's value at this ordered pair. (Contributed by Alexander van der Vekens, 26-May-2017.)
 |-  ( (( A F B))  =/=  _V  -> (( A F B))  =  ( A F B ) )
 
26-May-2017aovpcov0 27429 If the alternative value of the operation on an ordered pair is the universal class, the operation's value at this ordered pair is the empty set. (Contributed by Alexander van der Vekens, 26-May-2017.)
 |-  ( (( A F B))  =  _V  ->  ( A F B )  =  (/) )
 
26-May-2017aovrcl 27428 Reverse closure for an operation value, analogous to afvvv 27385. In contrast to ovrcl 5849, elementhood of the operation's value in a set is required, not containing an element. (Contributed by Alexander van der Vekens, 26-May-2017.)
 |-  Rel  dom 
 F   =>    |-  ( (( A F B))  e.  C  ->  ( A  e.  _V  /\  B  e.  _V ) )
 
26-May-2017aovprc 27427 The value of an operation when the one of the arguments is a proper class, analogous to ovprc 5846. (Contributed by Alexander van der Vekens, 26-May-2017.)
 |-  Rel  dom 
 F   =>    |-  ( -.  ( A  e.  _V  /\  B  e.  _V )  -> (( A F B))  =  _V )
 
26-May-2017aovvfunressn 27426 If the operation value of a class for an argument is a set, the class restricted to the singleton of the argument is a function. (Contributed by Alexander van der Vekens, 26-May-2017.)
 |-  ( (( A F B))  e.  C  ->  Fun  ( F  |`  { <. A ,  B >. } )
 )
 
26-May-2017nfunsnaov 27425 If the restriction of a class to a singleton is not a function, its operation value is the universal class. (Contributed by Alexander van der Vekens, 26-May-2017.)
 |-  ( -.  Fun  ( F  |`  { <. A ,  B >. } )  -> (( A F B))  =  _V )
 
26-May-2017aovvdm 27424 If the operation value of a class for an ordered pair is a set, the ordered pair is contained in the domain of the class. (Contributed by Alexander van der Vekens, 26-May-2017.)
 |-  ( (( A F B))  e.  C  -> 
 <. A ,  B >.  e. 
 dom  F )
 
26-May-2017ndmaovg 27423 The value of an operation outside its domain, analogous to ndmovg 5964. (Contributed by Alexander van der Vekens, 26-May-2017.)
 |-  (
 ( dom  F  =  ( R  X.  S ) 
 /\  -.  ( A  e.  R  /\  B  e.  S ) )  -> (( A F B))  =  _V )
 
26-May-2017ndmaov 27422 The value of an operation outside its domain, analogous to ndmafv 27380. (Contributed by Alexander van der Vekens, 26-May-2017.)
 |-  ( -.  <. A ,  B >.  e.  dom  F  -> (( A F B))  =  _V )
 
26-May-2017aovnfundmuv 27421 If an ordered pair is not in the domain of a class or the class is not a function restricted to the ordered pair, then the operation value for this pair is the universal class. (Contributed by Alexander van der Vekens, 26-May-2017.)
 |-  ( -.  Fdef@  <. A ,  B >.  -> (( A F B))  =  _V )
 
26-May-2017aovfundmoveq 27420 If a class is a function restricted to an ordered pair of its domain, then the value of the operation on this pair is equal for both definitions. (Contributed by Alexander van der Vekens, 26-May-2017.)
 |-  ( Fdef@ 
 <. A ,  B >.  -> (( A F B))  =  ( A F B ) )
 
26-May-2017csbaovg 27419 Move class substitution in and out of an operation. (Contributed by Alexander van der Vekens, 26-May-2017.)
 |-  ( A  e.  D  ->  [_ A  /  x ]_ (( B F C))  = (( [_ A  /  x ]_ B [_ A  /  x ]_ F [_ A  /  x ]_ C))  )
 
26-May-2017nfaov 27418 Bound-variable hypothesis builder for operation value, analogous to nfov 5842. To prove a deduction version of this analogous to nfovd 5841 is not quickly possible because many deduction versions for bound-variable hypothesis builder for constructs the definition of alternative operation values is based on are not available (see nfafv 27376). (Contributed by Alexander van der Vekens, 26-May-2017.)
 |-  F/_ x A   &    |-  F/_ x F   &    |-  F/_ x B   =>    |-  F/_ x (( A F B))
 
26-May-2017aoveq123d 27417 Equality deduction for operation value, analogous to oveq123d 5840. (Contributed by Alexander van der Vekens, 26-May-2017.)
 |-  ( ph  ->  F  =  G )   &    |-  ( ph  ->  A  =  B )   &    |-  ( ph  ->  C  =  D )   =>    |-  ( ph  -> (( A F C))  = (( B G D))  )
 
26-May-2017df-aov 27416 Define the value of an operation. In contrast to df-ov 5822, the alternative definition for a function value ( see df-afv 27371) is used. By this, the value of the operation applied to two arguments is the universal class if the operation is not defined for these two arguments. There are still no restrictions of any kind on what those class expressions may be, although only certain kinds of class expressions - a binary operation  F and its arguments  A and  B- will be useful for proving meaningful theorems. (Contributed by Alexander van der Vekens, 26-May-2017.)
 |- (( A F B))  =  ( F' <. A ,  B >. )
 
26-May-2017afvnfundmuv 27379 If a set is not in the domain of a class or the class is not a function restricted to the set, then the function value for this set is the universe. (Contributed by Alexander van der Vekens, 26-May-2017.)
 |-  ( -.  Fdef@  A  ->  ( F'
 A )  =  _V )
 
26-May-2017nfafv 27376 Bound-variable hypothesis builder for function value, analogous to nffv 5492. To prove a deduction version of this analogous to nffvd 5494 is not easily possible because a deduction version of nfdfat 27368 cannot be shown easily. (Contributed by Alexander van der Vekens, 26-May-2017.)
 |-  F/_ x F   &    |-  F/_ x A   =>    |-  F/_ x ( F' A )
 
26-May-2017afveq12d 27373 Equality deduction for function value, analogous to fveq12d 5491. (Contributed by Alexander van der Vekens, 26-May-2017.)
 |-  ( ph  ->  F  =  G )   &    |-  ( ph  ->  A  =  B )   =>    |-  ( ph  ->  ( F' A )  =  ( G' B ) )
 
26-May-2017nfdfat 27368 Bound-variable hypothesis builder for "defined at". To prove a deduction version of this theorem is not easily possible because many deduction versions for bound-variable hypothesis builder for constructs the definition of "defined at" is based on are not available (e.g. for Fun/Rel, dom, C_, etc.). (Contributed by Alexander van der Vekens, 26-May-2017.)
 |-  F/_ x F   &    |-  F/_ x A   =>    |- 
 F/ x  Fdef@  A
 
26-May-2017dfateq12d 27367 Equality deduction for "defined at". (Contributed by Alexander van der Vekens, 26-May-2017.)
 |-  ( ph  ->  F  =  G )   &    |-  ( ph  ->  A  =  B )   =>    |-  ( ph  ->  ( Fdef@  A  <->  Gdef@  B ) )
 
26-May-2017fveqvfvv 27360 If a function's value at an argument is the universal class (which can never be the case because of fvex 5499), the function's value at this argument is any set (especially the empty set). In short "If a function's value is a proper class, it is a set", which sounds strange/contradictory, but which is a consequence of that a contradiction implies anything ( see pm2.21i 125). (Contributed by Alexander van der Vekens, 26-May-2017.)
 |-  (
 ( F `  A )  =  _V  ->  ( F `  A )  =  B )
 
26-May-2017fvfundmfvn0 27359 If a class' value at an argument is not the empty set, the argument is contained in the domain of the class, and the class restricted to the argument is a function. (Contributed by Alexander van der Vekens, 26-May-2017.)
 |-  (
 ( F `  A )  =/=  (/)  ->  ( A  e.  dom  F  /\  Fun  ( F  |`  { A } ) ) )
 
26-May-2017nvelim 27351 If a class is the universal class it doesn't belong to any class, generalisation of nvel 4154. (Contributed by Alexander van der Vekens, 26-May-2017.)
 |-  ( A  =  _V  ->  -.  A  e.  B )
 
25-May-2017ffnafv 27410 A function maps to a class to which all values belong, analogous to ffnfv 5646. (Contributed by Alexander van der Vekens, 25-May-2017.)
 |-  ( F : A --> B  <->  ( F  Fn  A  /\  A. x  e.  A  ( F' x )  e.  B )
 )
 
25-May-2017fafvelrn 27409 A function's value belongs to its codomain, analogous to ffvelrn 5624. (Contributed by Alexander van der Vekens, 25-May-2017.)
 |-  (
 ( F : A --> B  /\  C  e.  A )  ->  ( F' C )  e.  B )
 
25-May-2017fnafvelrn 27408 A function's value belongs to its range, analogous to fnfvelrn 5623. (Contributed by Alexander van der Vekens, 25-May-2017.)
 |-  (
 ( F  Fn  A  /\  B  e.  A ) 
 ->  ( F' B )  e.  ran  F )
 
25-May-2017afvelrn 27407 A function's value belongs to its range, analogous to fvelrn 5622. (Contributed by Alexander van der Vekens, 25-May-2017.)
 |-  (
 ( Fun  F  /\  A  e.  dom  F ) 
 ->  ( F' A )  e.  ran  F )
 
25-May-2017afvelima 27406 Function value in an image, analogous to fvelima 5535. (Contributed by Alexander van der Vekens, 25-May-2017.)
 |-  (
 ( Fun  F  /\  A  e.  ( F " B ) )  ->  E. x  e.  B  ( F' x )  =  A )
 
25-May-2017dfaimafn2 27405 Alternate definition of the image of a function as an indexed union of singletons of function values, analogous to dfimafn2 5533. (Contributed by Alexander van der Vekens, 25-May-2017.)
 |-  (
 ( Fun  F  /\  A  C_  dom  F )  ->  ( F " A )  =  U_ x  e.  A  { ( F' x ) } )
 
25-May-2017dfaimafn 27404 Alternate definition of the image of a function, analogous to dfimafn 5532. (Contributed by Alexander van der Vekens, 25-May-2017.)
 |-  (
 ( Fun  F  /\  A  C_  dom  F )  ->  ( F " A )  =  { y  |  E. x  e.  A  ( F' x )  =  y } )
 
25-May-2017afvelrnb 27402 A member of a function's range is a value of the function, analogous to fvelrnb 5531 with the additional requirement that the member must be a set. (Contributed by Alexander van der Vekens, 25-May-2017.)
 |-  (
 ( F  Fn  A  /\  B  e.  V ) 
 ->  ( B  e.  ran  F  <->  E. x  e.  A  ( F' x )  =  B ) )
 
25-May-2017fnrnafv 27401 The range of a function expressed as a collection of the function's values, analogous to fnrnfv 5530. (Contributed by Alexander van der Vekens, 25-May-2017.)
 |-  ( F  Fn  A  ->  ran  F  =  { y  |  E. x  e.  A  y  =  ( F' x ) } )
 
25-May-2017dfafn5b 27400 Representation of a function in terms of its values, analogous to dffn5 5529 (only if it is assumed that the function value for each x is a set). (Contributed by Alexander van der Vekens, 25-May-2017.)
 |-  ( A. x  e.  A  ( F' x )  e.  V  ->  ( F  Fn  A  <->  F  =  ( x  e.  A  |->  ( F' x ) ) ) )
 
25-May-2017dfafn5a 27399 Representation of a function in terms of its values, analogous to dffn5 5529 (only one direction of implication!). (Contributed by Alexander van der Vekens, 25-May-2017.)
 |-  ( F  Fn  A  ->  F  =  ( x  e.  A  |->  ( F' x ) ) )
 
25-May-2017funbrafv2b 27398 Function value in terms of a binary relation, analogous to funbrfv2b 5528. (Contributed by Alexander van der Vekens, 25-May-2017.)
 |-  ( Fun  F  ->  ( A F B  <->  ( A  e.  dom 
 F  /\  ( F' A )  =  B ) ) )
 
25-May-2017funbrafv 27397 The second argument of a binary relation on a function is the function's value, analogous to funbrfv 5522. (Contributed by Alexander van der Vekens, 25-May-2017.)
 |-  ( Fun  F  ->  ( A F B  ->  ( F'
 A )  =  B ) )
 
25-May-2017funopafvb 27396 Equivalence of function value and ordered pair membership, analogous to funopfvb 5527. (Contributed by Alexander van der Vekens, 25-May-2017.)
 |-  (
 ( Fun  F  /\  A  e.  dom  F ) 
 ->  ( ( F' A )  =  B  <->  <. A ,  B >.  e.  F ) )
 
25-May-2017funbrafvb 27395 Equivalence of function value and binary relation, analogous to funbrfvb 5526. (Contributed by Alexander van der Vekens, 25-May-2017.)
 |-  (
 ( Fun  F  /\  A  e.  dom  F ) 
 ->  ( ( F' A )  =  B  <->  A F B ) )
 
25-May-2017fnopafvb 27394 Equivalence of function value and ordered pair membership, analogous to fnopfvb 5525. (Contributed by Alexander van der Vekens, 25-May-2017.)
 |-  (
 ( F  Fn  A  /\  B  e.  A ) 
 ->  ( ( F' B )  =  C  <->  <. B ,  C >.  e.  F ) )
 
25-May-2017fnbrafvb 27393 Equivalence of function value and binary relation, analogous to fnbrfvb 5524. (Contributed by Alexander van der Vekens, 25-May-2017.)
 |-  (
 ( F  Fn  A  /\  B  e.  A ) 
 ->  ( ( F' B )  =  C  <->  B F C ) )
 
25-May-2017afvfv0bi 27392 The function's value at an argument is the empty set if and only if the value of the alternative function at this argument is either the empty set or the universe. (Contributed by Alexander van der Vekens, 25-May-2017.)
 |-  (
 ( F `  A )  =  (/)  <->  ( ( F'
 A )  =  (/)  \/  ( F' A )  =  _V ) )
 
25-May-2017afv0nbfvbi 27391 The function's value at an argument is an element of a set if and only if the value of the alternative function at this argument is an element of that set, if the set does not contain the empty set. (Contributed by Alexander van der Vekens, 25-May-2017.)
 |-  ( (/)  e/  B  ->  ( ( F' A )  e.  B  <->  ( F `  A )  e.  B ) )
 
25-May-2017afvfvn0fveq 27390 If the function's value at an argument is not the empty set, it equals the value of the alternative function at this argument. (Contributed by Alexander van der Vekens, 25-May-2017.)
 |-  (
 ( F `  A )  =/=  (/)  ->  ( F' A )  =  ( F `
  A ) )
 
25-May-2017afv0fv0 27389 If the value of the alternative function at an argument is the empty set, the function's value at this argument is the empty set. (Contributed by Alexander van der Vekens, 25-May-2017.)
 |-  (
 ( F' A )  =  (/)  ->  ( F `  A )  =  (/) )
 
25-May-2017afvvfveq 27388 The value of the alternative function at a set as argument equals the function's value at this argument. (Contributed by Alexander van der Vekens, 25-May-2017.)
 |-  (
 ( F' A )  e.  B  ->  ( F' A )  =  ( F `  A ) )
 
25-May-2017afvnufveq 27387 The value of the alternative function at a set as argument equals the function's value at this argument. (Contributed by Alexander van der Vekens, 25-May-2017.)
 |-  (
 ( F' A )  =/=  _V  ->  ( F' A )  =  ( F `  A ) )
 
25-May-2017afvpcfv0 27386 If the value of the alternative function at an argument is the universe, the function's value at this argument is the empty set. (Contributed by Alexander van der Vekens, 25-May-2017.)
 |-  (
 ( F' A )  =  _V  ->  ( F `  A )  =  (/) )
 
25-May-2017afvvv 27385 If a function's value at an argument is a set, the argument is also a set. (Contributed by Alexander van der Vekens, 25-May-2017.)
 |-  (
 ( F' A )  e.  B  ->  A  e.  _V )
 
25-May-2017afvprc 27384 A function's value at a proper class is the universe, compare with fvprc 5482. (Contributed by Alexander van der Vekens, 25-May-2017.)
 |-  ( -.  A  e.  _V  ->  ( F' A )  =  _V )
 
25-May-2017afvvfunressn 27383 If the function value of a class for an argument is a set, the class restricted to the singleton of the argument is a function. (Contributed by Alexander van der Vekens, 25-May-2017.)
 |-  (
 ( F' A )  e.  B  ->  Fun  ( F  |`  { A }
 ) )
 
25-May-2017nfunsnafv 27382 If the restriction of a class to a singleton is not a function, its value is the universe, compare with nfunsn 5519 (Contributed by Alexander van der Vekens, 25-May-2017.)
 |-  ( -.  Fun  ( F  |`  { A } )  ->  ( F'
 A )  =  _V )
 
25-May-2017afvvdm 27381 If the function value of a class for an argument is a set, the argument is contained in the domain of the class. (Contributed by Alexander van der Vekens, 25-May-2017.)
 |-  (
 ( F' A )  e.  B  ->  A  e.  dom  F )
 
25-May-2017ndmafv 27380 The value of a class outside its domain is the universe, compare with ndmfv 5513. (Contributed by Alexander van der Vekens, 25-May-2017.)
 |-  ( -.  A  e.  dom  F  ->  ( F' A )  =  _V )
 
25-May-2017afvfundmfveq 27378 If a class is a function restricted to a member of its domain, then the function value for this member is equal for both definitions. (Contributed by Alexander van der Vekens, 25-May-2017.)
 |-  ( Fdef@  A  ->  ( F' A )  =  ( F `
  A ) )
 
25-May-2017df-afv 27371 Alternative definition of the value of a function,  ( F' A ), also known as function application. In contrast to  ( F' A )  =  (/) (see df-fv 5229 and ndmfv 5513),  ( F' A )  =  _V if F is not defined for A! (Contributed by Alexander van der Vekens, 25-May-2017.)
 |-  ( F' A )  =  if ( Fdef@  A ,  U. { x  |  ( F " { A } )  =  { x } } ,  _V )
 
25-May-2017df-dfat 27366 Definition of the predicate that determines if some class  F is defined as function for an argument  A or, in other words, if the function value for some class 
F for an argument  A is defined. We say that  F is defined at  A if a  F is a function restricted to the member  A of its domain. (Contributed by Alexander van der Vekens, 25-May-2017.)
 |-  ( Fdef@  A  <->  ( A  e.  dom 
 F  /\  Fun  ( F  |`  { A } )
 ) )
 
18-May-2017fsnunfv 5681 Recover the added point from a point-added function. (Contributed by Stefan O'Rear, 28-Feb-2015.) (Revised by NM, 18-May-2017.)
 |-  ( ( X  e.  V  /\  Y  e.  W  /\  -.  X  e.  dom  F )  ->  ( ( F  u.  { <. X ,  Y >. } ) `  X )  =  Y )
 
5-May-2017ballotlemsima 23067 The image by  S of an interval before the first pick. (Contributed by Thierry Arnoux, 5-May-2017.)
 |-  M  e.  NN   &    |-  N  e.  NN   &    |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
 )  |  ( # `  c )  =  M }   &    |-  P  =  ( x  e.  ~P O  |->  ( ( # `  x )  /  ( # `  O ) ) )   &    |-  F  =  ( c  e.  O  |->  ( i  e.  ZZ  |->  ( ( # `  (
 ( 1 ... i
 )  i^i  c )
 )  -  ( # `  ( ( 1 ... i )  \  c
 ) ) ) ) )   &    |-  E  =  {
 c  e.  O  |  A. i  e.  (
 1 ... ( M  +  N ) ) 0  <  ( ( F `
  c ) `  i ) }   &    |-  N  <  M   &    |-  I  =  ( c  e.  ( O 
 \  E )  |->  sup ( { k  e.  ( 1 ... ( M  +  N )
 )  |  ( ( F `  c ) `
  k )  =  0 } ,  RR ,  `'  <  ) )   &    |-  S  =  ( c  e.  ( O  \  E )  |->  ( i  e.  ( 1
 ... ( M  +  N ) )  |->  if ( i  <_  ( I `  c ) ,  ( ( ( I `
  c )  +  1 )  -  i
 ) ,  i ) ) )   =>    |-  ( ( C  e.  ( O  \  E ) 
 /\  J  e.  (
 1 ... ( I `  C ) ) ) 
 ->  ( ( S `  C ) " (
 1 ... J ) )  =  ( ( ( S `  C ) `
  J ) ... ( I `  C ) ) )
 
2-May-2017addeq0 23036 Two complex which add up to zero are each other's negatives. (Contributed by Thierry Arnoux, 2-May-2017.)
 |-  (
 ( A  e.  CC  /\  B  e.  CC )  ->  ( ( A  +  B )  =  0  <->  A  =  -u B ) )
 
2-May-2017fzsplit3 23023 Split a finite interval of integers into two parts. (Contributed by Thierry Arnoux, 2-May-2017.)
 |-  ( K  e.  ( M ... N )  ->  ( M ... N )  =  ( ( M ... ( K  -  1
 ) )  u.  ( K ... N ) ) )
 
2-May-2017ax12b 1659 Two equivalent ways of expressing ax-12 1869. See the comment for ax-12 1869. (Contributed by NM, 2-May-2017.)
 |-  ( ( -.  x  =  y  ->  ( y  =  z  ->  A. x  y  =  z )
 ) 
 <->  ( -.  x  =  y  ->  ( -.  x  =  z  ->  ( y  =  z  ->  A. x  y  =  z ) ) ) )
 
1-May-2017lvecdim 15904 The dimension theorem for vector spaces: any two bases of the same vector space are equinumerous. Proven by using lssacsex 15891 and lbsacsbs 15903 to show that being a basis for a vector space is equivalent to being a basis for the associated algebraic closure system, and then using acsexdimd 14280. (Contributed by David Moews, 1-May-2017.)
 |-  J  =  (LBasis `  W )   =>    |-  ( ( W  e.  LVec  /\  S  e.  J  /\  T  e.  J )  ->  S  ~~  T )
 
1-May-2017lbsacsbs 15903 Being a basis in a vector space is equivalent to being a basis in the associated algebraic closure system. Equivalent to islbs2 15901. (Contributed by David Moews, 1-May-2017.)
 |-  A  =  ( LSubSp `  W )   &    |-  N  =  (mrCls `  A )   &    |-  X  =  (
 Base `  W )   &    |-  I  =  (mrInd `  A )   &    |-  J  =  (LBasis `  W )   =>    |-  ( W  e.  LVec  ->  ( S  e.  J  <->  ( S  e.  I  /\  ( N `  S )  =  X ) ) )
 
1-May-2017lssacsex 15891 In a vector space, subspaces form an algebraic closure system whose closure operator has the exchange property. Strengthening of lssacs 15718 by lspsolv 15890. (Contributed by David Moews, 1-May-2017.)
 |-  A  =  ( LSubSp `  W )   &    |-  N  =  (mrCls `  A )   &    |-  X  =  (
 Base `  W )   =>    |-  ( W  e.  LVec 
 ->  ( A  e.  (ACS `  X )  /\  A. s  e.  ~P  X A. y  e.  X  A. z  e.  ( ( N `  ( s  u.  { y } ) )  \  ( N `  s ) ) y  e.  ( N `  ( s  u. 
 { z } )
 ) ) )
 
1-May-2017acsexdimd 14280 In an algebraic closure system whose closure operator has the exchange property, if two independent sets have equal closure, they are equinumerous. See mreexfidimd 13546 for the finite case and acsinfdimd 14279 for the infinite case. This is a special case of Theorem 4.2.2 in [FaureFrolicher] p. 87. (Contributed by David Moews, 1-May-2017.)
 |-  ( ph  ->  A  e.  (ACS `  X )
 )   &    |-  N  =  (mrCls `  A )   &    |-  I  =  (mrInd `  A )   &    |-  ( ph  ->  A. s  e.  ~P  X A. y  e.  X  A. z  e.  ( ( N `  ( s  u.  { y }
 ) )  \  ( N `  s ) ) y  e.  ( N `
  ( s  u. 
 { z } )
 ) )   &    |-  ( ph  ->  S  e.  I )   &    |-  ( ph  ->  T  e.  I
 )   &    |-  ( ph  ->  ( N `  S )  =  ( N `  T ) )   =>    |-  ( ph  ->  S  ~~  T )
 
1-May-2017acsinfdimd 14279 In an algebraic closure system, if two independent sets have equal closure and one is infinite, then they are equinumerous. This is proven by using acsdomd 14278 twice with acsinfd 14277. See Section II.5 in [Cohn] p. 81 to 82. (Contributed by David Moews, 1-May-2017.)
 |-  ( ph  ->  A  e.  (ACS `  X )
 )   &    |-  N  =  (mrCls `  A )   &    |-  I  =  (mrInd `  A )   &    |-  ( ph  ->  S  e.  I )   &    |-  ( ph  ->  T  e.  I
 )   &    |-  ( ph  ->  ( N `  S )  =  ( N `  T ) )   &    |-  ( ph  ->  -.  S  e.  Fin )   =>    |-  ( ph  ->  S  ~~  T )
 
1-May-2017acsdomd 14278 In an algebraic closure system, if 
S and  T have the same closure and  S is infinite independent, then  T dominates  S. This follows from applying acsinfd 14277 and then applying unirnfdomd 8184 to the map given in acsmap2d 14276. See Section II.5 in [Cohn] p. 81 to 82. (Contributed by David Moews, 1-May-2017.)
 |-  ( ph  ->  A  e.  (ACS `  X )
 )   &    |-  N  =  (mrCls `  A )   &    |-  I  =  (mrInd `  A )   &    |-  ( ph  ->  S  e.  I )   &    |-  ( ph  ->  T  C_  X )   &    |-  ( ph  ->  ( N `  S )  =  ( N `  T ) )   &    |-  ( ph  ->  -.  S  e.  Fin )   =>    |-  ( ph  ->  S  ~<_  T )
 
1-May-2017acsinfd 14277 In an algebraic closure system, if 
S and  T have the same closure and  S is infinite independent, then  T is infinite. This follows from applying unirnffid 7142 to the map given in acsmap2d 14276. See Section II.5 in [Cohn] p. 81 to 82. (Contributed by David Moews, 1-May-2017.)
 |-  ( ph  ->  A  e.  (ACS `  X )
 )   &    |-  N  =  (mrCls `  A )   &    |-  I  =  (mrInd `  A )   &    |-  ( ph  ->  S  e.  I )   &    |-  ( ph  ->  T  C_  X )   &    |-  ( ph  ->  ( N `  S )  =  ( N `  T ) )   &    |-  ( ph  ->  -.  S  e.  Fin )   =>    |-  ( ph  ->  -.  T  e.  Fin )
 
1-May-2017acsmap2d 14276 In an algebraic closure system, if 
S and  T have the same closure and  S is independent, then there is a map  f from  T into the set of finite subsets of  S such that  S equals the union of  ran  f. This is proven by taking the map  f from acsmapd 14275 and observing that, since  S and  T have the same closure, the closure of  U. ran  f must contain  S. Since  S is independent, by mrissmrcd 13536,  U. ran  f must equal  S. See Section II.5 in [Cohn] p. 81 to 82. (Contributed by David Moews, 1-May-2017.)
 |-  ( ph  ->  A  e.  (ACS `  X )
 )   &    |-  N  =  (mrCls `  A )   &    |-  I  =  (mrInd `  A )   &    |-  ( ph  ->  S  e.  I )   &    |-  ( ph  ->  T  C_  X )   &    |-  ( ph  ->  ( N `  S )  =  ( N `  T ) )   =>    |-  ( ph  ->  E. f
 ( f : T --> ( ~P S  i^i  Fin )  /\  S  =  U. ran  f ) )
 
1-May-2017acsmapd 14275 In an algebraic closure system, if 
T is contained in the closure of  S, there is a map  f from  T into the set of finite subsets of  S such that the closure of  U. ran  f contains  T. This is proven by applying acsficl2d 14273 to each element of  T. See Section II.5 in [Cohn] p. 81 to 82. (Contributed by David Moews, 1-May-2017.)
 |-  ( ph  ->  A  e.  (ACS `  X )
 )   &    |-  N  =  (mrCls `  A )   &    |-  ( ph  ->  S 
 C_  X )   &    |-  ( ph  ->  T  C_  ( N `  S ) )   =>    |-  ( ph  ->  E. f
 ( f : T --> ( ~P S  i^i  Fin )  /\  T  C_  ( N `  U. ran  f
 ) ) )
 
1-May-2017acsfiindd 14274 In an algebraic closure system, a set is independent if and only if all its finite subsets are independent. Part of Proposition 4.1.3 in [FaureFrolicher] p. 83. (Contributed by David Moews, 1-May-2017.)
 |-  ( ph  ->  A  e.  (ACS `  X )
 )   &    |-  N  =  (mrCls `  A )   &    |-  I  =  (mrInd `  A )   &    |-  ( ph  ->  S 
 C_  X )   =>    |-  ( ph  ->  ( S  e.  I  <->  ( ~P S  i^i  Fin )  C_  I
 ) )
 
1-May-2017acsficl2d 14273 In an algebraic closure system, an element is in the closure of a set if and only if it is in the closure of a finite subset. Alternate form of acsficl 14268. Deduction form. (Contributed by David Moews, 1-May-2017.)
 |-  ( ph  ->  A  e.  (ACS `  X )
 )   &    |-  N  =  (mrCls `  A )   &    |-  ( ph  ->  S 
 C_  X )   =>    |-  ( ph  ->  ( Y  e.  ( N `
  S )  <->  E. x  e.  ( ~P S  i^i  Fin ) Y  e.  ( N `  x ) ) )
 
1-May-2017acsficld 14272 In an algebraic closure system, the closure of a set is the union of the closures of its finite subsets. Deduction form of acsficl 14268. (Contributed by David Moews, 1-May-2017.)
 |-  ( ph  ->  A  e.  (ACS `  X )
 )   &    |-  N  =  (mrCls `  A )   &    |-  ( ph  ->  S 
 C_  X )   =>    |-  ( ph  ->  ( N `  S )  =  U. ( N
 " ( ~P S  i^i  Fin ) ) )
 
1-May-2017acsmred 13552 An algebraic closure system is also a Moore system. Deduction form of acsmre 13548. (Contributed by David Moews, 1-May-2017.)
 |-  ( ph  ->  A  e.  (ACS `  X )
 )   =>    |-  ( ph  ->  A  e.  (Moore `  X )
 )
 
1-May-2017mreexfidimd 13546 In a Moore system whose closure operator has the exchange property, if two independent sets have equal closure and one is finite, then they are equinumerous. Proven by using mreexdomd 13545 twice. This implies a special case of Theorem 4.2.2 in [FaureFrolicher] p. 87. (Contributed by David Moews, 1-May-2017.)
 |-  ( ph  ->  A  e.  (Moore `  X )
 )   &    |-  N  =  (mrCls `  A )   &    |-  I  =  (mrInd `  A )   &    |-  ( ph  ->  A. s  e.  ~P  X A. y  e.  X  A. z  e.  ( ( N `  ( s  u.  { y }
 ) )  \  ( N `  s ) ) y  e.  ( N `
  ( s  u. 
 { z } )
 ) )   &    |-  ( ph  ->  S  e.  I )   &    |-  ( ph  ->  T  e.  I
 )   &    |-  ( ph  ->  S  e.  Fin )   &    |-  ( ph  ->  ( N `  S )  =  ( N `  T ) )   =>    |-  ( ph  ->  S 
 ~~  T )
 
1-May-2017mreexdomd 13545 In a Moore system whose closure operator has the exchange property, if  S is independent and contained in the closure of  T, and either  S or  T is finite, then  T dominates  S. This is an immediate consequence of mreexexd 13544. (Contributed by David Moews, 1-May-2017.)
 |-  ( ph  ->  A  e.  (Moore `  X )
 )   &    |-  N  =  (mrCls `  A )   &    |-  I  =  (mrInd `  A )   &    |-  ( ph  ->  A. s  e.  ~P  X A. y  e.  X  A. z  e.  ( ( N `  ( s  u.  { y }
 ) )  \  ( N `  s ) ) y  e.  ( N `
  ( s  u. 
 { z } )
 ) )   &    |-  ( ph  ->  S 
 C_  ( N `  T ) )   &    |-  ( ph  ->  T  C_  X )   &    |-  ( ph  ->  ( S  e.  Fin  \/  T  e.  Fin ) )   &    |-  ( ph  ->  S  e.  I
 )   =>    |-  ( ph  ->  S  ~<_  T )
 
1-May-2017mreexexd 13544 Exchange-type theorem. In a Moore system whose closure operator has the exchange property, if  F and  G are disjoint from  H,  ( F  u.  H ) is independent,  F is contained in the closure of  ( G  u.  H ), and either  F or  G is finite, then there is a subset  q of  G equinumerous to  F such that  ( q  u.  H ) is independent. This implies the case of Proposition 4.2.1 in [FaureFrolicher] p. 86 where either  ( A  \  B ) or  ( B  \  A ) is finite. The theorem is proven by induction using mreexexlem3d 13542 for the base case and mreexexlem4d 13543 for the induction step. (Contributed by David Moews, 1-May-2017.)
 |-  ( ph  ->  A  e.  (Moore `  X )
 )   &    |-  N  =  (mrCls `  A )   &    |-  I  =  (mrInd `  A )   &    |-  ( ph  ->  A. s  e.  ~P  X A. y  e.  X  A. z  e.  ( ( N `  ( s  u.  { y }
 ) )  \  ( N `  s ) ) y  e.  ( N `
  ( s  u. 
 { z } )
 ) )   &    |-  ( ph  ->  F 
 C_  ( X  \  H ) )   &    |-  ( ph  ->  G  C_  ( X  \  H ) )   &    |-  ( ph  ->  F  C_  ( N `  ( G  u.  H ) ) )   &    |-  ( ph  ->  ( F  u.  H )  e.  I
 )   &    |-  ( ph  ->  ( F  e.  Fin  \/  G  e.  Fin ) )   =>    |-  ( ph  ->  E. q  e.  ~P  G ( F  ~~  q  /\  ( q  u.  H )  e.  I )
 )
 
1-May-2017mreexexlem4d 13543 Induction step of the induction in mreexexd 13544. (Contributed by David Moews, 1-May-2017.)
 |-  ( ph  ->  A  e.  (Moore `  X )
 )   &    |-  N  =  (mrCls `  A )   &    |-  I  =  (mrInd `  A )   &    |-  ( ph  ->  A. s  e.  ~P  X A. y  e.  X  A. z  e.  ( ( N `  ( s  u.  { y }
 ) )  \  ( N `  s ) ) y  e.  ( N `
  ( s  u. 
 { z } )
 ) )   &    |-  ( ph  ->  F 
 C_  ( X  \  H ) )   &    |-  ( ph  ->  G  C_  ( X  \  H ) )   &    |-  ( ph  ->  F  C_  ( N `  ( G  u.  H ) ) )   &    |-  ( ph  ->  ( F  u.  H )  e.  I
 )   &    |-  ( ph  ->  L  e.  om )   &