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	fnresi 5201	Functionality and domain of restricted identity. (Contributed by set.mm contributors, 27-Aug-2004.)
|- ( _I |` A) Fn A
Theorem	fnima 5202	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 5203	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 5204	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 5205*	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 5206*	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 5207*	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 5208*	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 5209*	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 5210*	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 5211	Equality theorem for functions. (Contributed by set.mm contributors, 1-Aug-1994.)
|- (F = G -> (F:A-->B <-> G:A-->B))
Theorem	feq2 5212	Equality theorem for functions. (Contributed by set.mm contributors, 1-Aug-1994.)
|- (A = B -> (F:A-->C <-> F:B-->C))
Theorem	feq3 5213	Equality theorem for functions. (Contributed by set.mm contributors, 1-Aug-1994.)
|- (A = B -> (F:C-->A <-> F:C-->B))
Theorem	feq23 5214	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 5215	Equality deduction for functions. (Contributed by set.mm contributors, 19-Feb-2008.)
|- (ph -> F = G)   =>   |- (ph -> (F:A-->B <-> G:A-->B))
Theorem	feq2d 5216	Equality deduction for functions. (Contributed by Paul Chapman, 22-Jun-2011.)
|- (ph -> A = B)   =>   |- (ph -> (F:A-->C <-> F:B-->C))
Theorem	feq12d 5217	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 5218	Equality inference for functions. (Contributed by Paul Chapman, 22-Jun-2011.)
|- F = G   =>   |- (F:A-->B <-> G:A-->B)
Theorem	feq2i 5219	Equality inference for functions. (Contributed by set.mm contributors, 5-Sep-2011.)
|- A = B   =>   |- (F:A-->C <-> F:B-->C)
Theorem	feq23i 5220	Equality inference for functions. (Contributed by Paul Chapman, 22-Jun-2011.)
|- A = C   &   |- B = D   =>   |- (F:A-->B <-> F:C-->D)
Theorem	feq23d 5221	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 5222	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 5223	Eliminate a mapping hypothesis for the weak deduction theorem dedth 3704, 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 5224	A mapping is a function. (Contributed by set.mm contributors, 2-Aug-1994.)
|- (F:A-->B -> F Fn A)
Theorem	dffn2 5225	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 5226	A mapping is a function. (Contributed by set.mm contributors, 3-Aug-1994.)
|- (F:A-->B -> Fun F)
Theorem	fdm 5227	The domain of a mapping. (Contributed by set.mm contributors, 2-Aug-1994.)
|- (F:A-->B -> dom F = A)
Theorem	fdmi 5228	The domain of a mapping. (Contributed by set.mm contributors, 28-Jul-2008.)
|- F:A-->B   =>   |- dom F = A
Theorem	frn 5229	The range of a mapping. (Contributed by set.mm contributors, 3-Aug-1994.)
|- (F:A-->B -> ran F C_ B)
Theorem	dffn3 5230	A function maps to its range. (Contributed by set.mm contributors, 1-Sep-1999.)
|- (F Fn A <-> F:A-->ran F)
Theorem	fss 5231	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 5232	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 5233	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 5234	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 5235	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 5236	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 5237	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 5238	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 5239	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 5240	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 5241	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 5242	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 5243*	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 5244	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 5245	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 5246*	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 5247	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 5248	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 5249	The empty function. (Contributed by set.mm contributors, 14-Aug-1999.)
|- (/):(/)-->A
Theorem	f00 5250	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 5251	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 5252	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 5253	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 5254	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 5255	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 5256	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 5257	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 5258*	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 5259	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 5260	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 5261	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 5262	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 5263	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 5264	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 5265	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 5266	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 5267	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 5268	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 5269	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 5270	An onto mapping is a mapping. (Contributed by set.mm contributors, 3-Aug-1994.)
|- (F:A-onto->B -> F:A-->B)
Theorem	fofun 5271	An onto mapping is a function. (Contributed by set.mm contributors, 29-Mar-2008.)
|- (F:A-onto->B -> Fun F)
Theorem	fofn 5272	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 5273	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 5274	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 5275	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 5276	A function maps onto its range. (Contributed by set.mm contributors, 10-May-1998.)
|- (F Fn A <-> F:A-onto->ran F)
Theorem	funforn 5277	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 5278	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 5279	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 5280	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 5281	A nonzero constant function is onto. (Contributed by set.mm contributors, 12-Jan-2007.)
|- ((F:A-->{B} /\ F =/= (/)) -> F:A-onto->{B})
Theorem	f1oeq1 5282	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 5283	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 5284	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 5285	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 5286	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 5287	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 5288	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 5289	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 5290	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 5291	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 5292	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 5293	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 5294	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 5295	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 5296	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 5297	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 5298	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 5299	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 5300	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)