P. 392 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 39101-39200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	pfxccatin12lem1 39101	Lemma 1 for pfxccatin12 39103. Could replace swrdccatin12lem2b 12885. (Contributed by AV, 9-May-2020.)
|- ( ( M e. ( 0 ... L ) /\ N e. ( L ... X ) ) -> ( ( K e. ( 0..^ ( N - M ) ) /\ -. K e. ( 0..^ ( L - M ) ) ) -> ( K - ( L - M ) ) e. ( 0..^ ( N - L ) ) ) )
Theorem	pfxccatin12lem2 39102	Lemma 2 for pfxccatin12 39103. Could replace swrdccatin12lem2 12888. (Contributed by AV, 9-May-2020.)
|- L = ( # ` A )   =>    |- ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) -> ( ( K e. ( 0..^ ( N - M ) ) /\ -. K e. ( 0..^ ( L - M ) ) ) -> ( ( ( A ++ B ) substr <. M , N >. ) ` K ) = ( ( B prefix ( N - L ) ) ` ( K - ( # ` ( A substr <. M , L >. ) ) ) ) ) )
Theorem	pfxccatin12 39103	The subword of a concatenation of two words within both of the concatenated words. Could replace swrdccatin12 12890. (Contributed by AV, 9-May-2020.)
|- L = ( # ` A )   =>    |- ( ( A e. Word V /\ B e. Word V ) -> ( ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) -> ( ( A ++ B ) substr <. M , N >. ) = ( ( A substr <. M , L >. ) ++ ( B prefix ( N - L ) ) ) ) )
Theorem	pfxccat3 39104	The subword of a concatenation is either a subword of the first concatenated word or a subword of the second concatenated word or a concatenation of a suffix of the first word with a prefix of the second word. Could replace swrdccat3 12891. (Contributed by AV, 10-May-2020.)
|- L = ( # ` A )   =>    |- ( ( A e. Word V /\ B e. Word V ) -> ( ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( L + ( # ` B ) ) ) ) -> ( ( A ++ B ) substr <. M , N >. ) = if ( N <_ L , ( A substr <. M , N >. ) , if ( L <_ M , ( B substr <. ( M - L ) , ( N - L ) >. ) , ( ( A substr <. M , L >. ) ++ ( B prefix ( N - L ) ) ) ) ) ) )
Theorem	pfxccatpfx1 39105	A prefix of a concatenation being a prefix of the first concatenated word. (Contributed by AV, 10-May-2020.)
|- L = ( # ` A )   =>    |- ( ( A e. Word V /\ B e. Word V /\ N e. ( 0 ... L ) ) -> ( ( A ++ B ) prefix N ) = ( A prefix N ) )
Theorem	pfxccatpfx2 39106	A prefix of a concatenation of two words being the first word concatenated with a prefix of the second word. (Contributed by AV, 10-May-2020.)
|- L = ( # ` A )   &    |- M = ( # ` B )   =>    |- ( ( A e. Word V /\ B e. Word V /\ N e. ( ( L + 1 ) ... ( L + M ) ) ) -> ( ( A ++ B ) prefix N ) = ( A ++ ( B prefix ( N - L ) ) ) )
Theorem	pfxccat3a 39107	A prefix of a concatenation is either a prefix of the first concatenated word or a concatenation of the first word with a prefix of the second word. Could replace swrdccat3a 12893. (Contributed by AV, 10-May-2020.)
|- L = ( # ` A )   &    |- M = ( # ` B )   =>    |- ( ( A e. Word V /\ B e. Word V ) -> ( N e. ( 0 ... ( L + M ) ) -> ( ( A ++ B ) prefix N ) = if ( N <_ L , ( A prefix N ) , ( A ++ ( B prefix ( N - L ) ) ) ) ) )
Theorem	pfxccatid 39108	A prefix of a concatenation of length of the first concatenated word is the first word itself. Could replace swrdccatid 12896. (Contributed by AV, 10-May-2020.)
|- ( ( A e. Word V /\ B e. Word V /\ N = ( # ` A ) ) -> ( ( A ++ B ) prefix N ) = A )
Theorem	ccats1pfxeqbi 39109	A word is a prefix of a word with length greater by 1 than the first word iff the second word is the first word concatenated with the last symbol of the second word. Could replace ccats1swrdeqbi 12897. (Contributed by AV, 10-May-2020.)
|- ( ( W e. Word V /\ U e. Word V /\ ( # ` U ) = ( ( # ` W ) + 1 ) ) -> ( W = ( U prefix ( # ` W ) ) <-> U = ( W ++ <" ( lastS ` U ) "> ) ) )
Theorem	pfxccatin12d 39110	The subword of a concatenation of two words within both of the concatenated words. Could replace swrdccatin12d 12900. (Contributed by AV, 10-May-2020.)
|- ( ph -> ( # ` A ) = L )   &    |- ( ph -> ( A e. Word V /\ B e. Word V ) )   &    |- ( ph -> M e. ( 0 ... L ) )   &    |- ( ph -> N e. ( L ... ( L + ( # ` B ) ) ) )   =>    |- ( ph -> ( ( A ++ B ) substr <. M , N >. ) = ( ( A substr <. M , L >. ) ++ ( B prefix ( N - L ) ) ) )
Theorem	reuccatpfxs1lem 39111*	Lemma for reuccatpfxs1 39112. Could replace reuccats1lem 12879. (Contributed by AV, 9-May-2020.)
|- ( ( ( W e. Word V /\ U e. X ) /\ A. s e. V ( ( W ++ <" s "> ) e. X -> S = s ) /\ A. x e. X ( x e. Word V /\ ( # ` x ) = ( ( # ` W ) + 1 ) ) ) -> ( W = ( U prefix ( # ` W ) ) -> U = ( W ++ <" S "> ) ) )
Theorem	reuccatpfxs1 39112*	There is a unique word having the length of a given word increased by 1 with the given word as prefix if there is a unique symbol which extends the given word. Could replace reuccats1 12880. (Contributed by AV, 10-May-2020.)
|- ( ( W e. Word V /\ A. x e. X ( x e. Word V /\ ( # ` x ) = ( ( # ` W ) + 1 ) ) ) -> ( E! v e. V ( W ++ <" v "> ) e. X -> E! w e. X W = ( w prefix ( # ` W ) ) ) )
Theorem	splvalpfx 39113	Value of the substring replacement operator. (Contributed by AV, 11-May-2020.)
|- ( ( S e. V /\ ( F e. NN0 /\ T e. X /\ R e. Y ) ) -> ( S splice <. F , T , R >. ) = ( ( ( S prefix F ) ++ R ) ++ ( S substr <. T , ( # ` S ) >. ) ) )
Theorem	repswpfx 39114	A prefix of a repeated symbol word is a repeated symbol word. (Contributed by AV, 11-May-2020.)
|- ( ( S e. V /\ N e. NN0 /\ L e. ( 0 ... N ) ) -> ( ( S repeatS N ) prefix L ) = ( S repeatS L ) )
Theorem	cshword2 39115	Perform a cyclical shift for a word. (Contributed by AV, 11-May-2020.)
|- ( ( W e. Word V /\ N e. ZZ ) -> ( W cyclShift N ) = ( ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ++ ( W prefix ( N mod ( # ` W ) ) ) ) )
Theorem	pfxco 39116	Mapping of words commutes with the prefix operation. (Contributed by AV, 15-May-2020.)
|- ( ( W e. Word A /\ N e. ( 0 ... ( # ` W ) ) /\ F : A --> B ) -> ( F o. ( W prefix N ) ) = ( ( F o. W ) prefix N ) )
21.33.7  Auxiliary theorems for graph theory Additional theorems for classical first-order logic with equality, ZF set theory and theory of real and complex numbers used for proving the theorems for graph theory.
21.33.7.1  Negated equality and membership - extension
Theorem	elnelall 39117	A contradiction concerning membership implies anything. (Contributed by Alexander van der Vekens, 25-Jan-2018.)
|- ( A e. B -> ( A e/ B -> ph ) )
21.33.7.2  Subclasses and subsets - extension
Theorem	clel5 39118*	Alternate definition of class membership: a class X is an element of another class A iff there is an element of A equal to X. (Contributed by AV, 13-Nov-2020.)
|- ( X e. A <-> E. x e. A X = x )
Theorem	dfss7 39119*	Alternate definition of subclass relationship: a class A is a subclass of another class B iff each element of A is equal to an element of B. (Contributed by AV, 13-Nov-2020.)
|- ( A C_ B <-> A. x e. A E. y e. B x = y )
Theorem	sssseq 39120	If a class is a subclass of another class, the classes are equal iff the other class is a subclass of the first class. (Contributed by AV, 23-Dec-2020.)
|- ( B C_ A -> ( A C_ B <-> A = B ) )
Theorem	prcssprc 39121	The superclass of a proper class is a proper class. (Contributed by AV, 27-Dec-2020.)
|- ( ( A C_ B /\ A e/ _V ) -> B e/ _V )
21.33.7.3  The empty set - extension
Theorem	ralnralall 39122*	A contradiction concerning restricted generalization for a nonempty set implies anything. (Contributed by Alexander van der Vekens, 4-Sep-2018.)
|- ( A =/= (/) -> ( ( A. x e. A ph /\ A. x e. A -. ph ) -> ps ) )
Theorem	falseral0 39123*	A false statement can only be true for elements of an empty set. (Contributed by AV, 30-Oct-2020.)
|- ( ( A. x -. ph /\ A. x e. A ph ) -> A = (/) )
Theorem	ralralimp 39124*	Selecting one of two alternatives within a restricted generalization if one of the alternatives is false. (Contributed by AV, 6-Sep-2018.) (Proof shortened by AV, 13-Oct-2018.)
|- ( ( ph /\ A =/= (/) ) -> ( A. x e. A ( ( ph -> ( th \/ ta ) ) /\ -. th ) -> ta ) )
Theorem	n0rex 39125*	There is an element in a nonempty class which is an element of the class. (Contributed by AV, 17-Dec-2020.)
|- ( A =/= (/) -> E. x e. A x e. A )
Theorem	ssn0rex 39126*	There is an element in a class with a nonempty subclass which is an element of the subclass. (Contributed by AV, 17-Dec-2020.)
|- ( ( A C_ B /\ A =/= (/) ) -> E. x e. B x e. A )
21.33.7.4  Unordered and ordered pairs - extension
Theorem	elpwdifsn 39127	A subset of a set is an element of the power set of the difference of the set with a singleton if the subset does not contain the singleton element. (Contributed by AV, 10-Jan-2020.)
|- ( ( S e. W /\ S C_ V /\ A e/ S ) -> S e. ~P ( V \ { A } ) )
Theorem	pr1eqbg 39128	A (proper) pair is equal to another (maybe inproper) pair containing one element of the first pair if and only if the other element of the first pair is contained in the second pair. (Contributed by Alexander van der Vekens, 26-Jan-2018.)
|- ( ( ( A e. U /\ B e. V /\ C e. X ) /\ A =/= B ) -> ( A = C <-> { A , B } = { B , C } ) )
Theorem	pr1nebg 39129	A (proper) pair is not equal to another (maybe inproper) pair containing one element of the first pair if and only if the other element of the first pair is not contained in the second pair. (Contributed by Alexander van der Vekens, 26-Jan-2018.)
|- ( ( ( A e. U /\ B e. V /\ C e. X ) /\ A =/= B ) -> ( A =/= C <-> { A , B } =/= { B , C } ) )
Theorem	prelpw 39130	A pair of two sets belongs to the power class of a class containing those two sets and vice versa. (Contributed by AV, 8-Jan-2020.)
|- ( ( A e. V /\ B e. W ) -> ( ( A e. C /\ B e. C ) <-> { A , B } e. ~P C ) )
Theorem	rexdifpr 39131	Restricted existential quantification over a set with two elements removed. (Contributed by Alexander van der Vekens, 7-Feb-2018.)
|- ( E. x e. ( A \ { B , C } ) ph <-> E. x e. A ( x =/= B /\ x =/= C /\ ph ) )
Theorem	issn 39132*	A sufficient condition for a (nonempty) set to be a singleton. (Contributed by AV, 20-Sep-2020.)
|- ( E. x e. A A. y e. A x = y -> E. z A = { z } )
Theorem	n0snor2el 39133*	A nonempty set is either a singleton or contains at least two different elements. (Contributed by AV, 20-Sep-2020.)
|- ( A =/= (/) -> ( E. x e. A E. y e. A x =/= y \/ E. z A = { z } ) )
Theorem	opidg 39134	The ordered pair <. A , A >. in Kuratowski's representation. Closed form of opid 4199. (Contributed by AV, 18-Sep-2020.)
|- ( A e. _V -> <. A , A >. = { { A } } )
Theorem	snopeqop 39135	Equivalence for an ordered pair equal to a singleton of an ordered pair. (Contributed by AV, 18-Sep-2020.)
|- A e. _V   &    |- B e. _V   &    |- C e. _V   &    |- D e. _V   =>    |- ( { <. A , B >. } = <. C , D >. <-> ( A = B /\ C = D /\ C = { A } ) )
Theorem	propeqop 39136	Equivalence for an ordered pair equal to a pair of ordered pairs. (Contributed by AV, 18-Sep-2020.)
|- A e. _V   &    |- B e. _V   &    |- C e. _V   &    |- D e. _V   &    |- E e. _V   &    |- F e. _V   =>    |- ( { <. A , B >. , <. C , D >. } = <. E , F >. <-> ( ( A = C /\ E = { A } ) /\ ( ( A = B /\ F = { A , D } ) \/ ( A = D /\ F = { A , B } ) ) ) )
Theorem	propssopi 39137	If a pair of ordered pairs is a subset of an ordered pair, their first components are equal. (Contributed by AV, 20-Sep-2020.)
|- A e. _V   &    |- B e. _V   &    |- C e. _V   &    |- D e. _V   &    |- E e. _V   &    |- F e. _V   =>    |- ( { <. A , B >. , <. C , D >. } C_ <. E , F >. -> A = C )
Theorem	ssprss 39138	A pair as subset of a pair. (Contributed by AV, 26-Oct-2020.)
|- ( ( A e. V /\ B e. W ) -> ( { A , B } C_ { C , D } <-> ( ( A = C \/ A = D ) /\ ( B = C \/ B = D ) ) ) )
Theorem	ssprsseq 39139	A proper pair is a subset of a pair iff it is equal to the superset. (Contributed by AV, 26-Oct-2020.)
|- ( ( A e. V /\ B e. W /\ A =/= B ) -> ( { A , B } C_ { C , D } <-> { A , B } = { C , D } ) )
Theorem	elpr2elpr 39140*	For an element of an unordered pair which is a subset of a given set, there is another (maybe the same) element of the given set being an element of the unordered pair. (Contributed by AV, 5-Dec-2020.)
|- ( ( X e. V /\ Y e. V /\ A e. { X , Y } ) -> E. b e. V { X , Y } = { A , b } )
21.33.7.5  Indexed union and intersection - extension
Theorem	iunopeqop 39141*	Equivalence for an ordered pair equal to an indexed union of singletons of ordered pairs. (Contributed by AV, 20-Sep-2020.)
|- B e. _V   &    |- C e. _V   &    |- D e. _V   =>    |- ( A =/= (/) -> ( U_ x e. A { <. x , B >. } = <. C , D >. -> E. z A = { z } ) )
Theorem	otiunsndisjX 39142*	The union of singletons consisting of ordered triples which have distinct first and third components are disjunct. (Contributed by Alexander van der Vekens, 10-Mar-2018.)
|- ( B e. X -> Disj a e. V U_ c e. W { <. a , B , c >. } )
21.33.7.6  Ordered-pair class abstractions - extension
Theorem	opabn1stprc 39143*	An ordered-pair class abstraction which does not depend on the first abstraction variable is a proper class. There must be, however, at least one set which satisfies the restricting wwf. (Contributed by AV, 27-Dec-2020.)
|- ( E. y ph -> { <. x , y >. | ph } e/ _V )
21.33.7.7  Introduce the Axiom of Power Sets - extension
Theorem	ralxfrd2 39144*	Transfer universal quantification from a variable x to another variable y contained in expression A. Variant of ralxfrd 4631. (Contributed by Alexander van der Vekens, 25-Apr-2018.)
|- ( ( ph /\ y e. C ) -> A e. B )   &    |- ( ( ph /\ x e. B ) -> E. y e. C x = A )   &    |- ( ( ph /\ y e. C /\ x = A ) -> ( ps <-> ch ) )   =>    |- ( ph -> ( A. x e. B ps <-> A. y e. C ch ) )
Theorem	rexxfrd2 39145*	Transfer existence from a variable x to another variable y contained in expression A. Variant of rexxfrd 4632. (Contributed by Alexander van der Vekens, 25-Apr-2018.)
|- ( ( ph /\ y e. C ) -> A e. B )   &    |- ( ( ph /\ x e. B ) -> E. y e. C x = A )   &    |- ( ( ph /\ y e. C /\ x = A ) -> ( ps <-> ch ) )   =>    |- ( ph -> ( E. x e. B ps <-> E. y e. C ch ) )
21.33.7.8  Relations - extension
Theorem	resresdm 39146	A restriction by an arbitrary set is a restriction by its domain. (Contributed by AV, 16-Nov-2020.)
|- ( F = ( E |` A ) -> F = ( E |` dom F ) )
Theorem	resisresindm 39147	The restriction of a relation by a set B is identical with the restriction by the intersection of B with the domain of the relation. (Contributed by Alexander van der Vekens, 3-Feb-2018.)
|- ( Rel F -> ( F |` B ) = ( F |` ( B i^i dom F ) ) )
Theorem	ssrelrn 39148*	If a relation is a subset of a cartesian product, then for each element of the range of the relation there is an element of the first set of the cartesian product which is related to the element of the range by the relation. (Contributed by AV, 24-Oct-2020.)
|- ( ( R C_ ( A X. B ) /\ Y e. ran R ) -> E. a e. A a R Y )
21.33.7.9  Functions - extension
Theorem	fvifeq 39149	Equality of function values with conditional arguments, see also fvif 5903. (Contributed by Alexander van der Vekens, 21-May-2018.)
|- ( A = if ( ph , B , C ) -> ( F ` A ) = if ( ph , ( F ` B ) , ( F ` C ) ) )
Theorem	2f1fvneq 39150	If two one-to-one functions are applied on different arguments, also the values are different. (Contributed by Alexander van der Vekens, 25-Jan-2018.)
|- ( ( ( E : D -1-1-> R /\ F : C -1-1-> D ) /\ ( A e. C /\ B e. C ) /\ A =/= B ) -> ( ( ( E ` ( F ` A ) ) = X /\ ( E ` ( F ` B ) ) = Y ) -> X =/= Y ) )
Theorem	f1cofveqaeq 39151	If the values of a composition of one-to-one functions for two arguments are equal, the arguments themselves must be equal. (Contributed by AV, 3-Feb-2021.)
|- ( ( ( F : B -1-1-> C /\ G : A -1-1-> B ) /\ ( X e. A /\ Y e. A ) ) -> ( ( F ` ( G ` X ) ) = ( F ` ( G ` Y ) ) -> X = Y ) )
Theorem	f1cofveqaeqALT 39152	Alternate proof of f1cofveqaeq 39151, 1 essential step shorter, but having more bytes (305 vs. 282). (Contributed by AV, 3-Feb-2021.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( ( ( F : B -1-1-> C /\ G : A -1-1-> B ) /\ ( X e. A /\ Y e. A ) ) -> ( ( F ` ( G ` X ) ) = ( F ` ( G ` Y ) ) -> X = Y ) )
Theorem	rnfdmpr 39153	The range of a one-to-one function F of an unordered pair into a set is the unordered pair of the function values. (Contributed by Alexander van der Vekens, 2-Feb-2018.)
|- ( ( X e. V /\ Y e. W ) -> ( F Fn { X , Y } -> ran F = { ( F ` X ) , ( F ` Y ) } ) )
Theorem	imarnf1pr 39154	The image of the range of a function F under a function E if F is a function of a pair into the domain of E. (Contributed by Alexander van der Vekens, 2-Feb-2018.)
|- ( ( X e. V /\ Y e. W ) -> ( ( ( F : { X , Y } --> dom E /\ E : dom E --> R ) /\ ( ( E ` ( F ` X ) ) = A /\ ( E ` ( F ` Y ) ) = B ) ) -> ( E " ran F ) = { A , B } ) )
Theorem	funiun 39155*	A function is a union of singletons of ordered pairs indexed by its domain. (Contributed by AV, 18-Sep-2020.)
|- ( Fun F -> F = U_ x e. dom F { <. x , ( F ` x ) >. } )
Theorem	funopsn 39156*	If a function is an ordered pair then it is a singleton of an ordered pair. (Contributed by AV, 20-Sep-2020.)
|- X e. _V   &    |- Y e. _V   =>    |- ( ( Fun F /\ F = <. X , Y >. ) -> E. a ( X = { a } /\ F = { <. a , a >. } ) )
Theorem	funop 39157*	An ordered pair is a function iff it is a singleton of an ordered pair. (Contributed by AV, 20-Sep-2020.)
|- X e. _V   &    |- Y e. _V   =>    |- ( Fun <. X , Y >. <-> E. a ( X = { a } /\ <. X , Y >. = { <. a , a >. } ) )
Theorem	funop1 39158*	A function is an ordered pair iff it is a singleton of an ordered pair. (Contributed by AV, 20-Sep-2020.)
|- ( E. x E. y F = <. x , y >. -> ( Fun F <-> E. x E. y F = { <. x , y >. } ) )
Theorem	f1ssf1 39159	A subset of an injective function is injective. (Contributed by AV, 20-Nov-2020.)
|- ( ( Fun F /\ Fun `' F /\ G C_ F ) -> Fun `' G )
Theorem	funsndifnop 39160	A singleton of an ordered pair is not an ordered pair if the components are different. (Contributed by AV, 23-Sep-2020.)
|- A e. V   &    |- B e. W   &    |- G = { <. A , B >. }   =>    |- ( A =/= B -> -. G e. ( _V X. _V ) )
Theorem	funsneqopsn 39161	A singleton of an ordered pair is an ordered pair of equal singletons if the components are equal. (Contributed by AV, 24-Sep-2020.)
|- A e. V   &    |- B e. W   &    |- G = { <. A , B >. }   =>    |- ( A = B -> G = <. { A } , { A } >. )
Theorem	funsneqop 39162	A singleton of an ordered pair is an ordered pair if the components are equal. (Contributed by AV, 24-Sep-2020.)
|- A e. V   &    |- B e. W   &    |- G = { <. A , B >. }   =>    |- ( A = B -> G e. ( _V X. _V ) )
Theorem	funsneqopb 39163	A singleton of an ordered pair is an ordered pair iff the components are equal. (Contributed by AV, 24-Sep-2020.)
|- A e. V   &    |- B e. W   &    |- G = { <. A , B >. }   =>    |- ( A = B <-> G e. ( _V X. _V ) )
Theorem	fundmge2nop 39164	A function with a domain containing (at least) two different elements is not an ordered pair. (Contributed by AV, 12-Oct-2020.)
|- ( ( Fun G /\ 2 <_ ( # ` dom G ) ) -> -. G e. ( _V X. _V ) )
Theorem	fun2dmnop 39165	A function with a domain containing (at least) two different elements is not an ordered pair. (Contributed by AV, 21-Sep-2020.) (Proof shortened by AV, 12-Oct-2020.)
|- A e. V   &    |- B e. W   =>    |- ( ( Fun G /\ A =/= B /\ { A , B } C_ dom G ) -> -. G e. ( _V X. _V ) )
Theorem	fun2dmnopgexmpl 39166	A function with a domain containing (at least) two different elements is not an ordered pair. (Contributed by AV, 21-Sep-2020.)
|- ( G = { <. 0 , 1 >. , <. 1 , 1 >. } -> -. G e. ( _V X. _V ) )
Theorem	opabresex0d 39167*	A collection of ordered pairs, the class of all possible second components being a set, with a restriction of a binary relation is a set. (Contributed by Alexander van der Vekens, 1-Nov-2017.) (Revised by AV, 1-Jan-2021.)
|- ( ( ph /\ x R y ) -> x e. C )   &    |- ( ( ph /\ x R y ) -> th )   &    |- ( ( ph /\ x e. C ) -> { y | th } e. V )   &    |- ( ph -> C e. W )   =>    |- ( ph -> { <. x , y >. | ( x R y /\ ps ) } e. _V )
Theorem	opabbrfex0d 39168*	A collection of ordered pairs, the class of all possible second components being a set, is a set. (Contributed by AV, 15-Jan-2021.)
|- ( ( ph /\ x R y ) -> x e. C )   &    |- ( ( ph /\ x R y ) -> th )   &    |- ( ( ph /\ x e. C ) -> { y | th } e. V )   &    |- ( ph -> C e. W )   =>    |- ( ph -> { <. x , y >. | x R y } e. _V )
Theorem	opabresexd 39169*	A collection of ordered pairs, the second component being a function, with a restriction of a binary relation is a set. (Contributed by Alexander van der Vekens, 1-Nov-2017.) (Revised by AV, 15-Jan-2021.)
|- ( ( ph /\ x R y ) -> x e. C )   &    |- ( ( ph /\ x R y ) -> y : A --> B )   &    |- ( ( ph /\ x e. C ) -> A e. U )   &    |- ( ( ph /\ x e. C ) -> B e. V )   &    |- ( ph -> C e. W )   =>    |- ( ph -> { <. x , y >. | ( x R y /\ ps ) } e. _V )
Theorem	opabbrfexd 39170*	A collection of ordered pairs, the second component being a function, is a set. (Contributed by AV, 15-Jan-2021.)
|- ( ( ph /\ x R y ) -> x e. C )   &    |- ( ( ph /\ x R y ) -> y : A --> B )   &    |- ( ( ph /\ x e. C ) -> A e. U )   &    |- ( ( ph /\ x e. C ) -> B e. V )   &    |- ( ph -> C e. W )   =>    |- ( ph -> { <. x , y >. | x R y } e. _V )
Theorem	opabresex2d 39171*	Restrictions of a collection of ordered pairs of related elements are sets. (Contributed by Alexander van der Vekens, 1-Nov-2017.) (Revised by AV, 15-Jan-2021.)
|- ( ( ph /\ x ( W ` G ) y ) -> ps )   &    |- ( ph -> { <. x , y >. | ps } e. V )   =>    |- ( ph -> { <. x , y >. | ( x ( W ` G ) y /\ th ) } e. _V )
Theorem	mptmpt2opabbrd 39172*	The operation value of a function value of a collection of ordered pairs of elements related in two ways. (Contributed by Alexander van Vekens, 8-Nov-2017.) (Revised by AV, 15-Jan-2021.)
|- ( ph -> G e. W )   &    |- ( ph -> X e. ( A ` G ) )   &    |- ( ph -> Y e. ( B ` G ) )   &    |- ( ph -> { <. f , h >. | ps } e. V )   &    |- ( ( ph /\ f ( D ` G ) h ) -> ps )   &    |- ( ( a = X /\ b = Y ) -> ( ta <-> th ) )   &    |- ( g = G -> ( ch <-> ta ) )   &    |- M = ( g e. _V |-> ( a e. ( A ` g ) , b e. ( B ` g ) |-> { <. f , h >. | ( ch /\ f ( D ` g ) h ) } ) )   =>    |- ( ph -> ( X ( M ` G ) Y ) = { <. f , h >. | ( th /\ f ( D ` G ) h ) } )
Theorem	mptmpt2opabovd 39173*	The operation value of a function value of a collection of ordered pairs of related elements (Contributed by Alexander van der Vekens, 8-Nov-2017.) (Revised by AV, 15-Jan-2021.)
|- ( ph -> G e. W )   &    |- ( ph -> X e. ( A ` G ) )   &    |- ( ph -> Y e. ( B ` G ) )   &    |- ( ph -> { <. f , h >. | ps } e. V )   &    |- ( ( ph /\ f ( D ` G ) h ) -> ps )   &    |- M = ( g e. _V |-> ( a e. ( A ` g ) , b e. ( B ` g ) |-> { <. f , h >. | ( f ( a ( C ` g ) b ) h /\ f ( D ` g ) h ) } ) )   =>    |- ( ph -> ( X ( M ` G ) Y ) = { <. f , h >. | ( f ( X ( C ` G ) Y ) h /\ f ( D ` G ) h ) } )
Theorem	fpropnf1 39174	A function, given by an unordered pair of ordered pairs, which is not injective/one-to-one. (Contributed by Alexander van der Vekens, 22-Oct-2017.) (Revised by AV, 8-Jan-2021.)
|- F = { <. X , Z >. , <. Y , Z >. }   =>    |- ( ( ( X e. U /\ Y e. V /\ Z e. W ) /\ X =/= Y ) -> ( Fun F /\ -. Fun `' F ) )
21.33.7.10  Restricted iota - extension
Theorem	riotaeqimp 39175*	If two restricted iota descriptors for an equality are equal, then the terms of the equality are equal. (Contributed by AV, 6-Dec-2020.)
|- I = ( iota_ a e. V X = A )   &    |- J = ( iota_ a e. V Y = A )   &    |- ( ph -> E! a e. V X = A )   &    |- ( ph -> E! a e. V Y = A )   =>    |- ( ( ph /\ I = J ) -> X = Y )
21.33.7.11  Equinumerosity - extension
Theorem	resfnfinfin 39176	The restriction of a function by a finite set is finite. (Contributed by Alexander van der Vekens, 3-Feb-2018.)
|- ( ( F Fn A /\ B e. Fin ) -> ( F |` B ) e. Fin )
Theorem	residfi 39177	A restricted identity function is finite iff the restricting class is finite. (Contributed by AV, 10-Jan-2020.)
|- ( ( _I |` A ) e. Fin <-> A e. Fin )
21.33.7.12  Subtraction - extension
Theorem	cnambpcma 39178	((a-b)+c)-a = c-a holds for complex numbers a,b,c. (Contributed by Alexander van der Vekens, 23-Mar-2018.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( ( A - B ) + C ) - A ) = ( C - B ) )
Theorem	cnapbmcpd 39179	((a+b)-c)+d = ((a+d)+b)-c holds for complex numbers a,b,c,d. (Contributed by Alexander van der Vekens, 23-Mar-2018.)
|- ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( ( A + B ) - C ) + D ) = ( ( ( A + D ) + B ) - C ) )
21.33.7.13  Multiplication - extension
Theorem	2txmxeqx 39180	Two times a complex number minus the number itself results in the number itself. (Contributed by Alexander van der Vekens, 8-Jun-2018.)
|- ( X e. CC -> ( ( 2 x. X ) - X ) = X )
21.33.7.14  Ordering on reals (cont.) - extension
Theorem	leaddsuble 39181	Addition and subtraction on one side of 'less or equal'. (Contributed by Alexander van der Vekens, 18-Mar-2018.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( B <_ C <-> ( ( A + B ) - C ) <_ A ) )
Theorem	2leaddle2 39182	If two real numbers are less than a third real number, the sum of the real numbers is less than twice the third real number. (Contributed by Alexander van der Vekens, 21-May-2018.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A < C /\ B < C ) -> ( A + B ) < ( 2 x. C ) ) )
Theorem	ltnltne 39183	Variant of trichotomy law for 'less than'. (Contributed by Alexander van der Vekens, 8-Jun-2018.)
|- ( ( A e. RR /\ B e. RR ) -> ( A < B <-> ( -. B < A /\ -. B = A ) ) )
Theorem	p1lep2 39184	A real number increasd by 1 is less than or equal to the number increased by 2. (Contributed by Alexander van der Vekens, 17-Sep-2018.)
|- ( N e. RR -> ( N + 1 ) <_ ( N + 2 ) )
Theorem	lelttrdi 39185	If a number is less than another number, and the other number is less than or equal to a third number, the first number is less than the third number. (Contributed by Alexander van der Vekens, 24-Mar-2018.)
|- ( ph -> ( A e. RR /\ B e. RR /\ C e. RR ) )   &    |- ( ph -> B <_ C )   =>    |- ( ph -> ( A < B -> A < C ) )
Theorem	ltsubsubaddltsub 39186	If the result of subtracting two numbers is greater than a number, the result of adding one of these subtracted numbers to the number is less than the result of subtracting the other subtracted number only. (Contributed by Alexander van der Vekens, 9-Jun-2018.)
|- ( ( J e. RR /\ ( L e. RR /\ M e. RR /\ N e. RR ) ) -> ( J < ( ( L - M ) - N ) <-> ( J + M ) < ( L - N ) ) )
Theorem	zm1nn 39187	An integer minus 1 is positive under certain circumstances. (Contributed by Alexander van der Vekens, 9-Jun-2018.)
|- ( ( N e. NN0 /\ L e. ZZ ) -> ( ( J e. RR /\ 0 <_ J /\ J < ( ( L - N ) - 1 ) ) -> ( L - 1 ) e. NN ) )
21.33.7.15  Nonnegative integers (as a subset of complex numbers) - extension
Theorem	lesubnn0 39188	Subtracting a nonnegative integer from a nonnegative integer which is greater than or equal to the first one results in a nonnegative integer. (Contributed by Alexander van der Vekens, 6-Apr-2018.)
|- ( ( A e. NN0 /\ B e. NN0 ) -> ( B <_ A -> ( A - B ) e. NN0 ) )
Theorem	ltsubnn0 39189	Subtracting a nonnegative integer from a nonnegative integer which is greater than the first one results in a nonnegative integer. (Contributed by Alexander van der Vekens, 6-Apr-2018.)
|- ( ( A e. NN0 /\ B e. NN0 ) -> ( B < A -> ( A - B ) e. NN0 ) )
Theorem	nn0resubcl 39190	Closure law for subtraction of reals, restricted to nonnegative integers. (Contributed by Alexander van der Vekens, 6-Apr-2018.)
|- ( ( A e. NN0 /\ B e. NN0 ) -> ( A - B ) e. RR )
21.33.7.16  Upper sets of integers - extension
Theorem	eluzge0nn0 39191	If an integer is greater than or equal to a nonnegative integer, then it is a nonnegative integer. (Contributed by Alexander van der Vekens, 27-Aug-2018.)
|- ( N e. ( ZZ>= ` M ) -> ( 0 <_ M -> N e. NN0 ) )
21.33.7.17  Finite intervals of integers - extension
Theorem	ssfz12 39192	Subset relationship for finite sets of sequential integers. (Contributed by Alexander van der Vekens, 16-Mar-2018.)
|- ( ( K e. ZZ /\ L e. ZZ /\ K <_ L ) -> ( ( K ... L ) C_ ( M ... N ) -> ( M <_ K /\ L <_ N ) ) )
Theorem	elfz2z 39193	Membership of an integer in a finite set of sequential integers starting at 0. (Contributed by Alexander van der Vekens, 25-May-2018.)
|- ( ( K e. ZZ /\ N e. ZZ ) -> ( K e. ( 0 ... N ) <-> ( 0 <_ K /\ K <_ N ) ) )
Theorem	2elfz3nn0 39194	If there are two elements in a finite set of sequential integers starting at 0, these two elements as well as the upper bound are nonnegative integers. (Contributed by Alexander van der Vekens, 7-Apr-2018.)
|- ( ( A e. ( 0 ... N ) /\ B e. ( 0 ... N ) ) -> ( A e. NN0 /\ B e. NN0 /\ N e. NN0 ) )
Theorem	fz0addcom 39195	The addition of two members of a finite set of sequential integers starting at 0 is commutative. (Contributed by Alexander van der Vekens, 22-May-2018.) (Revised by Alexander van der Vekens, 9-Jun-2018.)
|- ( ( A e. ( 0 ... N ) /\ B e. ( 0 ... N ) ) -> ( A + B ) = ( B + A ) )
Theorem	2elfz2melfz 39196	If the sum of two integers of a 0 based finite set of sequential integers is greater than the upper bound, the difference between one of the integers and the difference between the upper bound and the other integer is in the 0 based finite set of sequential integers with the first integer as upper bound. (Contributed by Alexander van der Vekens, 7-Apr-2018.) (Revised by Alexander van der Vekens, 31-May-2018.)
|- ( ( A e. ( 0 ... N ) /\ B e. ( 0 ... N ) ) -> ( N < ( A + B ) -> ( B - ( N - A ) ) e. ( 0 ... A ) ) )
Theorem	fz0addge0 39197	The sum of two integers in 0 based finite sets of sequential integers is greater than or equal to zero. (Contributed by Alexander van der Vekens, 8-Jun-2018.)
|- ( ( A e. ( 0 ... M ) /\ B e. ( 0 ... N ) ) -> 0 <_ ( A + B ) )
Theorem	elfzlble 39198	Membership of an integer in a finite set of sequential integers with the integer as upper bound and a lower bound less than or equal to the integer. (Contributed by AV, 21-Oct-2018.)
|- ( ( N e. ZZ /\ M e. NN0 ) -> N e. ( ( N - M ) ... N ) )
Theorem	elfzelfzlble 39199	Membership of an element of a finite set of sequential integers in a finite set of sequential integers with the same upper bound and a lower bound less than the upper bound. (Contributed by AV, 21-Oct-2018.)
|- ( ( M e. ZZ /\ K e. ( 0 ... N ) /\ N < ( M + K ) ) -> K e. ( ( N - M ) ... N ) )
21.33.7.18  Half-open integer ranges - extension
Theorem	subsubelfzo0 39200	Subtracting a difference from a number which is not less than the difference results in a bounded nonnegative integer. (Contributed by Alexander van der Vekens, 21-May-2018.)
|- ( ( A e. ( 0..^ N ) /\ I e. ( 0..^ N ) /\ -. I < ( N - A ) ) -> ( I - ( N - A ) ) e. ( 0..^ A ) )