P. 317 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 31601-31700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	dfso3 31601*	Expansion of the definition of a strict order. (Contributed by Scott Fenton, 6-Jun-2016.)
|- ( R Or A <-> A. x e. A A. y e. A A. z e. A ( -. x R x /\ ( ( x R y /\ y R z ) -> x R z ) /\ ( x R y \/ x = y \/ y R x ) ) )
Theorem	brtpid1 31602	A binary relation involving unordered triplets. (Contributed by Scott Fenton, 7-Jun-2016.)
|- A { <. A , B >. , C , D } B
Theorem	brtpid2 31603	A binary relation involving unordered triplets. (Contributed by Scott Fenton, 7-Jun-2016.)
|- A { C , <. A , B >. , D } B
Theorem	brtpid3 31604	A binary relation involving unordered triplets. (Contributed by Scott Fenton, 7-Jun-2016.)
|- A { C , D , <. A , B >. } B
Theorem	ceqsrexv2 31605*	Alternate elimitation of a restricted existential quantifier, using implicit substitution. (Contributed by Scott Fenton, 5-Sep-2017.)
|- ( x = A -> ( ph <-> ps ) )   =>    |- ( E. x e. B ( x = A /\ ph ) <-> ( A e. B /\ ps ) )
Theorem	iota5f 31606*	A method for computing iota. (Contributed by Scott Fenton, 13-Dec-2017.)
|- F/ x ph   &    |- F/_ x A   &    |- ( ( ph /\ A e. V ) -> ( ps <-> x = A ) )   =>    |- ( ( ph /\ A e. V ) -> ( iota x ps ) = A )
Theorem	ceqsralv2 31607*	Alternate elimination of a restricted universal quantifier, using implicit substitution. (Contributed by Scott Fenton, 7-Dec-2020.)
|- ( x = A -> ( ph <-> ps ) )   =>    |- ( A. x e. B ( x = A -> ph ) <-> ( A e. B -> ps ) )
Theorem	dford5 31608	A class is ordinal iff it is a subclass of On and transitive. (Contributed by Scott Fenton, 21-Nov-2021.)
|- ( Ord A <-> ( A C_ On /\ Tr A ) )
Theorem	jath 31609	Closed form of ja 173. Proved using the completeness script. (Proof modification is discouraged.) (Contributed by Scott Fenton, 13-Dec-2021.)
|- ( ( -. ph -> ch ) -> ( ( ps -> ch ) -> ( ( ph -> ps ) -> ch ) ) )
20.8.5  Properties of real and complex numbers
Theorem	sqdivzi 31610	Distribution of square over division. (Contributed by Scott Fenton, 7-Jun-2013.)
|- A e. CC   &    |- B e. CC   =>    |- ( B =/= 0 -> ( ( A / B ) ^ 2 ) = ( ( A ^ 2 ) / ( B ^ 2 ) ) )
Theorem	subdivcomb1 31611	Bring a term in a subtraction into the numerator. (Contributed by Scott Fenton, 3-Jul-2013.)
|- ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( ( C x. A ) - B ) / C ) = ( A - ( B / C ) ) )
Theorem	subdivcomb2 31612	Bring a term in a subtraction into the numerator. (Contributed by Scott Fenton, 3-Jul-2013.)
|- ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( A - ( C x. B ) ) / C ) = ( ( A / C ) - B ) )
Theorem	supfz 31613	The supremum of a finite sequence of integers. (Contributed by Scott Fenton, 8-Aug-2013.)
|- ( N e. ( ZZ>= ` M ) -> sup ( ( M ... N ) , ZZ , < ) = N )
Theorem	inffz 31614	The infimum of a finite sequence of integers. (Contributed by Scott Fenton, 8-Aug-2013.) (Revised by AV, 10-Oct-2021.)
|- ( N e. ( ZZ>= ` M ) -> inf ( ( M ... N ) , ZZ , < ) = M )
Theorem	inffzOLD 31615	The infimum of a finite sequence of integers. (Contributed by Scott Fenton, 8-Aug-2013.) Obsolete version of inffz 31614 as of 10-Oct-2021. (New usage is discouraged.) (Proof modification is discouraged.)
|- ( N e. ( ZZ>= ` M ) -> sup ( ( M ... N ) , ZZ , `' < ) = M )
Theorem	fz0n 31616	The sequence ( 0 ... ( N - 1 ) ) is empty iff N is zero. (Contributed by Scott Fenton, 16-May-2014.)
|- ( N e. NN0 -> ( ( 0 ... ( N - 1 ) ) = (/) <-> N = 0 ) )
Theorem	shftvalg 31617	Value of a sequence shifted by A. (Contributed by Scott Fenton, 16-Dec-2017.)
|- ( ( F e. V /\ A e. CC /\ B e. CC ) -> ( ( F shift A ) ` B ) = ( F ` ( B - A ) ) )
Theorem	divcnvlin 31618*	Limit of the ratio of two linear functions. (Contributed by Scott Fenton, 17-Dec-2017.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> A e. CC )   &    |- ( ph -> B e. ZZ )   &    |- ( ph -> F e. V )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) = ( ( k + A ) / ( k + B ) ) )   =>    |- ( ph -> F ~~> 1 )
Theorem	climlec3 31619*	Comparison of a constant to the limit of a sequence. (Contributed by Scott Fenton, 5-Jan-2018.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> B e. RR )   &    |- ( ph -> F ~~> A )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) <_ B )   =>    |- ( ph -> A <_ B )
Theorem	logi 31620	Calculate the logarithm of _i. (Contributed by Scott Fenton, 13-Apr-2020.)
|- ( log ` _i ) = ( _i x. ( pi / 2 ) )
Theorem	iexpire 31621	_i raised to itself is real. (Contributed by Scott Fenton, 13-Apr-2020.)
|- ( _i ^c _i ) e. RR
Theorem	bcneg1 31622	The binomial coefficent over negative one is zero. (Contributed by Scott Fenton, 29-May-2020.)
|- ( N e. NN0 -> ( N _C -u 1 ) = 0 )
Theorem	bcm1nt 31623	The proportion of one bionmial coefficient to another with N decreased by 1. (Contributed by Scott Fenton, 23-Jun-2020.)
|- ( ( N e. NN /\ K e. ( 0 ... ( N - 1 ) ) ) -> ( N _C K ) = ( ( ( N - 1 ) _C K ) x. ( N / ( N - K ) ) ) )
Theorem	bcprod 31624*	A product identity for binomial coefficents. (Contributed by Scott Fenton, 23-Jun-2020.)
|- ( N e. NN -> prod_ k e. ( 1 ... ( N - 1 ) ) ( ( N - 1 ) _C k ) = prod_ k e. ( 1 ... ( N - 1 ) ) ( k ^ ( ( 2 x. k ) - N ) ) )
Theorem	bccolsum 31625*	A column-sum rule for binomial coefficents. (Contributed by Scott Fenton, 24-Jun-2020.)
|- ( ( N e. NN0 /\ C e. NN0 ) -> sum_ k e. ( 0 ... N ) ( k _C C ) = ( ( N + 1 ) _C ( C + 1 ) ) )
20.8.6  Infinite products
Theorem	iprodefisumlem 31626	Lemma for iprodefisum 31627. (Contributed by Scott Fenton, 11-Feb-2018.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F : Z --> CC )   =>    |- ( ph -> seq M ( x. , ( exp o. F ) ) = ( exp o. seq M ( + , F ) ) )
Theorem	iprodefisum 31627*	Applying the exponential function to an infinite sum yields an infinite product. (Contributed by Scott Fenton, 11-Feb-2018.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) = B )   &    |- ( ( ph /\ k e. Z ) -> B e. CC )   &    |- ( ph -> seq M ( + , F ) e. dom ~~> )   =>    |- ( ph -> prod_ k e. Z ( exp ` B ) = ( exp ` sum_ k e. Z B ) )
Theorem	iprodgam 31628*	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 ) )
20.8.7  Factorial limits
Theorem	faclimlem1 31629*	Lemma for faclim 31632. 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 31630*	Lemma for faclim 31632. 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 31631	Lemma for faclim 31632. 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 31632*	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 31633*	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 31634*	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 )
20.8.8  Greatest common divisor and divisibility
Theorem	pdivsq 31635	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 31636	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 31637	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 31638	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 ) )
20.8.9  Properties of relationships
Theorem	brtp 31639	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 31640	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 31641*	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 31642*	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 31643	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 31644	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 31645	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 31646*	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 31647*	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 31648*	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	cnvco1 31649	Another distributive law of converse over class composition. (Contributed by Scott Fenton, 3-May-2014.)
|- `' ( `' A o. B ) = ( `' B o. A )
Theorem	cnvco2 31650	Another distributive law of converse over class composition. (Contributed by Scott Fenton, 3-May-2014.)
|- `' ( A o. `' B ) = ( B o. `' A )
Theorem	eldm3 31651	Quantifier-free definition of membership in a domain. (Contributed by Scott Fenton, 21-Jan-2017.)
|- ( A e. dom B <-> ( B |` { A } ) =/= (/) )
Theorem	elrn3 31652	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 31653	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 31654	The converse of a strict ordering is still a strict ordering. (Contributed by Scott Fenton, 13-Jun-2018.)
|- ( R Or A -> `' R Or A )
Theorem	sotrd 31655	Transitivity law for strict orderings, deduction form. (Contributed by Scott Fenton, 24-Nov-2021.)
|- ( ph -> R Or A )   &    |- ( ph -> X e. A )   &    |- ( ph -> Y e. A )   &    |- ( ph -> Z e. A )   &    |- ( ph -> X R Y )   &    |- ( ph -> Y R Z )   =>    |- ( ph -> X R Z )
Theorem	sotr3 31656	Transitivity law for strict orderings. (Contributed by Scott Fenton, 24-Nov-2021.)
|- ( ( R Or A /\ ( X e. A /\ Y e. A /\ Z e. A ) ) -> ( ( X R Y /\ -. Z R Y ) -> X R Z ) )
Theorem	soasym 31657	Asymmetry law for strict orderings. (Contributed by Scott Fenton, 24-Nov-2021.)
|- ( ( R Or A /\ ( X e. A /\ Y e. A ) ) -> ( X R Y -> -. Y R X ) )
Theorem	sotrine 31658	Trichotomy law for strict orderings. (Contributed by Scott Fenton, 8-Dec-2021.)
|- ( ( R Or A /\ ( B e. A /\ C e. A ) ) -> ( B =/= C <-> ( B R C \/ C R B ) ) )
Theorem	eqfunresadj 31659	Law for adjoining an element to restrictions of functions. (Contributed by Scott Fenton, 6-Dec-2021.)
|- ( ( ( Fun F /\ Fun G ) /\ ( F |` X ) = ( G |` X ) /\ ( Y e. dom F /\ Y e. dom G /\ ( F ` Y ) = ( G ` Y ) ) ) -> ( F |` ( X u. { Y } ) ) = ( G |` ( X u. { Y } ) ) )
Theorem	eqfunressuc 31660	Law for equality of restriction to successors. This is primarily useful when X is an ordinal, but it does not require that. (Contributed by Scott Fenton, 6-Dec-2021.)
|- ( ( ( Fun F /\ Fun G ) /\ ( F |` X ) = ( G |` X ) /\ ( X e. dom F /\ X e. dom G /\ ( F ` X ) = ( G ` X ) ) ) -> ( F |` suc X ) = ( G |` suc X ) )
Theorem	funeldmb 31661	If (/) is not part of the range of a function F, then A is in the domain of F iff ( F ` A ) =/= (/). (Contributed by Scott Fenton, 7-Dec-2021.)
|- ( ( Fun F /\ -. (/) e. ran F ) -> ( A e. dom F <-> ( F ` A ) =/= (/) ) )
Theorem	elintfv 31662*	Membership in an intersection of function values. (Contributed by Scott Fenton, 9-Dec-2021.)
|- X e. _V   =>    |- ( ( F Fn A /\ B C_ A ) -> ( X e. |^| ( F " B ) <-> A. y e. B X e. ( F ` y ) ) )
20.8.10  Properties of functions and mappings
Theorem	funpsstri 31663	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 31664	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 31665	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	funsseq 31666	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 31667	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 31668	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	fprb 31669*	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 31670	Uniqueness condition for the binary relation 1st. (Contributed by Scott Fenton, 11-Apr-2014.) (Proof shortened by Mario Carneiro, 3-May-2015.)
|- A e. _V   &    |- B e. _V   =>    |- ( <. A , B >. 1st C <-> C = A )
Theorem	br2ndeq 31671	Uniqueness condition for the binary relation 2nd. (Contributed by Scott Fenton, 11-Apr-2014.) (Proof shortened by Mario Carneiro, 3-May-2015.)
|- A e. _V   &    |- B e. _V   =>    |- ( <. A , B >. 2nd C <-> C = B )
Theorem	br1steqg 31672	Uniqueness condition for the binary relation 1st. (Contributed by Scott Fenton, 2-Jul-2020.) Revised to remove sethood hypothesis on C. (Revised by Peter Mazsa, 17-Jan-2022.)
|- ( ( A e. V /\ B e. W ) -> ( <. A , B >. 1st C <-> C = A ) )
Theorem	br2ndeqg 31673	Uniqueness condition for the binary relation 2nd. (Contributed by Scott Fenton, 2-Jul-2020.) Revised to remove sethood hypothesis on C. (Revised by Peter Mazsa, 17-Jan-2022.)
|- ( ( A e. V /\ B e. W ) -> ( <. A , B >. 2nd C <-> C = B ) )
Theorem	br1steqgOLD 31674	Obsolete version of br1steqg 31672 as of 9-Feb-2022. (Contributed by Scott Fenton, 2-Jul-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ( A e. V /\ B e. W /\ C e. X ) -> ( <. A , B >. 1st C <-> C = A ) )
Theorem	br2ndeqgOLD 31675	Obsolete version of br2ndeqg 31673 as of 9-Feb-2022. (Contributed by Scott Fenton, 2-Jul-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ( A e. V /\ B e. W /\ C e. X ) -> ( <. A , B >. 2nd C <-> C = B ) )
Theorem	dfdm5 31676	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 31677	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 31678	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 31679	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 } ) ) =/= (/) )
Theorem	fv1stcnv 31680	The value of the converse of 1st restricted to a singleton. (Contributed by Scott Fenton, 2-Jul-2020.)
|- ( ( X e. A /\ Y e. V ) -> ( `' ( 1st |` ( A X. { Y } ) ) ` X ) = <. X , Y >. )
Theorem	fv2ndcnv 31681	The value of the converse of 2nd restricted to a singleton. (Contributed by Scott Fenton, 2-Jul-2020.)
|- ( ( X e. V /\ Y e. A ) -> ( `' ( 2nd |` ( { X } X. A ) ) ` Y ) = <. X , Y >. )
Theorem	imaindm 31682	The image is unaffected by intersection with the domain. (Contributed by Scott Fenton, 17-Dec-2021.)
|- ( R " A ) = ( R " ( A i^i dom R ) )
20.8.11  Epsilon induction
Theorem	setinds 31683*	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 31684*	_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 31685*	_E induction schema, using implicit substitution. (Contributed by Scott Fenton, 10-Mar-2011.)
|- ( x = y -> ( ph <-> ps ) )   &    |- ( A. y e. x ps -> ph )   =>    |- ph
20.8.12  Ordinal numbers
Theorem	elpotr 31686*	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 31687	Given ax-reg 8497, 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 31688	Lemma for dfon2 31697. (Contributed by Scott Fenton, 28-Feb-2011.)
|- Tr U. { x | ( ph /\ Tr x /\ ps ) }
Theorem	dfon2lem2 31689*	Lemma for dfon2 31697. (Contributed by Scott Fenton, 28-Feb-2011.)
|- U. { x | ( x C_ A /\ ph /\ ps ) } C_ A
Theorem	dfon2lem3 31690*	Lemma for dfon2 31697. 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 31691*	Lemma for dfon2 31697. 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 31692*	Lemma for dfon2 31697. 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 31693*	Lemma for dfon2 31697. 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 31694*	Lemma for dfon2 31697. 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 31695*	Lemma for dfon2 31697. 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 31696*	Lemma for dfon2 31697. 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 31697*	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 ) }
Theorem	domep 31698	The domain of the epsilon relation is the universe. (Contributed by Scott Fenton, 27-Oct-2010.)
|- dom _E = _V
Theorem	rdgprc0 31699	The value of the recursive definition generator at (/) when the base value is a proper class. (Contributed by Scott Fenton, 26-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|- ( -. I e. _V -> ( rec ( F , I ) ` (/) ) = (/) )
Theorem	rdgprc 31700	The value of the recursive definition generator when I is a proper class. (Contributed by Scott Fenton, 26-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|- ( -. I e. _V -> rec ( F , I ) = rec ( F , (/) ) )