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	funeqi 5301	Equality inference for the function predicate. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
|- A = B   =>    |- ( Fun A <-> Fun B )
Theorem	funeqd 5302	Equality deduction for the function predicate. (Contributed by NM, 23-Feb-2013.)
|- ( ph -> A = B )   =>    |- ( ph -> ( Fun A <-> Fun B ) )
Theorem	nffun 5303	Bound-variable hypothesis builder for a function. (Contributed by NM, 30-Jan-2004.)
|- F/_ x F   =>    |- F/ x Fun F
Theorem	sbcfung 5304	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 5305*	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 5306*	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 5307*	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 5308 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 5308*	Alternate definition of a function. One possibility for the definition of a function in [Enderton] p. 42. Compare dffun7 5307. (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 5309*	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 5310	An equivalence for the function predicate. (Contributed by NM, 13-Aug-2004.)
|- ( Fun A <-> A Fn dom A )
Theorem	funfnd 5311	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 5312	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 5313	The universe is not a function. (Contributed by Raph Levien, 27-Jan-2004.)
|- -. Fun _V
Theorem	funopg 5314	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 5315*	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 5316*	A class of ordered pairs of values is a function. (Contributed by NM, 14-Nov-1995.)
|- Fun { <. x , y >. | y = A }
Theorem	funopab4 5317*	A class of ordered pairs of values in the form used by df-mpt 4115 is a function. (Contributed by NM, 17-Feb-2013.)
|- Fun { <. x , y >. | ( ph /\ y = A ) }
Theorem	funmpt 5318	A function in maps-to notation is a function. (Contributed by Mario Carneiro, 13-Jan-2013.)
|- Fun ( x e. A |-> B )
Theorem	funmpt2 5319	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 5320	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 5321	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	funssres 5322	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 5323	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 5324	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 5325*	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 5326	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 5327	A function with removed elements is still a function. (Contributed by AV, 7-Jun-2021.)
|- ( Fun F -> Fun ( F \ A ) )
Theorem	funcnvsn 5328	The converse singleton of an ordered pair is a function. This is equivalent to funsn 5331 via cnvsn 5174, but stating it this way allows us to skip the sethood assumptions on A and B. (Contributed by NM, 30-Apr-2015.)
|- Fun `' { <. A , B >. }
Theorem	funsng 5329	A singleton of an ordered pair is a function. Theorem 10.5 of [Quine] p. 65. (Contributed by NM, 28-Jun-2011.)
|- ( ( A e. V /\ B e. W ) -> Fun { <. A , B >. } )
Theorem	fnsng 5330	Functionality and domain of the singleton of an ordered pair. (Contributed by Mario Carneiro, 30-Apr-2015.)
|- ( ( A e. V /\ B e. W ) -> { <. A , B >. } Fn { A } )
Theorem	funsn 5331	A singleton of an ordered pair is a function. Theorem 10.5 of [Quine] p. 65. (Contributed by NM, 12-Aug-1994.)
|- A e. _V   &    |- B e. _V   =>    |- Fun { <. A , B >. }
Theorem	funinsn 5332	A function based on the singleton of an ordered pair. Unlike funsng 5329, this holds even if A or B is a proper class. (Contributed by Jim Kingdon, 17-Apr-2022.)
|- Fun ( { <. A , B >. } i^i ( V X. W ) )
Theorem	funprg 5333	A set of two pairs is a function if their first members are different. (Contributed by FL, 26-Jun-2011.)
|- ( ( ( A e. V /\ B e. W ) /\ ( C e. X /\ D e. Y ) /\ A =/= B ) -> Fun { <. A , C >. , <. B , D >. } )
Theorem	funtpg 5334	A set of three pairs is a function if their first members are different. (Contributed by Alexander van der Vekens, 5-Dec-2017.)
|- ( ( ( X e. U /\ Y e. V /\ Z e. W ) /\ ( A e. F /\ B e. G /\ C e. H ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> Fun { <. X , A >. , <. Y , B >. , <. Z , C >. } )
Theorem	funpr 5335	A function with a domain of two elements. (Contributed by Jeff Madsen, 20-Jun-2010.)
|- A e. _V   &    |- B e. _V   &    |- C e. _V   &    |- D e. _V   =>    |- ( A =/= B -> Fun { <. A , C >. , <. B , D >. } )
Theorem	funtp 5336	A function with a domain of three elements. (Contributed by NM, 14-Sep-2011.)
|- A e. _V   &    |- B e. _V   &    |- C e. _V   &    |- D e. _V   &    |- E e. _V   &    |- F e. _V   =>    |- ( ( A =/= B /\ A =/= C /\ B =/= C ) -> Fun { <. A , D >. , <. B , E >. , <. C , F >. } )
Theorem	fnsn 5337	Functionality and domain of the singleton of an ordered pair. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
|- A e. _V   &    |- B e. _V   =>    |- { <. A , B >. } Fn { A }
Theorem	fnprg 5338	Function with a domain of two different values. (Contributed by FL, 26-Jun-2011.) (Revised by Mario Carneiro, 26-Apr-2015.)
|- ( ( ( A e. V /\ B e. W ) /\ ( C e. X /\ D e. Y ) /\ A =/= B ) -> { <. A , C >. , <. B , D >. } Fn { A , B } )
Theorem	fntpg 5339	Function with a domain of three different values. (Contributed by Alexander van der Vekens, 5-Dec-2017.)
|- ( ( ( X e. U /\ Y e. V /\ Z e. W ) /\ ( A e. F /\ B e. G /\ C e. H ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> { <. X , A >. , <. Y , B >. , <. Z , C >. } Fn { X , Y , Z } )
Theorem	fntp 5340	A function with a domain of three elements. (Contributed by NM, 14-Sep-2011.) (Revised by Mario Carneiro, 26-Apr-2015.)
|- A e. _V   &    |- B e. _V   &    |- C e. _V   &    |- D e. _V   &    |- E e. _V   &    |- F e. _V   =>    |- ( ( A =/= B /\ A =/= C /\ B =/= C ) -> { <. A , D >. , <. B , E >. , <. C , F >. } Fn { A , B , C } )
Theorem	fun0 5341	The empty set is a function. Theorem 10.3 of [Quine] p. 65. (Contributed by NM, 7-Apr-1998.)
|- Fun (/)
Theorem	funcnvcnv 5342	The double converse of a function is a function. (Contributed by NM, 21-Sep-2004.)
|- ( Fun A -> Fun `' `' A )
Theorem	funcnv2 5343*	A simpler equivalence for single-rooted (see funcnv 5344). (Contributed by NM, 9-Aug-2004.)
|- ( Fun `' A <-> A. y E* x x A y )
Theorem	funcnv 5344*	The converse of a class is a function iff the class is single-rooted, which means that for any y in the range of A there is at most one x such that x A y. Definition of single-rooted in [Enderton] p. 43. See funcnv2 5343 for a simpler version. (Contributed by NM, 13-Aug-2004.)
|- ( Fun `' A <-> A. y e. ran A E* x x A y )
Theorem	funcnv3 5345*	A condition showing a class is single-rooted. (See funcnv 5344). (Contributed by NM, 26-May-2006.)
|- ( Fun `' A <-> A. y e. ran A E! x e. dom A x A y )
Theorem	funcnveq 5346*	Another way of expressing that a class is single-rooted. Counterpart to dffun2 5290. (Contributed by Jim Kingdon, 24-Dec-2018.)
|- ( Fun `' A <-> A. x A. y A. z ( ( x A y /\ z A y ) -> x = z ) )
Theorem	fun2cnv 5347*	The double converse of a class is a function iff the class is single-valued. Each side is equivalent to Definition 6.4(2) of [TakeutiZaring] p. 23, who use the notation "Un(A)" for single-valued. Note that A is not necessarily a function. (Contributed by NM, 13-Aug-2004.)
|- ( Fun `' `' A <-> A. x E* y x A y )
Theorem	svrelfun 5348	A single-valued relation is a function. (See fun2cnv 5347 for "single-valued.") Definition 6.4(4) of [TakeutiZaring] p. 24. (Contributed by NM, 17-Jan-2006.)
|- ( Fun A <-> ( Rel A /\ Fun `' `' A ) )
Theorem	fncnv 5349*	Single-rootedness (see funcnv 5344) of a class cut down by a cross product. (Contributed by NM, 5-Mar-2007.)
|- ( `' ( R i^i ( A X. B ) ) Fn B <-> A. y e. B E! x e. A x R y )
Theorem	fun11 5350*	Two ways of stating that A is one-to-one (but not necessarily a function). Each side is equivalent to Definition 6.4(3) of [TakeutiZaring] p. 24, who use the notation "Un2 (A)" for one-to-one (but not necessarily a function). (Contributed by NM, 17-Jan-2006.)
|- ( ( Fun `' `' A /\ Fun `' A ) <-> A. x A. y A. z A. w ( ( x A y /\ z A w ) -> ( x = z <-> y = w ) ) )
Theorem	fununi 5351*	The union of a chain (with respect to inclusion) of functions is a function. (Contributed by NM, 10-Aug-2004.)
|- ( A. f e. A ( Fun f /\ A. g e. A ( f C_ g \/ g C_ f ) ) -> Fun U. A )
Theorem	funcnvuni 5352*	The union of a chain (with respect to inclusion) of single-rooted sets is single-rooted. (See funcnv 5344 for "single-rooted" definition.) (Contributed by NM, 11-Aug-2004.)
|- ( A. f e. A ( Fun `' f /\ A. g e. A ( f C_ g \/ g C_ f ) ) -> Fun `' U. A )
Theorem	fun11uni 5353*	The union of a chain (with respect to inclusion) of one-to-one functions is a one-to-one function. (Contributed by NM, 11-Aug-2004.)
|- ( A. f e. A ( ( Fun f /\ Fun `' f ) /\ A. g e. A ( f C_ g \/ g C_ f ) ) -> ( Fun U. A /\ Fun `' U. A ) )
Theorem	funin 5354	The intersection with a function is a function. Exercise 14(a) of [Enderton] p. 53. (Contributed by NM, 19-Mar-2004.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)
|- ( Fun F -> Fun ( F i^i G ) )
Theorem	funres11 5355	The restriction of a one-to-one function is one-to-one. (Contributed by NM, 25-Mar-1998.)
|- ( Fun `' F -> Fun `' ( F |` A ) )
Theorem	funcnvres 5356	The converse of a restricted function. (Contributed by NM, 27-Mar-1998.)
|- ( Fun `' F -> `' ( F |` A ) = ( `' F |` ( F " A ) ) )
Theorem	cnvresid 5357	Converse of a restricted identity function. (Contributed by FL, 4-Mar-2007.)
|- `' ( _I |` A ) = ( _I |` A )
Theorem	funcnvres2 5358	The converse of a restriction of the converse of a function equals the function restricted to the image of its converse. (Contributed by NM, 4-May-2005.)
|- ( Fun F -> `' ( `' F |` A ) = ( F |` ( `' F " A ) ) )
Theorem	funimacnv 5359	The image of the preimage of a function. (Contributed by NM, 25-May-2004.)
|- ( Fun F -> ( F " ( `' F " A ) ) = ( A i^i ran F ) )
Theorem	funimass1 5360	A kind of contraposition law that infers a subclass of an image from a preimage subclass. (Contributed by NM, 25-May-2004.)
|- ( ( Fun F /\ A C_ ran F ) -> ( ( `' F " A ) C_ B -> A C_ ( F " B ) ) )
Theorem	funimass2 5361	A kind of contraposition law that infers an image subclass from a subclass of a preimage. (Contributed by NM, 25-May-2004.)
|- ( ( Fun F /\ A C_ ( `' F " B ) ) -> ( F " A ) C_ B )
Theorem	imadiflem 5362	One direction of imadif 5363. This direction does not require Fun `' F. (Contributed by Jim Kingdon, 25-Dec-2018.)
|- ( ( F " A ) \ ( F " B ) ) C_ ( F " ( A \ B ) )
Theorem	imadif 5363	The image of a difference is the difference of images. (Contributed by NM, 24-May-1998.)
|- ( Fun `' F -> ( F " ( A \ B ) ) = ( ( F " A ) \ ( F " B ) ) )
Theorem	imainlem 5364	One direction of imain 5365. This direction does not require Fun `' F. (Contributed by Jim Kingdon, 25-Dec-2018.)
|- ( F " ( A i^i B ) ) C_ ( ( F " A ) i^i ( F " B ) )
Theorem	imain 5365	The image of an intersection is the intersection of images. (Contributed by Paul Chapman, 11-Apr-2009.)
|- ( Fun `' F -> ( F " ( A i^i B ) ) = ( ( F " A ) i^i ( F " B ) ) )
Theorem	funimaexglem 5366	Lemma for funimaexg 5367. It constitutes the interesting part of funimaexg 5367, in which B C_ dom A. (Contributed by Jim Kingdon, 27-Dec-2018.)
|- ( ( Fun A /\ B e. C /\ B C_ dom A ) -> ( A " B ) e. _V )
Theorem	funimaexg 5367	Axiom of Replacement using abbreviations. Axiom 39(vi) of [Quine] p. 284. Compare Exercise 9 of [TakeutiZaring] p. 29. (Contributed by NM, 10-Sep-2006.)
|- ( ( Fun A /\ B e. C ) -> ( A " B ) e. _V )
Theorem	funimaex 5368	The image of a set under any function is also a set. Equivalent of Axiom of Replacement. Axiom 39(vi) of [Quine] p. 284. Compare Exercise 9 of [TakeutiZaring] p. 29. (Contributed by NM, 17-Nov-2002.)
|- B e. _V   =>    |- ( Fun A -> ( A " B ) e. _V )
Theorem	isarep1 5369*	Part of a study of the Axiom of Replacement used by the Isabelle prover. The object PrimReplace is apparently the image of the function encoded by ph ( x , y ) i.e. the class ( { <. x , y >. | ph } " A ). If so, we can prove Isabelle's "Axiom of Replacement" conclusion without using the Axiom of Replacement, for which I (N. Megill) currently have no explanation. (Contributed by NM, 26-Oct-2006.) (Proof shortened by Mario Carneiro, 4-Dec-2016.)
|- ( b e. ( { <. x , y >. | ph } " A ) <-> E. x e. A [ b / y ] ph )
Theorem	isarep2 5370*	Part of a study of the Axiom of Replacement used by the Isabelle prover. In Isabelle, the sethood of PrimReplace is apparently postulated implicitly by its type signature " [ i, [ i, i ] => o ] => i", which automatically asserts that it is a set without using any axioms. To prove that it is a set in Metamath, we need the hypotheses of Isabelle's "Axiom of Replacement" as well as the Axiom of Replacement in the form funimaex 5368. (Contributed by NM, 26-Oct-2006.)
|- A e. _V   &    |- A. x e. A A. y A. z ( ( ph /\ [ z / y ] ph ) -> y = z )   =>    |- E. w w = ( { <. x , y >. | ph } " A )
Theorem	fneq1 5371	Equality theorem for function predicate with domain. (Contributed by NM, 1-Aug-1994.)
|- ( F = G -> ( F Fn A <-> G Fn A ) )
Theorem	fneq2 5372	Equality theorem for function predicate with domain. (Contributed by NM, 1-Aug-1994.)
|- ( A = B -> ( F Fn A <-> F Fn B ) )
Theorem	fneq1d 5373	Equality deduction for function predicate with domain. (Contributed by Paul Chapman, 22-Jun-2011.)
|- ( ph -> F = G )   =>    |- ( ph -> ( F Fn A <-> G Fn A ) )
Theorem	fneq2d 5374	Equality deduction for function predicate with domain. (Contributed by Paul Chapman, 22-Jun-2011.)
|- ( ph -> A = B )   =>    |- ( ph -> ( F Fn A <-> F Fn B ) )
Theorem	fneq12d 5375	Equality deduction for function predicate with domain. (Contributed by NM, 26-Jun-2011.)
|- ( ph -> F = G )   &    |- ( ph -> A = B )   =>    |- ( ph -> ( F Fn A <-> G Fn B ) )
Theorem	fneq12 5376	Equality theorem for function predicate with domain. (Contributed by Thierry Arnoux, 31-Jan-2017.)
|- ( ( F = G /\ A = B ) -> ( F Fn A <-> G Fn B ) )
Theorem	fneq1i 5377	Equality inference for function predicate with domain. (Contributed by Paul Chapman, 22-Jun-2011.)
|- F = G   =>    |- ( F Fn A <-> G Fn A )
Theorem	fneq2i 5378	Equality inference for function predicate with domain. (Contributed by NM, 4-Sep-2011.)
|- A = B   =>    |- ( F Fn A <-> F Fn B )
Theorem	nffn 5379	Bound-variable hypothesis builder for a function with domain. (Contributed by NM, 30-Jan-2004.)
|- F/_ x F   &    |- F/_ x A   =>    |- F/ x F Fn A
Theorem	fnfun 5380	A function with domain is a function. (Contributed by NM, 1-Aug-1994.)
|- ( F Fn A -> Fun F )
Theorem	fnrel 5381	A function with domain is a relation. (Contributed by NM, 1-Aug-1994.)
|- ( F Fn A -> Rel F )
Theorem	fndm 5382	The domain of a function. (Contributed by NM, 2-Aug-1994.)
|- ( F Fn A -> dom F = A )
Theorem	fndmi 5383	The domain of a function. (Contributed by Wolf Lammen, 1-Jun-2024.)
|- F Fn A   =>    |- dom F = A
Theorem	fndmd 5384	The domain of a function. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- ( ph -> F Fn A )   =>    |- ( ph -> dom F = A )
Theorem	funfni 5385	Inference to convert a function and domain antecedent. (Contributed by NM, 22-Apr-2004.)
|- ( ( Fun F /\ B e. dom F ) -> ph )   =>    |- ( ( F Fn A /\ B e. A ) -> ph )
Theorem	fndmu 5386	A function has a unique domain. (Contributed by NM, 11-Aug-1994.)
|- ( ( F Fn A /\ F Fn B ) -> A = B )
Theorem	fnbr 5387	The first argument of binary relation on a function belongs to the function's domain. (Contributed by NM, 7-May-2004.)
|- ( ( F Fn A /\ B F C ) -> B e. A )
Theorem	fnop 5388	The first argument of an ordered pair in a function belongs to the function's domain. (Contributed by NM, 8-Aug-1994.)
|- ( ( F Fn A /\ <. B , C >. e. F ) -> B e. A )
Theorem	fneu 5389*	There is exactly one value of a function. (Contributed by NM, 22-Apr-2004.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)
|- ( ( F Fn A /\ B e. A ) -> E! y B F y )
Theorem	fneu2 5390*	There is exactly one value of a function. (Contributed by NM, 7-Nov-1995.)
|- ( ( F Fn A /\ B e. A ) -> E! y <. B , y >. e. F )
Theorem	fnun 5391	The union of two functions with disjoint domains. (Contributed by NM, 22-Sep-2004.)
|- ( ( ( F Fn A /\ G Fn B ) /\ ( A i^i B ) = (/) ) -> ( F u. G ) Fn ( A u. B ) )
Theorem	fnunsn 5392	Extension of a function with a new ordered pair. (Contributed by NM, 28-Sep-2013.) (Revised by Mario Carneiro, 30-Apr-2015.)
|- ( ph -> X e. _V )   &    |- ( ph -> Y e. _V )   &    |- ( ph -> F Fn D )   &    |- G = ( F u. { <. X , Y >. } )   &    |- E = ( D u. { X } )   &    |- ( ph -> -. X e. D )   =>    |- ( ph -> G Fn E )
Theorem	fnco 5393	Composition of two functions. (Contributed by NM, 22-May-2006.)
|- ( ( F Fn A /\ G Fn B /\ ran G C_ A ) -> ( F o. G ) Fn B )
Theorem	fnresdm 5394	A function does not change when restricted to its domain. (Contributed by NM, 5-Sep-2004.)
|- ( F Fn A -> ( F |` A ) = F )
Theorem	fnresdisj 5395	A function restricted to a class disjoint with its domain is empty. (Contributed by NM, 23-Sep-2004.)
|- ( F Fn A -> ( ( A i^i B ) = (/) <-> ( F |` B ) = (/) ) )
Theorem	2elresin 5396	Membership in two functions restricted by each other's domain. (Contributed by NM, 8-Aug-1994.)
|- ( ( F Fn A /\ G Fn B ) -> ( ( <. x , y >. e. F /\ <. x , z >. e. G ) <-> ( <. x , y >. e. ( F |` ( A i^i B ) ) /\ <. x , z >. e. ( G |` ( A i^i B ) ) ) ) )
Theorem	fnssresb 5397	Restriction of a function with a subclass of its domain. (Contributed by NM, 10-Oct-2007.)
|- ( F Fn A -> ( ( F |` B ) Fn B <-> B C_ A ) )
Theorem	fnssres 5398	Restriction of a function with a subclass of its domain. (Contributed by NM, 2-Aug-1994.)
|- ( ( F Fn A /\ B C_ A ) -> ( F |` B ) Fn B )
Theorem	fnssresd 5399	Restriction of a function to a subclass of its domain. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
|- ( ph -> F Fn A )   &    |- ( ph -> B C_ A )   =>    |- ( ph -> ( F |` B ) Fn B )
Theorem	fnresin1 5400	Restriction of a function's domain with an intersection. (Contributed by NM, 9-Aug-1994.)
|- ( F Fn A -> ( F |` ( A i^i B ) ) Fn ( A i^i B ) )