P. 54 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 5301-5400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	cnvex 5301	The converse of a set is a set. Corollary 6.8(1) of [TakeutiZaring] p. 26. (Contributed by NM, 19-Dec-2003.)
|- A e. _V   =>    |- `' A e. _V
Theorem	relcnvexb 5302	A relation is a set iff its converse is a set. (Contributed by FL, 3-Mar-2007.)
|- ( Rel R -> ( R e. _V <-> `' R e. _V ) )
Theorem	ressn 5303	Restriction of a class to a singleton. (Contributed by Mario Carneiro, 28-Dec-2014.)
|- ( A |` { B } ) = ( { B } X. ( A " { B } ) )
Theorem	cnviinm 5304*	The converse of an intersection is the intersection of the converse. (Contributed by Jim Kingdon, 18-Dec-2018.)
|- ( E. y y e. A -> `' |^|_ x e. A B = |^|_ x e. A `' B )
Theorem	cnvpom 5305*	The converse of a partial order relation is a partial order relation. (Contributed by NM, 15-Jun-2005.)
|- ( E. x x e. A -> ( R Po A <-> `' R Po A ) )
Theorem	cnvsom 5306*	The converse of a strict order relation is a strict order relation. (Contributed by Jim Kingdon, 19-Dec-2018.)
|- ( E. x x e. A -> ( R Or A <-> `' R Or A ) )
Theorem	coexg 5307	The composition of two sets is a set. (Contributed by NM, 19-Mar-1998.)
|- ( ( A e. V /\ B e. W ) -> ( A o. B ) e. _V )
Theorem	coex 5308	The composition of two sets is a set. (Contributed by NM, 15-Dec-2003.)
|- A e. _V   &    |- B e. _V   =>    |- ( A o. B ) e. _V
Theorem	xpcom 5309*	Composition of two cross products. (Contributed by Jim Kingdon, 20-Dec-2018.)
|- ( E. x x e. B -> ( ( B X. C ) o. ( A X. B ) ) = ( A X. C ) )
2.6.7  Definite description binder (inverted iota)
Syntax	cio 5310	Extend class notation with Russell's definition description binder (inverted iota).
class ( iota x ph )
Theorem	iotajust 5311*	Soundness justification theorem for df-iota 5312. (Contributed by Andrew Salmon, 29-Jun-2011.)
|- U. { y | { x | ph } = { y } } = U. { z | { x | ph } = { z } }
Definition	df-iota 5312*	Define Russell's definition description binder, which can be read as "the unique x such that ph," where ph ordinarily contains x as a free variable. Our definition is meaningful only when there is exactly one x such that ph is true (see iotaval 5324); otherwise, it evaluates to the empty set (see iotanul 5328). Russell used the inverted iota symbol iota to represent the binder. Sometimes proofs need to expand an iota-based definition. That is, given "X = the x for which ... x ... x ..." holds, the proof needs to get to "... X ... X ...". A general strategy to do this is to use iotacl 5337 (for unbounded iota). This can be easier than applying a version that applies an explicit substitution, because substituting an iota into its own property always has a bound variable clash which must be first renamed or else guarded with NF. (Contributed by Andrew Salmon, 30-Jun-2011.)
|- ( iota x ph ) = U. { y | { x | ph } = { y } }
Theorem	dfiota2 5313*	Alternate definition for descriptions. Definition 8.18 in [Quine] p. 56. (Contributed by Andrew Salmon, 30-Jun-2011.)
|- ( iota x ph ) = U. { y | A. x ( ph <-> x = y ) }
Theorem	nfiota1 5314	Bound-variable hypothesis builder for the iota class. (Contributed by Andrew Salmon, 11-Jul-2011.) (Revised by Mario Carneiro, 15-Oct-2016.)
|- F/_ x ( iota x ph )
Theorem	nfiotadw 5315*	Bound-variable hypothesis builder for the iota class. (Contributed by Jim Kingdon, 21-Dec-2018.)
|- F/ y ph   &    |- ( ph -> F/ x ps )   =>    |- ( ph -> F/_ x ( iota y ps ) )
Theorem	nfiotaw 5316*	Bound-variable hypothesis builder for the iota class. (Contributed by NM, 23-Aug-2011.)
|- F/ x ph   =>    |- F/_ x ( iota y ph )
Theorem	cbviota 5317	Change bound variables in a description binder. (Contributed by Andrew Salmon, 1-Aug-2011.)
|- ( x = y -> ( ph <-> ps ) )   &    |- F/ y ph   &    |- F/ x ps   =>    |- ( iota x ph ) = ( iota y ps )
Theorem	cbviotavw 5318*	Change bound variables in a description binder. Version of cbviotav 5319 with a disjoint variable condition. (Contributed by Andrew Salmon, 1-Aug-2011.) (Revised by GG, 30-Sep-2024.)
|- ( x = y -> ( ph <-> ps ) )   =>    |- ( iota x ph ) = ( iota y ps )
Theorem	cbviotav 5319*	Change bound variables in a description binder. (Contributed by Andrew Salmon, 1-Aug-2011.)
|- ( x = y -> ( ph <-> ps ) )   =>    |- ( iota x ph ) = ( iota y ps )
Theorem	sb8iota 5320	Variable substitution in description binder. Compare sb8eu 2093. (Contributed by NM, 18-Mar-2013.)
|- F/ y ph   =>    |- ( iota x ph ) = ( iota y [ y / x ] ph )
Theorem	iotaeq 5321	Equality theorem for descriptions. (Contributed by Andrew Salmon, 30-Jun-2011.)
|- ( A. x x = y -> ( iota x ph ) = ( iota y ph ) )
Theorem	iotabi 5322	Equivalence theorem for descriptions. (Contributed by Andrew Salmon, 30-Jun-2011.)
|- ( A. x ( ph <-> ps ) -> ( iota x ph ) = ( iota x ps ) )
Theorem	uniabio 5323*	Part of Theorem 8.17 in [Quine] p. 56. This theorem serves as a lemma for the fundamental property of iota. (Contributed by Andrew Salmon, 11-Jul-2011.)
|- ( A. x ( ph <-> x = y ) -> U. { x | ph } = y )
Theorem	iotaval 5324*	Theorem 8.19 in [Quine] p. 57. This theorem is the fundamental property of iota. (Contributed by Andrew Salmon, 11-Jul-2011.)
|- ( A. x ( ph <-> x = y ) -> ( iota x ph ) = y )
Theorem	iotauni 5325	Equivalence between two different forms of iota. (Contributed by Andrew Salmon, 12-Jul-2011.)
|- ( E! x ph -> ( iota x ph ) = U. { x | ph } )
Theorem	iotaint 5326	Equivalence between two different forms of iota. (Contributed by Mario Carneiro, 24-Dec-2016.)
|- ( E! x ph -> ( iota x ph ) = |^| { x | ph } )
Theorem	iota1 5327	Property of iota. (Contributed by NM, 23-Aug-2011.) (Revised by Mario Carneiro, 23-Dec-2016.)
|- ( E! x ph -> ( ph <-> ( iota x ph ) = x ) )
Theorem	iotanul 5328	Theorem 8.22 in [Quine] p. 57. This theorem is the result if there isn't exactly one x that satisfies ph. (Contributed by Andrew Salmon, 11-Jul-2011.)
|- ( -. E! x ph -> ( iota x ph ) = (/) )
Theorem	euiotaex 5329	Theorem 8.23 in [Quine] p. 58, with existential uniqueness condition added. This theorem proves the existence of the iota class under our definition. (Contributed by Jim Kingdon, 21-Dec-2018.)
|- ( E! x ph -> ( iota x ph ) e. _V )
Theorem	iotass 5330*	Value of iota based on a proposition which holds only for values which are subsets of a given class. (Contributed by Mario Carneiro and Jim Kingdon, 21-Dec-2018.)
|- ( A. x ( ph -> x C_ A ) -> ( iota x ph ) C_ A )
Theorem	iotaexab 5331	Existence of the iota class when all the possible values are contained in a set. (Contributed by Jim Kingdon, 27-May-2025.)
|- ( { x | ph } e. V -> ( iota x ph ) e. _V )
Theorem	iota4 5332	Theorem *14.22 in [WhiteheadRussell] p. 190. (Contributed by Andrew Salmon, 12-Jul-2011.)
|- ( E! x ph -> [. ( iota x ph ) / x ]. ph )
Theorem	iota4an 5333	Theorem *14.23 in [WhiteheadRussell] p. 191. (Contributed by Andrew Salmon, 12-Jul-2011.)
|- ( E! x ( ph /\ ps ) -> [. ( iota x ( ph /\ ps ) ) / x ]. ph )
Theorem	iota5 5334*	A method for computing iota. (Contributed by NM, 17-Sep-2013.)
|- ( ( ph /\ A e. V ) -> ( ps <-> x = A ) )   =>    |- ( ( ph /\ A e. V ) -> ( iota x ps ) = A )
Theorem	iotabidv 5335*	Formula-building deduction for iota. (Contributed by NM, 20-Aug-2011.)
|- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( iota x ps ) = ( iota x ch ) )
Theorem	iotabii 5336	Formula-building deduction for iota. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- ( ph <-> ps )   =>    |- ( iota x ph ) = ( iota x ps )
Theorem	iotacl 5337	Membership law for descriptions. This can useful for expanding an unbounded iota-based definition (see df-iota 5312). (Contributed by Andrew Salmon, 1-Aug-2011.)
|- ( E! x ph -> ( iota x ph ) e. { x | ph } )
Theorem	iota2df 5338	A condition that allows us to represent "the unique element such that ph " with a class expression A. (Contributed by NM, 30-Dec-2014.)
|- ( ph -> B e. V )   &    |- ( ph -> E! x ps )   &    |- ( ( ph /\ x = B ) -> ( ps <-> ch ) )   &    |- F/ x ph   &    |- ( ph -> F/ x ch )   &    |- ( ph -> F/_ x B )   =>    |- ( ph -> ( ch <-> ( iota x ps ) = B ) )
Theorem	iota2d 5339*	A condition that allows us to represent "the unique element such that ph " with a class expression A. (Contributed by NM, 30-Dec-2014.)
|- ( ph -> B e. V )   &    |- ( ph -> E! x ps )   &    |- ( ( ph /\ x = B ) -> ( ps <-> ch ) )   =>    |- ( ph -> ( ch <-> ( iota x ps ) = B ) )
Theorem	eliota 5340*	An element of an iota expression. (Contributed by Jim Kingdon, 22-Nov-2024.)
|- ( A e. ( iota x ph ) <-> E. y ( A e. y /\ A. x ( ph <-> x = y ) ) )
Theorem	eliotaeu 5341	An inhabited iota expression has a unique value. (Contributed by Jim Kingdon, 22-Nov-2024.)
|- ( A e. ( iota x ph ) -> E! x ph )
Theorem	iota2 5342*	The unique element such that ph. (Contributed by Jeff Madsen, 1-Jun-2011.) (Revised by Mario Carneiro, 23-Dec-2016.)
|- ( x = A -> ( ph <-> ps ) )   =>    |- ( ( A e. B /\ E! x ph ) -> ( ps <-> ( iota x ph ) = A ) )
Theorem	sniota 5343	A class abstraction with a unique member can be expressed as a singleton. (Contributed by Mario Carneiro, 23-Dec-2016.)
|- ( E! x ph -> { x | ph } = { ( iota x ph ) } )
Theorem	iotam 5344*	Representation of "the unique element such that ph " with a class expression A which is inhabited (that means that "the unique element such that ph " exists). (Contributed by AV, 30-Jan-2024.)
|- ( x = A -> ( ph <-> ps ) )   =>    |- ( ( A e. V /\ E. w w e. A /\ A = ( iota x ph ) ) -> ps )
Theorem	csbiotag 5345*	Class substitution within a description binder. (Contributed by Scott Fenton, 6-Oct-2017.)
|- ( A e. V -> [_ A / x ]_ ( iota y ph ) = ( iota y [. A / x ]. ph ) )
2.6.8  Functions
Syntax	wfun 5346	Extend the definition of a wff to include the function predicate. (Read: A is a function.)
wff Fun A
Syntax	wfn 5347	Extend the definition of a wff to include the function predicate with a domain. (Read: A is a function on B.)
wff A Fn B
Syntax	wf 5348	Extend the definition of a wff to include the function predicate with domain and codomain. (Read: F maps A into B.)
wff F : A --> B
Syntax	wf1 5349	Extend the definition of a wff to include one-to-one functions. (Read: F maps A one-to-one into B.) The notation ("1-1" above the arrow) is from Definition 6.15(5) of [TakeutiZaring] p. 27.
wff F : A -1-1-> B
Syntax	wfo 5350	Extend the definition of a wff to include onto functions. (Read: F maps A onto B.) The notation ("onto" below the arrow) is from Definition 6.15(4) of [TakeutiZaring] p. 27.
wff F : A -onto-> B
Syntax	wf1o 5351	Extend the definition of a wff to include one-to-one onto functions. (Read: F maps A one-to-one onto B.) The notation ("1-1" above the arrow and "onto" below the arrow) is from Definition 6.15(6) of [TakeutiZaring] p. 27.
wff F : A -1-1-onto-> B
Syntax	cfv 5352	Extend the definition of a class to include the value of a function. (Read: The value of F at A, or " F of A.")
class ( F ` A )
Syntax	wiso 5353	Extend the definition of a wff to include the isomorphism property. (Read: H is an R, S isomorphism of A onto B.)
wff H Isom R , S ( A , B )
Definition	df-fun 5354	Define predicate that determines if some class A is a function. Definition 10.1 of [Quine] p. 65. For example, the expression Fun _I is true (funi 5384). This is not the same as defining a specific function's mapping, which is typically done using the format of cmpt 4171 with the maps-to notation (see df-mpt 4173). Contrast this predicate with the predicates to determine if some class is a function with a given domain (df-fn 5355), a function with a given domain and codomain (df-f 5356), a one-to-one function (df-f1 5357), an onto function (df-fo 5358), or a one-to-one onto function (df-f1o 5359). For alternate definitions, see dffun2 5362, dffun4 5363, dffun6 5366, dffun7 5379, dffun8 5380, and dffun9 5381. (Contributed by NM, 1-Aug-1994.)
|- ( Fun A <-> ( Rel A /\ ( A o. `' A ) C_ _I ) )
Definition	df-fn 5355	Define a function with domain. Definition 6.15(1) of [TakeutiZaring] p. 27. (Contributed by NM, 1-Aug-1994.)
|- ( A Fn B <-> ( Fun A /\ dom A = B ) )
Definition	df-f 5356	Define a function (mapping) with domain and codomain. Definition 6.15(3) of [TakeutiZaring] p. 27. (Contributed by NM, 1-Aug-1994.)
|- ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )
Definition	df-f1 5357	Define a one-to-one function. Compare Definition 6.15(5) of [TakeutiZaring] p. 27. We use their notation ("1-1" above the arrow). (Contributed by NM, 1-Aug-1994.)
|- ( F : A -1-1-> B <-> ( F : A --> B /\ Fun `' F ) )
Definition	df-fo 5358	Define an onto function. Definition 6.15(4) of [TakeutiZaring] p. 27. We use their notation ("onto" under the arrow). (Contributed by NM, 1-Aug-1994.)
|- ( F : A -onto-> B <-> ( F Fn A /\ ran F = B ) )
Definition	df-f1o 5359	Define a one-to-one onto function. Compare Definition 6.15(6) of [TakeutiZaring] p. 27. We use their notation ("1-1" above the arrow and "onto" below the arrow). (Contributed by NM, 1-Aug-1994.)
|- ( F : A -1-1-onto-> B <-> ( F : A -1-1-> B /\ F : A -onto-> B ) )
Definition	df-fv 5360*	Define the value of a function, ( F ` A ), also known as function application. For example, ( _I ` (/) ) = (/). Typically, function F is defined using maps-to notation (see df-mpt 4173), but this is not required. For example, F = { <. 2 , 6 >. , <. 3 , 9 >. } -> ( F ` 3 ) = 9. We will later define two-argument functions using ordered pairs as ( A F B ) = ( F ` <. A , B >. ). This particular definition is quite convenient: it can be applied to any class and evaluates to the empty set when it is not meaningful. The left apostrophe notation originated with Peano and was adopted in Definition *30.01 of [WhiteheadRussell] p. 235, Definition 10.11 of [Quine] p. 68, and Definition 6.11 of [TakeutiZaring] p. 26. It means the same thing as the more familiar F ( A ) notation for a function's value at A, i.e., " F of A," but without context-dependent notational ambiguity. (Contributed by NM, 1-Aug-1994.) Revised to use iota. (Revised by Scott Fenton, 6-Oct-2017.)
|- ( F ` A ) = ( iota x A F x )
Definition	df-isom 5361*	Define the isomorphism predicate. We read this as " H is an R, S isomorphism of A onto B". Normally, R and S are ordering relations on A and B respectively. Definition 6.28 of [TakeutiZaring] p. 32, whose notation is the same as ours except that R and S are subscripts. (Contributed by NM, 4-Mar-1997.)
|- ( H Isom R , S ( A , B ) <-> ( H : A -1-1-onto-> B /\ A. x e. A A. y e. A ( x R y <-> ( H ` x ) S ( H ` y ) ) ) )
Theorem	dffun2 5362*	Alternate definition of a function. (Contributed by NM, 29-Dec-1996.)
|- ( Fun A <-> ( Rel A /\ A. x A. y A. z ( ( x A y /\ x A z ) -> y = z ) ) )
Theorem	dffun4 5363*	Alternate definition of a function. Definition 6.4(4) of [TakeutiZaring] p. 24. (Contributed by NM, 29-Dec-1996.)
|- ( Fun A <-> ( Rel A /\ A. x A. y A. z ( ( <. x , y >. e. A /\ <. x , z >. e. A ) -> y = z ) ) )
Theorem	dffun5r 5364*	A way of proving a relation is a function, analogous to mo2r 2133. (Contributed by Jim Kingdon, 27-May-2020.)
|- ( ( Rel A /\ A. x E. z A. y ( <. x , y >. e. A -> y = z ) ) -> Fun A )
Theorem	dffun6f 5365*	Definition of function, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 9-Mar-1995.) (Revised by Mario Carneiro, 15-Oct-2016.)
|- F/_ x A   &    |- F/_ y A   =>    |- ( Fun A <-> ( Rel A /\ A. x E* y x A y ) )
Theorem	dffun6 5366*	Alternate definition of a function using "at most one" notation. (Contributed by NM, 9-Mar-1995.)
|- ( Fun F <-> ( Rel F /\ A. x E* y x F y ) )
Theorem	funmo 5367*	A function has at most one value for each argument. (Contributed by NM, 24-May-1998.)
|- ( Fun F -> E* y A F y )
Theorem	dffun4f 5368*	Definition of function like dffun4 5363 but using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Jim Kingdon, 17-Mar-2019.)
|- F/_ x A   &    |- F/_ y A   &    |- F/_ z A   =>    |- ( Fun A <-> ( Rel A /\ A. x A. y A. z ( ( <. x , y >. e. A /\ <. x , z >. e. A ) -> y = z ) ) )
Theorem	funrel 5369	A function is a relation. (Contributed by NM, 1-Aug-1994.)
|- ( Fun A -> Rel A )
Theorem	0nelfun 5370	A function does not contain the empty set. (Contributed by BJ, 26-Nov-2021.)
|- ( Fun R -> (/) e/ R )
Theorem	funss 5371	Subclass theorem for function predicate. (Contributed by NM, 16-Aug-1994.) (Proof shortened by Mario Carneiro, 24-Jun-2014.)
|- ( A C_ B -> ( Fun B -> Fun A ) )
Theorem	funeq 5372	Equality theorem for function predicate. (Contributed by NM, 16-Aug-1994.)
|- ( A = B -> ( Fun A <-> Fun B ) )
Theorem	funeqi 5373	Equality inference for the function predicate. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
|- A = B   =>    |- ( Fun A <-> Fun B )
Theorem	funeqd 5374	Equality deduction for the function predicate. (Contributed by NM, 23-Feb-2013.)
|- ( ph -> A = B )   =>    |- ( ph -> ( Fun A <-> Fun B ) )
Theorem	nffun 5375	Bound-variable hypothesis builder for a function. (Contributed by NM, 30-Jan-2004.)
|- F/_ x F   =>    |- F/ x Fun F
Theorem	sbcfung 5376	Distribute proper substitution through the function predicate. (Contributed by Alexander van der Vekens, 23-Jul-2017.)
|- ( A e. V -> ( [. A / x ]. Fun F <-> Fun [_ A / x ]_ F ) )
Theorem	funeu 5377*	There is exactly one value of a function. (Contributed by NM, 22-Apr-2004.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)
|- ( ( Fun F /\ A F B ) -> E! y A F y )
Theorem	funeu2 5378*	There is exactly one value of a function. (Contributed by NM, 3-Aug-1994.)
|- ( ( Fun F /\ <. A , B >. e. F ) -> E! y <. A , y >. e. F )
Theorem	dffun7 5379*	Alternate definition of a function. One possibility for the definition of a function in [Enderton] p. 42. (Enderton's definition is ambiguous because "there is only one" could mean either "there is at most one" or "there is exactly one". However, dffun8 5380 shows that it does not matter which meaning we pick.) (Contributed by NM, 4-Nov-2002.)
|- ( Fun A <-> ( Rel A /\ A. x e. dom A E* y x A y ) )
Theorem	dffun8 5380*	Alternate definition of a function. One possibility for the definition of a function in [Enderton] p. 42. Compare dffun7 5379. (Contributed by NM, 4-Nov-2002.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)
|- ( Fun A <-> ( Rel A /\ A. x e. dom A E! y x A y ) )
Theorem	dffun9 5381*	Alternate definition of a function. (Contributed by NM, 28-Mar-2007.) (Revised by NM, 16-Jun-2017.)
|- ( Fun A <-> ( Rel A /\ A. x e. dom A E* y e. ran A x A y ) )
Theorem	funfn 5382	An equivalence for the function predicate. (Contributed by NM, 13-Aug-2004.)
|- ( Fun A <-> A Fn dom A )
Theorem	funfnd 5383	A function is a function over its domain. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- ( ph -> Fun A )   =>    |- ( ph -> A Fn dom A )
Theorem	funi 5384	The identity relation is a function. Part of Theorem 10.4 of [Quine] p. 65. (Contributed by NM, 30-Apr-1998.)
|- Fun _I
Theorem	nfunv 5385	The universe is not a function. (Contributed by Raph Levien, 27-Jan-2004.)
|- -. Fun _V
Theorem	funopg 5386	A Kuratowski ordered pair is a function only if its components are equal. (Contributed by NM, 5-Jun-2008.) (Revised by Mario Carneiro, 26-Apr-2015.)
|- ( ( A e. V /\ B e. W /\ Fun <. A , B >. ) -> A = B )
Theorem	funopab 5387*	A class of ordered pairs is a function when there is at most one second member for each pair. (Contributed by NM, 16-May-1995.)
|- ( Fun { <. x , y >. | ph } <-> A. x E* y ph )
Theorem	funopabeq 5388*	A class of ordered pairs of values is a function. (Contributed by NM, 14-Nov-1995.)
|- Fun { <. x , y >. | y = A }
Theorem	funopab4 5389*	A class of ordered pairs of values in the form used by df-mpt 4173 is a function. (Contributed by NM, 17-Feb-2013.)
|- Fun { <. x , y >. | ( ph /\ y = A ) }
Theorem	funmpt 5390	A function in maps-to notation is a function. (Contributed by Mario Carneiro, 13-Jan-2013.)
|- Fun ( x e. A |-> B )
Theorem	funmpt2 5391	Functionality of a class given by a maps-to notation. (Contributed by FL, 17-Feb-2008.) (Revised by Mario Carneiro, 31-May-2014.)
|- F = ( x e. A |-> B )   =>    |- Fun F
Theorem	funco 5392	The composition of two functions is a function. Exercise 29 of [TakeutiZaring] p. 25. (Contributed by NM, 26-Jan-1997.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)
|- ( ( Fun F /\ Fun G ) -> Fun ( F o. G ) )
Theorem	funres 5393	A restriction of a function is a function. Compare Exercise 18 of [TakeutiZaring] p. 25. (Contributed by NM, 16-Aug-1994.)
|- ( Fun F -> Fun ( F |` A ) )
Theorem	funresd 5394	A restriction of a function is a function. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- ( ph -> Fun F )   =>    |- ( ph -> Fun ( F |` A ) )
Theorem	funssres 5395	The restriction of a function to the domain of a subclass equals the subclass. (Contributed by NM, 15-Aug-1994.)
|- ( ( Fun F /\ G C_ F ) -> ( F |` dom G ) = G )
Theorem	fun2ssres 5396	Equality of restrictions of a function and a subclass. (Contributed by NM, 16-Aug-1994.)
|- ( ( Fun F /\ G C_ F /\ A C_ dom G ) -> ( F |` A ) = ( G |` A ) )
Theorem	funun 5397	The union of functions with disjoint domains is a function. Theorem 4.6 of [Monk1] p. 43. (Contributed by NM, 12-Aug-1994.)
|- ( ( ( Fun F /\ Fun G ) /\ ( dom F i^i dom G ) = (/) ) -> Fun ( F u. G ) )
Theorem	fununmo 5398*	If the union of classes is a function, there is at most one element in relation to an arbitrary element regarding one of these classes. (Contributed by AV, 18-Jul-2019.)
|- ( Fun ( F u. G ) -> E* y x F y )
Theorem	fununfun 5399	If the union of classes is a function, the classes itselves are functions. (Contributed by AV, 18-Jul-2019.)
|- ( Fun ( F u. G ) -> ( Fun F /\ Fun G ) )
Theorem	fundif 5400	A function with removed elements is still a function. (Contributed by AV, 7-Jun-2021.)
|- ( Fun F -> Fun ( F \ A ) )