P. 394 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 39301-39400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	restuni3 39301	The underlying set of a subspace induced by the subspace operator ↾t. The result can be applied, for instance, to topologies and sigma-algebras. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   =>    |- ( ph -> U. ( A ↾t B ) = ( U. A i^i B ) )
Theorem	rabssf 39302	Restricted class abstraction in a subclass relationship. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- F/_ x B   =>    |- ( { x e. A | ph } C_ B <-> A. x e. A ( ph -> x e. B ) )
Theorem	eliuniin2 39303*	Indexed union of indexed intersections. See eliincex 39293 for a counterexample showing that the precondition C =/= (/) cannot be simply dropped. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- F/_ x C   &    |- A = U_ x e. B |^|_ y e. C D   =>    |- ( C =/= (/) -> ( Z e. A <-> E. x e. B A. y e. C Z e. D ) )
Theorem	restuni4 39304	The underlying set of a subspace induced by the ↾t operator. The result can be applied, for instance, to topologies and sigma-algebras. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- ( ph -> A e. V )   &    |- ( ph -> B C_ U. A )   =>    |- ( ph -> U. ( A ↾t B ) = B )
Theorem	restuni6 39305	The underlying set of a subspace topology. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   =>    |- ( ph -> U. ( A ↾t B ) = ( U. A i^i B ) )
Theorem	restuni5 39306	The underlying set of a subspace induced by the ↾t operator. The result can be applied, for instance, to topologies and sigma-algebras. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- X = U. J   =>    |- ( ( J e. V /\ A C_ X ) -> A = U. ( J ↾t A ) )
Theorem	unirestss 39307	The union of an elementwise intersection is a subset of the underlying set. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   =>    |- ( ph -> U. ( A ↾t B ) C_ U. A )
Theorem	ne0d 39308	If a set has elements, then it is not empty. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- ( ph -> B e. A )   =>    |- ( ph -> A =/= (/) )
Theorem	iniin1 39309*	Indexed intersection of intersection. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- ( A =/= (/) -> ( |^|_ x e. A C i^i B ) = |^|_ x e. A ( C i^i B ) )
Theorem	iniin2 39310*	Indexed intersection of intersection. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- ( A =/= (/) -> ( B i^i |^|_ x e. A C ) = |^|_ x e. A ( B i^i C ) )
Theorem	cbvrabv2 39311*	A more general version of cbvrabv 3199. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- ( x = y -> A = B )   &    |- ( x = y -> ( ph <-> ps ) )   =>    |- { x e. A | ph } = { y e. B | ps }
Theorem	iinssiin 39312	Subset implication for an indexed intersection. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/ x ph   &    |- ( ( ph /\ x e. A ) -> B C_ C )   =>    |- ( ph -> |^|_ x e. A B C_ |^|_ x e. A C )
Theorem	eliind2 39313*	Membership in indexed intersection. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/ x ph   &    |- ( ph -> A e. V )   &    |- ( ( ph /\ x e. B ) -> A e. C )   =>    |- ( ph -> A e. |^|_ x e. B C )
Theorem	iinssd 39314*	Subset implication for an indexed intersection. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- ( ph -> X e. A )   &    |- ( x = X -> B = D )   &    |- ( ph -> D C_ C )   =>    |- ( ph -> |^|_ x e. A B C_ C )
Theorem	ralrimia 39315	Inference from Theorem 19.21 of [Margaris] p. 90 (restricted quantifier version). (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/ x ph   &    |- ( ( ph /\ x e. A ) -> ps )   =>    |- ( ph -> A. x e. A ps )
Theorem	tpid2g 39316	Closed theorem form of tpid2 4304. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- ( A e. B -> A e. { C , A , D } )
Theorem	rabbida2 39317	Equivalent wff's yield equal restricted class abstractions. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/ x ph   &    |- ( ph -> A = B )   &    |- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> { x e. A | ps } = { x e. B | ch } )
Theorem	iinexd 39318*	The existence of an indexed union. x is normally a free-variable parameter in B, which should be read B ( x ). (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- ( ph -> A =/= (/) )   &    |- ( ph -> A. x e. A B e. C )   =>    |- ( ph -> |^|_ x e. A B e. _V )
Theorem	rabexf 39319	Separation Scheme in terms of a restricted class abstraction. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/_ x A   &    |- A e. V   =>    |- { x e. A | ph } e. _V
Theorem	rabbida3 39320	Equivalent wff's yield equal restricted class abstractions. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/ x ph   &    |- ( ph -> ( ( x e. A /\ ps ) <-> ( x e. B /\ ch ) ) )   =>    |- ( ph -> { x e. A | ps } = { x e. B | ch } )
Theorem	resexd 39321	The restriction of a set is a set. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- ( ph -> A e. V )   =>    |- ( ph -> ( A |` B ) e. _V )
Theorem	tpid1g 39322	Closed theorem form of tpid1 4303. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- ( A e. B -> A e. { A , C , D } )
Theorem	fnexd 39323	If the domain of a function is a set, the function is a set. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- ( ph -> F Fn A )   &    |- ( ph -> A e. V )   =>    |- ( ph -> F e. _V )
Theorem	r19.36vf 39324	Restricted quantifier version of one direction of 19.36 2098. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/ x ps   =>    |- ( E. x e. A ( ph -> ps ) -> ( A. x e. A ph -> ps ) )
Theorem	raleqd 39325	Equality deduction for restricted universal quantifier. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/_ x A   &    |- F/_ x B   &    |- ( ph -> A = B )   =>    |- ( ph -> ( A. x e. A ps <-> A. x e. B ps ) )
Theorem	ralimda 39326	Deduction quantifying both antecedent and consequent. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/ x ph   &    |- ( ( ph /\ x e. A ) -> ( ps -> ch ) )   =>    |- ( ph -> ( A. x e. A ps -> A. x e. A ch ) )
Theorem	iinssf 39327	Subset implication for an indexed intersection. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/_ x C   =>    |- ( E. x e. A B C_ C -> |^|_ x e. A B C_ C )
Theorem	iinssdf 39328	Subset implication for an indexed intersection. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/_ x A   &    |- F/_ x X   &    |- F/_ x C   &    |- F/_ x D   &    |- ( ph -> X e. A )   &    |- ( x = X -> B = D )   &    |- ( ph -> D C_ C )   =>    |- ( ph -> |^|_ x e. A B C_ C )
Theorem	ifcli 39329	Membership (closure) of a conditional operator. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- A e. C   &    |- B e. C   =>    |- if ( ph , A , B ) e. C
Theorem	resabs2i 39330	Absorption law for restriction. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- B C_ C   =>    |- ( ( A |` B ) |` C ) = ( A |` B )
Theorem	ssdf2 39331	A sufficient condition for a subclass relationship. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- F/ x ph   &    |- F/_ x A   &    |- F/_ x B   &    |- ( ( ph /\ x e. A ) -> x e. B )   =>    |- ( ph -> A C_ B )
Theorem	rabssd 39332	Restricted class abstraction in a subclass relationship. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- F/ x ph   &    |- F/_ x B   &    |- ( ( ph /\ x e. A /\ ch ) -> x e. B )   =>    |- ( ph -> { x e. A | ch } C_ B )
Theorem	ssrind 39333	Add right intersection to subclass relation. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- ( ph -> A C_ B )   =>    |- ( ph -> ( A i^i C ) C_ ( B i^i C ) )
Theorem	rexnegd 39334	Minus a real number. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- ( ph -> A e. RR )   =>    |- ( ph -> -e A = -u A )
Theorem	rexlimd3 39335	* Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- F/ x ph   &    |- F/ x ch   &    |- ( ( ( ph /\ x e. A ) /\ ps ) -> ch )   =>    |- ( ph -> ( E. x e. A ps -> ch ) )
Theorem	resabs1i 39336	Absorption law for restriction. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- B C_ C   =>    |- ( ( A |` C ) |` B ) = ( A |` B )
Theorem	nel1nelin 39337	Membership in an intersection implies membership in the first set. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- ( -. A e. B -> -. A e. ( B i^i C ) )
Theorem	nel2nelin 39338	Membership in an intersection implies membership in the second set. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- ( -. A e. C -> -. A e. ( B i^i C ) )
Theorem	rexlimdva2 39339*	Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- ( ( ( ph /\ x e. A ) /\ ps ) -> ch )   =>    |- ( ph -> ( E. x e. A ps -> ch ) )
Theorem	nel1nelini 39340	Membership in an intersection implies membership in the first set. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- -. A e. B   =>    |- -. A e. ( B i^i C )
Theorem	nel2nelini 39341	Membership in an intersection implies membership in the second set. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- -. A e. C   =>    |- -. A e. ( B i^i C )
Theorem	eliunid 39342*	Membership in indexed union. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
|- ( ( x e. A /\ C e. B ) -> C e. U_ x e. A B )
Theorem	reximddv3 39343*	Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
|- ( ( ( ph /\ x e. A ) /\ ps ) -> ch )   &    |- ( ph -> E. x e. A ps )   =>    |- ( ph -> E. x e. A ch )
Theorem	reximdd 39344	Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
|- F/ x ph   &    |- ( ( ph /\ x e. A /\ ps ) -> ch )   &    |- ( ph -> E. x e. A ps )   =>    |- ( ph -> E. x e. A ch )
Theorem	unfid 39345	The union of two finite sets is finite. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
|- ( ph -> A e. Fin )   &    |- ( ph -> B e. Fin )   =>    |- ( ph -> ( A u. B ) e. Fin )
20.32.2  Functions
Theorem	unima 39346	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 39347	Equality deduction for functions. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> F = G )   &    |- ( ph -> F : A --> B )   =>    |- ( ph -> G : A --> B )
Theorem	fnresdmss 39348	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 39349*	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	fvmpt2bd 39350*	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 39351*	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 39352	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 39353*	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 39354	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 39355*	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 39356	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 39357*	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	rnmptpr 39358*	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 39359*	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 39360*	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 ) )
Theorem	f1oeq2d 39361	Equality deduction for one-to-one onto functions. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> A = B )   =>    |- ( ph -> ( F : A -1-1-onto-> C <-> F : B -1-1-onto-> C ) )
Theorem	rnresun 39362	Distribution law for range of a restriction over a union. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ran ( F |` ( A u. B ) ) = ( ran ( F |` A ) u. ran ( F |` B ) )
Theorem	f1oeq1d 39363	Equality deduction for one-to-one onto functions. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> F = G )   =>    |- ( ph -> ( F : A -1-1-onto-> B <-> G : A -1-1-onto-> B ) )
Theorem	dffo3f 39364*	An onto mapping expressed in terms of function values. As dffo3 6374 but with less disjoint vars constraints. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- F/_ x F   =>    |- ( F : A -onto-> B <-> ( F : A --> B /\ A. y e. B E. x e. A y = ( F ` x ) ) )
Theorem	rnresss 39365	The range of a restriction is a subset of the whole range. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ran ( A |` B ) C_ ran A
Theorem	elrnmptd 39366*	The range of a function in maps-to notation. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- F = ( x e. A |-> B )   &    |- ( ph -> E. x e. A C = B )   &    |- ( ph -> C e. V )   =>    |- ( ph -> C e. ran F )
Theorem	elrnmptf 39367	The range of a function in maps-to notation. Same as elrnmpt 5372, but using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- F/_ x C   &    |- F = ( x e. A |-> B )   =>    |- ( C e. V -> ( C e. ran F <-> E. x e. A C = B ) )
Theorem	rnmptssrn 39368*	Inclusion relation for two ranges expressed in map-to notation. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ( ph /\ x e. A ) -> B e. V )   &    |- ( ( ph /\ x e. A ) -> E. y e. C B = D )   =>    |- ( ph -> ran ( x e. A |-> B ) C_ ran ( y e. C |-> D ) )
Theorem	disjf1 39369*	A 1 to 1 mapping built from disjoint, nonempty sets. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- F/ x ph   &    |- F = ( x e. A |-> B )   &    |- ( ( ph /\ x e. A ) -> B e. V )   &    |- ( ( ph /\ x e. A ) -> B =/= (/) )   &    |- ( ph -> Disj x e. A B )   =>    |- ( ph -> F : A -1-1-> V )
Theorem	rnsnf 39370	The range of a function whose domain is a singleton. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> A e. V )   &    |- ( ph -> F : { A } --> B )   =>    |- ( ph -> ran F = { ( F ` A ) } )
Theorem	wessf1ornlem 39371*	Given a function F on a well ordered domain A there exists a subset of A such that F restricted to such subset is injective and onto the range of F (without using the axiom of choice). (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> F Fn A )   &    |- ( ph -> A e. V )   &    |- ( ph -> R We A )   &    |- G = ( y e. ran F |-> ( iota_ x e. ( `' F " { y } ) A. z e. ( `' F " { y } ) -. z R x ) )   =>    |- ( ph -> E. x e. ~P A ( F |` x ) : x -1-1-onto-> ran F )
Theorem	wessf1orn 39372*	Given a function F on a well ordered domain A there exists a subset of A such that F restricted to such subset is injective and onto the range of F (without using the axiom of choice). (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> F Fn A )   &    |- ( ph -> A e. V )   &    |- ( ph -> R We A )   =>    |- ( ph -> E. x e. ~P A ( F |` x ) : x -1-1-onto-> ran F )
Theorem	foelrnf 39373*	Property of a surjective function. As foelrn 6378 but with less disjoint vars constraints. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- F/_ x F   =>    |- ( ( F : A -onto-> B /\ C e. B ) -> E. x e. A C = ( F ` x ) )
Theorem	nelrnres 39374	If A is not in the range, it is not in the range of any restriction. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( -. A e. ran B -> -. A e. ran ( B |` C ) )
Theorem	disjrnmpt2 39375*	Disjointness of the range of a function in map-to notation. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- F = ( x e. A |-> B )   =>    |- (Disj x e. A B -> Disj y e. ran F y )
Theorem	elrnmpt1sf 39376*	Elementhood in an image set. Same as elrnmpt1s 5373, but using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- F/_ x C   &    |- F = ( x e. A |-> B )   &    |- ( x = D -> B = C )   =>    |- ( ( D e. A /\ C e. V ) -> C e. ran F )
Theorem	founiiun0 39377*	Union expressed as an indexed union, when a map onto is given. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( F : A -onto-> ( B u. { (/) } ) -> U. B = U_ x e. A ( F ` x ) )
Theorem	disjf1o 39378*	A bijection built from disjoint sets. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- F/ x ph   &    |- F = ( x e. A |-> B )   &    |- ( ( ph /\ x e. A ) -> B e. V )   &    |- ( ph -> Disj x e. A B )   &    |- C = { x e. A | B =/= (/) }   &    |- D = ( ran F \ { (/) } )   =>    |- ( ph -> ( F |` C ) : C -1-1-onto-> D )
Theorem	fompt 39379*	Express being onto for a mapping operation. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- F = ( x e. A |-> C )   =>    |- ( F : A -onto-> B <-> ( A. x e. A C e. B /\ A. y e. B E. x e. A y = C ) )
Theorem	disjinfi 39380*	Only a finite number of disjoint sets can have a non empty intersection with a finite set C (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ( ph /\ x e. A ) -> B e. V )   &    |- ( ph -> Disj x e. A B )   &    |- ( ph -> C e. Fin )   =>    |- ( ph -> { x e. A | ( B i^i C ) =/= (/) } e. Fin )
Theorem	fvovco 39381	Value of the composition of an operator, with a given function. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- ( ph -> F : X --> ( V X. W ) )   &    |- ( ph -> Y e. X )   =>    |- ( ph -> ( ( O o. F ) ` Y ) = ( ( 1st ` ( F ` Y ) ) O ( 2nd ` ( F ` Y ) ) ) )
Theorem	ssnnf1octb 39382*	There exists a bijection between a subset of NN and a given nonempty countable set. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- ( ( A ~<_ om /\ A =/= (/) ) -> E. f ( dom f C_ NN /\ f : dom f -1-1-onto-> A ) )
Theorem	mapdm0OLD 39383	The empty set is the only map with empty domain. (Contributed by Glauco Siliprandi, 11-Oct-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( A e. V -> ( A ^m (/) ) = { (/) } )
Theorem	nnf1oxpnn 39384	There is a bijection between the set of positive integers and the Cartesian product of the set of positive integers with itself. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- E. f f : NN -1-1-onto-> ( NN X. NN )
Theorem	rnmptssd 39385*	The range of an operation given by the "maps to" notation as a subset. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- F/ x ph   &    |- F = ( x e. A |-> B )   &    |- ( ( ph /\ x e. A ) -> B e. C )   =>    |- ( ph -> ran F C_ C )
Theorem	projf1o 39386*	A biijection from a set to a projection in a two dimensional space. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- ( ph -> A e. V )   &    |- F = ( x e. B |-> <. A , x >. )   =>    |- ( ph -> F : B -1-1-onto-> ( { A } X. B ) )
Theorem	fvmap 39387	Function value for a member of a set exponentiation. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ph -> F e. ( A ^m B ) )   &    |- ( ph -> C e. B )   =>    |- ( ph -> ( F ` C ) e. A )
Theorem	mapsnd 39388*	The value of set exponentiation with a singleton exponent. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   =>    |- ( ph -> ( A ^m { B } ) = { f | E. y e. A f = { <. B , y >. } } )
Theorem	fvixp2 39389*	Projection of a factor of an indexed Cartesian product. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
|- ( ( F e. X_ x e. A B /\ x e. A ) -> ( F ` x ) e. B )
Theorem	fidmfisupp 39390	A function with a finite domain is finitely supported. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
|- ( ph -> F : D --> R )   &    |- ( ph -> D e. Fin )   &    |- ( ph -> Z e. V )   =>    |- ( ph -> F finSupp Z )
Theorem	mapsnend 39391	Set exponentiation to a singleton exponent is equinumerous to its base. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   =>    |- ( ph -> ( A ^m { B } ) ~~ A )
Theorem	choicefi 39392*	For a finite set, a choice function exists, without using the axiom of choice. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
|- ( ph -> A e. Fin )   &    |- ( ( ph /\ x e. A ) -> B e. W )   &    |- ( ( ph /\ x e. A ) -> B =/= (/) )   =>    |- ( ph -> E. f ( f Fn A /\ A. x e. A ( f ` x ) e. B ) )
Theorem	mpct 39393	The exponentiation of a countable set to a finite set is countable. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
|- ( ph -> A ~<_ om )   &    |- ( ph -> B e. Fin )   =>    |- ( ph -> ( A ^m B ) ~<_ om )
Theorem	cnmetcoval 39394	Value of the distance function of the metric space of complex numbers, composed with a function. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- D = ( abs o. - )   &    |- ( ph -> F : A --> ( CC X. CC ) )   &    |- ( ph -> B e. A )   =>    |- ( ph -> ( ( D o. F ) ` B ) = ( abs ` ( ( 1st ` ( F ` B ) ) - ( 2nd ` ( F ` B ) ) ) ) )
Theorem	fcomptss 39395*	Express composition of two functions as a maps-to applying both in sequence. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- ( ph -> F : A --> B )   &    |- ( ph -> B C_ C )   &    |- ( ph -> G : C --> D )   =>    |- ( ph -> ( G o. F ) = ( x e. A |-> ( G ` ( F ` x ) ) ) )
Theorem	elmapsnd 39396	Membership in a set exponentiated to a singleton. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- ( ph -> F Fn { A } )   &    |- ( ph -> B e. V )   &    |- ( ph -> ( F ` A ) e. B )   =>    |- ( ph -> F e. ( B ^m { A } ) )
Theorem	mapss2 39397	Subset inheritance for set exponentiation. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ph -> C e. Z )   &    |- ( ph -> C =/= (/) )   =>    |- ( ph -> ( A C_ B <-> ( A ^m C ) C_ ( B ^m C ) ) )
Theorem	fsneq 39398	Equality condition for two functions defined on a singleton. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- ( ph -> A e. V )   &    |- B = { A }   &    |- ( ph -> F Fn B )   &    |- ( ph -> G Fn B )   =>    |- ( ph -> ( F = G <-> ( F ` A ) = ( G ` A ) ) )
Theorem	difmap 39399	Difference of two sets exponentiations. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ph -> C e. Z )   &    |- ( ph -> C =/= (/) )   =>    |- ( ph -> ( ( A \ B ) ^m C ) C_ ( ( A ^m C ) \ ( B ^m C ) ) )
Theorem	unirnmap 39400	Given a subset of a set exponentiation, the base set can be restricted. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- ( ph -> A e. V )   &    |- ( ph -> X C_ ( B ^m A ) )   =>    |- ( ph -> X C_ ( ran U. X ^m A ) )