P. 53 of Theorem List - New Foundations Explorer

Theorem List for New Foundations Explorer - 5201-5300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	fnima 5201	The image of a function's domain is its range. (The proof was shortened by Andrew Salmon, 17-Sep-2011.) (Contributed by set.mm contributors, 4-Nov-2004.) (Revised by set.mm contributors, 18-Sep-2011.)
|- (F Fn A -> (F"A) = ran F)
Theorem	fn0 5202	A function with empty domain is empty. (The proof was shortened by Andrew Salmon, 17-Sep-2011.) (Contributed by set.mm contributors, 15-Apr-1998.) (Revised by set.mm contributors, 18-Sep-2011.)
|- (F Fn (/) <-> F = (/))
Theorem	fnimadisj 5203	A class that is disjoint with the domain of a function has an empty image under the function. (Contributed by FL, 24-Jan-2007.)
|- ((F Fn A /\ (A i^i C) = (/)) -> (F"C) = (/))
Theorem	iunfopab 5204*	Two ways to express a function as a class of ordered pairs. (The proof was shortened by Andrew Salmon, 17-Sep-2011.) (Unnecessary distinct variable restrictions were removed by David Abernethy, 19-Sep-2011.) (Contributed by set.mm contributors, 19-Dec-2008.)
|- B e. _V   =>   |- U_x e. A {<.x, B>.} = {<.x, y>. | (x e. A /\ y = B)}
Theorem	fnopabg 5205*	Functionality and domain of an ordered-pair class abstraction. (Contributed by NM, 30-Jan-2004.) (Proof shortened by Mario Carneiro, 4-Dec-2016.)
|- F = {<.x, y>. | (x e. A /\ ph)}   =>   |- (A.x e. A E!yph <-> F Fn A)
Theorem	fnopab2g 5206*	Functionality and domain of an ordered-pair class abstraction. (Contributed by set.mm contributors, 23-Mar-2006.)
|- F = {<.x, y>. | (x e. A /\ y = B)}   =>   |- (A.x e. A B e. _V <-> F Fn A)
Theorem	fnopab 5207*	Functionality and domain of an ordered-pair class abstraction. (Contributed by set.mm contributors, 5-Mar-1996.)
|- (x e. A -> E!yph)   &   |- F = {<.x, y>. | (x e. A /\ ph)}   =>   |- F Fn A
Theorem	fnopab2 5208*	Functionality and domain of an ordered-pair class abstraction. (Contributed by set.mm contributors, 29-Jan-2004.)
|- B e. _V   &   |- F = {<.x, y>. | (x e. A /\ y = B)}   =>   |- F Fn A
Theorem	dmopab2 5209*	Domain of an ordered-pair class abstraction that specifies a function. (Contributed by set.mm contributors, 6-Sep-2005.)
|- B e. _V   &   |- F = {<.x, y>. | (x e. A /\ y = B)}   =>   |- dom F = A
Theorem	feq1 5210	Equality theorem for functions. (Contributed by set.mm contributors, 1-Aug-1994.)
|- (F = G -> (F:A-->B <-> G:A-->B))
Theorem	feq2 5211	Equality theorem for functions. (Contributed by set.mm contributors, 1-Aug-1994.)
|- (A = B -> (F:A-->C <-> F:B-->C))
Theorem	feq3 5212	Equality theorem for functions. (Contributed by set.mm contributors, 1-Aug-1994.)
|- (A = B -> (F:C-->A <-> F:C-->B))
Theorem	feq23 5213	Equality theorem for functions. (Contributed by FL, 14-Jul-2007.) (The proof was shortened by Andrew Salmon, 17-Sep-2011.)
|- ((A = C /\ B = D) -> (F:A-->B <-> F:C-->D))
Theorem	feq1d 5214	Equality deduction for functions. (Contributed by set.mm contributors, 19-Feb-2008.)
|- (ph -> F = G)   =>   |- (ph -> (F:A-->B <-> G:A-->B))
Theorem	feq2d 5215	Equality deduction for functions. (Contributed by Paul Chapman, 22-Jun-2011.)
|- (ph -> A = B)   =>   |- (ph -> (F:A-->C <-> F:B-->C))
Theorem	feq12d 5216	Equality deduction for functions. (Contributed by Paul Chapman, 22-Jun-2011.)
|- (ph -> F = G)   &   |- (ph -> A = B)   =>   |- (ph -> (F:A-->C <-> G:B-->C))
Theorem	feq1i 5217	Equality inference for functions. (Contributed by Paul Chapman, 22-Jun-2011.)
|- F = G   =>   |- (F:A-->B <-> G:A-->B)
Theorem	feq2i 5218	Equality inference for functions. (Contributed by set.mm contributors, 5-Sep-2011.)
|- A = B   =>   |- (F:A-->C <-> F:B-->C)
Theorem	feq23i 5219	Equality inference for functions. (Contributed by Paul Chapman, 22-Jun-2011.)
|- A = C   &   |- B = D   =>   |- (F:A-->B <-> F:C-->D)
Theorem	feq23d 5220	Equality deduction for functions. (Contributed by set.mm contributors, 8-Jun-2013.)
|- (ph -> A = C)   &   |- (ph -> B = D)   =>   |- (ph -> (F:A-->B <-> F:C-->D))
Theorem	nff 5221	Bound-variable hypothesis builder for a mapping. (Contributed by NM, 29-Jan-2004.) (Revised by Mario Carneiro, 15-Oct-2016.)
|- F/_xF   &   |- F/_xA   &   |- F/_xB   =>   |- F/x F:A-->B
Theorem	elimf 5222	Eliminate a mapping hypothesis for the weak deduction theorem dedth 3703, when a special case G:A-->B is provable, in order to convert F:A-->B from a hypothesis to an antecedent. (Contributed by set.mm contributors, 24-Aug-2006.)
|- G:A-->B   =>   |- if(F:A-->B, F, G):A-->B
Theorem	ffn 5223	A mapping is a function. (Contributed by set.mm contributors, 2-Aug-1994.)
|- (F:A-->B -> F Fn A)
Theorem	dffn2 5224	Any function is a mapping into _V. (The proof was shortened by Andrew Salmon, 17-Sep-2011.) (Contributed by set.mm contributors, 31-Oct-1995.) (Revised by set.mm contributors, 18-Sep-2011.)
|- (F Fn A <-> F:A-->_V)
Theorem	ffun 5225	A mapping is a function. (Contributed by set.mm contributors, 3-Aug-1994.)
|- (F:A-->B -> Fun F)
Theorem	fdm 5226	The domain of a mapping. (Contributed by set.mm contributors, 2-Aug-1994.)
|- (F:A-->B -> dom F = A)
Theorem	fdmi 5227	The domain of a mapping. (Contributed by set.mm contributors, 28-Jul-2008.)
|- F:A-->B   =>   |- dom F = A
Theorem	frn 5228	The range of a mapping. (Contributed by set.mm contributors, 3-Aug-1994.)
|- (F:A-->B -> ran F C_ B)
Theorem	dffn3 5229	A function maps to its range. (Contributed by set.mm contributors, 1-Sep-1999.)
|- (F Fn A <-> F:A-->ran F)
Theorem	fss 5230	Expanding the codomain of a mapping. (The proof was shortened by Andrew Salmon, 17-Sep-2011.) (Contributed by set.mm contributors, 10-May-1998.) (Revised by set.mm contributors, 18-Sep-2011.)
|- ((F:A-->B /\ B C_ C) -> F:A-->C)
Theorem	fco 5231	Composition of two mappings. (The proof was shortened by Andrew Salmon, 17-Sep-2011.) (Contributed by set.mm contributors, 29-Aug-1999.) (Revised by set.mm contributors, 18-Sep-2011.)
|- ((F:B-->C /\ G:A-->B) -> (F o. G):A-->C)
Theorem	fssxp 5232	A mapping is a class of ordered pairs. (The proof was shortened by Andrew Salmon, 17-Sep-2011.) (Contributed by set.mm contributors, 3-Aug-1994.) (Revised by set.mm contributors, 18-Sep-2011.)
|- (F:A-->B -> F C_ (A X. B))
Theorem	funssxp 5233	Two ways of specifying a partial function from A to B. (Contributed by set.mm contributors, 13-Nov-2007.)
|- ((Fun F /\ F C_ (A X. B)) <-> (F:dom F-->B /\ dom F C_ A))
Theorem	ffdm 5234	A mapping is a partial function. (Contributed by set.mm contributors, 25-Nov-2007.)
|- (F:A-->B -> (F:dom F-->B /\ dom F C_ A))
Theorem	opelf 5235	The members of an ordered pair element of a mapping belong to the mapping's domain and codomain. (Contributed by set.mm contributors, 9-Jan-2015.)
|- ((F:A-->B /\ <.C, D>. e. F) -> (C e. A /\ D e. B))
Theorem	fun 5236	The union of two functions with disjoint domains. (Contributed by set.mm contributors, 22-Sep-2004.)
|- (((F:A-->C /\ G:B-->D) /\ (A i^i B) = (/)) -> (F u. G):(A u. B)-->(C u. D))
Theorem	fnfco 5237	Composition of two functions. (Contributed by set.mm contributors, 22-May-2006.)
|- ((F Fn A /\ G:B-->A) -> (F o. G) Fn B)
Theorem	fssres 5238	Restriction of a function with a subclass of its domain. (Contributed by set.mm contributors, 23-Sep-2004.)
|- ((F:A-->B /\ C C_ A) -> (F |` C):C-->B)
Theorem	fssres2 5239	Restriction of a restricted function with a subclass of its domain. (Contributed by set.mm contributors, 21-Jul-2005.)
|- (((F |` A):A-->B /\ C C_ A) -> (F |` C):C-->B)
Theorem	fcoi1 5240	Composition of a mapping and restricted identity. (The proof was shortened by Andrew Salmon, 17-Sep-2011.) (Contributed by set.mm contributors, 13-Dec-2003.) (Revised by set.mm contributors, 18-Sep-2011.)
|- (F:A-->B -> (F o. ( _I |` A)) = F)
Theorem	fcoi2 5241	Composition of restricted identity and a mapping. (The proof was shortened by Andrew Salmon, 17-Sep-2011.) (Contributed by set.mm contributors, 13-Dec-2003.) (Revised by set.mm contributors, 18-Sep-2011.)
|- (F:A-->B -> (( _I |` B) o. F) = F)
Theorem	feu 5242*	There is exactly one value of a function in its codomain. (Contributed by set.mm contributors, 10-Dec-2003.)
|- ((F:A-->B /\ C e. A) -> E!y e. B <.C, y>. e. F)
Theorem	fcnvres 5243	The converse of a restriction of a function. (Contributed by set.mm contributors, 26-Mar-1998.)
|- (F:A-->B -> `'(F |` A) = (`'F |` B))
Theorem	fimacnvdisj 5244	The preimage of a class disjoint with a mapping's codomain is empty. (Contributed by FL, 24-Jan-2007.)
|- ((F:A-->B /\ (B i^i C) = (/)) -> (`'F"C) = (/))
Theorem	fint 5245*	Function into an intersection. (The proof was shortened by Andrew Salmon, 17-Sep-2011.) (Contributed by set.mm contributors, 14-Oct-1999.) (Revised by set.mm contributors, 18-Sep-2011.)
|- B =/= (/)   =>   |- (F:A-->|^|B <-> A.x e. B F:A-->x)
Theorem	fin 5246	Mapping into an intersection. (The proof was shortened by Andrew Salmon, 17-Sep-2011.) (Contributed by set.mm contributors, 14-Sep-1999.) (Revised by set.mm contributors, 18-Sep-2011.)
|- (F:A-->(B i^i C) <-> (F:A-->B /\ F:A-->C))
Theorem	dmfex 5247	If a mapping is a set, its domain is a set. (The proof was shortened by Andrew Salmon, 17-Sep-2011.) (Contributed by set.mm contributors, 27-Aug-2006.) (Revised by set.mm contributors, 18-Sep-2011.)
|- ((F e. C /\ F:A-->B) -> A e. _V)
Theorem	f0 5248	The empty function. (Contributed by set.mm contributors, 14-Aug-1999.)
|- (/):(/)-->A
Theorem	f00 5249	A class is a function with empty codomain iff it and its domain are empty. (Contributed by set.mm contributors, 10-Dec-2003.)
|- (F:A-->(/) <-> (F = (/) /\ A = (/)))
Theorem	fconst 5250	A cross product with a singleton is a constant function. (The proof was shortened by Andrew Salmon, 17-Sep-2011.) (Contributed by set.mm contributors, 14-Aug-1999.) (Revised by set.mm contributors, 18-Sep-2011.)
|- B e. _V   =>   |- (A X. {B}):A-->{B}
Theorem	fconstg 5251	A cross product with a singleton is a constant function. (Contributed by set.mm contributors, 19-Oct-2004.)
|- (B e. V -> (A X. {B}):A-->{B})
Theorem	fnconstg 5252	A cross product with a singleton is a constant function. (Contributed by set.mm contributors, 24-Jul-2014.)
|- (B e. V -> (A X. {B}) Fn A)
Theorem	f1eq1 5253	Equality theorem for one-to-one functions. (Contributed by set.mm contributors, 10-Feb-1997.)
|- (F = G -> (F:A-1-1->B <-> G:A-1-1->B))
Theorem	f1eq2 5254	Equality theorem for one-to-one functions. (Contributed by set.mm contributors, 10-Feb-1997.)
|- (A = B -> (F:A-1-1->C <-> F:B-1-1->C))
Theorem	f1eq3 5255	Equality theorem for one-to-one functions. (Contributed by set.mm contributors, 10-Feb-1997.)
|- (A = B -> (F:C-1-1->A <-> F:C-1-1->B))
Theorem	nff1 5256	Bound-variable hypothesis builder for a one-to-one function. (Contributed by NM, 16-May-2004.)
|- F/_xF   &   |- F/_xA   &   |- F/_xB   =>   |- F/x F:A-1-1->B
Theorem	dff12 5257*	Alternate definition of a one-to-one function. (Contributed by set.mm contributors, 31-Dec-1996.) (Revised by set.mm contributors, 22-Sep-2004.)
|- (F:A-1-1->B <-> (F:A-->B /\ A.yE*x xFy))
Theorem	f1f 5258	A one-to-one mapping is a mapping. (Contributed by set.mm contributors, 31-Dec-1996.)
|- (F:A-1-1->B -> F:A-->B)
Theorem	f1fn 5259	A one-to-one mapping is a function on its domain. (Contributed by set.mm contributors, 8-Mar-2014.)
|- (F:A-1-1->B -> F Fn A)
Theorem	f1fun 5260	A one-to-one mapping is a function. (Contributed by set.mm contributors, 8-Mar-2014.)
|- (F:A-1-1->B -> Fun F)
Theorem	f1dm 5261	The domain of a one-to-one mapping. (Contributed by set.mm contributors, 8-Mar-2014.)
|- (F:A-1-1->B -> dom F = A)
Theorem	f1ss 5262	A function that is one-to-one is also one-to-one on some superset of its range. (Contributed by Mario Carneiro, 12-Jan-2013.)
|- ((F:A-1-1->B /\ B C_ C) -> F:A-1-1->C)
Theorem	f1funfun 5263	Two ways to express that a set A is one-to-one. Each side is equivalent to Definition 6.4(3) of [TakeutiZaring] p. 24, who use the notation "Un2 (A)" for one-to-one. We do not introduce a separate notation since we rarely use it. (Contributed by set.mm contributors, 13-Aug-2004.) (Revised by Scott Fenton, 18-Apr-2021.)
|- (A:dom A-1-1->_V <-> (Fun `'A /\ Fun A))
Theorem	f1co 5264	Composition of one-to-one functions. Exercise 30 of [TakeutiZaring] p. 25. (Contributed by set.mm contributors, 28-May-1998.)
|- ((F:B-1-1->C /\ G:A-1-1->B) -> (F o. G):A-1-1->C)
Theorem	foeq1 5265	Equality theorem for onto functions. (Contributed by set.mm contributors, 1-Aug-1994.)
|- (F = G -> (F:A-onto->B <-> G:A-onto->B))
Theorem	foeq2 5266	Equality theorem for onto functions. (Contributed by set.mm contributors, 1-Aug-1994.)
|- (A = B -> (F:A-onto->C <-> F:B-onto->C))
Theorem	foeq3 5267	Equality theorem for onto functions. (Contributed by set.mm contributors, 1-Aug-1994.)
|- (A = B -> (F:C-onto->A <-> F:C-onto->B))
Theorem	nffo 5268	Bound-variable hypothesis builder for an onto function. (Contributed by NM, 16-May-2004.)
|- F/_xF   &   |- F/_xA   &   |- F/_xB   =>   |- F/x F:A-onto->B
Theorem	fof 5269	An onto mapping is a mapping. (Contributed by set.mm contributors, 3-Aug-1994.)
|- (F:A-onto->B -> F:A-->B)
Theorem	fofun 5270	An onto mapping is a function. (Contributed by set.mm contributors, 29-Mar-2008.)
|- (F:A-onto->B -> Fun F)
Theorem	fofn 5271	An onto mapping is a function on its domain. (Contributed by set.mm contributors, 16-Dec-2008.)
|- (F:A-onto->B -> F Fn A)
Theorem	forn 5272	The codomain of an onto function is its range. (Contributed by set.mm contributors, 3-Aug-1994.)
|- (F:A-onto->B -> ran F = B)
Theorem	dffo2 5273	Alternate definition of an onto function. (Contributed by set.mm contributors, 22-Mar-2006.)
|- (F:A-onto->B <-> (F:A-->B /\ ran F = B))
Theorem	foima 5274	The image of the domain of an onto function. (Contributed by set.mm contributors, 29-Nov-2002.)
|- (F:A-onto->B -> (F"A) = B)
Theorem	dffn4 5275	A function maps onto its range. (Contributed by set.mm contributors, 10-May-1998.)
|- (F Fn A <-> F:A-onto->ran F)
Theorem	funforn 5276	A function maps its domain onto its range. (Contributed by set.mm contributors, 23-Jul-2004.)
|- (Fun A <-> A:dom A-onto->ran A)
Theorem	fodmrnu 5277	An onto function has unique domain and range. (Contributed by set.mm contributors, 5-Nov-2006.)
|- ((F:A-onto->B /\ F:C-onto->D) -> (A = C /\ B = D))
Theorem	fores 5278	Restriction of a function. (Contributed by set.mm contributors, 4-Mar-1997.)
|- ((Fun F /\ A C_ dom F) -> (F |` A):A-onto->(F"A))
Theorem	foco 5279	Composition of onto functions. (Contributed by set.mm contributors, 22-Mar-2006.)
|- ((F:B-onto->C /\ G:A-onto->B) -> (F o. G):A-onto->C)
Theorem	foconst 5280	A nonzero constant function is onto. (Contributed by set.mm contributors, 12-Jan-2007.)
|- ((F:A-->{B} /\ F =/= (/)) -> F:A-onto->{B})
Theorem	f1oeq1 5281	Equality theorem for one-to-one onto functions. (Contributed by set.mm contributors, 10-Feb-1997.)
|- (F = G -> (F:A-1-1-onto->B <-> G:A-1-1-onto->B))
Theorem	f1oeq2 5282	Equality theorem for one-to-one onto functions. (Contributed by set.mm contributors, 10-Feb-1997.)
|- (A = B -> (F:A-1-1-onto->C <-> F:B-1-1-onto->C))
Theorem	f1oeq3 5283	Equality theorem for one-to-one onto functions. (Contributed by set.mm contributors, 10-Feb-1997.)
|- (A = B -> (F:C-1-1-onto->A <-> F:C-1-1-onto->B))
Theorem	f1oeq23 5284	Equality theorem for one-to-one onto functions. (Contributed by FL, 14-Jul-2012.)
|- ((A = B /\ C = D) -> (F:A-1-1-onto->C <-> F:B-1-1-onto->D))
Theorem	nff1o 5285	Bound-variable hypothesis builder for a one-to-one onto function. (Contributed by NM, 16-May-2004.)
|- F/_xF   &   |- F/_xA   &   |- F/_xB   =>   |- F/x F:A-1-1-onto->B
Theorem	f1of1 5286	A one-to-one onto mapping is a one-to-one mapping. (Contributed by set.mm contributors, 12-Dec-2003.)
|- (F:A-1-1-onto->B -> F:A-1-1->B)
Theorem	f1of 5287	A one-to-one onto mapping is a mapping. (Contributed by set.mm contributors, 12-Dec-2003.)
|- (F:A-1-1-onto->B -> F:A-->B)
Theorem	f1ofn 5288	A one-to-one onto mapping is function on its domain. (Contributed by set.mm contributors, 12-Dec-2003.)
|- (F:A-1-1-onto->B -> F Fn A)
Theorem	f1ofun 5289	A one-to-one onto mapping is a function. (Contributed by set.mm contributors, 12-Dec-2003.)
|- (F:A-1-1-onto->B -> Fun F)
Theorem	f1odm 5290	The domain of a one-to-one onto mapping. (Contributed by set.mm contributors, 8-Mar-2014.)
|- (F:A-1-1-onto->B -> dom F = A)
Theorem	dff1o2 5291	Alternate definition of one-to-one onto function. (The proof was shortened by Andrew Salmon, 22-Oct-2011.) (Contributed by set.mm contributors, 10-Feb-1997.) (Revised by set.mm contributors, 22-Oct-2011.)
|- (F:A-1-1-onto->B <-> (F Fn A /\ Fun `'F /\ ran F = B))
Theorem	dff1o3 5292	Alternate definition of one-to-one onto function. (The proof was shortened by Andrew Salmon, 22-Oct-2011.) (Contributed by set.mm contributors, 25-Mar-1998.) (Revised by set.mm contributors, 22-Oct-2011.)
|- (F:A-1-1-onto->B <-> (F:A-onto->B /\ Fun `'F))
Theorem	f1ofo 5293	A one-to-one onto function is an onto function. (Contributed by set.mm contributors, 28-Apr-2004.)
|- (F:A-1-1-onto->B -> F:A-onto->B)
Theorem	dff1o4 5294	Alternate definition of one-to-one onto function. (The proof was shortened by Andrew Salmon, 22-Oct-2011.) (Contributed by set.mm contributors, 25-Mar-1998.) (Revised by set.mm contributors, 22-Oct-2011.)
|- (F:A-1-1-onto->B <-> (F Fn A /\ `'F Fn B))
Theorem	dff1o5 5295	Alternate definition of one-to-one onto function. (The proof was shortened by Andrew Salmon, 22-Oct-2011.) (Contributed by set.mm contributors, 10-Dec-2003.) (Revised by set.mm contributors, 22-Oct-2011.)
|- (F:A-1-1-onto->B <-> (F:A-1-1->B /\ ran F = B))
Theorem	f1orn 5296	A one-to-one function maps onto its range. (Contributed by set.mm contributors, 13-Aug-2004.)
|- (F:A-1-1-onto->ran F <-> (F Fn A /\ Fun `'F))
Theorem	f1f1orn 5297	A one-to-one function maps one-to-one onto its range. (Contributed by set.mm contributors, 4-Sep-2004.)
|- (F:A-1-1->B -> F:A-1-1-onto->ran F)
Theorem	f1ocnvb 5298	A class is a one-to-one onto function iff its converse is a one-to-one onto function with domain and range interchanged. (Contributed by set.mm contributors, 8-Dec-2003.) (Modified by Scott Fenton, 17-Apr-2021.)
|- (F:A-1-1-onto->B <-> `'F:B-1-1-onto->A)
Theorem	f1ocnv 5299	The converse of a one-to-one onto function is also one-to-one onto. (The proof was shortened by Andrew Salmon, 22-Oct-2011.) (Contributed by set.mm contributors, 11-Feb-1997.) (Revised by set.mm contributors, 22-Oct-2011.)
|- (F:A-1-1-onto->B -> `'F:B-1-1-onto->A)
Theorem	f1ores 5300	The restriction of a one-to-one function maps one-to-one onto the image. (Contributed by set.mm contributors, 25-Mar-1998.)
|- ((F:A-1-1->B /\ C C_ A) -> (F |` C):C-1-1-onto->(F"C))