P. 292 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 29101-29200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	iprodgam 29101*	An infinite product version of Euler's gamma function. (Contributed by Scott Fenton, 12-Feb-2018.)
|- ( ph -> A e. ( CC \ ( ZZ \ NN ) ) )   =>    |- ( ph -> ( _G ` A ) = ( prod_ k e. NN ( ( ( 1 + ( 1 / k ) ) ^c A ) / ( 1 + ( A / k ) ) ) / A ) )
21.8.7  Falling and Rising Factorial
Syntax	cfallfac 29102	Declare the syntax for the falling factorial.
class FallFac
Syntax	crisefac 29103	Declare the syntax for the rising factorial.
class RiseFac
Definition	df-risefac 29104*	Define the rising factorial function. This is the function ( A x. ( A + 1 ) x. ... ( A + N ) ) for complex A and nonnegative integers N. (Contributed by Scott Fenton, 5-Jan-2018.)
|- RiseFac = ( x e. CC , n e. NN0 |-> prod_ k e. ( 0 ... ( n - 1 ) ) ( x + k ) )
Definition	df-fallfac 29105*	Define the falling factorial function. This is the function ( A x. ( A - 1 ) x. ... ( A - N ) ) for complex A and nonnegative integers N. (Contributed by Scott Fenton, 5-Jan-2018.)
|- FallFac = ( x e. CC , n e. NN0 |-> prod_ k e. ( 0 ... ( n - 1 ) ) ( x - k ) )
Theorem	risefacval 29106*	The value of the rising factorial function. (Contributed by Scott Fenton, 5-Jan-2018.)
|- ( ( A e. CC /\ N e. NN0 ) -> ( A RiseFac N ) = prod_ k e. ( 0 ... ( N - 1 ) ) ( A + k ) )
Theorem	fallfacval 29107*	The value of the falling factorial function. (Contributed by Scott Fenton, 5-Jan-2018.)
|- ( ( A e. CC /\ N e. NN0 ) -> ( A FallFac N ) = prod_ k e. ( 0 ... ( N - 1 ) ) ( A - k ) )
Theorem	risefacval2 29108*	One-based value of rising factorial. (Contributed by Scott Fenton, 15-Jan-2018.)
|- ( ( A e. CC /\ N e. NN0 ) -> ( A RiseFac N ) = prod_ k e. ( 1 ... N ) ( A + ( k - 1 ) ) )
Theorem	fallfacval2 29109*	One-based value of falling factorial. (Contributed by Scott Fenton, 15-Jan-2018.)
|- ( ( A e. CC /\ N e. NN0 ) -> ( A FallFac N ) = prod_ k e. ( 1 ... N ) ( A - ( k - 1 ) ) )
Theorem	fallfacval3 29110*	A product representation of falling factorial when A is a nonnegative integer. (Contributed by Scott Fenton, 20-Mar-2018.)
|- ( N e. ( 0 ... A ) -> ( A FallFac N ) = prod_ k e. ( ( A - ( N - 1 ) ) ... A ) k )
Theorem	risefaccllem 29111*	Lemma for rising factorial closure laws. (Contributed by Scott Fenton, 5-Jan-2018.)
|- S C_ CC   &    |- 1 e. S   &    |- ( ( x e. S /\ y e. S ) -> ( x x. y ) e. S )   &    |- ( ( A e. S /\ k e. NN0 ) -> ( A + k ) e. S )   =>    |- ( ( A e. S /\ N e. NN0 ) -> ( A RiseFac N ) e. S )
Theorem	fallfaccllem 29112*	Lemma for falling factorial closure laws. (Contributed by Scott Fenton, 5-Jan-2018.)
|- S C_ CC   &    |- 1 e. S   &    |- ( ( x e. S /\ y e. S ) -> ( x x. y ) e. S )   &    |- ( ( A e. S /\ k e. NN0 ) -> ( A - k ) e. S )   =>    |- ( ( A e. S /\ N e. NN0 ) -> ( A FallFac N ) e. S )
Theorem	risefaccl 29113	Closure law for rising factorial. (Contributed by Scott Fenton, 5-Jan-2018.)
|- ( ( A e. CC /\ N e. NN0 ) -> ( A RiseFac N ) e. CC )
Theorem	fallfaccl 29114	Closure law for falling factorial. (Contributed by Scott Fenton, 5-Jan-2018.)
|- ( ( A e. CC /\ N e. NN0 ) -> ( A FallFac N ) e. CC )
Theorem	rerisefaccl 29115	Closure law for rising factorial. (Contributed by Scott Fenton, 5-Jan-2018.)
|- ( ( A e. RR /\ N e. NN0 ) -> ( A RiseFac N ) e. RR )
Theorem	refallfaccl 29116	Closure law for falling factorial. (Contributed by Scott Fenton, 5-Jan-2018.)
|- ( ( A e. RR /\ N e. NN0 ) -> ( A FallFac N ) e. RR )
Theorem	nnrisefaccl 29117	Closure law for rising factorial. (Contributed by Scott Fenton, 5-Jan-2018.)
|- ( ( A e. NN /\ N e. NN0 ) -> ( A RiseFac N ) e. NN )
Theorem	zrisefaccl 29118	Closure law for rising factorial. (Contributed by Scott Fenton, 5-Jan-2018.)
|- ( ( A e. ZZ /\ N e. NN0 ) -> ( A RiseFac N ) e. ZZ )
Theorem	zfallfaccl 29119	Closure law for falling factorial. (Contributed by Scott Fenton, 5-Jan-2018.)
|- ( ( A e. ZZ /\ N e. NN0 ) -> ( A FallFac N ) e. ZZ )
Theorem	nn0risefaccl 29120	Closure law for rising factorial. (Contributed by Scott Fenton, 5-Jan-2018.)
|- ( ( A e. NN0 /\ N e. NN0 ) -> ( A RiseFac N ) e. NN0 )
Theorem	rprisefaccl 29121	Closure law for rising factorial. (Contributed by Scott Fenton, 9-Jan-2018.)
|- ( ( A e. RR+ /\ N e. NN0 ) -> ( A RiseFac N ) e. RR+ )
Theorem	risefallfac 29122	A relationship between rising and falling factorials. (Contributed by Scott Fenton, 15-Jan-2018.)
|- ( ( X e. CC /\ N e. NN0 ) -> ( X RiseFac N ) = ( ( -u 1 ^ N ) x. ( -u X FallFac N ) ) )
Theorem	fallrisefac 29123	A relationship between falling and rising factorials. (Contributed by Scott Fenton, 17-Jan-2018.)
|- ( ( X e. CC /\ N e. NN0 ) -> ( X FallFac N ) = ( ( -u 1 ^ N ) x. ( -u X RiseFac N ) ) )
Theorem	risefall0lem 29124	Lemma for risefac0 29125 and fallfac0 29126. Show a particular set of finite integers is empty. (Contributed by Scott Fenton, 5-Jan-2018.)
|- ( 0 ... ( 0 - 1 ) ) = (/)
Theorem	risefac0 29125	The value of the rising factorial when N = 0. (Contributed by Scott Fenton, 5-Jan-2018.)
|- ( A e. CC -> ( A RiseFac 0 ) = 1 )
Theorem	fallfac0 29126	The value of the falling factorial when N = 0. (Contributed by Scott Fenton, 5-Jan-2018.)
|- ( A e. CC -> ( A FallFac 0 ) = 1 )
Theorem	risefacp1 29127	The value of the rising factorial at a successor. (Contributed by Scott Fenton, 5-Jan-2018.)
|- ( ( A e. CC /\ N e. NN0 ) -> ( A RiseFac ( N + 1 ) ) = ( ( A RiseFac N ) x. ( A + N ) ) )
Theorem	fallfacp1 29128	The value of the falling factorial at a successor. (Contributed by Scott Fenton, 5-Jan-2018.)
|- ( ( A e. CC /\ N e. NN0 ) -> ( A FallFac ( N + 1 ) ) = ( ( A FallFac N ) x. ( A - N ) ) )
Theorem	risefacp1d 29129	The value of the rising factorial at a successor. (Contributed by Scott Fenton, 19-Mar-2018.)
|- ( ph -> A e. CC )   &    |- ( ph -> N e. NN0 )   =>    |- ( ph -> ( A RiseFac ( N + 1 ) ) = ( ( A RiseFac N ) x. ( A + N ) ) )
Theorem	fallfacp1d 29130	The value of the falling factorial at a successor. (Contributed by Scott Fenton, 19-Mar-2018.)
|- ( ph -> A e. CC )   &    |- ( ph -> N e. NN0 )   =>    |- ( ph -> ( A FallFac ( N + 1 ) ) = ( ( A FallFac N ) x. ( A - N ) ) )
Theorem	risefac1 29131	The value of rising factorial at one. (Contributed by Scott Fenton, 5-Jan-2018.)
|- ( A e. CC -> ( A RiseFac 1 ) = A )
Theorem	fallfac1 29132	The value of falling factorial at one. (Contributed by Scott Fenton, 5-Jan-2018.)
|- ( A e. CC -> ( A FallFac 1 ) = A )
Theorem	risefacfac 29133	Relate rising factorial to factorial. (Contributed by Scott Fenton, 5-Jan-2018.)
|- ( N e. NN0 -> ( 1 RiseFac N ) = ( ! ` N ) )
Theorem	fallfacfwd 29134	The forward difference of a falling factorial. (Contributed by Scott Fenton, 21-Jan-2018.)
|- ( ( A e. CC /\ N e. NN ) -> ( ( ( A + 1 ) FallFac N ) - ( A FallFac N ) ) = ( N x. ( A FallFac ( N - 1 ) ) ) )
Theorem	0fallfac 29135	The value of the zero falling factorial at natural N. (Contributed by Scott Fenton, 17-Feb-2018.)
|- ( N e. NN -> ( 0 FallFac N ) = 0 )
Theorem	0risefac 29136	The value of the zero rising factorial at natural N. (Contributed by Scott Fenton, 17-Feb-2018.)
|- ( N e. NN -> ( 0 RiseFac N ) = 0 )
Theorem	binomfallfaclem1 29137	Lemma for binomfallfac 29139. Closure law. (Contributed by Scott Fenton, 13-Mar-2018.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> N e. NN0 )   =>    |- ( ( ph /\ K e. ( 0 ... N ) ) -> ( ( N _C K ) x. ( ( A FallFac ( N - K ) ) x. ( B FallFac ( K + 1 ) ) ) ) e. CC )
Theorem	binomfallfaclem2 29138*	Lemma for binomfallfac 29139. Inductive step. (Contributed by Scott Fenton, 13-Mar-2018.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> N e. NN0 )   &    |- ( ps -> ( ( A + B ) FallFac N ) = sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( A FallFac ( N - k ) ) x. ( B FallFac k ) ) ) )   =>    |- ( ( ph /\ ps ) -> ( ( A + B ) FallFac ( N + 1 ) ) = sum_ k e. ( 0 ... ( N + 1 ) ) ( ( ( N + 1 ) _C k ) x. ( ( A FallFac ( ( N + 1 ) - k ) ) x. ( B FallFac k ) ) ) )
Theorem	binomfallfac 29139*	A version of the binomial theorem using falling factorials instead of exponentials. (Contributed by Scott Fenton, 13-Mar-2018.)
|- ( ( A e. CC /\ B e. CC /\ N e. NN0 ) -> ( ( A + B ) FallFac N ) = sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( A FallFac ( N - k ) ) x. ( B FallFac k ) ) ) )
Theorem	binomrisefac 29140*	A version of the binomial theorem using rising factorials instead of exponentials. (Contributed by Scott Fenton, 16-Mar-2018.)
|- ( ( A e. CC /\ B e. CC /\ N e. NN0 ) -> ( ( A + B ) RiseFac N ) = sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( A RiseFac ( N - k ) ) x. ( B RiseFac k ) ) ) )
Theorem	fallfacval4 29141	Represent the falling factorial via factorials when the first argument is a natural. (Contributed by Scott Fenton, 20-Mar-2018.)
|- ( N e. ( 0 ... A ) -> ( A FallFac N ) = ( ( ! ` A ) / ( ! ` ( A - N ) ) ) )
Theorem	bcfallfac 29142	Binomial coefficient in terms of falling factorials. (Contributed by Scott Fenton, 20-Mar-2018.)
|- ( K e. ( 0 ... N ) -> ( N _C K ) = ( ( N FallFac K ) / ( ! ` K ) ) )
Theorem	fallfacfac 29143	Relate falling factorial to factorial. (Contributed by Scott Fenton, 5-Jan-2018.)
|- ( N e. NN0 -> ( N FallFac N ) = ( ! ` N ) )
21.8.8  Factorial limits
Theorem	faclimlem1 29144*	Lemma for faclim 29147. Closed form for a particular sequence. (Contributed by Scott Fenton, 15-Dec-2017.)
|- ( M e. NN0 -> seq 1 ( x. , ( n e. NN |-> ( ( ( 1 + ( M / n ) ) x. ( 1 + ( 1 / n ) ) ) / ( 1 + ( ( M + 1 ) / n ) ) ) ) ) = ( x e. NN |-> ( ( M + 1 ) x. ( ( x + 1 ) / ( x + ( M + 1 ) ) ) ) ) )
Theorem	faclimlem2 29145*	Lemma for faclim 29147. Show a limit for the inductive step. (Contributed by Scott Fenton, 15-Dec-2017.)
|- ( M e. NN0 -> seq 1 ( x. , ( n e. NN |-> ( ( ( 1 + ( M / n ) ) x. ( 1 + ( 1 / n ) ) ) / ( 1 + ( ( M + 1 ) / n ) ) ) ) ) ~~> ( M + 1 ) )
Theorem	faclimlem3 29146	Lemma for faclim 29147. Algebraic manipulation for the final induction. (Contributed by Scott Fenton, 15-Dec-2017.)
|- ( ( M e. NN0 /\ B e. NN ) -> ( ( ( 1 + ( 1 / B ) ) ^ ( M + 1 ) ) / ( 1 + ( ( M + 1 ) / B ) ) ) = ( ( ( ( 1 + ( 1 / B ) ) ^ M ) / ( 1 + ( M / B ) ) ) x. ( ( ( 1 + ( M / B ) ) x. ( 1 + ( 1 / B ) ) ) / ( 1 + ( ( M + 1 ) / B ) ) ) ) )
Theorem	faclim 29147*	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 ) )
Theorem	iprodfac 29148*	An infinite product expression for factorial. (Contributed by Scott Fenton, 15-Dec-2017.)
|- ( A e. NN0 -> ( ! ` A ) = prod_ k e. NN ( ( ( 1 + ( 1 / k ) ) ^ A ) / ( 1 + ( A / k ) ) ) )
Theorem	faclim2 29149*	Another factorial limit due to Euler. (Contributed by Scott Fenton, 17-Dec-2017.)
|- F = ( n e. NN |-> ( ( ( ! ` n ) x. ( ( n + 1 ) ^ M ) ) / ( ! ` ( n + M ) ) ) )   =>    |- ( M e. NN0 -> F ~~> 1 )
21.8.9  Greatest common divisor and divisibility
Theorem	pdivsq 29150	Condition for a prime dividing a square. (Contributed by Scott Fenton, 8-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|- ( ( P e. Prime /\ M e. ZZ ) -> ( P || M <-> P || ( M ^ 2 ) ) )
Theorem	dvdspw 29151	Exponentiation law for divisibility. (Contributed by Scott Fenton, 7-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|- ( ( K e. ZZ /\ M e. ZZ /\ N e. NN ) -> ( K || M -> K || ( M ^ N ) ) )
Theorem	gcd32 29152	Swap the second and third arguments of a gcd. (Contributed by Scott Fenton, 8-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|- ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> ( ( A gcd B ) gcd C ) = ( ( A gcd C ) gcd B ) )
Theorem	gcdabsorb 29153	Absorption law for gcd. (Contributed by Scott Fenton, 8-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|- ( ( A e. ZZ /\ B e. ZZ ) -> ( ( A gcd B ) gcd B ) = ( A gcd B ) )
21.8.10  Properties of relationships
Theorem	brtp 29154	A condition for a binary relation over an unordered triple. (Contributed by Scott Fenton, 8-Jun-2011.)
|- X e. _V   &    |- Y e. _V   =>    |- ( X { <. A , B >. , <. C , D >. , <. E , F >. } Y <-> ( ( X = A /\ Y = B ) \/ ( X = C /\ Y = D ) \/ ( X = E /\ Y = F ) ) )
Theorem	dftr6 29155	A potential definition of transitivity for sets. (Contributed by Scott Fenton, 18-Mar-2012.)
|- A e. _V   =>    |- ( Tr A <-> A e. ( _V \ ran ( ( _E o. _E ) \ _E ) ) )
Theorem	coep 29156*	Composition with epsilon. (Contributed by Scott Fenton, 18-Feb-2013.)
|- A e. _V   &    |- B e. _V   =>    |- ( A ( _E o. R ) B <-> E. x e. B A R x )
Theorem	coepr 29157*	Composition with the converse of epsilon. (Contributed by Scott Fenton, 18-Feb-2013.)
|- A e. _V   &    |- B e. _V   =>    |- ( A ( R o. `' _E ) B <-> E. x e. A x R B )
Theorem	dffr5 29158	A quantifier free definition of a well-founded relationship. (Contributed by Scott Fenton, 11-Apr-2011.)
|- ( R Fr A <-> ( ~P A \ { (/) } ) C_ ran ( _E \ ( _E o. `' R ) ) )
Theorem	dfso2 29159	Quantifier free definition of a strict order. (Contributed by Scott Fenton, 22-Feb-2013.)
|- ( R Or A <-> ( R Po A /\ ( A X. A ) C_ ( R u. ( _I u. `' R ) ) ) )
Theorem	dfpo2 29160	Quantifier free definition of a partial ordering. (Contributed by Scott Fenton, 22-Feb-2013.)
|- ( R Po A <-> ( ( R i^i ( _I |` A ) ) = (/) /\ ( ( R i^i ( A X. A ) ) o. ( R i^i ( A X. A ) ) ) C_ R ) )
Theorem	br8 29161*	Substitution for an eight-place predicate. (Contributed by Scott Fenton, 26-Sep-2013.) (Revised by Mario Carneiro, 3-May-2015.)
|- ( a = A -> ( ph <-> ps ) )   &    |- ( b = B -> ( ps <-> ch ) )   &    |- ( c = C -> ( ch <-> th ) )   &    |- ( d = D -> ( th <-> ta ) )   &    |- ( e = E -> ( ta <-> et ) )   &    |- ( f = F -> ( et <-> ze ) )   &    |- ( g = G -> ( ze <-> si ) )   &    |- ( h = H -> ( si <-> rh ) )   &    |- ( x = X -> P = Q )   &    |- R = { <. p , q >. | E. x e. S E. a e. P E. b e. P E. c e. P E. d e. P E. e e. P E. f e. P E. g e. P E. h e. P ( p = <. <. a , b >. , <. c , d >. >. /\ q = <. <. e , f >. , <. g , h >. >. /\ ph ) }   =>    |- ( ( ( X e. S /\ A e. Q /\ B e. Q ) /\ ( C e. Q /\ D e. Q /\ E e. Q ) /\ ( F e. Q /\ G e. Q /\ H e. Q ) ) -> ( <. <. A , B >. , <. C , D >. >. R <. <. E , F >. , <. G , H >. >. <-> rh ) )
Theorem	br6 29162*	Substitution for a six-place predicate. (Contributed by Scott Fenton, 4-Oct-2013.) (Revised by Mario Carneiro, 3-May-2015.)
|- ( a = A -> ( ph <-> ps ) )   &    |- ( b = B -> ( ps <-> ch ) )   &    |- ( c = C -> ( ch <-> th ) )   &    |- ( d = D -> ( th <-> ta ) )   &    |- ( e = E -> ( ta <-> et ) )   &    |- ( f = F -> ( et <-> ze ) )   &    |- ( x = X -> P = Q )   &    |- R = { <. p , q >. | E. x e. S E. a e. P E. b e. P E. c e. P E. d e. P E. e e. P E. f e. P ( p = <. a , <. b , c >. >. /\ q = <. d , <. e , f >. >. /\ ph ) }   =>    |- ( ( X e. S /\ ( A e. Q /\ B e. Q /\ C e. Q ) /\ ( D e. Q /\ E e. Q /\ F e. Q ) ) -> ( <. A , <. B , C >. >. R <. D , <. E , F >. >. <-> ze ) )
Theorem	br4 29163*	Substitution for a four-place predicate. (Contributed by Scott Fenton, 9-Oct-2013.) (Revised by Mario Carneiro, 14-Oct-2013.)
|- ( a = A -> ( ph <-> ps ) )   &    |- ( b = B -> ( ps <-> ch ) )   &    |- ( c = C -> ( ch <-> th ) )   &    |- ( d = D -> ( th <-> ta ) )   &    |- ( x = X -> P = Q )   &    |- R = { <. p , q >. | E. x e. S E. a e. P E. b e. P E. c e. P E. d e. P ( p = <. a , b >. /\ q = <. c , d >. /\ ph ) }   =>    |- ( ( X e. S /\ ( A e. Q /\ B e. Q ) /\ ( C e. Q /\ D e. Q ) ) -> ( <. A , B >. R <. C , D >. <-> ta ) )
Theorem	dfres3 29164	Alternate definition of restriction. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|- ( A |` B ) = ( A i^i ( B X. ran A ) )
Theorem	cnvco1 29165	Another distributive law of converse over class composition. (Contributed by Scott Fenton, 3-May-2014.)
|- `' ( `' A o. B ) = ( `' B o. A )
Theorem	cnvco2 29166	Another distributive law of converse over class composition. (Contributed by Scott Fenton, 3-May-2014.)
|- `' ( A o. `' B ) = ( B o. `' A )
Theorem	eldm3 29167	Quantifier-free definition of membership in a domain. (Contributed by Scott Fenton, 21-Jan-2017.)
|- ( A e. dom B <-> ( B |` { A } ) =/= (/) )
Theorem	elrn3 29168	Quantifier-free definition of membership in a range. (Contributed by Scott Fenton, 21-Jan-2017.)
|- ( A e. ran B <-> ( B i^i ( _V X. { A } ) ) =/= (/) )
Theorem	pocnv 29169	The converse of a partial ordering is still a partial ordering. (Contributed by Scott Fenton, 13-Jun-2018.)
|- ( R Po A -> `' R Po A )
Theorem	socnv 29170	The converse of a strict ordering is still a strict ordering. (Contributed by Scott Fenton, 13-Jun-2018.)
|- ( R Or A -> `' R Or A )
21.8.11  Properties of functions and mappings
Theorem	funpsstri 29171	A condition for subset trichotomy for functions. (Contributed by Scott Fenton, 19-Apr-2011.)
|- ( ( Fun H /\ ( F C_ H /\ G C_ H ) /\ ( dom F C_ dom G \/ dom G C_ dom F ) ) -> ( F C. G \/ F = G \/ G C. F ) )
Theorem	fundmpss 29172	If a class F is a proper subset of a function G, then dom F C. dom G. (Contributed by Scott Fenton, 20-Apr-2011.)
|- ( Fun G -> ( F C. G -> dom F C. dom G ) )
Theorem	fvresval 29173	The value of a function at a restriction is either null or the same as the function itself. (Contributed by Scott Fenton, 4-Sep-2011.)
|- ( ( ( F |` B ) ` A ) = ( F ` A ) \/ ( ( F |` B ) ` A ) = (/) )
Theorem	mptrel 29174	The maps-to notation always describes a relationship. (Contributed by Scott Fenton, 16-Apr-2012.)
|- Rel ( x e. A |-> B )
Theorem	funsseq 29175	Given two functions with equal domains, equality only requires one direction of the subset relationship. (Contributed by Scott Fenton, 24-Apr-2012.) (Proof shortened by Mario Carneiro, 3-May-2015.)
|- ( ( Fun F /\ Fun G /\ dom F = dom G ) -> ( F = G <-> F C_ G ) )
Theorem	fununiq 29176	The uniqueness condition of functions. (Contributed by Scott Fenton, 18-Feb-2013.)
|- A e. _V   &    |- B e. _V   &    |- C e. _V   =>    |- ( Fun F -> ( ( A F B /\ A F C ) -> B = C ) )
Theorem	funbreq 29177	An equality condition for functions. (Contributed by Scott Fenton, 18-Feb-2013.)
|- A e. _V   &    |- B e. _V   &    |- C e. _V   =>    |- ( ( Fun F /\ A F B ) -> ( A F C <-> B = C ) )
Theorem	mpteq12d 29178	An equality inference for the maps to notation. Compare mpteq12dv 4515. (Contributed by Scott Fenton, 8-Aug-2013.) (Revised by Mario Carneiro, 11-Dec-2016.)
|- F/ x ph   &    |- ( ph -> A = C )   &    |- ( ph -> B = D )   =>    |- ( ph -> ( x e. A |-> B ) = ( x e. C |-> D ) )
Theorem	fprb 29179*	A condition for functionhood over a pair. (Contributed by Scott Fenton, 16-Sep-2013.)
|- A e. _V   &    |- B e. _V   =>    |- ( A =/= B -> ( F : { A , B } --> R <-> E. x e. R E. y e. R F = { <. A , x >. , <. B , y >. } ) )
Theorem	br1steq 29180	Uniqueness condition for binary relationship over the 1st relationship. (Contributed by Scott Fenton, 11-Apr-2014.) (Proof shortened by Mario Carneiro, 3-May-2015.)
|- A e. _V   &    |- B e. _V   &    |- C e. _V   =>    |- ( <. A , B >. 1st C <-> C = A )
Theorem	br2ndeq 29181	Uniqueness condition for binary relationship over the 2nd relationship. (Contributed by Scott Fenton, 11-Apr-2014.) (Proof shortened by Mario Carneiro, 3-May-2015.)
|- A e. _V   &    |- B e. _V   &    |- C e. _V   =>    |- ( <. A , B >. 2nd C <-> C = B )
Theorem	dfdm5 29182	Definition of domain in terms of 1st and image. (Contributed by Scott Fenton, 11-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|- dom A = ( ( 1st |` ( _V X. _V ) ) " A )
Theorem	dfrn5 29183	Definition of range in terms of 2nd and image. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|- ran A = ( ( 2nd |` ( _V X. _V ) ) " A )
Theorem	opelco3 29184	Alternate way of saying that an ordered pair is in a composition. (Contributed by Scott Fenton, 6-May-2018.)
|- ( <. A , B >. e. ( C o. D ) <-> B e. ( C " ( D " { A } ) ) )
Theorem	elima4 29185	Quantifier-free expression saying that a class is a member of an image. (Contributed by Scott Fenton, 8-May-2018.)
|- ( A e. ( R " B ) <-> ( R i^i ( B X. { A } ) ) =/= (/) )
21.8.12  Epsilon induction
Theorem	setinds 29186*	Principle of _E induction (set induction). If a property passes from all elements of x to x itself, then it holds for all x. (Contributed by Scott Fenton, 10-Mar-2011.)
|- ( A. y e. x [. y / x ]. ph -> ph )   =>    |- ph
Theorem	setinds2f 29187*	_E induction schema, using implicit substitution. (Contributed by Scott Fenton, 10-Mar-2011.) (Revised by Mario Carneiro, 11-Dec-2016.)
|- F/ x ps   &    |- ( x = y -> ( ph <-> ps ) )   &    |- ( A. y e. x ps -> ph )   =>    |- ph
Theorem	setinds2 29188*	_E induction schema, using implicit substitution. (Contributed by Scott Fenton, 10-Mar-2011.)
|- ( x = y -> ( ph <-> ps ) )   &    |- ( A. y e. x ps -> ph )   =>    |- ph
21.8.13  Ordinal numbers
Theorem	elpotr 29189*	A class of transitive sets is partially ordered by _E. (Contributed by Scott Fenton, 15-Oct-2010.)
|- ( A. z e. A Tr z -> _E Po A )
Theorem	dford5reg 29190	Given ax-reg 8021, an ordinal is a transitive class totally ordered by epsilon. (Contributed by Scott Fenton, 28-Jan-2011.)
|- ( Ord A <-> ( Tr A /\ _E Or A ) )
Theorem	dfon2lem1 29191	Lemma for dfon2 29200. (Contributed by Scott Fenton, 28-Feb-2011.)
|- Tr U. { x | ( ph /\ Tr x /\ ps ) }
Theorem	dfon2lem2 29192*	Lemma for dfon2 29200 (Contributed by Scott Fenton, 28-Feb-2011.)
|- U. { x | ( x C_ A /\ ph /\ ps ) } C_ A
Theorem	dfon2lem3 29193*	Lemma for dfon2 29200. All sets satisfying the new definition are transitive and untangled. (Contributed by Scott Fenton, 25-Feb-2011.)
|- ( A e. V -> ( A. x ( ( x C. A /\ Tr x ) -> x e. A ) -> ( Tr A /\ A. z e. A -. z e. z ) ) )
Theorem	dfon2lem4 29194*	Lemma for dfon2 29200. If two sets satisfy the new definition, then one is a subset of the other. (Contributed by Scott Fenton, 25-Feb-2011.)
|- A e. _V   &    |- B e. _V   =>    |- ( ( A. x ( ( x C. A /\ Tr x ) -> x e. A ) /\ A. y ( ( y C. B /\ Tr y ) -> y e. B ) ) -> ( A C_ B \/ B C_ A ) )
Theorem	dfon2lem5 29195*	Lemma for dfon2 29200. Two sets satisfying the new definition also satisfy trichotomy with respect to e.. (Contributed by Scott Fenton, 25-Feb-2011.)
|- A e. _V   &    |- B e. _V   =>    |- ( ( A. x ( ( x C. A /\ Tr x ) -> x e. A ) /\ A. y ( ( y C. B /\ Tr y ) -> y e. B ) ) -> ( A e. B \/ A = B \/ B e. A ) )
Theorem	dfon2lem6 29196*	Lemma for dfon2 29200. A transitive class of sets satisfying the new definition satisfies the new definition. (Contributed by Scott Fenton, 25-Feb-2011.)
|- ( ( Tr S /\ A. x e. S A. z ( ( z C. x /\ Tr z ) -> z e. x ) ) -> A. y ( ( y C. S /\ Tr y ) -> y e. S ) )
Theorem	dfon2lem7 29197*	Lemma for dfon2 29200. All elements of a new ordinal are new ordinals. (Contributed by Scott Fenton, 25-Feb-2011.)
|- A e. _V   =>    |- ( A. x ( ( x C. A /\ Tr x ) -> x e. A ) -> ( B e. A -> A. y ( ( y C. B /\ Tr y ) -> y e. B ) ) )
Theorem	dfon2lem8 29198*	Lemma for dfon2 29200. The intersection of a nonempty class A of new ordinals is itself a new ordinal and is contained within A (Contributed by Scott Fenton, 26-Feb-2011.)
|- ( ( A =/= (/) /\ A. x e. A A. y ( ( y C. x /\ Tr y ) -> y e. x ) ) -> ( A. z ( ( z C. |^| A /\ Tr z ) -> z e. |^| A ) /\ |^| A e. A ) )
Theorem	dfon2lem9 29199*	Lemma for dfon2 29200. A class of new ordinals is well-founded by _E. (Contributed by Scott Fenton, 3-Mar-2011.)
|- ( A. x e. A A. y ( ( y C. x /\ Tr y ) -> y e. x ) -> _E Fr A )
Theorem	dfon2 29200*	On consists of all sets that contain all its transitive proper subsets. This definition comes from J. R. Isbell, "A Definition of Ordinal Numbers," American Mathematical Monthly, vol 67 (1960), pp. 51-52. (Contributed by Scott Fenton, 20-Feb-2011.)
|- On = { x | A. y ( ( y C. x /\ Tr y ) -> y e. x ) }