P. 375 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 37401-37500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	elunnel2 37401	A member of a union that is not a member of the second class, is a member of the first class. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ( A e. ( B u. C ) /\ -. A e. C ) -> A e. B )
Theorem	adantlllr 37402	Deduction adding a conjunct to antecedent. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) -> ta )   =>    |- ( ( ( ( ( ph /\ et ) /\ ps ) /\ ch ) /\ th ) -> ta )
Theorem	3adantlr3 37403	Deduction adding a conjunct to antecedent. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ( ( ph /\ ( ps /\ ch ) ) /\ th ) -> ta )   =>    |- ( ( ( ph /\ ( ps /\ ch /\ et ) ) /\ th ) -> ta )
Theorem	nnxrd 37404	A natural number is an extended real. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. NN )   =>    |- ( ph -> A e. RR* )
Theorem	3adantll2 37405	Deduction adding a conjunct to antecedent. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) -> ta )   =>    |- ( ( ( ( ph /\ et /\ ps ) /\ ch ) /\ th ) -> ta )
Theorem	3adantll3 37406	Deduction adding a conjunct to antecedent. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) -> ta )   =>    |- ( ( ( ( ph /\ ps /\ et ) /\ ch ) /\ th ) -> ta )
Theorem	ssnel 37407	If not element of a set, then not element of a subset. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ( A C_ B /\ -. C e. B ) -> -. C e. A )
Theorem	adant423 37408	Deduction adding conjuncts to antecedent. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ( ph /\ ps ) -> ch )   =>    |- ( ( ( ( ph /\ th ) /\ ta ) /\ ps ) -> ch )
Theorem	jcn 37409	Inference joining the consequents of two premises. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> ps )   &    |- ( ph -> -. ch )   =>    |- ( ph -> -. ( ps -> ch ) )
Theorem	elabrexg 37410*	Elementhood in an image set. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ( x e. A /\ B e. V ) -> B e. { y | E. x e. A y = B } )
Theorem	unicntop 37411	The underlying set of the standard topology on the complex numers is the set of complex numbers. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- CC = U. ( TopOpen ` ℂfld )
Theorem	ifeq123d 37412	Equality deduction for conditional operator. (Contributed by Glauco Siliprandi, 11-Dec-2019.) AV: This theorem already exists as ifbieq12d 3920. TODO (NM): Please replace the usage of this theorem by ifbieq12d 3920 then delete this theorem. (New usage is discouraged.)
|- ( ph -> ( ps <-> ch ) )   &    |- ( ph -> A = B )   &    |- ( ph -> C = D )   =>    |- ( ph -> if ( ps , A , C ) = if ( ch , B , D ) )
Theorem	sncldre 37413	A singleton is closed w.r.t. the standard topology on the reals. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( A e. RR -> { A } e. ( Clsd ` ( topGen ` ran (,) ) ) )
Theorem	cnopn 37414	The set of complex numbers is open with respect to the standard topology on complex numbers. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- CC e. ( TopOpen ` ℂfld )
Theorem	n0p 37415	A polynomial with a nonzero coefficient is not the zero polynomial. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- ( ( P e. (Poly ` ZZ ) /\ N e. NN0 /\ ( (coeff ` P ) ` N ) =/= 0 ) -> P =/= 0p )
Theorem	rabeqd 37416*	Equality theorem for restricted class abstractions. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- ( ph -> A = B )   =>    |- ( ph -> { x e. A | ps } = { x e. B | ps } )
Theorem	pm2.65ni 37417	Inference rule for proof by contradiction. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- ( -. ph -> ps )   &    |- ( -. ph -> -. ps )   =>    |- ph
Theorem	raleqdOLD 37418*	Equality theorem for restricted universal quantifier. (Contributed by Glauco Siliprandi, 5-Apr-2020.) Obsolete as of 18-Jul-2020. Use raleqdv 3005 instead, which is the same. (New usage is discouraged.) (Proof modification is discouraged.)
|- ( ph -> A = B )   =>    |- ( ph -> ( A. x e. A ps <-> A. x e. B ps ) )
Theorem	elini 37419	Membership in an intersection of two classes. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- A e. B   &    |- A e. C   =>    |- A e. ( B i^i C )
Theorem	pwssfi 37420	Every element of the power set of A is finite if and only if A is finite. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( A e. V -> ( A e. Fin <-> ~P A C_ Fin ) )
Theorem	iuneq2df 37421	Equality deduction for indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- F/ x ph   &    |- ( ( ph /\ x e. A ) -> B = C )   =>    |- ( ph -> U_ x e. A B = U_ x e. A C )
Theorem	nnfoctb 37422*	There exists a mapping from NN onto any (nonempty) countable set. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ( A ~<_ om /\ A =/= (/) ) -> E. f f : NN -onto-> A )
Theorem	prssd 37423	A pair of elements of a class is a subset of the class. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> A e. C )   &    |- ( ph -> B e. C )   =>    |- ( ph -> { A , B } C_ C )
Theorem	ssinss1d 37424	Intersection preserves subclass relationship. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> A C_ C )   =>    |- ( ph -> ( A i^i B ) C_ C )
Theorem	0un 37425	The union of the empty set with a class is itself. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( (/) u. A ) = A
Theorem	elpwinss 37426	An element of the powerset of B intersected with anything, is a subset of B. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( A e. ( ~P B i^i C ) -> A C_ B )
Theorem	unidmex 37427	If F is a set, then U. dom F is a set (common case). (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> F e. V )   &    |- X = U. dom F   =>    |- ( ph -> X e. _V )
Theorem	ndisj2 37428*	A non disjointness condition. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( x = y -> B = C )   =>    |- ( -. Disj x e. A B <-> E. x e. A E. y e. A ( x =/= y /\ ( B i^i C ) =/= (/) ) )
Theorem	zenom 37429	The set of integer numbers is equinumerous to omega (the set of finite ordinal numbers). (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ZZ ~~ om
Theorem	rexsngf 37430*	Restricted existential quantification over a singleton. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- F/ x ps   &    |- ( x = A -> ( ph <-> ps ) )   =>    |- ( A e. V -> ( E. x e. { A } ph <-> ps ) )
Theorem	uzwo4 37431*	Well-ordering principle: any nonempty subset of an upper set of integers has the least element. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- F/ j ps   &    |- ( j = k -> ( ph <-> ps ) )   =>    |- ( ( S C_ ( ZZ>= ` M ) /\ E. j e. S ph ) -> E. j e. S ( ph /\ A. k e. S ( k < j -> -. ps ) ) )
Theorem	0in 37432	The intersection of the empty set with a class is the empty set. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( (/) i^i A ) = (/)
Theorem	unisn0 37433	The union of the singleton of the empty set is the empty set. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- U. { (/) } = (/)
Theorem	ssin0 37434	If two classes are disjoint, two respective subclasses are disjoint. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ( ( A i^i B ) = (/) /\ C C_ A /\ D C_ B ) -> ( C i^i D ) = (/) )
Theorem	inabs3 37435	Absorption law for intersection. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( C C_ B -> ( ( A i^i B ) i^i C ) = ( A i^i C ) )
Theorem	pwpwuni 37436	Relationship between power class and union. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( A e. V -> ( A e. ~P ~P B <-> U. A e. ~P B ) )
Theorem	disjiun2 37437*	In a disjoint collection, an indexed union is disjoint from an additional term. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> Disj x e. A B )   &    |- ( ph -> C C_ A )   &    |- ( ph -> D e. ( A \ C ) )   &    |- ( x = D -> B = E )   =>    |- ( ph -> ( U_ x e. C B i^i E ) = (/) )
Theorem	0pwfi 37438	The empty set is in any power set, and it's finite. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- (/) e. ( ~P A i^i Fin )
Theorem	ssinss2d 37439	Intersection preserves subclass relationship. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> B C_ C )   =>    |- ( ph -> ( A i^i B ) C_ C )
Theorem	zct 37440	The set of integer numbers is countable. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ZZ ~<_ om
Theorem	iunxsngf2 37441*	A singleton index picks out an instance of an indexed union's argument. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- F/_ x C   &    |- ( x = A -> B = C )   =>    |- ( A e. V -> U_ x e. { A } B = C )
Theorem	pwfin0 37442	A finite set always belongs to a power class. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ~P A i^i Fin ) =/= (/)
Theorem	uzct 37443	An upper integer set is countable. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- Z = ( ZZ>= ` N )   =>    |- Z ~<_ om
Theorem	iunxsnf 37444*	A singleton index picks out an instance of an indexed union's argument. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- F/_ x C   &    |- A e. _V   &    |- ( x = A -> B = C )   =>    |- U_ x e. { A } B = C
Theorem	fiiuncl 37445*	If a set is closed under the union of two sets, then it is closed under finite indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- F/ x ph   &    |- ( ( ph /\ x e. A ) -> B e. D )   &    |- ( ( ph /\ y e. D /\ z e. D ) -> ( y u. z ) e. D )   &    |- ( ph -> A e. Fin )   &    |- ( ph -> A =/= (/) )   =>    |- ( ph -> U_ x e. A B e. D )
Theorem	iunp1 37446*	The addition of the next set to a union indexed by a finite set of sequential integers. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- F/_ k B   &    |- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( k = ( N + 1 ) -> A = B )   =>    |- ( ph -> U_ k e. ( M ... ( N + 1 ) ) A = ( U_ k e. ( M ... N ) A u. B ) )
Theorem	fiunicl 37447*	If a set is closed under the union of two sets, then it is closed under finite union. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ( ph /\ x e. A /\ y e. A ) -> ( x u. y ) e. A )   &    |- ( ph -> A e. Fin )   &    |- ( ph -> A =/= (/) )   =>    |- ( ph -> U. A e. A )
Theorem	nnnfi 37448	The set of positive integers is infinite. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- -. NN e. Fin
Theorem	ixpeq2d 37449	Equality theorem for infinite Cartesian product. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- F/ x ph   &    |- ( ( ph /\ x e. A ) -> B = C )   =>    |- ( ph -> X_ x e. A B = X_ x e. A C )
Theorem	disjxp1 37450*	The sets of a cartesian product are disjoint if the sets in the first argument are disjoint. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- ( ph -> Disj x e. A B )   =>    |- ( ph -> Disj x e. A ( B X. C ) )
Theorem	elpwd 37451	Membership in a power class. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- ( ph -> A e. V )   &    |- ( ph -> A C_ B )   =>    |- ( ph -> A e. ~P B )
Theorem	disjsnxp 37452*	The sets in the cartesian product of singletons with other sets, are disjoint. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- Disj j e. A ( { j } X. B )
Theorem	ssfid 37453	A subset of a finite set is finite. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
|- ( ph -> A e. Fin )   &    |- ( ph -> B C_ A )   =>    |- ( ph -> B e. Fin )
Theorem	eliind 37454*	Membership in indexed intersection. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
|- ( ph -> A e. |^|_ x e. B C )   &    |- ( ph -> K e. B )   &    |- ( x = K -> ( A e. C <-> A e. D ) )   =>    |- ( ph -> A e. D )
Theorem	rspcef 37455	Restricted existential specialization, using implicit substitution. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
|- F/ x ps   &    |- F/_ x A   &    |- F/_ x B   &    |- ( x = A -> ( ph <-> ps ) )   =>    |- ( ( A e. B /\ ps ) -> E. x e. B ph )
Theorem	inn0f 37456	A non-empty intersection. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
|- F/_ x A   &    |- F/_ x B   =>    |- ( ( A i^i B ) =/= (/) <-> E. x e. A x e. B )
Theorem	ixpssmapc 37457*	An infinite Cartesian product is a subset of set exponentiation. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
|- F/ x ph   &    |- ( ph -> C e. V )   &    |- ( ( ph /\ x e. A ) -> B C_ C )   =>    |- ( ph -> X_ x e. A B C_ ( C ^m A ) )
Theorem	inn0 37458*	A non-empty intersection. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
|- ( ( A i^i B ) =/= (/) <-> E. x e. A x e. B )
Theorem	elintd 37459*	Membership in class intersection. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
|- F/ x ph   &    |- ( ph -> A e. V )   &    |- ( ( ph /\ x e. B ) -> A e. x )   =>    |- ( ph -> A e. |^| B )
Theorem	eqneltri 37460	If a class is not an element of another class, an equal class is also not an element. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
|- A = B   &    |- -. B e. C   =>    |- -. A e. C
Theorem	eqnbrtrd 37461	Substitution of equal classes into the negation of a binary relation. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
|- ( ph -> A = B )   &    |- ( ph -> -. B R C )   =>    |- ( ph -> -. A R C )
Theorem	ssdf 37462*	A sufficient condition for a subclass relationship. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
|- F/ x ph   &    |- ( ( ph /\ x e. A ) -> x e. B )   =>    |- ( ph -> A C_ B )
Theorem	brneqtrd 37463	Substitution of equal classes into the negation of a binary relation. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
|- ( ph -> -. A R B )   &    |- ( ph -> B = C )   =>    |- ( ph -> -. A R C )
Theorem	ssnct 37464	A set containing an uncountable set is itself uncountable. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
|- ( ph -> -. A ~<_ om )   &    |- ( ph -> A C_ B )   =>    |- ( ph -> -. B ~<_ om )
Theorem	ssuniint 37465*	Sufficient condition for being a subclass of the union of an intersection. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
|- F/ x ph   &    |- ( ph -> A e. V )   &    |- ( ( ph /\ x e. B ) -> A e. x )   =>    |- ( ph -> A C_ U. |^| B )
Theorem	elintdv 37466*	Membership in class intersection. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
|- ( ph -> A e. V )   &    |- ( ( ph /\ x e. B ) -> A e. x )   =>    |- ( ph -> A e. |^| B )
Theorem	ssd 37467*	A sufficient condition for a subclass relationship. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
|- ( ( ph /\ x e. A ) -> x e. B )   =>    |- ( ph -> A C_ B )
Theorem	ralimralim 37468	Introducing any antecedent in a restricted universal quantification. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- ( A. x e. A ph -> A. x e. A ( ps -> ph ) )
Theorem	snelmap 37469	Membership of the element in the range of a constant map. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ph -> A =/= (/) )   &    |- ( ph -> ( A X. { x } ) e. ( B ^m A ) )   =>    |- ( ph -> x e. B )
Theorem	difex 37470	Existence of a difference. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- A e. V   =>    |- ( A \ B ) e. _V
Theorem	dfcleqf 37471	Equality connective between classes. Same as dfcleq 2456, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- F/_ x A   &    |- F/_ x B   =>    |- ( A = B <-> A. x ( x e. A <-> x e. B ) )
Theorem	xrnmnfpnf 37472	An extended real that is neither real nor minus infinity, is plus infinity. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- ( ph -> A e. RR* )   &    |- ( ph -> -. A e. RR )   &    |- ( ph -> A =/= -oo )   =>    |- ( ph -> A = +oo )
Theorem	nelrnmpt 37473*	Non-membership in the range of a function in maps-to notaion. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- F/ x ph   &    |- F = ( x e. A |-> B )   &    |- ( ph -> C e. V )   &    |- ( ( ph /\ x e. A ) -> C =/= B )   =>    |- ( ph -> -. C e. ran F )
Theorem	snn0d 37474	The singleton of a set is not empty. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- ( ph -> A e. V )   =>    |- ( ph -> { A } =/= (/) )
Theorem	rabid3 37475	Membership in a restricted abstraction (special case). (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- A = { x e. B | ph }   =>    |- ( x e. A <-> ( x e. B /\ ph ) )
Theorem	opelxpd 37476	Ordered pair membership in a Cartesian product (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- ( ph -> A e. C )   &    |- ( ph -> B e. D )   =>    |- ( ph -> <. A , B >. e. ( C X. D ) )
Theorem	iuneq1i 37477*	Equality theorem for indexed union. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- A = B   =>    |- U_ x e. A C = U_ x e. B C
Theorem	nssrex 37478*	Negation of subclass relationship. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- ( -. A C_ B <-> E. x e. A -. x e. B )
Theorem	nelpr2 37479	If a class is not an element of an unordered pair, it is not the second listed element. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- ( ph -> A e. V )   &    |- ( ph -> -. A e. { B , C } )   =>    |- ( ph -> A =/= C )
Theorem	nelpr1 37480	If a class is not an element of an unordered pair, it is not the first listed element. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- ( ph -> A e. V )   &    |- ( ph -> -. A e. { B , C } )   =>    |- ( ph -> A =/= B )
Theorem	iunssf 37481	Subset theorem for an indexed union. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- F/_ x C   =>    |- ( U_ x e. A B C_ C <-> A. x e. A B C_ C )
Theorem	elpwi2 37482	Membership in a power class. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- B e. V   &    |- A C_ B   =>    |- A e. ~P B
21.30.2  Functions
Theorem	unima 37483	Image of a union. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ( F Fn A /\ B C_ A /\ C C_ A ) -> ( F " ( B u. C ) ) = ( ( F " B ) u. ( F " C ) ) )
Theorem	feq1dd 37484	Equality deduction for functions. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> F = G )   &    |- ( ph -> F : A --> B )   =>    |- ( ph -> G : A --> B )
Theorem	fnresdmss 37485	A function does not change when restricted to a set that contains its domain. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ( F Fn A /\ A C_ B ) -> ( F |` B ) = F )
Theorem	fmptsnxp 37486*	Maps-to notation and cross product for a singleton function. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ( A e. V /\ B e. W ) -> ( x e. { A } |-> B ) = ( { A } X. { B } ) )
Theorem	mptex2 37487*	If a class given as a map-to notation is a set, it's image values are set. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> ( t e. A |-> B ) : A --> C )   =>    |- ( ( ph /\ t e. A ) -> B e. C )
Theorem	fvmpt2bd 37488*	Value of a function given by the "maps to" notation. Deduction version. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> F = ( x e. A |-> B ) )   =>    |- ( ( ph /\ x e. A /\ B e. C ) -> ( F ` x ) = B )
Theorem	rnmptfi 37489*	The range of a function with finite domain is finite. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- A = ( x e. B |-> C )   =>    |- ( B e. Fin -> ran A e. Fin )
Theorem	fresin2 37490	Restriction of a function with respect to the intersection with its domain. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( F : A --> B -> ( F |` ( C i^i A ) ) = ( F |` C ) )
Theorem	rnmptc 37491*	Range of a constant function in map to notation. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- F = ( x e. A |-> B )   &    |- ( ( ph /\ x e. A ) -> B e. C )   &    |- ( ph -> A =/= (/) )   =>    |- ( ph -> ran F = { B } )
Theorem	ffi 37492	A function with finite domain is finite. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ( F : A --> B /\ A e. Fin ) -> F e. Fin )
Theorem	suprnmpt 37493*	An explicit bound for the range of a bounded function. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A =/= (/) )   &    |- ( ( ph /\ x e. A ) -> B e. RR )   &    |- ( ph -> E. y e. RR A. x e. A B <_ y )   &    |- F = ( x e. A |-> B )   &    |- C = sup ( ran F , RR , < )   =>    |- ( ph -> ( C e. RR /\ A. x e. A B <_ C ) )
Theorem	rnffi 37494	The range of a function with finite domain is finite. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ( F : A --> B /\ A e. Fin ) -> ran F e. Fin )
Theorem	mptelpm 37495*	A function in maps-to notation is a partial map . (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- ( ( ph /\ x e. A ) -> B e. C )   &    |- ( ph -> A C_ D )   &    |- ( ph -> C e. V )   &    |- ( ph -> D e. W )   =>    |- ( ph -> ( x e. A |-> B ) e. ( C ^pm D ) )
Theorem	f1oeq3d 37496	Equality deduction for one-to-one onto functions. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> A = B )   =>    |- ( ph -> ( F : C -1-1-onto-> A <-> F : C -1-1-onto-> B ) )
Theorem	fimass 37497	The image of a class is a subset of its codomain. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( F : A --> B -> ( F " X ) C_ B )
Theorem	rnmptpr 37498*	Range of a function defined on an unordered pair. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- F = ( x e. { A , B } |-> C )   &    |- ( x = A -> C = D )   &    |- ( x = B -> C = E )   =>    |- ( ph -> ran F = { D , E } )
Theorem	resmpti 37499*	Restriction of the mapping operation. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- B C_ A   =>    |- ( ( x e. A |-> C ) |` B ) = ( x e. B |-> C )
Theorem	founiiun 37500*	Union expressed as an indexed union, when a map onto is given. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( F : A -onto-> B -> U. B = U_ x e. A ( F ` x ) )