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	coass 5301	Associative law for class composition. Theorem 27 of [Suppes] p. 64. Also Exercise 21 of [Enderton] p. 53. Interestingly, this law holds for any classes whatsoever, not just functions or even relations. (Contributed by NM, 27-Jan-1997.)
|- ( ( A o. B ) o. C ) = ( A o. ( B o. C ) )
Theorem	relcnvtr 5302	A relation is transitive iff its converse is transitive. (Contributed by FL, 19-Sep-2011.)
|- ( Rel R -> ( ( R o. R ) C_ R <-> ( `' R o. `' R ) C_ `' R ) )
Theorem	relssdmrn 5303	A relation is included in the cross product of its domain and range. Exercise 4.12(t) of [Mendelson] p. 235. (Contributed by NM, 3-Aug-1994.)
|- ( Rel A -> A C_ ( dom A X. ran A ) )
Theorem	cnvssrndm 5304	The converse is a subset of the cartesian product of range and domain. (Contributed by Mario Carneiro, 2-Jan-2017.)
|- `' A C_ ( ran A X. dom A )
Theorem	cossxp 5305	Composition as a subset of the cross product of factors. (Contributed by Mario Carneiro, 12-Jan-2017.)
|- ( A o. B ) C_ ( dom B X. ran A )
Theorem	cossxp2 5306	The composition of two relations is a relation, with bounds on its domain and codomain. (Contributed by BJ, 10-Jul-2022.)
|- ( ph -> R C_ ( A X. B ) )   &    |- ( ph -> S C_ ( B X. C ) )   =>    |- ( ph -> ( S o. R ) C_ ( A X. C ) )
Theorem	cocnvres 5307	Restricting a relation and a converse relation when they are composed together. (Contributed by BJ, 10-Jul-2022.)
|- ( S o. `' R ) = ( ( S |` dom R ) o. `' ( R |` dom S ) )
Theorem	cocnvss 5308	Upper bound for the composed of a relation and an inverse relation. (Contributed by BJ, 10-Jul-2022.)
|- ( S o. `' R ) C_ ( ran ( R |` dom S ) X. ran ( S |` dom R ) )
Theorem	relrelss 5309	Two ways to describe the structure of a two-place operation. (Contributed by NM, 17-Dec-2008.)
|- ( ( Rel A /\ Rel dom A ) <-> A C_ ( ( _V X. _V ) X. _V ) )
Theorem	unielrel 5310	The membership relation for a relation is inherited by class union. (Contributed by NM, 17-Sep-2006.)
|- ( ( Rel R /\ A e. R ) -> U. A e. U. R )
Theorem	relfld 5311	The double union of a relation is its field. (Contributed by NM, 17-Sep-2006.)
|- ( Rel R -> U. U. R = ( dom R u. ran R ) )
Theorem	relresfld 5312	Restriction of a relation to its field. (Contributed by FL, 15-Apr-2012.)
|- ( Rel R -> ( R |` U. U. R ) = R )
Theorem	relcoi2 5313	Composition with the identity relation restricted to a relation's field. (Contributed by FL, 2-May-2011.)
|- ( Rel R -> ( ( _I |` U. U. R ) o. R ) = R )
Theorem	relcoi1 5314	Composition with the identity relation restricted to a relation's field. (Contributed by FL, 8-May-2011.)
|- ( Rel R -> ( R o. ( _I |` U. U. R ) ) = R )
Theorem	unidmrn 5315	The double union of the converse of a class is its field. (Contributed by NM, 4-Jun-2008.)
|- U. U. `' A = ( dom A u. ran A )
Theorem	relcnvfld 5316	if R is a relation, its double union equals the double union of its converse. (Contributed by FL, 5-Jan-2009.)
|- ( Rel R -> U. U. R = U. U. `' R )
Theorem	dfdm2 5317	Alternate definition of domain df-dm 4779 that doesn't require dummy variables. (Contributed by NM, 2-Aug-2010.)
|- dom A = U. U. ( `' A o. A )
Theorem	unixpm 5318*	The double class union of an inhabited cross product is the union of its members. (Contributed by Jim Kingdon, 18-Dec-2018.)
|- ( E. x x e. ( A X. B ) -> U. U. ( A X. B ) = ( A u. B ) )
Theorem	unixp0im 5319	The union of an empty cross product is empty. (Contributed by Jim Kingdon, 18-Dec-2018.)
|- ( ( A X. B ) = (/) -> U. ( A X. B ) = (/) )
Theorem	cnvexg 5320	The converse of a set is a set. Corollary 6.8(1) of [TakeutiZaring] p. 26. (Contributed by NM, 17-Mar-1998.)
|- ( A e. V -> `' A e. _V )
Theorem	cnvex 5321	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 5322	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 5323	Restriction of a class to a singleton. (Contributed by Mario Carneiro, 28-Dec-2014.)
|- ( A |` { B } ) = ( { B } X. ( A " { B } ) )
Theorem	cnviinm 5324*	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 5325*	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 5326*	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 5327	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 5328	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 5329*	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 5330	Extend class notation with Russell's definition description binder (inverted iota).
class ( iota x ph )
Theorem	iotajust 5331*	Soundness justification theorem for df-iota 5332. (Contributed by Andrew Salmon, 29-Jun-2011.)
|- U. { y | { x | ph } = { y } } = U. { z | { x | ph } = { z } }
Definition	df-iota 5332*	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 5344); otherwise, it evaluates to the empty set (see iotanul 5348). 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 5357 (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 5333*	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 5334	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 5335*	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 5336*	Bound-variable hypothesis builder for the iota class. (Contributed by NM, 23-Aug-2011.)
|- F/ x ph   =>    |- F/_ x ( iota y ph )
Theorem	cbviota 5337	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 5338*	Change bound variables in a description binder. Version of cbviotav 5339 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 5339*	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 5340	Variable substitution in description binder. Compare sb8eu 2099. (Contributed by NM, 18-Mar-2013.)
|- F/ y ph   =>    |- ( iota x ph ) = ( iota y [ y / x ] ph )
Theorem	iotaeq 5341	Equality theorem for descriptions. (Contributed by Andrew Salmon, 30-Jun-2011.)
|- ( A. x x = y -> ( iota x ph ) = ( iota y ph ) )
Theorem	iotabi 5342	Equivalence theorem for descriptions. (Contributed by Andrew Salmon, 30-Jun-2011.)
|- ( A. x ( ph <-> ps ) -> ( iota x ph ) = ( iota x ps ) )
Theorem	uniabio 5343*	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 5344*	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 5345	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 5346	Equivalence between two different forms of iota. (Contributed by Mario Carneiro, 24-Dec-2016.)
|- ( E! x ph -> ( iota x ph ) = |^| { x | ph } )
Theorem	iota1 5347	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 5348	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 5349	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 5350*	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 5351	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 5352	Theorem *14.22 in [WhiteheadRussell] p. 190. (Contributed by Andrew Salmon, 12-Jul-2011.)
|- ( E! x ph -> [. ( iota x ph ) / x ]. ph )
Theorem	iota4an 5353	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 5354*	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 5355*	Formula-building deduction for iota. (Contributed by NM, 20-Aug-2011.)
|- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( iota x ps ) = ( iota x ch ) )
Theorem	iotabii 5356	Formula-building deduction for iota. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- ( ph <-> ps )   =>    |- ( iota x ph ) = ( iota x ps )
Theorem	iotacl 5357	Membership law for descriptions. This can useful for expanding an unbounded iota-based definition (see df-iota 5332). (Contributed by Andrew Salmon, 1-Aug-2011.)
|- ( E! x ph -> ( iota x ph ) e. { x | ph } )
Theorem	iota2df 5358	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 5359*	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 5360*	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 5361	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 5362*	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 5363	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 5364*	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 5365*	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 5366	Extend the definition of a wff to include the function predicate. (Read: A is a function.)
wff Fun A
Syntax	wfn 5367	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 5368	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 5369	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 5370	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 5371	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 5372	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 5373	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 5374	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 5404). This is not the same as defining a specific function's mapping, which is typically done using the format of cmpt 4187 with the maps-to notation (see df-mpt 4189). Contrast this predicate with the predicates to determine if some class is a function with a given domain (df-fn 5375), a function with a given domain and codomain (df-f 5376), a one-to-one function (df-f1 5377), an onto function (df-fo 5378), or a one-to-one onto function (df-f1o 5379). For alternate definitions, see dffun2 5382, dffun4 5383, dffun6 5386, dffun7 5399, dffun8 5400, and dffun9 5401. (Contributed by NM, 1-Aug-1994.)
|- ( Fun A <-> ( Rel A /\ ( A o. `' A ) C_ _I ) )
Definition	df-fn 5375	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 5376	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 5377	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 5378	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 5379	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 5380*	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 4189), 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 5381*	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 5382*	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 5383*	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 5384*	A way of proving a relation is a function, analogous to mo2r 2139. (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 5385*	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 5386*	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 5387*	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 5388*	Definition of function like dffun4 5383 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 5389	A function is a relation. (Contributed by NM, 1-Aug-1994.)
|- ( Fun A -> Rel A )
Theorem	0nelfun 5390	A function does not contain the empty set. (Contributed by BJ, 26-Nov-2021.)
|- ( Fun R -> (/) e/ R )
Theorem	funss 5391	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 5392	Equality theorem for function predicate. (Contributed by NM, 16-Aug-1994.)
|- ( A = B -> ( Fun A <-> Fun B ) )
Theorem	funeqi 5393	Equality inference for the function predicate. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
|- A = B   =>    |- ( Fun A <-> Fun B )
Theorem	funeqd 5394	Equality deduction for the function predicate. (Contributed by NM, 23-Feb-2013.)
|- ( ph -> A = B )   =>    |- ( ph -> ( Fun A <-> Fun B ) )
Theorem	nffun 5395	Bound-variable hypothesis builder for a function. (Contributed by NM, 30-Jan-2004.)
|- F/_ x F   =>    |- F/ x Fun F
Theorem	sbcfung 5396	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 5397*	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 5398*	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 5399*	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 5400 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 5400*	Alternate definition of a function. One possibility for the definition of a function in [Enderton] p. 42. Compare dffun7 5399. (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 ) )