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 (Unicode, GIF) or 1000 (Unicode, GIF) 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 8337091, also available here: set.mm (30MB) or set.mm.bz2 (compressed, 8MB).

The original proofs of theorems with recently shortened proofs can often be found by appending "OLD" to the theorem name, for example 19.43OLD for 19.43.

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

Recent news items    (11-Nov-2017) Alan Sare updated his completeusersproof program.

(3-Oct-2017) Sean B. Palmer created a web page that runs the metamath program under emulated Linux in JavaScript.

(3-Oct-2017) Sean B. Palmer wrote some programs to work with our shortest known proofs of the PM propositional calculus theorems.

(28-Sep-2017) Ivan Kuckir wrote a tutorial blog entry, Introduction to Metamath, that summarizes the language syntax. (It may have been written some time ago, but I was not aware of it before.)

(26-Sep-2017) The default directory for the Metamath Proof Explorer (MPE) has been changed from the GIF version (mpegif) to the Unicode version (mpeuni) throughout the site. Please let me know if you find broken links or other issues.

(24-Sep-2017) Saveliy Skresanov added a new proof to the 100 theorem list, Ceva's Theorem cevath, bringing the Metamath total to 67.

(3-Sep-2017) Brendan Leahy added a new proof to the 100 theorem list, Area of a Circle areacirc, bringing the Metamath total to 66.

(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.

(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.    Older news...

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

Last updated on 8-Dec-2017 at 10:35 AM ET.
Recent Additions to the Metamath Proof Explorer   Notes (last updated 14-May-2017 )
DateLabelDescription
Theorem
 
7-Dec-2017fprodf1o 24172 Re-index a finite product using a bijection. (Contributed by Scott Fenton, 7-Dec-2017.)
 |-  (
 k  =  G  ->  B  =  D )   &    |-  ( ph  ->  C  e.  Fin )   &    |-  ( ph  ->  F : C -1-1-onto-> A )   &    |-  ( ( ph  /\  n  e.  C ) 
 ->  ( F `  n )  =  G )   &    |-  (
 ( ph  /\  k  e.  A )  ->  B  e.  CC )   =>    |-  ( ph  -> k  e.  A B  = n  e.  C D )
 
7-Dec-2017prodfc 24171 A lemma to facilitate conversions from the function form to the class-variable form of a product. (Contributed by Scott Fenton, 7-Dec-2017.)
 |- j  e.  A ( ( k  e.  A  |->  B ) `
  j )  =
 k  e.  A B
 
7-Dec-2017prod2id 24170 The second class argument to a product can be chosen so that it is always a set. (Contributed by Scott Fenton, 7-Dec-2017.)
 |- k  e.  A B  = k  e.  A (  _I  `  B )
 
7-Dec-2017prod1 24169 Any product of one over a valid set is one. (Contributed by Scott Fenton, 7-Dec-2017.)
 |-  (
 ( A  C_  ( ZZ>=
 `  M )  \/  A  e.  Fin )  ->
 k  e.  A 1  =  1 )
 
6-Dec-2017fprod 24164 The value of a product over a nonempty finite set. (Contributed by Scott Fenton, 6-Dec-2017.)
 |-  (
 k  =  ( F `
  n )  ->  B  =  C )   &    |-  ( ph  ->  M  e.  NN )   &    |-  ( ph  ->  F : ( 1 ...
 M ) -1-1-onto-> A )   &    |-  ( ( ph  /\  k  e.  A ) 
 ->  B  e.  CC )   &    |-  (
 ( ph  /\  n  e.  ( 1 ... M ) )  ->  ( G `
  n )  =  C )   =>    |-  ( ph  -> k  e.  A B  =  ( 
 seq  1 (  x. 
 ,  G ) `  M ) )
 
6-Dec-2017iprodn0 24163 Non-zero series product with an upper integer index set (i.e. an infinite product.) (Contributed by Scott Fenton, 6-Dec-2017.)
 |-  Z  =  ( ZZ>= `  M )   &    |-  ( ph  ->  M  e.  ZZ )   &    |-  ( ph  ->  X  =/=  0 )   &    |-  ( ph  ->  seq 
 M (  x.  ,  F )  ~~>  X )   &    |-  (
 ( ph  /\  k  e.  Z )  ->  ( F `  k )  =  B )   &    |-  ( ( ph  /\  k  e.  Z ) 
 ->  B  e.  CC )   =>    |-  ( ph  -> k  e.  Z B  =  X )
 
6-Dec-2017zprodn0 24162 Non-zero series product with index set a subset of the upper integers. (Contributed by Scott Fenton, 6-Dec-2017.)
 |-  Z  =  ( ZZ>= `  M )   &    |-  ( ph  ->  M  e.  ZZ )   &    |-  ( ph  ->  X  =/=  0 )   &    |-  ( ph  ->  seq 
 M (  x.  ,  F )  ~~>  X )   &    |-  ( ph  ->  A  C_  Z )   &    |-  ( ( ph  /\  k  e.  Z )  ->  ( F `  k )  =  if ( k  e.  A ,  B , 
 1 ) )   &    |-  (
 ( ph  /\  k  e.  A )  ->  B  e.  CC )   =>    |-  ( ph  -> k  e.  A B  =  X )
 
5-Dec-2017cprod0 24168 A product over the empty set is one. (Contributed by Scott Fenton, 5-Dec-2017.)
 |- k  e.  (/) A  =  1
 
5-Dec-2017prodfclim1 24167 The constant one product converges to one. (Contributed by Scott Fenton, 5-Dec-2017.)
 |-  Z  =  ( ZZ>= `  M )   =>    |-  ( M  e.  ZZ  ->  seq 
 M (  x.  ,  ( Z  X.  { 1 } ) )  ~~>  1 )
 
5-Dec-2017prodf1f 24166 A one-valued infinite product is equal to the constant one function. (Contributed by Scott Fenton, 5-Dec-2017.)
 |-  Z  =  ( ZZ>= `  M )   =>    |-  ( M  e.  ZZ  ->  seq 
 M (  x.  ,  ( Z  X.  { 1 } ) )  =  ( Z  X.  {
 1 } ) )
 
5-Dec-2017prodf1 24165 The value of the partial products in a one-valued infinite product. (Contributed by Scott Fenton, 5-Dec-2017.)
 |-  Z  =  ( ZZ>= `  M )   =>    |-  ( N  e.  Z  ->  ( 
 seq  M (  x.  ,  ( Z  X.  { 1 } ) ) `  N )  =  1
 )
 
5-Dec-2017iprod 24161 Series product with an upper integer index set (i.e. an infinite product.) (Contributed by Scott Fenton, 5-Dec-2017.)
 |-  Z  =  ( ZZ>= `  M )   &    |-  ( ph  ->  M  e.  ZZ )   &    |-  ( ph  ->  E. n  e.  Z  E. y ( y  =/=  0  /\  seq 
 n (  x.  ,  F )  ~~>  y ) )   &    |-  ( ( ph  /\  k  e.  Z )  ->  ( F `  k )  =  B )   &    |-  ( ( ph  /\  k  e.  Z ) 
 ->  B  e.  CC )   =>    |-  ( ph  -> k  e.  Z B  =  (  ~~>  `  seq  M (  x.  ,  F ) ) )
 
5-Dec-2017zprod 24160 Series product with index set a subset of the upper integers. (Contributed by Scott Fenton, 5-Dec-2017.)
 |-  Z  =  ( ZZ>= `  M )   &    |-  ( ph  ->  M  e.  ZZ )   &    |-  ( ph  ->  E. n  e.  Z  E. y ( y  =/=  0  /\  seq 
 n (  x.  ,  F )  ~~>  y ) )   &    |-  ( ph  ->  A  C_  Z )   &    |-  ( ( ph  /\  k  e.  Z )  ->  ( F `  k )  =  if ( k  e.  A ,  B , 
 1 ) )   &    |-  (
 ( ph  /\  k  e.  A )  ->  B  e.  CC )   =>    |-  ( ph  -> k  e.  A B  =  (  ~~>  ` 
 seq  M (  x.  ,  F ) ) )
 
4-Dec-2017funpartlem 24552 Lemma for funpartfun 24553. Show membership in the restriction. (Contributed by Scott Fenton, 4-Dec-2017.)
 |-  ( A  e.  dom  ( (Image
 F  o. Singleton )  i^i  ( _V  X.  Singletons ) )  <->  E. x ( F
 " { A }
 )  =  { x } )
 
4-Dec-2017prodmo 24159 A product has at most one limit. (Contributed by Scott Fenton, 4-Dec-2017.)
 |-  F  =  ( k  e.  ZZ  |->  if ( k  e.  A ,  B ,  1 ) )   &    |-  ( ( ph  /\  k  e.  A ) 
 ->  B  e.  CC )   &    |-  G  =  ( j  e.  NN  |->  [_ ( f `  j
 )  /  k ]_ B )   =>    |-  ( ph  ->  E* x ( E. m  e.  ZZ  ( A  C_  ( ZZ>= `  m )  /\  E. n  e.  ( ZZ>= `  m ) E. y ( y  =/=  0  /\  seq  n (  x.  ,  F )  ~~>  y )  /\  seq  m (  x.  ,  F )  ~~>  x )  \/  E. m  e.  NN  E. f ( f : ( 1
 ... m ) -1-1-onto-> A  /\  x  =  (  seq  1 (  x.  ,  G ) `  m ) ) ) )
 
4-Dec-2017prodmolem2 24158 Lemma for prodmo 24159. (Contributed by Scott Fenton, 4-Dec-2017.)
 |-  F  =  ( k  e.  ZZ  |->  if ( k  e.  A ,  B ,  1 ) )   &    |-  ( ( ph  /\  k  e.  A ) 
 ->  B  e.  CC )   &    |-  G  =  ( j  e.  NN  |->  [_ ( f `  j
 )  /  k ]_ B )   =>    |-  ( ( ph  /\  E. m  e.  ZZ  ( A  C_  ( ZZ>= `  m )  /\  E. n  e.  ( ZZ>= `  m ) E. y ( y  =/=  0  /\  seq  n (  x.  ,  F )  ~~>  y )  /\  seq  m (  x.  ,  F )  ~~>  x ) )  ->  ( E. m  e.  NN  E. f ( f : ( 1 ... m )
 -1-1-onto-> A  /\  z  =  ( 
 seq  1 (  x. 
 ,  G ) `  m ) )  ->  x  =  z )
 )
 
4-Dec-2017prodmolem2a 24157 Lemma for prodmo 24159. (Contributed by Scott Fenton, 4-Dec-2017.)
 |-  F  =  ( k  e.  ZZ  |->  if ( k  e.  A ,  B ,  1 ) )   &    |-  ( ( ph  /\  k  e.  A ) 
 ->  B  e.  CC )   &    |-  G  =  ( j  e.  NN  |->  [_ ( f `  j
 )  /  k ]_ B )   &    |-  H  =  ( j  e.  NN  |->  [_ ( K `  j ) 
 /  k ]_ B )   &    |-  ( ph  ->  N  e.  NN )   &    |-  ( ph  ->  M  e.  ZZ )   &    |-  ( ph  ->  A  C_  ( ZZ>=
 `  M ) )   &    |-  ( ph  ->  f :
 ( 1 ... N )
 -1-1-onto-> A )   &    |-  ( ph  ->  K 
 Isom  <  ,  <  (
 ( 1 ... ( # `
  A ) ) ,  A ) )   =>    |-  ( ph  ->  seq  M (  x.  ,  F )  ~~>  (  seq  1 (  x. 
 ,  G ) `  N ) )
 
4-Dec-2017prodmolem3 24156 Lemma for prodmo 24159. (Contributed by Scott Fenton, 4-Dec-2017.)
 |-  F  =  ( k  e.  ZZ  |->  if ( k  e.  A ,  B ,  1 ) )   &    |-  ( ( ph  /\  k  e.  A ) 
 ->  B  e.  CC )   &    |-  G  =  ( j  e.  NN  |->  [_ ( f `  j
 )  /  k ]_ B )   &    |-  H  =  ( j  e.  NN  |->  [_ ( K `  j ) 
 /  k ]_ B )   &    |-  ( ph  ->  ( M  e.  NN  /\  N  e.  NN ) )   &    |-  ( ph  ->  f : ( 1 ... M ) -1-1-onto-> A )   &    |-  ( ph  ->  K : ( 1 ...
 N ) -1-1-onto-> A )   =>    |-  ( ph  ->  (  seq  1 (  x.  ,  G ) `  M )  =  (  seq  1 (  x.  ,  H ) `  N ) )
 
4-Dec-2017prodrb 24155 Rebase the starting point of a product. (Contributed by Scott Fenton, 4-Dec-2017.)
 |-  F  =  ( k  e.  ZZ  |->  if ( k  e.  A ,  B ,  1 ) )   &    |-  ( ( ph  /\  k  e.  A ) 
 ->  B  e.  CC )   &    |-  ( ph  ->  M  e.  ZZ )   &    |-  ( ph  ->  N  e.  ZZ )   &    |-  ( ph  ->  A 
 C_  ( ZZ>= `  M ) )   &    |-  ( ph  ->  A 
 C_  ( ZZ>= `  N ) )   =>    |-  ( ph  ->  (  seq  M (  x.  ,  F )  ~~>  C  <->  seq  N (  x. 
 ,  F )  ~~>  C )
 )
 
4-Dec-2017prodrblem2 24154 Lemma for prodrb 24155. (Contributed by Scott Fenton, 4-Dec-2017.)
 |-  F  =  ( k  e.  ZZ  |->  if ( k  e.  A ,  B ,  1 ) )   &    |-  ( ( ph  /\  k  e.  A ) 
 ->  B  e.  CC )   &    |-  ( ph  ->  M  e.  ZZ )   &    |-  ( ph  ->  N  e.  ZZ )   &    |-  ( ph  ->  A 
 C_  ( ZZ>= `  M ) )   &    |-  ( ph  ->  A 
 C_  ( ZZ>= `  N ) )   =>    |-  ( ( ph  /\  N  e.  ( ZZ>= `  M )
 )  ->  (  seq  M (  x.  ,  F ) 
 ~~>  C  <->  seq  N (  x. 
 ,  F )  ~~>  C )
 )
 
4-Dec-2017fprodcvg 24153 The sequence of partial products of a finite product converges to the whole product. (Contributed by Scott Fenton, 4-Dec-2017.)
 |-  F  =  ( k  e.  ZZ  |->  if ( k  e.  A ,  B ,  1 ) )   &    |-  ( ( ph  /\  k  e.  A ) 
 ->  B  e.  CC )   &    |-  ( ph  ->  N  e.  ( ZZ>=
 `  M ) )   &    |-  ( ph  ->  A  C_  ( M ... N ) )   =>    |-  ( ph  ->  seq  M (  x.  ,  F )  ~~>  (  seq  M (  x. 
 ,  F ) `  N ) )
 
4-Dec-2017prodrblem 24152 Lemma for prodrb 24155. (Contributed by Scott Fenton, 4-Dec-2017.)
 |-  F  =  ( k  e.  ZZ  |->  if ( k  e.  A ,  B ,  1 ) )   &    |-  ( ( ph  /\  k  e.  A ) 
 ->  B  e.  CC )   &    |-  ( ph  ->  N  e.  ( ZZ>=
 `  M ) )   =>    |-  ( ( ph  /\  A  C_  ( ZZ>= `  N )
 )  ->  (  seq  M (  x.  ,  F )  |`  ( ZZ>= `  N ) )  =  seq  N (  x.  ,  F ) )
 
4-Dec-2017prodf 24151 An infinite product of complex terms is a function from an upper set of integers to  CC. (Contributed by Scott Fenton, 4-Dec-2017.)
 |-  Z  =  ( ZZ>= `  M )   &    |-  ( ph  ->  M  e.  ZZ )   &    |-  ( ( ph  /\  k  e.  Z )  ->  ( F `  k )  e. 
 CC )   =>    |-  ( ph  ->  seq  M (  x.  ,  F ) : Z --> CC )
 
4-Dec-2017cprod2id 24150 The second class argument to a sum can be chosen so that it is always a set. (Contributed by Scott Fenton, 4-Dec-2017.)
 |- k  e.  A B  = k  e.  A (  _I  `  B )
 
4-Dec-2017cprodeq12rdv 24149 Equality deduction for sum. (Contributed by Scott Fenton, 4-Dec-2017.)
 |-  ( ph  ->  A  =  B )   &    |-  ( ( ph  /\  k  e.  B )  ->  C  =  D )   =>    |-  ( ph  -> k  e.  A C  = k  e.  B D )
 
4-Dec-2017cprodeq12dv 24148 Equality deduction for sum. (Contributed by Scott Fenton, 4-Dec-2017.)
 |-  ( ph  ->  A  =  B )   &    |-  ( ( ph  /\  k  e.  A )  ->  C  =  D )   =>    |-  ( ph  -> k  e.  A C  = k  e.  B D )
 
4-Dec-20172cprodeq2dv 24147 Equality deduction for double sum. (Contributed by Scott Fenton, 4-Dec-2017.)
 |-  (
 ( ph  /\  j  e.  A  /\  k  e.  B )  ->  C  =  D )   =>    |-  ( ph  -> j  e.  A k  e.  B C  = j  e.  A k  e.  B D )
 
4-Dec-2017cprodeq2sdv 24146 Equality deduction for sum. (Contributed by Scott Fenton, 4-Dec-2017.)
 |-  ( ph  ->  B  =  C )   =>    |-  ( ph  -> k  e.  A B  = k  e.  A C )
 
4-Dec-2017cprodeq2dv 24145 Equality deduction for sum. (Contributed by Scott Fenton, 4-Dec-2017.)
 |-  (
 ( ph  /\  k  e.  A )  ->  B  =  C )   =>    |-  ( ph  -> k  e.  A B  = k  e.  A C )
 
4-Dec-2017cprodeq2d 24144 Equality deduction for sum. Note that unlike cprodeq2dv 24145, 
k may occur in  ph. (Contributed by Scott Fenton, 4-Dec-2017.)
 |-  ( ph  ->  A. k  e.  A  B  =  C )   =>    |-  ( ph  -> k  e.  A B  = k  e.  A C )
 
4-Dec-2017cprodeq1d 24143 Equality deduction for sum. (Contributed by Scott Fenton, 4-Dec-2017.)
 |-  ( ph  ->  A  =  B )   =>    |-  ( ph  -> k  e.  A C  = k  e.  B C )
 
4-Dec-2017cprodeq12i 24142 Equality inference for sum. (Contributed by Scott Fenton, 4-Dec-2017.)
 |-  A  =  B   &    |-  ( k  e.  A  ->  C  =  D )   =>    |- k  e.  A C  = k  e.  B D
 
4-Dec-2017cprodeq2i 24141 Equality inference for sum. (Contributed by Scott Fenton, 4-Dec-2017.)
 |-  (
 k  e.  A  ->  B  =  C )   =>    |- k  e.  A B  = k  e.  A C
 
4-Dec-2017cprodeq1i 24140 Equality inference for product. (Contributed by Scott Fenton, 4-Dec-2017.)
 |-  A  =  B   =>    |- k  e.  A C  = k  e.  B C
 
4-Dec-2017cbvcprodi 24139 Change bound variable in a product. (Contributed by Scott Fenton, 4-Dec-2017.)
 |-  F/_ k B   &    |-  F/_ j C   &    |-  ( j  =  k  ->  B  =  C )   =>    |- j  e.  A B  = k  e.  A C
 
4-Dec-2017cbvcprodv 24138 Change bound variable in a product. (Contributed by Scott Fenton, 4-Dec-2017.)
 |-  (
 j  =  k  ->  B  =  C )   =>    |- j  e.  A B  = k  e.  A C
 
4-Dec-2017cbvcprod 24137 Change bound variable in a product. (Contributed by Scott Fenton, 4-Dec-2017.)
 |-  (
 j  =  k  ->  B  =  C )   &    |-  F/_ k A   &    |-  F/_ j A   &    |-  F/_ k B   &    |-  F/_ j C   =>    |- j  e.  A B  = k  e.  A C
 
4-Dec-2017cprodeq2 24136 Equality theorem for product. (Contributed by Scott Fenton, 4-Dec-2017.)
 |-  ( A. k  e.  A  B  =  C  -> k  e.  A B  = k  e.  A C )
 
4-Dec-2017cprodeq2ii 24135 Equality theorem for product, with the class expressions  B and  C guarded by  _I to be always sets. (Contributed by Scott Fenton, 4-Dec-2017.)
 |-  ( A. k  e.  A  (  _I  `  B )  =  (  _I  `  C )  -> k  e.  A B  = k  e.  A C )
 
4-Dec-2017cprodeq2w 24134 Equality theorem for product, when the class expressions  B and  C are equal everywhere. Proved using only Extensionality. (Contributed by Scott Fenton, 4-Dec-2017.)
 |-  ( A. k  B  =  C  -> k  e.  A B  = k  e.  A C )
 
4-Dec-2017nfcprod1 24132 Bound-variable hypothesis builder for product. (Contributed by Scott Fenton, 4-Dec-2017.)
 |-  F/_ k A   =>    |-  F/_ k k  e.  A B
 
4-Dec-2017cprodex 24129 A product is a set. (Contributed by Scott Fenton, 4-Dec-2017.)
 |- k  e.  A B  e.  _V
 
4-Dec-2017df-cprod 24128 Define the product of a series with an index set of integers  A. This definition takes most of the aspects of df-sum 12175 and adapts them for multiplication instead of addition. However, we insist that in the infinite case, there is a non-zero tail of the sequence. This ensures that the convergence criteria match those of infinite sums. (Contributed by Scott Fenton, 4-Dec-2017.)
 |- k  e.  A B  =  (
 iota x ( E. m  e.  ZZ  ( A  C_  ( ZZ>= `  m )  /\  E. n  e.  ( ZZ>=
 `  m ) E. y ( y  =/=  0  /\  seq  n (  x.  ,  ( k  e.  ZZ  |->  if (
 k  e.  A ,  B ,  1 )
 ) )  ~~>  y )  /\  seq  m (  x. 
 ,  ( k  e. 
 ZZ  |->  if ( k  e.  A ,  B , 
 1 ) ) )  ~~>  x )  \/  E. m  e.  NN  E. f ( f : ( 1
 ... m ) -1-1-onto-> A  /\  x  =  (  seq  1 (  x.  ,  ( n  e.  NN  |->  [_ (
 f `  n )  /  k ]_ B ) ) `  m ) ) ) )
 
4-Dec-2017spvw 1655 Version of sp 1728 when  x does not occur in  ph. This provides the other direction of ax-17 1606. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 10-Apr-2017.) (Proof shortened by Wolf Lammen, 4-Dec-2017.)
 |-  ( A. x ph  -> 
 ph )
 
4-Dec-201719.3v 1654 Special case of Theorem 19.3 of [Margaris] p. 89. (Contributed by NM, 1-Aug-2017.) (Revised by Wolf Lammen to remove dependency on ax-8, 4-Dec-2017.)
 |-  ( A. x ph  <->  ph )
 
4-Dec-201719.9v 1653 Special case of Theorem 19.9 of [Margaris] p. 89. (Contributed by NM, 28-May-1995.) (Revised by NM, 1-Aug-2017.) (Revised by Wolf Lammen to remove dependency on ax-8, 4-Dec-2017.)
 |-  ( E. x ph  <->  ph )
 
4-Dec-201719.8w 1649 Weak version of 19.8a 1730. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 1-Aug-2017.) (Proof shortened by Wolf Lammen, 4-Dec-2017.)
 |-  ( ph  ->  A. x ph )   =>    |-  ( ph  ->  E. x ph )
 
4-Dec-201719.2 1648 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 1792 for a more conventional proof. (Contributed by NM, 2-Aug-2017.) (Revised by Wolf Lammen to remove dependency on ax-8, 4-Dec-2017.)
 |-  ( A. x ph  ->  E. x ph )
 
4-Dec-2017exlimdv 1626 Deduction from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 27-Apr-1994.) (Revised by Wolf Lammen to remove dependency on ax-9 and ax-8, 4-Dec-2017.)
 |-  ( ph  ->  ( ps  ->  ch ) )   =>    |-  ( ph  ->  ( E. x ps  ->  ch ) )
 
4-Dec-2017exlimiv 1624 Inference from Theorem 19.23 of [Margaris] p. 90.

This inference, along with our many variants such as rexlimdv 2679, is used to implement a metatheorem called "Rule C" that is given in many logic textbooks. See, for example, Rule C in [Mendelson] p. 81, Rule C in [Margaris] p. 40, or Rule C in Hirst and Hirst's A Primer for Logic and Proof p. 59 (PDF p. 65) at http://www.mathsci.appstate.edu/~hirstjl/primer/hirst.pdf.

In informal proofs, the statement "Let  C be an element such that..." almost always means an implicit application of Rule C.

In essence, Rule C states that if we can prove that some element  x exists satisfying a wff, i.e.  E. x ph ( x ) where  ph ( x ) has  x free, then we can use  ph ( C ) as a hypothesis for the proof where  C is a new (ficticious) constant not appearing previously in the proof, nor in any axioms used, nor in the theorem to be proved. The purpose of Rule C is to get rid of the existential quantifier.

We cannot do this in Metamath directly. Instead, we use the original  ph (containing  x) as an antecedent for the main part of the proof. We eventually arrive at  ( ph  ->  ps ) where  ps is the theorem to be proved and does not contain  x. Then we apply exlimiv 1624 to arrive at  ( E. x ph  ->  ps ). Finally, we separately prove  E. x ph and detach it with modus ponens ax-mp 8 to arrive at the final theorem  ps. (Contributed by NM, 5-Aug-1993.) (Revised by Wolf Lammen to remove dependency on ax-9 and ax-8, 4-Dec-2017.)

 |-  ( ph  ->  ps )   =>    |-  ( E. x ph  ->  ps )
 
4-Dec-2017ax17e 1608 A rephrasing of ax-17 1606 using the existential quantifier. (Contributed by Wolf Lammen, 4-Dec-2017.)
 |-  ( E. x ph  -> 
 ph )
 
1-Dec-2017nfcprod 24133 Bound-variable hypothesis builder for product: if  x is (effectively) not free in  A and  B, it is not free in ∏ k  e.  A B. (Contributed by Scott Fenton, 1-Dec-2017.)
 |-  F/_ x A   &    |-  F/_ x B   =>    |-  F/_ x k  e.  A B
 
1-Dec-2017cprodeq1 24131 Equality theorem for a product. (Contributed by Scott Fenton, 1-Dec-2017.)
 |-  ( A  =  B  -> k  e.  A C  = k  e.  B C )
 
1-Dec-2017cprodeq1f 24130 Equality theorem for a product. (Contributed by Scott Fenton, 1-Dec-2017.)
 |-  F/_ k A   &    |-  F/_ k B   =>    |-  ( A  =  B  ->
 k  e.  A C  = k  e.  B C )
 
29-Nov-2017tz6.12-1-afv 28142 Function value (Theorem 6.12(1) of [TakeutiZaring] p. 27, analogous to tz6.12-1 5560. (Contributed by Alexander van der Vekens, 29-Nov-2017.)
 |-  (
 ( A F y 
 /\  E! y  A F y )  ->  ( F''' A )  =  y
 )
 
29-Nov-2017tz6.12-afv 28141 Function value. Theorem 6.12(1) of [TakeutiZaring] p. 27, analogous to tz6.12 5561. (Contributed by Alexander van der Vekens, 29-Nov-2017.)
 |-  (
 ( <. A ,  y >.  e.  F  /\  E! y <. A ,  y >.  e.  F )  ->  ( F''' A )  =  y )
 
29-Nov-2017afveu 28121 The value of a function at a unique point, analogous to fveu 5533. (Contributed by Alexander van der Vekens, 29-Nov-2017.)
 |-  ( E! x  A F x  ->  ( F''' A )  =  U. { x  |  A F x }
 )
 
29-Nov-2017eu2ndop1stv 28083 If there is a unique second component in an ordered pair contained in a given set, the first component must be a set. (Contributed by Alexander van der Vekens, 29-Nov-2017.)
 |-  ( E! y <. A ,  y >.  e.  V  ->  A  e.  _V )
 
29-Nov-2017faclimlem9 24125 Lemma for faclim 24126. Final inductive step. (Contributed by Scott Fenton, 29-Nov-2017.)
 |-  (
 ( M  e.  NN  /\  B  e.  NN0 )  ->  ( ( (  seq  1 (  x.  ,  ( n  e.  NN  |->  ( ( ( 1  +  (
 1  /  n )
 ) ^ B ) 
 /  ( 1  +  ( B  /  n ) ) ) ) ) `  M )  x.  ( ( B  +  1 )  x.  ( ( M  +  1 )  /  ( B  +  ( M  +  1 ) ) ) ) )  x.  ( ( ( 1  +  ( 1  /  ( M  +  1
 ) ) ) ^
 ( B  +  1 ) )  /  (
 1  +  ( ( B  +  1 ) 
 /  ( M  +  1 ) ) ) ) )  =  ( ( (  seq  1
 (  x.  ,  ( n  e.  NN  |->  ( ( ( 1  +  (
 1  /  n )
 ) ^ B ) 
 /  ( 1  +  ( B  /  n ) ) ) ) ) `  M )  x.  ( ( ( 1  +  ( 1 
 /  ( M  +  1 ) ) ) ^ B )  /  ( 1  +  ( B  /  ( M  +  1 ) ) ) ) )  x.  (
 ( B  +  1 )  x.  ( ( ( M  +  1 )  +  1 ) 
 /  ( B  +  ( ( M  +  1 )  +  1
 ) ) ) ) ) )
 
29-Nov-2017faclimlem8 24124 Lemma for faclim 24126. Base induction case. (Contributed by Scott Fenton, 29-Nov-2017.)
 |-  ( B  e.  NN0  ->  (
 ( ( 1  +  ( 1  /  1
 ) ) ^ ( B  +  1 )
 )  /  ( 1  +  ( ( B  +  1 )  /  1
 ) ) )  =  ( ( ( ( 1  +  ( 1 
 /  1 ) ) ^ B )  /  ( 1  +  ( B  /  1 ) ) )  x.  ( ( B  +  1 )  x.  ( ( 1  +  1 )  /  ( B  +  (
 1  +  1 ) ) ) ) ) )
 
28-Nov-2017alcomw9bAUX7 29631 Special case of alcom 1723 proved from ax-7v 29419. (Contributed by NM, 28-Nov-2017.)
 |-  ( A. x A. y ( x  =  y  /\  x  =  z )  <->  A. y A. x ( x  =  y  /\  x  =  z )
 )
 
28-Nov-2017ax7w9AUX7 29630 Special case of ax-7 1720 proved from ax-7v 29419. (Contributed by NM, 28-Nov-2017.)
 |-  ( A. x A. y ( x  =  y  /\  x  =  z )  ->  A. y A. x ( x  =  y  /\  x  =  z
 ) )
 
28-Nov-2017exsbNEW7 29571 An equivalent expression for existence. (Contributed by NM, 2-Feb-2005.) (Revised by NM, 28-Nov-2017.) Revised to prove from ax-7v 29419 instead of ax-7 1720.
 |-  ( E. x ph  <->  E. y A. x ( x  =  y  -> 
 ph ) )
 
28-Nov-2017alneu 28082 If a statement holds for all sets, there is not a unique set for which the statement holds. (Contributed by Alexander van der Vekens, 28-Nov-2017.)
 |-  ( A. x ph  ->  -.  E! x ph )
 
27-Nov-2017rlimdmafv 28145 Two ways to express that a function has a limit, analogous to rlimdm 12041. (Contributed by Alexander van der Vekens, 27-Nov-2017.)
 |-  ( ph  ->  F : A --> CC )   &    |-  ( ph  ->  sup ( A ,  RR* ,  <  )  =  +oo )   =>    |-  ( ph  ->  ( F  e.  dom  ~~> r  <->  F  ~~> r  (  ~~> r ''' F ) ) )
 
26-Nov-2017faclimlem7 24123 Lemma for faclim 24126. Sequence closure. (Contributed by Scott Fenton, 26-Nov-2017.)
 |-  (
 ( B  e.  NN0  /\  K  e.  NN )  ->  (  seq  1 (  x.  ,  ( n  e.  NN  |->  ( ( ( 1  +  (
 1  /  n )
 ) ^ B ) 
 /  ( 1  +  ( B  /  n ) ) ) ) ) `  K )  e.  CC )
 
26-Nov-2017faclimlem6 24122 Lemma for faclim 24126. Closure of the core expression. (Contributed by Scott Fenton, 26-Nov-2017.)
 |-  (
 ( B  e.  NN0  /\  N  e.  NN )  ->  ( ( ( 1  +  ( 1  /  N ) ) ^ B )  /  (
 1  +  ( B 
 /  N ) ) )  e.  CC )
 
26-Nov-2017faclimlem5 24121 Lemma for faclim 24126. A convergence statement in the induction. (Contributed by Scott Fenton, 26-Nov-2017.)
 |-  ( B  e.  NN0  ->  ( n  e.  NN  |->  ( ( B  +  1 )  x.  ( ( n  +  1 )  /  ( B  +  ( n  +  1 )
 ) ) ) )  ~~>  ( B  +  1
 ) )
 
26-Nov-2017faclimlem4 24120 Lemma for faclim 24126. Closure of a particular expression. (Contributed by Scott Fenton, 26-Nov-2017.)
 |-  (
 ( B  e.  NN0  /\  N  e.  NN )  ->  ( ( N  +  1 )  /  ( B  +  ( N  +  1 ) ) )  e.  CC )
 
26-Nov-2017faclimlem3 24119 Lemma for faclim 24126. Base case for induction. (Contributed by Scott Fenton, 26-Nov-2017.)
 |-  seq  1 (  x.  ,  ( n  e.  NN  |->  ( ( ( 1  +  (
 1  /  n )
 ) ^ 0 ) 
 /  ( 1  +  ( 0  /  n ) ) ) ) )  ~~>  1
 
26-Nov-2017faclimlem2 24118 Lemma for faclim 24126. Set up substitution rules. (Contributed by Scott Fenton, 26-Nov-2017.)
 |-  ( N  =  M  ->  ( ( ( 1  +  ( 1  /  N ) ) ^ A )  /  ( 1  +  ( A  /  N ) ) )  =  ( ( ( 1  +  ( 1  /  M ) ) ^ A )  /  (
 1  +  ( A 
 /  M ) ) ) )
 
26-Nov-2017faclimlem1 24117 Lemma for faclim 24126. Set up substitution rules. (Contributed by Scott Fenton, 26-Nov-2017.)
 |-  ( A  =  B  ->  ( ( ( 1  +  ( 1  /  N ) ) ^ A )  /  ( 1  +  ( A  /  N ) ) )  =  ( ( ( 1  +  ( 1  /  N ) ) ^ B )  /  (
 1  +  ( B 
 /  N ) ) ) )
 
25-Nov-2017nfsb4tw2AUXOLD7 29700 Weak version of nfsb4t 2033. Still uses ax-7OLD7 29632 via nfaldOLD7 29644. (Contributed by NM, 25-Nov-2017.)
 |-  ( A. x F/ z ph  ->  ( -.  A. z  z  =  y  ->  F/ z [ y  /  x ] ph ) )
 
25-Nov-2017a16nfNEW7 29525 If dtru 4217 is false, then there is only one element in the universe, so everything satisfies  F/. (Contributed by Mario Carneiro, 7-Oct-2016.) (Revised by NM, 25-Nov-2017.) Revised to prove from ax-7v 29419 instead of ax-7 1720.
 |-  ( A. x  x  =  y  ->  F/ z ph )
 
25-Nov-2017equveliNEW7 29503 A variable elimination law for equality with no distinct variable requirements. (Compare equviniNEW7 29502.) (Contributed by NM, 1-Mar-2013.) (Proof shortened by Mario Carneiro, 17-Oct-2016.) (Revised by NM, 25-Nov-2017.) Revised to prove from ax-7v 29419 instead of ax-7 1720.
 |-  ( A. z ( z  =  x  <->  z  =  y
 )  ->  x  =  y )
 
25-Nov-2017nfnaew3AUX7 29501 Weak version of nfnae 1909 not requiring ax-7 1720. (Contributed by NM, 25-Nov-2017.)
 |-  F/ z  -.  A. x  x  =  y
 
25-Nov-2017nfaew3AUX7 29500 Weak version of nfae 1907 not requiring ax-7 1720. (Contributed by NM, 25-Nov-2017.)
 |-  F/ z A. x  x  =  y
 
25-Nov-2017exdistrfNEW7 29482 Distribution of existential quantifiers, with a bound-variable hypothesis saying that  y is not free in  ph, but  x can be free in  ph (and there is no distinct variable condition on  x and  y). (Contributed by Mario Carneiro, 20-Mar-2013.) (Revised by NM, 25-Nov-2017.) Revised to prove from ax-7v 29419 instead of ax-7 1720.
 |-  ( -.  A. x  x  =  y  ->  F/ y ph )   =>    |-  ( E. x E. y ( ph  /\  ps )  ->  E. x ( ph  /\ 
 E. y ps )
 )
 
25-Nov-2017drnf2w3AUX7 29481 Weak version of drnf2 1923 not requiring ax-7 1720. (Contributed by NM, 25-Nov-2017.)
 |-  ( A. x  x  =  y  ->  ( ph  <->  ps ) )   =>    |-  ( A. x  x  =  y  ->  ( F/ x ph  <->  F/ x ps )
 )
 
25-Nov-2017drex2w3AUX7 29480 Weak version of drex2 1921 not requiring ax-7 1720. (Contributed by NM, 25-Nov-2017.)
 |-  ( A. x  x  =  y  ->  ( ph  <->  ps ) )   =>    |-  ( A. x  x  =  y  ->  ( E. x ph  <->  E. x ps )
 )
 
25-Nov-2017dral2w3AUX7 29479 Weak version of dral2 1919 not requiring ax-7 1720. (Contributed by NM, 25-Nov-2017.)
 |-  ( A. x  x  =  y  ->  ( ph  <->  ps ) )   =>    |-  ( A. x  x  =  y  ->  (
 A. x ph  <->  A. x ps )
 )
 
25-Nov-2017drnf2w2AUX7 29478 Weak version of drnf2 1923 not requiring ax-7 1720. (Contributed by NM, 25-Nov-2017.)
 |-  ( A. x  x  =  y  ->  ( ph  <->  ps ) )   =>    |-  ( A. x  x  =  y  ->  ( F/ z ph  <->  F/ z ps )
 )
 
25-Nov-2017drex2w2AUX7 29477 Weak version of drex2 1921 not requiring ax-7 1720. (Contributed by NM, 25-Nov-2017.)
 |-  ( A. x  x  =  y  ->  ( ph  <->  ps ) )   =>    |-  ( A. x  x  =  y  ->  ( E. z ph  <->  E. z ps )
 )
 
25-Nov-2017dral2w2AUX7 29476 Weak version of dral2 1919 not requiring ax-7 1720. (Contributed by NM, 25-Nov-2017.)
 |-  ( A. x  x  =  y  ->  ( ph  <->  ps ) )   =>    |-  ( A. x  x  =  y  ->  (
 A. z ph  <->  A. z ps )
 )
 
25-Nov-2017nfnaew2AUX7 29462 Weak version of nfnae 1909 not requiring ax-7 1720. (Contributed by NM, 25-Nov-2017.)
 |-  F/ z  -.  A. x  x  =  y
 
25-Nov-2017hbnaew2AUX7 29461 Weak version of hbnae 1908 not requiring ax-7 1720. (Contributed by NM, 25-Nov-2017.)
 |-  ( -.  A. x  x  =  y  ->  A. z  -.  A. x  x  =  y )
 
25-Nov-2017nfaew2AUX7 29460 Weak version of nfae 1907 not requiring ax-7 1720. (Contributed by NM, 25-Nov-2017.)
 |-  F/ z A. x  x  =  y
 
25-Nov-2017cbv3hvNEW7 29423 Lemma for ax10NEW7 29450. Similar to cbv3h 1936. Requires distinct variables but avoids ax-12 1878. (Contributed by NM, 25-Jul-2015.) (Revised by NM, 25-Nov-2017.) Revised to prove from ax-7v 29419 instead of ax-7 1720.
 |-  ( ph  ->  A. y ph )   &    |-  ( ps  ->  A. x ps )   &    |-  ( x  =  y  ->  (
 ph  ->  ps ) )   =>    |-  ( A. x ph 
 ->  A. y ps )
 
24-Nov-2017eupatrl 28385 An Eulerian path is a trail.

Unfortunately, the edge function  F of an Eulerian path has the domain  ( 1 ... ( # `  F
) ), whereas the edge functions of all kinds of walks defined here have the domain  ( 0..^ ( # `  F
) ) (i.e. the edge functions are "words of edge indices", see discussion and proposal of Mario Carneiro at https://groups.google.com/d/msg/metamath/KdVXdL3IH3k/2-BYcS_ACQAJ). Therefore, the arguments of the edge function of an Eulerian path must be shifted by 1 to obtain an edge function of a trail in this theorem, using the auxiliary theorems above (fargshiftlem 28379, fargshiftfv 28380, etc.). The definition of an Eulerian path and all related theorems should be modified as soon as the graph theory is integrated into the main part of set.mm. (Contributed by Alexander van der Vekens, 24-Nov-2017.)

 |-  G  =  ( x  e.  (
 0..^ ( # `  F ) )  |->  ( F `
  ( x  +  1 ) ) )   =>    |-  ( F ( V EulPaths  E ) P  ->  G ( V Trails  E ) P )
 
24-Nov-2017fargshiftfva 28384 The values of a shifted function correspond to the value of the original function. (Contributed by Alexander van der Vekens, 24-Nov-2017.)
 |-  G  =  ( x  e.  (
 0..^ ( # `  F ) )  |->  ( F `
  ( x  +  1 ) ) )   =>    |-  ( ( N  e.  NN0  /\  F : ( 1
 ... N ) --> dom  E )  ->  ( A. k  e.  ( 1 ... N ) ( E `  ( F `  k ) )  =  [_ k  /  x ]_ P  ->  A. l  e.  ( 0..^ N ) ( E `
  ( G `  l ) )  = 
 [_ ( l  +  1 )  /  x ]_ P ) )
 
24-Nov-2017fargshiftfo 28383 If a function is onto, then also the shifted function is onto. (Contributed by Alexander van der Vekens, 24-Nov-2017.)
 |-  G  =  ( x  e.  (
 0..^ ( # `  F ) )  |->  ( F `
  ( x  +  1 ) ) )   =>    |-  ( ( N  e.  NN0  /\  F : ( 1
 ... N ) -onto-> dom 
 E )  ->  G : ( 0..^ ( # `  F ) )
 -onto->
 dom  E )
 
23-Nov-2017ax7wnftAUX7 29627 Special case of ax-7 1720. (Contributed by NM, 23-Nov-2017.)
 |-  ( A. y F/ x ph  ->  ( A. x A. y ph  ->  A. y A. x ph ) )
 
23-Nov-2017ax7w7tAUX7 29626 Special case of ax-7 1720. (Contributed by NM, 23-Nov-2017.)
 |-  ( A. y ( ph  ->  A. x ph )  ->  ( A. x A. y ph  ->  A. y A. x ph ) )
 
23-Nov-2017ax7nfAUX7 29625 Special case of ax-7 1720. (Contributed by NM, 23-Nov-2017.)
 |-  F/ x ph   =>    |-  ( A. x A. y ph  ->  A. y A. x ph )
 
23-Nov-2017fargshiftf1 28382 If a function is 1-1, then also the shifted function is 1-1. (Contributed by Alexander van der Vekens, 23-Nov-2017.)
 |-  G  =  ( x  e.  (
 0..^ ( # `  F ) )  |->  ( F `
  ( x  +  1 ) ) )   =>    |-  ( ( N  e.  NN0  /\  F : ( 1
 ... N ) -1-1-> dom  E )  ->  G :
 ( 0..^ ( # `  F ) ) -1-1-> dom  E )
 
23-Nov-2017fargshiftf 28381 If a class is a function, then also its "shifted function" is a function. (Contributed by Alexander van der Vekens, 23-Nov-2017.)
 |-  G  =  ( x  e.  (
 0..^ ( # `  F ) )  |->  ( F `
  ( x  +  1 ) ) )   =>    |-  ( ( N  e.  NN0  /\  F : ( 1
 ... N ) --> dom  E )  ->  G : ( 0..^ ( # `  F ) ) --> dom  E )
 
23-Nov-2017fargshiftfv 28380 If a class is a function, then the values of the "shifted function" correspond to the function values of the class. (Contributed by Alexander van der Vekens, 23-Nov-2017.)
 |-  G  =  ( x  e.  (
 0..^ ( # `  F ) )  |->  ( F `
  ( x  +  1 ) ) )   =>    |-  ( ( N  e.  NN0  /\  F : ( 1
 ... N ) --> dom  E )  ->  ( X  e.  ( 0..^ N )  ->  ( G `  X )  =  ( F `  ( X  +  1
 ) ) ) )
 
23-Nov-2017fargshiftlem 28379 If a class is a function, then also its "shifted function" is a function. (Contributed by Alexander van der Vekens, 23-Nov-2017.)
 |-  (
 ( N  e.  NN0  /\  X  e.  ( 0..^ N ) )  ->  ( X  +  1
 )  e.  ( 1
 ... N ) )
 
22-Nov-2017faclim 24126 An infinite product expression relating to factorials. Originally due to Euler. (Contributed by Scott Fenton, 22-Nov-2017.)
 |-  F  =  ( n  e.  NN  |->  ( ( ( 1  +  ( 1  /  n ) ) ^ A )  /  (
 1  +  ( A 
 /  n ) ) ) )   =>    |-  ( A  e.  NN0  ->  seq  1 (  x.  ,  F )  ~~>  ( ! `  A ) )
 
21-Nov-2017ex-ovoliunnfl 25002 Demonstration of ovoliunnfl 25001. (Contributed by Brendan Leahy, 21-Nov-2017.)
 |-  (
 ( A  ~<_  NN  /\  A. x  e.  A  x  ~<_  NN )  ->  U. A  =/=  RR )
 
21-Nov-2017ovoliunnfl 25001 ovoliun 18880 is incompatible with the Feferman-Levy model. (Contributed by Brendan Leahy, 21-Nov-2017.)
 |-  (
 ( f  Fn  NN  /\ 
 A. n  e.  NN  ( ( f `  n )  C_  RR  /\  ( vol * `  (
 f `  n )
 )  e.  RR )
 )  ->  ( vol * `
  U_ m  e.  NN  ( f `  m ) )  <_  sup ( ran  seq  1 (  +  ,  ( m  e.  NN  |->  ( vol * `  (
 f `  m )
 ) ) ) , 
 RR* ,  <  ) )   =>    |-  ( ( A  ~<_  NN  /\  A. x  e.  A  x  ~<_  NN )  ->  U. A  =/=  RR )
 
20-Nov-2017ftc1cnnc 25025 Choice-free proof of ftc1cn 19406. (Contributed by Brendan Leahy, 20-Nov-2017.)
 |-  G  =  ( x  e.  ( A [,] B )  |->  S. ( A (,) x ) ( F `  t )  _d t
 )   &    |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  A  <_  B )   &    |-  ( ph  ->  F  e.  ( ( A (,) B ) -cn-> CC ) )   &    |-  ( ph  ->  F  e.  L ^1 )   =>    |-  ( ph  ->  ( RR  _D  G )  =  F )
 
19-Nov-2017n4cyclfrgra 28440 There is no 4-cycle in a friendship graph, see Proposition 1 of [MertziosUnger] p. 153 : "A friendship graph G contains no C4 as a subgraph ...". (Contributed by Alexander van der Vekens, 19-Nov-2017.)
 |-  (
 ( V FriendGrph  E  /\  F ( V Cycles  E ) P )  ->  ( # `  F )  =/=  4 )
 
19-Nov-20174cycl2vnunb 28439 In a 4-cycle, two distinct vertices have not a unique common neighbor. (Contributed by Alexander van der Vekens, 19-Nov-2017.)
 |-  (
 ( ( { A ,  B }  e.  ran  E 
 /\  { B ,  C }  e.  ran  E ) 
 /\  ( { C ,  D }  e.  ran  E 
 /\  { D ,  A }  e.  ran  E ) 
 /\  ( B  e.  V  /\  D  e.  V  /\  B  =/=  D ) )  ->  -.  E! x  e.  V  { { A ,  x } ,  { x ,  C } }  C_  ran  E )
 
19-Nov-20174cycl2v2nb 28438 In a (maybe degenerated) 4-cycle, two vertices have two (maybe not different) common neighbors. (Contributed by Alexander van der Vekens, 19-Nov-2017.)
 |-  (
 ( ( { A ,  B }  e.  ran  E 
 /\  { B ,  C }  e.  ran  E ) 
 /\  ( { C ,  D }  e.  ran  E 
 /\  { D ,  A }  e.  ran  E ) )  ->  ( { { A ,  B } ,  { B ,  C } }  C_  ran  E  /\  { { A ,  D } ,  { D ,  C } }  C_  ran 
 E ) )
 
19-Nov-20173cyclfrgra 28437 Every vertex in a friendship graph (with more than 1 vertex) is part of a 3-cycle. (Contributed by Alexander van der Vekens, 19-Nov-2017.)
 |-  (
 ( V FriendGrph  E  /\  1  <  ( # `  V ) )  ->  A. v  e.  V  E. f E. p ( f ( V Cycles  E ) p  /\  ( # `  f )  =  3  /\  ( p `  0 )  =  v ) )
 
19-Nov-2017ftc1cnnclem 25024 Lemma for ftc1cnnc 25025; cf. ftc1lem4 19402. The stronger assumptions of ftc1cn 19406 are exploited to make use of weaker theorems. (Contributed by Brendan Leahy, 19-Nov-2017.)
 |-  G  =  ( x  e.  ( A [,] B )  |->  S. ( A (,) x ) ( F `  t )  _d t
 )   &    |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  A  <_  B )   &    |-  ( ph  ->  F  e.  ( ( A (,) B ) -cn-> CC ) )   &    |-  ( ph  ->  F  e.  L ^1 )   &    |-  ( ph  ->  c  e.  ( A (,) B ) )   &    |-  H  =  ( z  e.  ( ( A [,] B ) 
 \  { c }
 )  |->  ( ( ( G `  z )  -  ( G `  c ) )  /  ( z  -  c
 ) ) )   &    |-  ( ph  ->  E  e.  RR+ )   &    |-  ( ph  ->  R  e.  RR+ )   &    |-  ( ( ph  /\  y  e.  ( A (,) B ) ) 
 ->  ( ( abs `  (
 y  -  c ) )  <  R  ->  ( abs `  ( ( F `  y )  -  ( F `  c ) ) )  <  E ) )   &    |-  ( ph  ->  X  e.  ( A [,] B ) )   &    |-  ( ph  ->  ( abs `  ( X  -  c ) )  <  R )   &    |-  ( ph  ->  Y  e.  ( A [,] B ) )   &    |-  ( ph  ->  ( abs `  ( Y  -  c ) )  <  R )   =>    |-  ( ( ph  /\  X  <  Y )  ->  ( abs `  ( ( ( ( G `  Y )  -  ( G `  X ) )  /  ( Y  -  X ) )  -  ( F `  c ) ) )  <  E )
 
19-Nov-2017itgabsnc 25020 Choice-free analogue of itgabs 19205. (Contributed by Brendan Leahy, 19-Nov-2017.)
 |-  (
 ( ph  /\  x  e.  A )  ->  B  e.  V )   &    |-  ( ph  ->  ( x  e.  A  |->  B )  e.  L ^1 )   &    |-  ( ph  ->  ( x  e.  A  |->  ( abs `  B )
 )  e. MblFn )   &    |-  ( ph  ->  ( x  e.  A  |->  ( ( * `  S. A B  _d x )  x.  B ) )  e. MblFn )   =>    |-  ( ph  ->  ( abs `  S. A B  _d x )  <_  S. A ( abs `  B )  _d x )
 
19-Nov-2017itgmulc2nc 25019 Choice-free analogue of itgmulc2 19204. (Contributed by Brendan Leahy, 19-Nov-2017.)
 |-  ( ph  ->  C  e.  CC )   &    |-  ( ( ph  /\  x  e.  A )  ->  B  e.  V )   &    |-  ( ph  ->  ( x  e.  A  |->  B )  e.  L ^1 )   &    |-  ( ph  ->  ( x  e.  A  |->  ( C  x.  B ) )  e. MblFn )   =>    |-  ( ph  ->  ( C  x.  S. A B  _d x )  =  S. A ( C  x.  B )  _d x )
 
19-Nov-2017itgmulc2nclem2 25018 Lemma for itgmulc2nc 25019; cf. itgmulc2lem2 19203. (Contributed by Brendan Leahy, 19-Nov-2017.)
 |-  ( ph  ->  C  e.  CC )   &    |-  ( ( ph  /\  x  e.  A )  ->  B  e.  V )   &    |-  ( ph  ->  ( x  e.  A  |->  B )  e.  L ^1 )   &    |-  ( ph  ->  ( x  e.  A  |->  ( C  x.  B ) )  e. MblFn )   &    |-  ( ph  ->  C  e.  RR )   &    |-  (
 ( ph  /\  x  e.  A )  ->  B  e.  RR )   =>    |-  ( ph  ->  ( C  x.  S. A B  _d x )  =  S. A ( C  x.  B )  _d x )
 
18-Nov-20174cycl4dv 28413 In a simple graph, the vertices of a 4-cycle are mutually different. (Contributed by Alexander van der Vekens, 18-Nov-2017.)
 |-  (
 ( V USGrph  E  /\  ( F  e. Word  dom  E  /\  Fun  `' F  /\  ( # `  F )  =  4 ) ) 
 ->  ( ( ( ( E `  ( F `
  0 ) )  =  { A ,  B }  /\  ( E `
  ( F `  1 ) )  =  { B ,  C } )  /\  ( ( E `  ( F `
  2 ) )  =  { C ,  D }  /\  ( E `
  ( F `  3 ) )  =  { D ,  A } ) )  ->  ( ( ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E )  /\  ( { C ,  D }  e.  ran  E  /\  { D ,  A }  e.  ran  E ) ) 
 /\  ( ( A  =/=  B  /\  A  =/=  C  /\  A  =/=  D )  /\  ( B  =/=  C  /\  B  =/=  D  /\  C  =/=  D ) ) ) ) )
 
18-Nov-2017usgraf1 28243 The edge function of an undirected simple graph without loops is a one to one function. (Contributed by Alexander van der Vekens, 18-Nov-2017.)
 |-  ( V USGrph  E  ->  E : dom  E -1-1-> ran  E )
 
18-Nov-2017usgraf1o 28242 The edge function of an undirected simple graph without loops is a one to one function. (Contributed by Alexander van der Vekens, 18-Nov-2017.)
 |-  ( V USGrph  E  ->  E : dom  E -1-1-onto-> ran  E )
 
18-Nov-20174fvwrd4 28220 The first four function values of a word of length at least 4. (Contributed by Alexander van der Vekens, 18-Nov-2017.)
 |-  (
 ( L  e.  ( ZZ>=
 `  3 )  /\  P : ( 0 ...
 L ) --> V ) 
 ->  E. a  e.  V  E. b  e.  V  E. c  e.  V  E. d  e.  V  ( ( ( P `
  0 )  =  a  /\  ( P `
  1 )  =  b )  /\  (
 ( P `  2
 )  =  c  /\  ( P `  3 )  =  d ) ) )
 
17-Nov-2017constr3cyclpe 28409 If there are three (different) vertices in a graph which are mutually connected by edges, there is a 3-cycle in the graph containing one of these vertices. (Contributed by Alexander van der Vekens, 17-Nov-2017.)
 |-  (
 ( V USGrph  E  /\  ( A  e.  V  /\  B  e.  V  /\  C  e.  V )  /\  ( { A ,  B }  e.  ran  E 
 /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) ) 
 ->  E. f E. p ( f ( V Cycles  E ) p  /\  ( # `  f )  =  3  /\  ( p `  0 )  =  A ) )
 
17-Nov-2017constr3cyclp 28408 Construction of a 3-cycle from three given edges in a graph, containing an endpoint of one of these edges. (Contributed by Alexander van der Vekens, 17-Nov-2017.)
 |-  F  =  { <. 0 ,  ( `' E `  { A ,  B } ) >. , 
 <. 1 ,  ( `' E `  { B ,  C } ) >. , 
 <. 2 ,  ( `' E `  { C ,  A } ) >. }   &    |-  P  =  ( { <. 0 ,  A >. , 
 <. 1 ,  B >. }  u.  { <. 2 ,  C >. ,  <. 3 ,  A >. } )   =>    |-  ( ( V USGrph  E  /\  ( A  e.  V  /\  B  e.  V  /\  C  e.  V ) 
 /\  ( { A ,  B }  e.  ran  E 
 /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) ) 
 ->  ( F ( V Cycles  E ) P  /\  ( # `  F )  =  3  /\  ( P `  0 )  =  A ) )
 
17-Nov-2017fzo0to42pr 28211 A half-open integer range from 0 to 4 is a union of two unordered pairs. (Contributed by Alexander van der Vekens, 17-Nov-2017.)
 |-  (
 0..^ 4 )  =  ( { 0 ,  1 }  u.  {
 2 ,  3 } )
 
17-Nov-2017itgmulc2nclem1 25017 Lemma for itgmulc2nc 25019; cf. itgmulc2lem1 19202. (Contributed by Brendan Leahy, 17-Nov-2017.)
 |-  ( ph  ->  C  e.  CC )   &    |-  ( ( ph  /\  x  e.  A )  ->  B  e.  V )   &    |-  ( ph  ->  ( x  e.  A  |->  B )  e.  L ^1 )   &    |-  ( ph  ->  ( x  e.  A  |->  ( C  x.  B ) )  e. MblFn )   &    |-  ( ph  ->  C  e.  RR )   &    |-  (
 ( ph  /\  x  e.  A )  ->  B  e.  RR )   &    |-  ( ph  ->  0 
 <_  C )   &    |-  ( ( ph  /\  x  e.  A ) 
 ->  0  <_  B )   =>    |-  ( ph  ->  ( C  x.  S. A B  _d x )  =  S. A ( C  x.  B )  _d x )
 
17-Nov-2017iblmulc2nc 25016 Choice-free analogue of iblmulc2 19201. (Contributed by Brendan Leahy, 17-Nov-2017.)
 |-  ( ph  ->  C  e.  CC )   &    |-  ( ( ph  /\  x  e.  A )  ->  B  e.  V )   &    |-  ( ph  ->  ( x  e.  A  |->  B )  e.  L ^1 )   &    |-  ( ph  ->  ( x  e.  A  |->  ( C  x.  B ) )  e. MblFn )   =>    |-  ( ph  ->  ( x  e.  A  |->  ( C  x.  B ) )  e.  L ^1 )
 
16-Nov-20173cyclfrgrarn 28436 Every vertex in a friendship graph ( with more than 1 vertex) is part of a 3-cycle. (Contributed by Alexander van der Vekens, 16-Nov-2017.)
 |-  (
 ( V FriendGrph  E  /\  1  <  ( # `  V ) )  ->  A. a  e.  V  E. b  e.  V  E. c  e.  V  ( { a ,  b }  e.  ran  E 
 /\  { b ,  c }  e.  ran  E  /\  { c ,  a }  e.  ran  E ) )
 
16-Nov-20173cyclfrgrarn1 28435 Every vertex in a friendship graph ( with more than 1 vertex) is part of a 3-cycle. (Contributed by Alexander van der Vekens, 16-Nov-2017.)
 |-  (
 ( V FriendGrph  E  /\  ( A  e.  V  /\  C  e.  V )  /\  A  =/=  C ) 
 ->  E. b  e.  V  E. c  e.  V  ( { A ,  b }  e.  ran  E  /\  { b ,  c }  e.  ran  E  /\  {
 c ,  A }  e.  ran  E ) )
 
16-Nov-20172pthfrgrarn2 28434 Between any two (different) vertices in a friendship graph is a 2-path (path of length 2), see Proposition 1 of [MertziosUnger] p. 153 : "A friendship graph G ..., as well as the distance between any two nodes in G is at most two". (Contributed by Alexander van der Vekens, 16-Nov-2017.)
 |-  ( V FriendGrph  E  ->  A. a  e.  V  A. c  e.  ( V  \  {
 a } ) E. b  e.  V  (
 ( { a ,  b }  e.  ran  E 
 /\  { b ,  c }  e.  ran  E ) 
 /\  ( a  =/=  b  /\  b  =/=  c ) ) )
 
16-Nov-2017itggt0cn 25023 itggt0 19212 holds for continuous functions in the absence of ax-cc 8077. (Contributed by Brendan Leahy, 16-Nov-2017.)
 |-  ( ph  ->  X  <  Y )   &    |-  ( ph  ->  ( x  e.  ( X (,) Y )  |->  B )  e.  L ^1 )   &    |-  (
 ( ph  /\  x  e.  ( X (,) Y ) )  ->  B  e.  RR+ )   &    |-  ( ph  ->  ( x  e.  ( X (,) Y )  |->  B )  e.  ( ( X (,) Y )
 -cn-> CC ) )   =>    |-  ( ph  ->  0  <  S. ( X (,) Y ) B  _d x )
 
16-Nov-2017itg2gt0cn 25006 itg2gt0 19131 holds on functions continuous on an open interval in the absence of ax-cc 8077. The fourth hypothesis is made unnecessary by the continuity hypothesis. (Contributed by Brendan Leahy, 16-Nov-2017.)
 |-  ( ph  ->  X  <  Y )   &    |-  ( ph  ->  F : RR --> ( 0 [,)  +oo ) )   &    |-  ( ( ph  /\  x  e.  ( X (,) Y ) ) 
 ->  0  <  ( F `
  x ) )   &    |-  ( ph  ->  ( F  |`  ( X (,) Y ) )  e.  (
 ( X (,) Y ) -cn-> CC ) )   =>    |-  ( ph  ->  0  <  ( S.2 `  F ) )
 
15-Nov-20172pthfrgrarn 28433 Between any two (different) vertices in a friendship graph is a 2-path (path of length 2), see Proposition 1 of [MertziosUnger] p. 153 : "A friendship graph G ..., as well as the distance between any two nodes in G is at most two". (Contributed by Alexander van der Vekens, 15-Nov-2017.)
 |-  ( V FriendGrph  E  ->  A. a  e.  V  A. c  e.  ( V  \  {
 a } ) E. b  e.  V  ( { a ,  b }  e.  ran  E  /\  { b ,  c }  e.  ran  E ) )
 
15-Nov-2017hashgt12el2 28219 In a set with more than one element are two different elements. (Contributed by Alexander van der Vekens, 15-Nov-2017.)
 |-  (
 ( V  e.  W  /\  1  <  ( # `  V )  /\  A  e.  V )  ->  E. b  e.  V  A  =/=  b
 )
 
15-Nov-2017hashgt12el 28218 In a set with more than one element are two different elements. (Contributed by Alexander van der Vekens, 15-Nov-2017.)
 |-  (
 ( V  e.  W  /\  1  <  ( # `  V ) )  ->  E. a  e.  V  E. b  e.  V  a  =/=  b )
 
14-Nov-20173v3e3cycl 28411 If and only if there is a 3-cycle in a graph, there are three (different) vertices in the graph which are mutually connected by edges. (Contributed by Alexander van der Vekens, 14-Nov-2017.)
 |-  ( V USGrph  E  ->  ( E. f E. p ( f ( V Cycles  E ) p  /\  ( # `  f
 )  =  3 )  <->  E. a  e.  V  E. b  e.  V  E. c  e.  V  ( { a ,  b }  e.  ran  E  /\  { b ,  c }  e.  ran  E  /\  {
 c ,  a }  e.  ran  E ) ) )
 
14-Nov-20173v3e3cycl2 28410 If there are three (different) vertices in a graph which are mutually connected by edges, there is a 3-cycle in the graph. (Contributed by Alexander van der Vekens, 14-Nov-2017.)
 |-  ( V USGrph  E  ->  ( E. a  e.  V  E. b  e.  V  E. c  e.  V  ( { a ,  b }  e.  ran  E 
 /\  { b ,  c }  e.  ran  E  /\  { c ,  a }  e.  ran  E )  ->  E. f E. p ( f ( V Cycles  E ) p  /\  ( # `  f )  =  3 ) ) )
 
13-Nov-2017equsalihAUX7 29465 One direction of equsalhNEW7 29466 with weaker hypothesis. TO DO: Delete if not used. (Contributed by NM, 13-Nov-2017.)
 |-  ( x  =  y  ->  (
 ph  ->  A. x ps )
 )   =>    |-  ( A. x ( x  =  y  ->  ph )  ->  ps )
 
13-Nov-2017constr3cycl 28407 Construction of a 3-cycle from three given edges in a graph. (Contributed by Alexander van der Vekens, 13-Nov-2017.)
 |-  F  =  { <. 0 ,  ( `' E `  { A ,  B } ) >. , 
 <. 1 ,  ( `' E `  { B ,  C } ) >. , 
 <. 2 ,  ( `' E `  { C ,  A } ) >. }   &    |-  P  =  ( { <. 0 ,  A >. , 
 <. 1 ,  B >. }  u.  { <. 2 ,  C >. ,  <. 3 ,  A >. } )   =>    |-  ( ( V USGrph  E  /\  ( A  e.  V  /\  B  e.  V  /\  C  e.  V ) 
 /\  ( { A ,  B }  e.  ran  E 
 /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) ) 
 ->  ( F ( V Cycles  E ) P  /\  ( # `  F )  =  3 ) )
 
13-Nov-2017constr3pth 28406 Construction of a path from three given edges in a graph. (Contributed by Alexander van der Vekens, 13-Nov-2017.)
 |-  F  =  { <. 0 ,  ( `' E `  { A ,  B } ) >. , 
 <. 1 ,  ( `' E `  { B ,  C } ) >. , 
 <. 2 ,  ( `' E `  { C ,  A } ) >. }   &    |-  P  =  ( { <. 0 ,  A >. , 
 <. 1 ,  B >. }  u.  { <. 2 ,  C >. ,  <. 3 ,  A >. } )   =>    |-  ( ( V USGrph  E  /\  ( A  e.  V  /\  B  e.  V  /\  C  e.  V ) 
 /\  ( { A ,  B }  e.  ran  E 
 /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) ) 
 ->  F ( V Paths  E ) P )
 
13-Nov-2017constr3trl 28405 Construction of a trail from three given edges in a graph. (Contributed by Alexander van der Vekens, 13-Nov-2017.)
 |-  F  =  { <. 0 ,  ( `' E `  { A ,  B } ) >. , 
 <. 1 ,  ( `' E `  { B ,  C } ) >. , 
 <. 2 ,  ( `' E `  { C ,  A } ) >. }   &    |-  P  =  ( { <. 0 ,  A >. , 
 <. 1 ,  B >. }  u.  { <. 2 ,  C >. ,  <. 3 ,  A >. } )   =>    |-  ( ( V USGrph  E  /\  ( A  e.  V  /\  B  e.  V  /\  C  e.  V ) 
 /\  ( { A ,  B }  e.  ran  E 
 /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) ) 
 ->  F ( V Trails  E ) P )
 
13-Nov-2017constr3pthlem2 28402 Lemma for constr3pth 28406. (Contributed by Alexander van der Vekens, 13-Nov-2017.)
 |-  F  =  { <. 0 ,  ( `' E `  { A ,  B } ) >. , 
 <. 1 ,  ( `' E `  { B ,  C } ) >. , 
 <. 2 ,  ( `' E `  { C ,  A } ) >. }   &    |-  P  =  ( { <. 0 ,  A >. , 
 <. 1 ,  B >. }  u.  { <. 2 ,  C >. ,  <. 3 ,  A >. } )   =>    |-  ( ( ( A  e.  V  /\  B  e.  V  /\  C  e.  V )  /\  B  =/=  C ) 
 ->  Fun  `' ( P  |`  ( 1..^ ( # `  F ) ) ) )
 
13-Nov-2017constr3pthlem1 28401 Lemma for constr3pth 28406. (Contributed by Alexander van der Vekens, 13-Nov-2017.)
 |-  F  =  { <. 0 ,  ( `' E `  { A ,  B } ) >. , 
 <. 1 ,  ( `' E `  { B ,  C } ) >. , 
 <. 2 ,  ( `' E `  { C ,  A } ) >. }   &    |-  P  =  ( { <. 0 ,  A >. , 
 <. 1 ,  B >. }  u.  { <. 2 ,  C >. ,  <. 3 ,  A >. } )   =>    |-  ( ( B  e.  V  /\  C  e.  W )  ->  ( P  |`  ( 1..^ ( # `  F ) ) )  =  { <. 1 ,  B >. ,  <. 2 ,  C >. } )
 
12-Nov-2017constr3trllem5 28400 Lemma for constr3trl 28405. (Contributed by Alexander van der Vekens, 12-Nov-2017.)
 |-  F  =  { <. 0 ,  ( `' E `  { A ,  B } ) >. , 
 <. 1 ,  ( `' E `  { B ,  C } ) >. , 
 <. 2 ,  ( `' E `  { C ,  A } ) >. }   &    |-  P  =  ( { <. 0 ,  A >. , 
 <. 1 ,  B >. }  u.  { <. 2 ,  C >. ,  <. 3 ,  A >. } )   =>    |-  ( ( V USGrph  E  /\  ( { A ,  B }  e.  ran  E 
 /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) ) 
 ->  A. k  e.  (
 0..^ ( # `  F ) ) ( E `
  ( F `  k ) )  =  { ( P `  k ) ,  ( P `  ( k  +  1 ) ) }
 )
 
12-Nov-2017constr3trllem2 28397 Lemma for constr3trl 28405. (Contributed by Alexander van der Vekens, 12-Nov-2017.)
 |-  F  =  { <. 0 ,  ( `' E `  { A ,  B } ) >. , 
 <. 1 ,  ( `' E `  { B ,  C } ) >. , 
 <. 2 ,  ( `' E `  { C ,  A } ) >. }   &    |-  P  =  ( { <. 0 ,  A >. , 
 <. 1 ,  B >. }  u.  { <. 2 ,  C >. ,  <. 3 ,  A >. } )   =>    |-  ( ( V USGrph  E  /\  ( { A ,  B }  e.  ran  E 
 /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) ) 
 ->  Fun  `' F )
 
12-Nov-2017constr3lem5 28394 Lemma for constr3trl 28405 etc. (Contributed by Alexander van der Vekens, 12-Nov-2017.)
 |-  F  =  { <. 0 ,  ( `' E `  { A ,  B } ) >. , 
 <. 1 ,  ( `' E `  { B ,  C } ) >. , 
 <. 2 ,  ( `' E `  { C ,  A } ) >. }   &    |-  P  =  ( { <. 0 ,  A >. , 
 <. 1 ,  B >. }  u.  { <. 2 ,  C >. ,  <. 3 ,  A >. } )   =>    |-  ( ( F `
  0 )  =  ( `' E `  { A ,  B }
 )  /\  ( F `  1 )  =  ( `' E `  { B ,  C } )  /\  ( F `  2 )  =  ( `' E ` 
 { C ,  A } ) )
 
12-Nov-2017f1ocnvfvrneq 28189 If the values of a one-to-one function for two arguments from the range of the function are equal, the arguments themselves must be equal. (Contributed by Alexander van der Vekens, 12-Nov-2017.)
 |-  (
 ( F : A -1-1-> B 
 /\  ( C  e.  ran 
 F  /\  D  e.  ran 
 F ) )  ->  ( ( `' F `  C )  =  ( `' F `  D ) 
 ->  C  =  D ) )
 
12-Nov-2017f1veqaeq 28188 If the values of the converse of a one-to-one function for two arguments are equal, the arguments themselves must be equal. (Contributed by Alexander van der Vekens, 12-Nov-2017.)
 |-  (
 ( F : A -1-1-> B 
 /\  ( C  e.  A  /\  D  e.  A ) )  ->  ( ( F `  C )  =  ( F `  D )  ->  C  =  D ) )
 
12-Nov-2017equequ1 1667 An equivalence law for equality. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 12-Nov-2017.)
 |-  ( x  =  y 
 ->  ( x  =  z  <-> 
 y  =  z ) )
 
12-Nov-2017exiftru 1647 A companion rule to ax-gen, valid only if an individual exists. Unlike ax-9 1644, it does not require equality on its interface. Some fundamental theorems of predicate logic can be proven from ax-gen 1536, ax-5 1547 and this theorem alone, not requiring ax-8 1661 or excessive distinct variable conditions. (Contributed by Wolf Lammen, 12-Nov-2017.)
 |-  ph   =>    |- 
 E. x ph
 
12-Nov-2017mpto2 1524 Modus ponendo tollens 2, one of the "indemonstrables" in Stoic logic. Note that this uses exclusive-or  \/_. See rule 2 on [Lopez-Astorga] p. 12 , rule 4 on [Sanford] p. 39 and rule A4 in [Hitchcock] p. 5 . (Contributed by David A. Wheeler, 3-Jul-2016.) (Proof shortened by Wolf Lammen, 12-Nov-2017.)
 |-  ph   &    |-  ( ph  \/_  ps )   =>    |- 
 -.  ps
 
11-Nov-2017constr3cycllem1 28404 Lemma for constr3cycl 28407. (Contributed by Alexander van der Vekens, 11-Nov-2017.)
 |-  F  =  { <. 0 ,  ( `' E `  { A ,  B } ) >. , 
 <. 1 ,  ( `' E `  { B ,  C } ) >. , 
 <. 2 ,  ( `' E `  { C ,  A } ) >. }   &    |-  P  =  ( { <. 0 ,  A >. , 
 <. 1 ,  B >. }  u.  { <. 2 ,  C >. ,  <. 3 ,  A >. } )   =>    |-  ( ( A  e.  V  /\  B  e.  V  /\  C  e.  V )  ->  ( P `
  0 )  =  ( P `  ( # `
  F ) ) )
 
11-Nov-2017constr3pthlem3 28403 Lemma for constr3pth 28406. (Contributed by Alexander van der Vekens, 11-Nov-2017.)
 |-  F  =  { <. 0 ,  ( `' E `  { A ,  B } ) >. , 
 <. 1 ,  ( `' E `  { B ,  C } ) >. , 
 <. 2 ,  ( `' E `  { C ,  A } ) >. }   &    |-  P  =  ( { <. 0 ,  A >. , 
 <. 1 ,  B >. }  u.  { <. 2 ,  C >. ,  <. 3 ,  A >. } )   =>    |-  ( ( ( A  e.  V  /\  B  e.  V  /\  C  e.  V )  /\  ( A  =/=  B  /\  B  =/=  C  /\  C  =/=  A ) ) 
 ->  ( ( P " { 0 ,  ( # `
  F ) }
 )  i^i  ( P " ( 1..^ ( # `  F ) ) ) )  =  (/) )
 
11-Nov-2017constr3trllem4 28399 Lemma for constr3trl 28405. (Contributed by Alexander van der Vekens, 11-Nov-2017.)
 |-  F  =  { <. 0 ,  ( `' E `  { A ,  B } ) >. , 
 <. 1 ,  ( `' E `  { B ,  C } ) >. , 
 <. 2 ,  ( `' E `  { C ,  A } ) >. }   &    |-  P  =  ( { <. 0 ,  A >. , 
 <. 1 ,  B >. }  u.  { <. 2 ,  C >. ,  <. 3 ,  A >. } )   =>    |-  ( ( A  e.  V  /\  B  e.  V  /\  C  e.  V )  ->  P :
 ( 0 ... 3
 ) --> V )
 
11-Nov-2017constr3trllem3 28398 Lemma for constr3trl 28405. (Contributed by Alexander van der Vekens, 11-Nov-2017.)
 |-  F  =  { <. 0 ,  ( `' E `  { A ,  B } ) >. , 
 <. 1 ,  ( `' E `  { B ,  C } ) >. , 
 <. 2 ,  ( `' E `  { C ,  A } ) >. }   &    |-  P  =  ( { <. 0 ,  A >. , 
 <. 1 ,  B >. }  u.  { <. 2 ,  C >. ,  <. 3 ,  A >. } )   =>    |-  ( ( A  e.  V  /\  B  e.  V  /\  C  e.  V )  ->  P :
 ( 0 ... ( # `
  F ) ) --> V )
 
11-Nov-2017constr3lem6 28395 Lemma for constr3pthlem3 28403. (Contributed by Alexander van der Vekens, 11-Nov-2017.)
 |-  F  =  { <. 0 ,  ( `' E `  { A ,  B } ) >. , 
 <. 1 ,  ( `' E `  { B ,  C } ) >. , 
 <. 2 ,  ( `' E `  { C ,  A } ) >. }   &    |-  P  =  ( { <. 0 ,  A >. , 
 <. 1 ,  B >. }  u.  { <. 2 ,  C >. ,  <. 3 ,  A >. } )   =>    |-  ( ( ( A  e.  V  /\  B  e.  V  /\  C  e.  V )  /\  ( A  =/=  B  /\  B  =/=  C  /\  C  =/=  A ) ) 
 ->  ( { ( P `
  0 ) ,  ( P `  3
 ) }  i^i  {
 ( P `  1
 ) ,  ( P `
  2 ) }
 )  =  (/) )
 
11-Nov-20173cycl3dv 28388 In a simple graph, the vertices of a 3-cycle are mutually different. (Contributed by Alexander van der Vekens, 11-Nov-2017.)
 |-  (
 ( V USGrph  E  /\  ( { A ,  B }  e.  ran  E  /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) ) 
 ->  ( A  =/=  B  /\  B  =/=  C  /\  C  =/=  A ) )
 
11-Nov-2017disjpr2 28185 The intersection of distinct pairs is disjoint, analogous to disjsn2 3707. (Contributed by Alexander van der Vekens, 11-Nov-2017.)
 |-  (
 ( ( A  =/=  C 
 /\  B  =/=  C )  /\  ( A  =/=  D 
 /\  B  =/=  D ) )  ->  ( { A ,  B }  i^i  { C ,  D } )  =  (/) )
 
11-Nov-2017itgsubnc 25013 Choice-free analogue of itgsub 19196. (Contributed by Brendan Leahy, 11-Nov-2017.)
 |-  (
 ( ph  /\  x  e.  A )  ->  B  e.  V )   &    |-  ( ph  ->  ( x  e.  A  |->  B )  e.  L ^1 )   &    |-  ( ( ph  /\  x  e.  A ) 
 ->  C  e.  V )   &    |-  ( ph  ->  ( x  e.  A  |->  C )  e.  L ^1 )   &    |-  ( ph  ->  ( x  e.  A  |->  ( B  -  C ) )  e. MblFn
 )   =>    |-  ( ph  ->  S. A ( B  -  C )  _d x  =  ( S. A B  _d x  -  S. A C  _d x ) )
 
11-Nov-2017iblsubnc 25012 Choice-free analogue of iblsub 19192. (Contributed by Brendan Leahy, 11-Nov-2017.)
 |-  (
 ( ph  /\  x  e.  A )  ->  B  e.  V )   &    |-  ( ph  ->  ( x  e.  A  |->  B )  e.  L ^1 )   &    |-  ( ( ph  /\  x  e.  A ) 
 ->  C  e.  V )   &    |-  ( ph  ->  ( x  e.  A  |->  C )  e.  L ^1 )   &    |-  ( ph  ->  ( x  e.  A  |->  ( B  -  C ) )  e. MblFn
 )   =>    |-  ( ph  ->  ( x  e.  A  |->  ( B  -  C ) )  e.  L ^1 )
 
11-Nov-2017itgaddnc 25011 Choice-free analogue of itgadd 19195. (Contributed by Brendan Leahy, 11-Nov-2017.)
 |-  (
 ( ph  /\  x  e.  A )  ->  B  e.  V )   &    |-  ( ph  ->  ( x  e.  A  |->  B )  e.  L ^1 )   &    |-  ( ( ph  /\  x  e.  A ) 
 ->  C  e.  V )   &    |-  ( ph  ->  ( x  e.  A  |->  C )  e.  L ^1 )   &    |-  ( ph  ->  ( x  e.  A  |->  ( B  +  C ) )  e. MblFn
 )   =>    |-  ( ph  ->  S. A ( B  +  C )  _d x  =  ( S. A B  _d x  +  S. A C  _d x ) )
 
11-Nov-2017mtp-or 1528 Modus tollendo ponens (inclusive-or version), aka disjunctive syllogism. This is similar to mtp-xor 1526, one of the five original "indemonstrables" in Stoic logic. However, in Stoic logic this rule used exclusive-or, while the name modus tollendo ponens often refers to a variant of the rule that uses inclusive-or instead. The rule says, "if  ph is not true, and  ph or  ps (or both) are true, then  ps must be true." An alternative phrasing is, "Once you eliminate the impossible, whatever remains, no matter how improbable, must be the truth." -- Sherlock Holmes (Sir Arthur Conan Doyle, 1890: The Sign of the Four, ch. 6). (Contributed by David A. Wheeler, 3-Jul-2016.) (Proof shortened by Wolf Lammen, 11-Nov-2017.)
 |- 
 -.  ph   &    |-  ( ph  \/  ps )   =>    |- 
 ps
 
11-Nov-2017mtp-xor 1526 Modus tollendo ponens (original exclusive-or version), aka disjunctive syllogism, one of the five "indemonstrables" in Stoic logic. The rule says, "if  ph is not true, and either  ph or  ps (exclusively) are true, then  ps must be true." Today the name "modus tollendo ponens" often refers to a variant, the inclusive-or version as defined in mtp-or 1528. See rule 3 on [Lopez-Astorga] p. 12 (note that the "or" is the same as mpto2 1524, that is, it is exclusive-or df-xor 1296), rule 3 of [Sanford] p. 39 (where it is not as clearly stated which kind of "or" is used but it appears to be in the same sense as mpto2 1524), and rule A5 in [Hitchcock] p. 5 (exclusive-or is expressly used). (Contributed by David A. Wheeler, 4-Jul-2016.) (Proof shortened by Wolf Lammen, 11-Nov-2017.)
 |- 
 -.  ph   &    |-  ( ph  \/_  ps )   =>    |- 
 ps
 
10-Nov-2017constr3trllem1 28396 Lemma for constr3trl 28405. (Contributed by Alexander van der Vekens, 10-Nov-2017.)
 |-  F  =  { <. 0 ,  ( `' E `  { A ,  B } ) >. , 
 <. 1 ,  ( `' E `  { B ,  C } ) >. , 
 <. 2 ,  ( `' E `  { C ,  A } ) >. }   &    |-  P  =  ( { <. 0 ,  A >. , 
 <. 1 ,  B >. }  u.  { <. 2 ,  C >. ,  <. 3 ,  A >. } )   =>    |-  ( ( V USGrph  E  /\  ( { A ,  B }  e.  ran  E 
 /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) ) 
 ->  F  e. Word  dom  E )
 
10-Nov-2017constr3lem4 28393 Lemma for constr3trl 28405 etc. The proof could be much shorter if a theorem "fvprg" analogous to fvsng 5730, fvpr1 5738 and fvpr2 5739 was available. (Contributed by Alexander van der Vekens, 10-Nov-2017.)
 |-  F  =  { <. 0 ,  ( `' E `  { A ,  B } ) >. , 
 <. 1 ,  ( `' E `  { B ,  C } ) >. , 
 <. 2 ,  ( `' E `  { C ,  A } ) >. }   &    |-  P  =  ( { <. 0 ,  A >. , 
 <. 1 ,  B >. }  u.  { <. 2 ,  C >. ,  <. 3 ,  A >. } )   =>    |-  ( ( A  e.  V  /\  B  e.  V  /\  C  e.  V )  ->  ( ( ( P `  0
 )  =  A  /\  ( P `  1 )  =  B )  /\  ( ( P `  2 )  =  C  /\  ( P `  3
 )  =  A ) ) )
 
10-Nov-2017constr3lem2 28392 Lemma for constr3trl 28405 etc. (Contributed by Alexander van der Vekens, 10-Nov-2017.)
 |-  F  =  { <. 0 ,  ( `' E `  { A ,  B } ) >. , 
 <. 1 ,  ( `' E `  { B ,  C } ) >. , 
 <. 2 ,  ( `' E `  { C ,  A } ) >. }   &    |-  P  =  ( { <. 0 ,  A >. , 
 <. 1 ,  B >. }  u.  { <. 2 ,  C >. ,  <. 3 ,  A >. } )   =>    |-  ( # `  F )  =  3
 
10-Nov-2017constr3lem1 28391 Lemma for constr3trl 28405 etc. (Contributed by Alexander van der Vekens, 10-Nov-2017.)
 |-  F  =  { <. 0 ,  ( `' E `  { A ,  B } ) >. , 
 <. 1 ,  ( `' E `  { B ,  C } ) >. , 
 <. 2 ,  ( `' E `  { C ,  A } ) >. }   &    |-  P  =  ( { <. 0 ,  A >. , 
 <. 1 ,  B >. }  u.  { <. 2 ,  C >. ,  <. 3 ,  A >. } )   =>    |-  ( F  e.  _V 
 /\  P  e.  _V )
 
10-Nov-2017hashtpg 28217 The size of an unordered triple of three different elements. (Contributed by Alexander van der Vekens, 10-Nov-2017.)
 |-  (
 ( A  e.  _V  /\  B  e.  _V  /\  C  e.  _V )  ->  ( ( A  =/=  B 
 /\  B  =/=  C  /\  C  =/=  A )  <-> 
 ( # `  { A ,  B ,  C }
 )  =  3 ) )
 
10-Nov-2017itgaddnclem2 25010 Lemma for itgaddnc 25011; cf. itgaddlem2 19194. (Contributed by Brendan Leahy, 10-Nov-2017.)
 |-  (
 ( ph  /\  x  e.  A )  ->  B  e.  V )   &    |-  ( ph  ->  ( x  e.  A  |->  B )  e.  L ^1 )   &    |-  ( ( ph  /\  x  e.  A ) 
 ->  C  e.  V )   &    |-  ( ph  ->  ( x  e.  A  |->  C )  e.  L ^1 )   &    |-  ( ph  ->  ( x  e.  A  |->  ( B  +  C ) )  e. MblFn
 )   &    |-  ( ( ph  /\  x  e.  A )  ->  B  e.  RR )   &    |-  ( ( ph  /\  x  e.  A ) 
 ->  C  e.  RR )   =>    |-  ( ph  ->  S. A ( B  +  C )  _d x  =  ( S. A B  _d x  +  S. A C  _d x ) )
 
9-Nov-20174cycl4dv4e 28414 If there is a cycle of length 4 in a graph, there are four (different) vertices in the graph which are mutually connected by edges. (Contributed by Alexander van der Vekens, 9-Nov-2017.)
 |-  (
 ( V USGrph  E  /\  F ( V Cycles  E ) P  /\  ( # `  F )  =  4 )  ->  E. a  e.  V  E. b  e.  V  E. c  e.  V  E. d  e.  V  ( ( ( { a ,  b }  e.  ran  E  /\  { b ,  c }  e.  ran  E )  /\  ( { c ,  d }  e.  ran  E  /\  { d ,  a }  e.  ran  E ) ) 
 /\  ( ( a  =/=  b  /\  a  =/=  c  /\  a  =/=  d )  /\  (
 b  =/=  c  /\  b  =/=  d  /\  c  =/=  d ) ) ) )
 
9-Nov-20174cycl4v4e 28412 If there is a cycle of length 4 in a graph, there are four (different) vertices in the graph which are mutually connected by edges. (Contributed by Alexander van der Vekens, 9-Nov-2017.)
 |-  (
 ( Fun  E  /\  F ( V Cycles  E ) P  /\  ( # `  F )  =  4 )  ->  E. a  e.  V  E. b  e.  V  E. c  e.  V  E. d  e.  V  ( ( {
 a ,  b }  e.  ran  E  /\  {
 b ,  c }  e.  ran  E )  /\  ( { c ,  d }  e.  ran  E  /\  { d ,  a }  e.  ran  E ) ) )
 
9-Nov-20173v3e3cycl1 28390 If there is a cycle of length 3 in a graph, there are three (different) vertices in the graph which are mutually connected by edges. (Contributed by Alexander van der Vekens, 9-Nov-2017.)
 |-  (
 ( Fun  E  /\  F ( V Cycles  E ) P  /\  ( # `  F )  =  3 )  ->  E. a  e.  V  E. b  e.  V  E. c  e.  V  ( { a ,  b }  e.  ran  E 
 /\  { b ,  c }  e.  ran  E  /\  { c ,  a }  e.  ran  E ) )
 
9-Nov-2017nvnencycllem 28389 Lemma for 3v3e3cycl1 28390 and 4cycl4v4e 28412. (Contributed by Alexander van der Vekens, 9-Nov-2017.)
 |-  (
 ( ( Fun  E  /\  F  e. Word  dom  E ) 
 /\  ( X  e.  NN0  /\  X  <  ( # `  F ) ) ) 
 ->  ( ( E `  ( F `  X ) )  =  { A ,  B }  ->  { A ,  B }  e.  ran  E ) )
 
9-Nov-2017usgrcyclnl2 28387 In an undirected simple graph (with no loops!) there are no cycles with length 2 (consisting of two edges ). (Contributed by Alexander van der Vekens, 9-Nov-2017.)
 |-  (
 ( V USGrph  E  /\  F ( V Cycles  E ) P )  ->  ( # `
  F )  =/=  2 )
 
9-Nov-2017fzo0to3tp 28210 A half-open integer range from 0 to 3 is an unordered triple. (Contributed by Alexander van der Vekens, 9-Nov-2017.)
 |-  (
 0..^ 3 )  =  { 0 ,  1 ,  2 }
 
8-Nov-2017cyclispthon 28378 A cycle is a path starting and ending at its first vertex. (Contributed by Alexander van der Vekens, 8-Nov-2017.)
 |-  ( F ( V Cycles  E ) P  ->  F ( ( P `  0
 ) ( V PathOn  E ) ( P `  0 ) ) P )
 
8-Nov-2017ispthon 28362 Properties of a pair of functions to be a path between two given vertices(in an undirected graph). (Contributed by Alexander van der Vekens, 8-Nov-2017.)
 |-  (
 ( ( V  e.  X  /\  E  e.  Y )  /\  ( F  e.  W  /\  P  e.  Z )  /\  ( A  e.  V  /\  B  e.  V ) )  ->  ( F ( A ( V PathOn  E ) B ) P  <->  ( F ( A ( V WalkOn  E ) B ) P  /\  F ( V Paths  E ) P ) ) )
 
8-Nov-2017pthon 28361 The set of paths between two vertices (in an undirected graph). (Contributed by Alexander van der Vekens, 8-Nov-2017.)
 |-  (
 ( ( V  e.  X  /\  E  e.  Y )  /\  ( A  e.  V  /\  B  e.  V ) )  ->  ( A ( V PathOn  E ) B )  =  { <. f ,  p >.  |  ( f ( A ( V WalkOn  E ) B ) p  /\  f ( V Paths  E ) p ) } )
 
7-Nov-2017usgrcyclnl1 28386 In an undirected simple graph (with no loops!) there are no cycles with length 1 (consisting of one edge ). (Contributed by Alexander van der Vekens, 7-Nov-2017.)
 |-  (
 ( V USGrph  E  /\  F ( V Cycles  E ) P )  ->  ( # `
  F )  =/=  1 )
 
7-Nov-2017cycliswlk 28377 A cycle is a walk. (Contributed by Alexander van der Vekens, 7-Nov-2017.)
 |-  ( F ( V Cycles  E ) P  ->  F ( V Walks  E ) P )
 
7-Nov-2017usgrnloop 28351 In an undirected simple graph, each walk has no loops! (Contributed by Alexander van der Vekens, 7-Nov-2017.)
 |-  (
 ( V USGrph  E  /\  F ( V Walks  E ) P )  ->  A. k  e.  ( 0..^ ( # `  F ) ) ( P `  k )  =/=  ( P `  ( k  +  1
 ) ) )
 
7-Nov-2017iblabsnc 25015 Choice-free analogue of iblabs 19199. As with ibladdnc 25008, a measurability hypothesis is needed. (Contributed by Brendan Leahy, 7-Nov-2017.)
 |-  (
 ( ph  /\  x  e.  A )  ->  B  e.  V )   &    |-  ( ph  ->  ( x  e.  A  |->  B )  e.  L ^1 )   &    |-  ( ph  ->  ( x  e.  A  |->  ( abs `  B )
 )  e. MblFn )   =>    |-  ( ph  ->  ( x  e.  A  |->  ( abs `  B ) )  e.  L ^1 )
 
7-Nov-2017iblabsnclem 25014 Lemma for iblabsnc 25015; cf. iblabslem 19198. (Contributed by Brendan Leahy, 7-Nov-2017.)
 |-  (
 ( ph  /\  x  e.  A )  ->  B  e.  V )   &    |-  ( ph  ->  ( x  e.  A  |->  B )  e.  L ^1 )   &    |-  G  =  ( x  e.  RR  |->  if ( x  e.  A ,  ( abs `  ( F `  B ) ) ,  0 ) )   &    |-  ( ph  ->  ( x  e.  A  |->  ( F `  B ) )  e.  L ^1 )   &    |-  (
 ( ph  /\  x  e.  A )  ->  ( F `  B )  e. 
 RR )   =>    |-  ( ph  ->  ( G  e. MblFn  /\  ( S.2 `  G )  e.  RR ) )
 
7-Nov-2017itgaddnclem1 25009 Lemma for itgaddnc 25011; cf. itgaddlem1 19193. (Contributed by Brendan Leahy, 7-Nov-2017.)
 |-  (
 ( ph  /\  x  e.  A )  ->  B  e.  V )   &    |-  ( ph  ->  ( x  e.  A  |->  B )  e.  L ^1 )   &    |-  ( ( ph  /\  x  e.  A ) 
 ->  C  e.  V )   &    |-  ( ph  ->  ( x  e.  A  |->  C )  e.  L ^1 )   &    |-  ( ph  ->  ( x  e.  A  |->  ( B  +  C ) )  e. MblFn
 )   &    |-  ( ( ph  /\  x  e.  A )  ->  B  e.  RR )   &    |-  ( ( ph  /\  x  e.  A ) 
 ->  C  e.  RR )   &    |-  (
 ( ph  /\  x  e.  A )  ->  0  <_  B )   &    |-  ( ( ph  /\  x  e.  A ) 
 ->  0  <_  C )   =>    |-  ( ph  ->  S. A ( B  +  C )  _d x  =  ( S. A B  _d x  +  S. A C  _d x ) )
 
6-Nov-2017bi123imp0 28560 Similar to 3imp 1145 except all implications are biconditionals. (Contributed by Alan Sare, 6-Nov-2017.)
 |-  ( ph 
 <->  ( ps  <->  ( ch  <->  th ) ) )   =>    |-  ( ( ph  /\  ps  /\ 
 ch )  ->  th )
 
6-Nov-2017bi23imp1 28559 Similar to 3imp 1145 except all but outermost implication are biconditionals. (Contributed by Alan Sare, 6-Nov-2017.)
 |-  ( ph  ->  ( ps  <->  ( ch  <->  th ) ) )   =>    |-  ( ( ph  /\  ps  /\ 
 ch )  ->  th )
 
6-Nov-2017bi12imp3 28558 Similar to 3imp 1145 except all but innermost implication are biconditionals. (Contributed by Alan Sare, 6-Nov-2017.)
 |-  ( ph 
 <->  ( ps  <->  ( ch  ->  th ) ) )   =>    |-  ( ( ph  /\ 
 ps  /\  ch )  ->  th )
 
6-Nov-2017bi13imp2 28557 Similar to 3imp 1145 except the outermost and innermost implications are biconditionals. (Contributed by Alan Sare, 6-Nov-2017.)
 |-  ( ph 
 <->  ( ps  ->  ( ch 
 <-> 
 th ) ) )   =>    |-  ( ( ph  /\  ps  /\ 
 ch )  ->  th )
 
6-Nov-2017bi13imp23 28556 3imp 1145 with outermost implication of the hypothesis a biconditional. (Contributed by Alan Sare, 6-Nov-2017.)
 |-  ( ph 
 <->  ( ps  ->  ( ch  ->  th ) ) )   =>    |-  ( ( ph  /\  ps  /\ 
 ch )  ->  th )
 
6-Nov-2017bi23imp13 28555 3imp 1145 with middle implication of the hypothesis a biconditional. (Contributed by Alan Sare, 6-Nov-2017.)
 |-  ( ph  ->  ( ps  <->  ( ch  ->  th ) ) )   =>    |-  ( ( ph  /\ 
 ps  /\  ch )  ->  th )
 
6-Nov-2017bi33imp12 28554 3imp 1145 with innermost implication of the hypothesis a biconditional. (Contributed by Alan Sare, 6-Nov-2017.)
 |-  ( ph  ->  ( ps  ->  ( ch  <->  th ) ) )   =>    |-  ( ( ph  /\  ps  /\ 
 ch )  ->  th )
 
6-Nov-2017bi123impia 28553 3impia 1148 with the implications of the hypothesis biconditionals. (Contributed by Alan Sare, 6-Nov-2017.)
 |-  (
 ( ph  /\  ps )  <->  ( ch  <->  th ) )   =>    |-  ( ( ph  /\ 
 ps  /\  ch )  ->  th )
 
6-Nov-2017bi13impia 28552 3impia 1148 with the outer implication of the hypothesis a biconditional. (Contributed by Alan Sare, 6-Nov-2017.)
 |-  (
 ( ph  /\  ps )  <->  ( ch  ->  th )
 )   =>    |-  ( ( ph  /\  ps  /\ 
 ch )  ->  th )
 
6-Nov-2017bi123impib 28551 3impib 1149 with the implications of the hypothesis biconditionals. (Contributed by Alan Sare, 6-Nov-2017.)
 |-  ( ph 
 <->  ( ( ps  /\  ch )  <->  th ) )   =>    |-  ( ( ph  /\ 
 ps  /\  ch )  ->  th )
 
6-Nov-2017bi13impib 28550 3impib 1149 with the outer implication of the hypothesis a biconditional. (Contributed by Alan Sare, 6-Nov-2017.)
 |-  ( ph 
 <->  ( ( ps  /\  ch )  ->  th )
 )   =>    |-  ( ( ph  /\  ps  /\ 
 ch )  ->  th )
 
6-Nov-2017bi23impib 28549 3impib 1149 with the inner implication of the hypothesis a biconditional. (Contributed by Alan Sare, 6-Nov-2017.)
 |-  ( ph  ->  ( ( ps 
 /\  ch )  <->  th ) )   =>    |-  ( ( ph  /\ 
 ps  /\  ch )  ->  th )
 
6-Nov-2017bi3impa 28548 Similar to 3impa 1146 with implication in hypothesis replaced by biconditional. (Contributed by Alan Sare, 6-Nov-2017.)
 |-  (
 ( ( ph  /\  ps )  /\  ch )  <->  th )   =>    |-  ( ( ph  /\  ps  /\ 
 ch )  ->  th )
 
6-Nov-2017bi3impb 28547 Similar to 3impb 1147 with implication in hypothesis replaced by biconditional. (Contributed by Alan Sare, 6-Nov-2017.)
 |-  (
 ( ph  /\  ( ps 
 /\  ch ) )  <->  th )   =>    |-  ( ( ph  /\  ps  /\ 
 ch )  ->  th )
 
6-Nov-2017bi2imp 28546 Importation inference similar to imp 418, except the both implications of the hypothesis are biconditionals. (Contributed by Alan Sare, 6-Nov-2017.)
 |-  ( ph 
 <->  ( ps  <->  ch ) )   =>    |-  ( ( ph  /\ 
 ps )  ->  ch )
 
6-Nov-2017biimp 28545 Importation inference similar to imp 418, except the outermost implication of the hypothesis is a biconditional. (Contributed by Alan Sare, 6-Nov-2017.)
 |-  ( ph 
 <->  ( ps  ->  ch )
 )   =>    |-  ( ( ph  /\  ps )  ->  ch )
 
6-Nov-2017bddiblnc 25021 Choice-free proof of bddibl 19210. (Contributed by Brendan Leahy, 2-Nov-2017.) (Revised by Brendan Leahy, 6-Nov-2017.)
 |-  (
 ( F  e. MblFn  /\  ( vol `  dom  F )  e.  RR  /\  E. x  e.  RR  A. y  e.  dom  F ( abs `  ( F `  y
 ) )  <_  x )  ->  F  e.  L ^1 )
 
5-Nov-2017trlonwlkon 28342 A trail between two vertices is a walk between these vertices. (Contributed by Alexander van der Vekens, 5-Nov-2017.)
 |-  ( F ( A ( V TrailOn  E ) B ) P  ->  F ( A ( V WalkOn  E ) B ) P )
 
5-Nov-2017trlonprop 28341 A trail between two vertices is a walk between these vertices. (Contributed by Alexander van der Vekens, 5-Nov-2017.)
 |-  ( F ( A ( V TrailOn  E ) B ) P  ->  ( (
 ( V  e.  _V  /\  E  e.  _V )  /\  ( F  e.  _V  /\  P  e.  _V )  /\  ( A  e.  V  /\  B  e.  V ) )  /\  ( F ( A ( V WalkOn  E ) B ) P  /\  F ( V Trails  E ) P ) ) )
 
5-Nov-2017brabv 28193 If two classes are in a relationship given by an ordered-pair class abstraction, the classes are sets. (Contributed by Alexander van der Vekens, 5-Nov-2017.)
 |-  ( X { <. x ,  y >.  |  ph } Y  ->  ( X  e.  _V  /\  Y  e.  _V )
 )
 
5-Nov-20170neqopab 28192 The empty set is never an element in an ordered-pair class abstraction. (Contributed by Alexander van der Vekens, 5-Nov-2017.)
 |-  -.  (/) 
 e.  { <. x ,  y >.  |  ph }
 
4-Nov-2017trlon 28339 The set of trails between two vertices (in an undirected graph). (Contributed by Alexander van der Vekens, 4-Nov-2017.)
 |-  (
 ( ( V  e.  X  /\  E  e.  Y )  /\  ( A  e.  V  /\  B  e.  V ) )  ->  ( A ( V TrailOn  E ) B )  =  { <. f ,  p >.  |  ( f ( A ( V WalkOn  E ) B ) p  /\  f ( V Trails  E ) p ) } )
 
3-Nov-2017istrlon 28340 Properties of a pair of functions to be a trail between two given vertices(in an undirected graph). (Contributed by Alexander van der Vekens, 3-Nov-2017.)
 |-  (
 ( ( V  e.  X  /\  E  e.  Y )  /\  ( F  e.  W  /\  P  e.  Z )  /\  ( A  e.  V  /\  B  e.  V ) )  ->  ( F ( A ( V TrailOn  E ) B ) P  <->  ( F ( A ( V WalkOn  E ) B ) P  /\  F ( V Trails  E ) P ) ) )
 
3-Nov-2017jaoi2 28176 If one part of a disjunction is already true, the other part can be true only if the first part is false. (Contributed by Alexander van der Vekens, 3-Nov-2017.)
 |-  (
 ( ph  \/  ( -.  ph  /\  ch )
 )  ->  ps )   =>    |-  (
 ( ph  \/  ch )  ->  ps )
 
2-Nov-2017wlkonwlk 28334 A walk is a walk between its endpoints. (Contributed by Alexander van der Vekens, 2-Nov-2017.)
 |-  ( F ( V Walks  E ) P  ->  F ( ( P `  0
 ) ( V WalkOn  E ) ( P `  ( # `  F ) ) ) P )
 
2-Nov-2017iswlkon 28332 Properties of a pair of functions to be a walk between two given vertices (in an undirected graph). (Contributed by Alexander van der Vekens, 2-Nov-2017.)
 |-  (
 ( ( V  e.  X  /\  E  e.  Y )  /\  ( F  e.  W  /\  P  e.  Z )  /\  ( A  e.  V  /\  B  e.  V ) )  ->  ( F ( A ( V WalkOn  E ) B ) P  <->  ( F ( V Walks  E ) P 
 /\  ( P `  0 )  =  A  /\  ( P `  ( # `
  F ) )  =  B ) ) )
 
2-Nov-2017cnicciblnc 25022 Choice-free proof of cniccibl 19211. (Contributed by Brendan Leahy, 2-Nov-2017.)
 |-  (
 ( A  e.  RR  /\  B  e.  RR  /\  F  e.  ( ( A [,] B ) -cn-> CC ) )  ->  F  e.  L ^1 )
 
1-Nov-2017redwlk 28364 A walk ending at the last but one vertex of the walk is a walk. (Contributed by Alexander van der Vekens, 1-Nov-2017.)
 |-  (
 ( F ( V Walks  E ) P  /\  1  <_  ( # `  F ) )  ->  ( F  |`  ( 0..^ ( ( # `  F )  -  1 ) ) ) ( V Walks  E ) ( P  |`  ( 0..^ ( # `  F ) ) ) )
 
1-Nov-2017redwlklem 28363 Lemma for redwlk 28364. (Contributed by Alexander van der Vekens, 1-Nov-2017.)
 |-  (
 ( F ( V Walks  E ) P  /\  1  <_  ( # `  F ) )  ->  ( # `  ( F  |`  ( 0..^ ( ( # `  F )  -  1 ) ) ) )  =  ( ( # `  F )  -  1 ) )
 
1-Nov-2017wlkres 28331 Restrictions of walks are sets. (Contributed by Alexander van der Vekens, 1-Nov-2017.)
 |-  (
 f ( V W E ) p  ->  f ( V Walks  E ) p )   =>    |-  ( ( V  e.  _V 
 /\  E  e.  _V )  ->  { <. f ,  p >.  |  (
 f ( V W E ) p  /\  ph ) }  e.  _V )
 
1-Nov-2017fzossrbm1 28209 Subset of a half open range. (Contributed by Alexander van der Vekens, 1-Nov-2017.)
 |-  ( N  e.  NN0  ->  (
 0..^ ( N  -  1 ) )  C_  ( 0..^ N ) )
 
1-Nov-2017opabbrex 28191 A collection of ordered pairs with an extension of a binary relation is a set. (Contributed by Alexander van der Vekens, 1-Nov-2017.)
 |-  (
 ( V  e.  _V  /\  E  e.  _V )  ->  ( f ( V W E ) p 
 ->  th ) )   &    |-  (
 ( V  e.  _V  /\  E  e.  _V )  ->  { <. f ,  p >.  |  th }  e.  _V )   =>    |-  ( ( V  e.  _V 
 /\  E  e.  _V )  ->  { <. f ,  p >.  |  (
 f ( V W E ) p  /\  ps ) }  e.  _V )
 
1-Nov-2017ibladdnc 25008 Choice-free analogue of itgadd 19195. A measurability hypothesis is necessitated by the loss of mbfadd 19032; for large classes of functions, such as continuous functions, it should be relatively easy to show. (Contributed by Brendan Leahy, 1-Nov-2017.)
 |-  (
 ( ph  /\  x  e.  A )  ->  B  e.  V )   &    |-  ( ph  ->  ( x  e.  A  |->  B )  e.  L ^1 )   &    |-  ( ( ph  /\  x  e.  A ) 
 ->  C  e.  V )   &    |-  ( ph  ->  ( x  e.  A  |->  C )  e.  L ^1 )   &    |-  ( ph  ->  ( x  e.  A  |->  ( B  +  C ) )  e. MblFn
 )   =>    |-  ( ph  ->  ( x  e.  A  |->  ( B  +  C ) )  e.  L ^1 )
 
31-Oct-2017pthdepisspth 28360 A path with different start end end points is a simple path (in an undirected graph). (Contributed by Alexander van der Vekens, 31-Oct-2017.)
 |-  (
 ( F ( V Paths  E ) P  /\  ( P `  0 )  =/=  ( P `  ( # `  F ) ) )  ->  F ( V SPaths  E ) P )
 
31-Oct-2017wlkbprop 28333 Basic properties of a walk. (Contributed by Alexander van der Vekens, 31-Oct-2017.)
 |-  ( F ( V Walks  E ) P  ->  ( ( # `  F )  e. 
 NN0  /\  ( V  e.  _V 
 /\  E  e.  _V )  /\  ( F  e.  _V 
 /\  P  e.  _V ) ) )
 
31-Oct-2017injresinj 28215 A function whose restriction is injective and the values of the remaining arguments are different from all other values is injective itself. (Contributed by Alexander van der Vekens, 31-Oct-2017.)
 |-  ( K  e.  NN0  ->  (
 ( F : ( 0 ... K ) --> V  /\  Fun  `' ( F  |`  ( 1..^ K ) )  /\  ( F `  0 )  =/=  ( F `  K ) )  ->  ( ( ( F
 " { 0 ,  K } )  i^i  ( F " (
 1..^ K ) ) )  =  (/)  ->  Fun  `' F ) ) )
 
31-Oct-2017injresinjlem 28214 Lemma for injresinj 28215. (Contributed by Alexander van der Vekens, 31-Oct-2017.)
 |-  ( -.  y  e.  (
 1..^ K )  ->  ( ( F `  0 )  =/=  ( F `  K )  ->  ( ( F :
 ( 0 ... K )
 --> V  /\  K  e.  NN0 )  ->  ( (
 ( F " {
 0 ,  K }
 )  i^i  ( F " ( 1..^ K ) ) )  =  (/)  ->  ( ( x  e.  ( 0 ... K )  /\  y  e.  (
 0 ... K ) ) 
 ->  ( ( F `  x )  =  ( F `  y )  ->  x  =  y )
 ) ) ) ) )
 
31-Oct-2017elfznelfzo 28213 A value in a finite set of sequential integers is a border value if it is not contained in the half-open integer range contained in the finite set of sequential integerss. (Contributed by Alexander van der Vekens, 31-Oct-2017.)
 |-  (
 ( y  e.  (
 0 ... K )  /\  -.  y  e.  ( 1..^ K ) )  ->  ( y  =  0  \/  y  =  K ) )
 
31-Oct-2017ibladdnclem 25007 Lemma for ibladdnc 25008; cf ibladdlem 19190, whose fifth hypothesis is rendered unnecessary by the weakened hypotheses of itg2addnc 25005. (Contributed by Brendan Leahy, 31-Oct-2017.)
 |-  (
 ( ph  /\  x  e.  A )  ->  B  e.  RR )   &    |-  ( ( ph  /\  x  e.  A ) 
 ->  C  e.  RR )   &    |-  (
 ( ph  /\  x  e.  A )  ->  D  =  ( B  +  C ) )   &    |-  ( ph  ->  ( x  e.  A  |->  B )  e. MblFn )   &    |-  ( ph  ->  (
 S.2 `  ( x  e.  RR  |->  if ( ( x  e.  A  /\  0  <_  B ) ,  B ,  0 ) ) )  e.  RR )   &    |-  ( ph  ->  ( S.2 `  ( x  e.  RR  |->  if (
 ( x  e.  A  /\  0  <_  C ) ,  C ,  0 ) ) )  e. 
 RR )   =>    |-  ( ph  ->  ( S.2 `  ( x  e. 
 RR  |->  if ( ( x  e.  A  /\  0  <_  D ) ,  D ,  0 ) ) )  e.  RR )
 
31-Oct-2017itg2addnc 25005 Alternate proof of itg2add 19130 using the "buffer zone" definition from the first lemma, in which every simple function in the set is divided into to by dividing its buffer by a third and finding the largest allowable function locked to a grid laid out in increments of the new, smaller buffer up to the original simple function. The measurability of this function follows from that of the augend, and subtracting it from the original simple function yields another simple function by i1fsub 19079, which is allowable by the fact that the grid must have a mark between one third and two thirds the original buffer. This has two advantages over the current approach: first, eliminating ax-cc 8077, and second, weakening the measurability hypothesis to only the augend. (Contributed by Brendan Leahy, 31-Oct-2017.)
 |-  ( ph  ->  F  e. MblFn )   &    |-  ( ph  ->  F : RR --> ( 0 [,)  +oo ) )   &    |-  ( ph  ->  (
 S.2 `  F )  e.  RR )   &    |-  ( ph  ->  G : RR --> ( 0 [,)  +oo ) )   &    |-  ( ph  ->  ( S.2 `  G )  e.  RR )   =>    |-  ( ph  ->  ( S.2 `  ( F  o F  +  G ) )  =  (
 ( S.2 `  F )  +  ( S.2 `  G ) ) )
 
30-Oct-2017hbaew5AUX7 29619 Weak version of hbae 1906 not requiring ax-7 1720. (Contributed by NM, 30-Oct-2017.)
 |-  ( A. u  u  =  v  ->  ( A. x  x  =  y  ->  A. z A. x  x  =  y ) )
 
30-Oct-2017hbaew4AUX7 29618 Weak version of hbae 1906 not requiring ax-7 1720. (Contributed by NM, 30-Oct-2017.)
 |-  ( A. x  x  =  z  ->  ( A. x  x  =  y  ->  A. z A. x  x  =  y ) )
 
30-Oct-2017hbaew3AUX7 29499 Weak version of hbae 1906 not requiring ax-7 1720. Has different distinct variable requirements from hbaewAUX7 29455. (Contributed by NM, 30-Oct-2017.)
 |-  ( A. x  x  =  y  ->  A. z A. x  x  =  y )
 
30-Oct-2017hbaew2AUX7 29456 Weak version of hbae 1906 not requiring ax-7 1720. Different distinct variable requirements from hbaewAUX7 29455. (Contributed by NM, 30-Oct-2017.)
 |-  ( A. x  x  =  y  ->  A. z A. x  x  =  y )
 
30-Oct-2017cyclnspth 28376 A (non trivial) cycle is not a simple path. (Contributed by Alexander van der Vekens, 30-Oct-2017.)
 |-  ( F  =/=  (/)  ->  ( F ( V Cycles  E ) P 
 ->  -.  F ( V SPaths  E ) P ) )
 
30-Oct-2017cycliscrct 28375 A cycle is a circuit. (Contributed by Alexander van der Vekens, 30-Oct-2017.)
 |-  ( F ( V Cycles  E ) P  ->  F ( V Circuits  E ) P )
 
30-Oct-2017cyclispth 28374 A cycle is a path. (Contributed by Alexander van der Vekens, 30-Oct-2017.)
 |-  ( F ( V Cycles  E ) P  ->  F ( V Paths  E ) P )
 
30-Oct-2017crctistrl 28373 A circuit is a trail. (Contributed by Alexander van der Vekens, 30-Oct-2017.)
 |-  ( F ( V Circuits  E ) P  ->  F ( V Trails  E ) P )
 
30-Oct-20170cycl 28372 A pair of an empty set (of edges) and a second set (of vertices) is a cycle if and only if the second set contains exactly one vertex (in an undirected graph). (Contributed by Alexander van der Vekens, 30-Oct-2017.)
 |-  (
 ( ( V  e.  X  /\  E  e.  Y )  /\  P  e.  Z )  ->  ( (/) ( V Cycles  E ) P  <->  P : ( 0
 ... 0 ) --> V ) )
 
30-Oct-20170crct 28371 A pair of an empty set (of edges) and a second set (of vertices) is a circuit if and only if the second set contains exactly one vertex (in an undirected graph). (Contributed by Alexander van der Vekens, 30-Oct-2017.)
 |-  (
 ( ( V  e.  X  /\  E  e.  Y )  /\  P  e.  Z )  ->  ( (/) ( V Circuits  E ) P  <->  P : ( 0
 ... 0 ) --> V ) )
 
30-Oct-2017iscycl 28370 Properties of a pair of functions to be a cycle (in an undirected graph). (Contributed by Alexander van der Vekens, 30-Oct-2017.)
 |-  (
 ( ( V  e.  X  /\  E  e.  Y )  /\  ( F  e.  W  /\  P  e.  Z ) )  ->  ( F ( V Cycles  E ) P 
 <->  ( F ( V Paths  E ) P  /\  ( P `  0 )  =  ( P `  ( # `  F ) ) ) ) )
 
30-Oct-2017iscrct 28369 Properties of a pair of functions to be a circuit (in an undirected graph). (Contributed by Alexander van der Vekens, 30-Oct-2017.)
 |-  (
 ( ( V  e.  X  /\  E  e.  Y )  /\  ( F  e.  W  /\  P  e.  Z ) )  ->  ( F ( V Circuits  E ) P 
 <->  ( F ( V Trails  E ) P  /\  ( P `  0 )  =  ( P `  ( # `  F ) ) ) ) )
 
30-Oct-2017cycls 28368 The set of cycles (in an undirected graph). (Contributed by Alexander van der Vekens, 30-Oct-2017.)
 |-  (
 ( V  e.  X  /\  E  e.  Y ) 
 ->  ( V Cycles  E )  =  { <. f ,  p >.  |  ( f ( V Paths  E ) p 
 /\  ( p `  0 )  =  ( p `  ( # `  f
 ) ) ) }
 )
 
30-Oct-2017crcts 28367 The set of circuits (in an undirected graph). (Contributed by Alexander van der Vekens, 30-Oct-2017.)
 |-  (
 ( V  e.  X  /\  E  e.  Y ) 
 ->  ( V Circuits  E )  =  { <. f ,  p >.  |  ( f ( V Trails  E ) p  /\  ( p `  0 )  =  ( p `  ( # `  f ) ) ) } )
 
30-Oct-20170spth 28357 A pair of an empty set (of edges) and a second set (of vertices) is a simple path if and only if the second set contains exactly one vertex (in an undirected graph). (Contributed by Alexander van der Vekens, 30-Oct-2017.)
 |-  (
 ( ( V  e.  X  /\  E  e.  Y )  /\  P  e.  Z )  ->  ( (/) ( V SPaths  E ) P  <->  P : ( 0
 ... 0 ) --> V ) )
 
30-Oct-20170pth 28356 A pair of an empty set (of edges) and a second set (of vertices) is a path if and only if the second set contains exactly one vertex (in an undirected graph). (Contributed by Alexander van der Vekens, 30-Oct-2017.)
 |-  (
 ( ( V  e.  X  /\  E  e.  Y )  /\  P  e.  Z )  ->  ( (/) ( V Paths  E ) P  <->  P : ( 0
 ... 0 ) --> V ) )
 
30-Oct-20170trl 28344 A pair of an empty set (of edges) and a second set (of vertices) is a trail if and only if the second set contains exactly one vertex (in an undirected graph). (Contributed by Alexander van der Vekens, 30-Oct-2017.)
 |-  (
 ( ( V  e.  X  /\  E  e.  Y )  /\  P  e.  Z )  ->  ( (/) ( V Trails  E ) P  <->  P : ( 0
 ... 0 ) --> V ) )
 
30-Oct-20170wlk 28343 A pair of an empty set (of edges) and a second set (of vertices) is a walk if and only if the second set contains exactly one vertex (in an undirected graph). (Contributed by Alexander van der Vekens, 30-Oct-2017.)
 |-  (
 ( ( V  e.  X  /\  E  e.  Y )  /\  P  e.  Z )  ->  ( (/) ( V Walks  E ) P  <->  P : ( 0
 ... 0 ) --> V ) )
 
30-Oct-2017fzon 28212 A half-open set of sequential integers is empty if the bounds are equal or reversed. (Contributed by Alexander van der Vekens, 30-Oct-2017.)
 |-  (
 ( M  e.  ZZ  /\  N  e.  ZZ )  ->  ( N  <_  M  <->  ( M..^ N )  =  (/) ) )
 
30-Oct-2017isprmpt2 28208 Properties of a pair in an extended binary relation. (Contributed by Alexander van der Vekens, 30-Oct-2017.)
 |-  ( ph  ->  M  =  { <. f ,  p >.  |  ( f W p 
 /\  ps ) } )   &    |-  (
 ( f  =  F  /\  p  =  P )  ->  ( ps  <->  ch ) )   =>    |-  ( ph  ->  ( ( F  e.  X  /\  P  e.  Y ) 
 ->  ( F M P  <->  ( F W P  /\  ch ) ) ) )
 
30-Oct-2017sprmpt2 28207 The extension of a binary relation which is the value of an operation given in maps-to notation. (Contributed by Alexander van der Vekens, 30-Oct-2017.)
 |-  M  =  ( v  e.  _V ,  e  e.  _V  |->  {
 <. f ,  p >.  |  ( f ( v W e ) p 
 /\  ch ) } )   &    |-  (
 ( v  =  V  /\  e  =  E )  ->  ( ch  <->  ps ) )   &    |-  (
 ( V  e.  _V  /\  E  e.  _V )  ->  ( f ( V W E ) p 
 ->  th ) )   &    |-  (
 ( V  e.  _V  /\  E  e.  _V )  ->  { <. f ,  p >.  |  th }  e.  _V )   =>    |-  ( ( V  e.  _V 
 /\  E  e.  _V )  ->  ( V M E )  =  { <. f ,  p >.  |  ( f ( V W E ) p 
 /\  ps ) } )
 
29-Oct-2017hbaew0AUX7 29617 Weak version of hbae 1906 not requiring ax-7 1720. (Contributed by NM, 29-Oct-2017.)
 |-  ( A. x  x  =  y  ->  A. z  x  =  y )
 
29-Oct-2017ax12olem3aAUX7 29434 Lemma for ax12o 1887. Show the equivalence of an intermediate equivalent to ax12o 1887 with the conjunction of ax-12 1878 and a variant with negated equalities. (Contributed by NM, 29-Oct-2017.)
 |-  (
 ( ph  ->  ( -. 
 A. x  -.  ps  ->  A. y ps )
 ) 
 <->  ( ( ph  ->  ( ps  ->  A. y ps ) )  /\  ( ph  ->  ( -.  ps  ->  A. x  -.  ps ) ) ) )
 
29-Oct-2017itg2addnclem2 25004 Lemma for itg2addnc 25005. The function described is a simple function. (Contributed by Brendan Leahy, 29-Oct-2017.)
 |-  ( ph  ->  F  e. MblFn )   &    |-  ( ph  ->  F : RR --> ( 0 [,)  +oo ) )   =>    |-  ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  ->  ( x  e. 
 RR  |->  if ( ( ( ( ( |_ `  (
 ( F `  x )  /  ( v  / 
 3 ) ) )  -  1 )  x.  ( v  /  3
 ) )  <_  ( h `  x )  /\  ( h `  x )  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  (
 v  /  3 )
 ) )  -  1
 )  x.  ( v 
 /  3 ) ) ,  ( h `  x ) ) )  e.  dom  S.1 )
 
28-Oct-2017sbhbwAUX7 29579 Weak version of sbhb 2059 not requiring ax-7 1720. (Contributed by NM, 28-Oct-2017.)
 |-  (
 ( ph  ->  A. x ph )  <->  A. y ( ph  ->  [ y  /  x ] ph ) )
 
28-Oct-2017sb8ewAUX7 29566 Weak version of sb8e 2046 not requiring ax-7 1720. (Contributed by NM, 28-Oct-2017.)
 |-  F/ y ph   =>    |-  ( E. x ph  <->  E. y [ y  /  x ] ph )
 
28-Oct-2017sb8wAUX7 29565 Weak version of sb8 2045 not requiring ax-7 1720. (Contributed by NM, 28-Oct-2017.)
 |-  F/ y ph   =>    |-  ( A. x ph  <->  A. y [ y  /  x ] ph )
 
28-Oct-2017aevwAUX7 29497 Weak version of aev 1944 not requiring ax-7 1720. (Contributed by NM, 28-Oct-2017.)
 |-  ( A. x  x  =  y  ->  A. z  w  =  v )
 
28-Oct-2017cbvexwAUX7 29495 Weak version of cbvex 1938 not requiring ax-7 1720. (Contributed by NM, 28-Oct-2017.)
 |-  F/ y ph   &    |-  F/ x ps   &    |-  ( x  =  y  ->  (
 ph 
 <->  ps ) )   =>    |-  ( E. x ph  <->  E. y ps )
 
28-Oct-2017cbvalwwAUX7 29494 Weak version of cbval 1937 not requiring ax-7 1720. (Contributed by NM, 28-Oct-2017.)
 |-  F/ y ph   &    |-  F/ x ps   &    |-  ( x  =  y  ->  (
 ph 
 <->  ps ) )   =>    |-  ( A. x ph  <->  A. y ps )
 
28-Oct-2017cbv3hwAUX7 29493 Weak version of cbv3h 1936 not requiring ax-7 1720. (Contributed by NM, 28-Oct-2017.)
 |-  ( ph  ->  A. y ph )   &    |-  ( ps  ->  A. x ps )   &    |-  ( x  =  y  ->  (
 ph  ->  ps ) )   =>    |-  ( A. x ph 
 ->  A. y ps )
 
28-Oct-2017cbv3wAUX7 29492 Weak version of cbv3 1935 not requiring ax-7 1720. (Contributed by NM, 28-Oct-2017.)
 |-  F/ y ph   &    |-  F/ x ps   &    |-  ( x  =  y  ->  (
 ph  ->  ps ) )   =>    |-  ( A. x ph 
 ->  A. y ps )
 
28-Oct-2017cbv2wAUX7 29491 Weak version of cbv2 1934 not requiring ax-7 1720. (Contributed by NM, 28-Oct-2017.)
 |-  ( ph  ->  F/ y ps )   &    |-  ( ph  ->  F/ x ch )   &    |-  ( ph  ->  ( x  =  y  ->  ( ps  <->  ch ) ) )   =>    |-  ( A. x A. y ph  ->  ( A. x ps  <->  A. y ch )
 )
 
28-Oct-2017cbv2hwAUX7 29490 Weak version of cbv2h 1933 not requiring ax-7 1720. (Contributed by NM, 28-Oct-2017.)
 |-  ( ph  ->  ( ps  ->  A. y ps ) )   &    |-  ( ph  ->  ( ch  ->  A. x ch )
 )   &    |-  ( ph  ->  ( x  =  y  ->  ( ps  <->  ch ) ) )   =>    |-  ( A. x A. y ph  ->  ( A. x ps 
 <-> 
 A. y ch )
 )
 
28-Oct-2017cbv1wAUX7 29489 Weak version of cbv1 1932 not requiring ax-7 1720. (Contributed by NM, 28-Oct-2017.)
 |-  ( ph  ->  F/ y ps )   &    |-  ( ph  ->  F/ x ch )   &    |-  ( ph  ->  ( x  =  y  ->  ( ps  ->  ch ) ) )   =>    |-  ( A. x A. y ph  ->  ( A. x ps  ->  A. y ch )
 )
 
28-Oct-2017cbv1hwAUX7 29488 Weak version of cbv1h 1931 not requiring ax-7 1720. (Contributed by NM, 28-Oct-2017.)
 |-  ( ph  ->  ( ps  ->  A. y ps ) )   &    |-  ( ph  ->  ( ch  ->  A. x ch )
 )   &    |-  ( ph  ->  ( x  =  y  ->  ( ps  ->  ch )
 ) )   =>    |-  ( A. x A. y ph  ->  ( A. x ps  ->  A. y ch ) )
 
28-Oct-2017a7swAUX7 29422 Weak version of a7s 1721 not requiring ax-7 1720. (Contributed by NM, 28-Oct-2017.)
 |-  ( A. x A. y ph  ->  ps )   =>    |-  ( A. y A. x ph  ->  ps )
 
27-Oct-2017ax7w1hAUX7 29616 Weak version of hbal 1722 not requiring ax-7 1720. (Contributed by NM, 27-Oct-2017.)
 |-  ( A. x  x  =  y  ->  ( ph  ->  A. x ph ) )   =>    |-  ( A. x  x  =  y  ->  ( A. y ph  ->  A. x A. y ph ) )
 
27-Oct-2017sbcomwAUX7 29562 Weak version of sbcom 2042 not requiring ax-7 1720. (Contributed by NM, 27-Oct-2017.)
 |-  ( [ y  /  z ] [ y  /  x ] ph  <->  [ y  /  x ] [ y  /  z ] ph )
 
27-Oct-2017sbco3wAUX7 29561 Weak version of sbco3 2041 not requiring ax-7 1720. (Contributed by NM, 27-Oct-2017.)
 |-  ( [ z  /  y ] [ y  /  x ] ph  <->  [ z  /  x ] [ x  /  y ] ph )
 
27-Oct-2017sbco2dwAUX7 29560 Weak version of sbco2d 2040 not requiring ax-7 1720. (Contributed by NM, 27-Oct-2017.)
 |-  F/ x ph   &    |-  F/ z ph   &    |-  ( ph  ->  F/ z ps )   =>    |-  ( ph  ->  ( [ y  /  z ] [ z  /  x ] ps  <->  [ y  /  x ] ps ) )
 
27-Oct-2017sbco2wAUX7 29559 Weak version of sbco2 2039 not requiring ax-7 1720. (Contributed by NM, 27-Oct-2017.)
 |-  F/ z ph   =>    |-  ( [ y  /  z ] [ z  /  x ] ph  <->  [ y  /  x ] ph )
 
27-Oct-2017nfsb4wAUX7 29552 Weak version of nfsb4t 2033 not requiring ax-7 1720. (Contributed by NM, 27-Oct-2017.)
 |-  F/ z ph   =>    |-  ( -.  A. z  z  =  y  ->  F/ z [ y  /  x ] ph )
 
27-Oct-2017nfsb4twAUX7 29551 Weak version of nfsb4t 2033 not requiring ax-7 1720. (Contributed by NM, 27-Oct-2017.)
 |-  ( A. x F/ z ph  ->  ( -.  A. z  z  =  y  ->  F/ z [ y  /  x ] ph ) )
 
27-Oct-2017sbequ5wAUX7 29533 Weak version of sbequ5 1984 not requiring ax-7 1720. (Contributed by NM, 27-Oct-2017.)
 |-  ( [ w  /  z ] A. x  x  =  y  <->  A. x  x  =  y )
 
27-Oct-2017equs5bAUX7 29510 Lemma used in proofs of substitution properties. (Contributed by NM, 27-Oct-2017.)
 |-  ( -.  A. x  x  =  y  ->  ( E. x ( x  =  y  /\  ph )  <->  A. x ( x  =  y  ->  ph ) ) )
 
27-Oct-2017drnf2wAUX7 29475 Weak version of drnf2 1923 not requiring ax-7 1720. (Contributed by NM, 27-Oct-2017.)
 |-  ( A. x  x  =  y  ->  ( ph  <->  ps ) )   =>    |-  ( A. x  x  =  y  ->  ( F/ z ph  <->  F/ z ps )
 )
 
27-Oct-2017drex2wAUX7 29474 Weak version of drex2 1921 not requiring ax-7 1720. (Contributed by NM, 27-Oct-2017.)
 |-  ( A. x  x  =  y  ->  ( ph  <->  ps ) )   =>