P. 52 of Theorem List - New Foundations Explorer

Theorem List for New Foundations Explorer - 5101-5200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	cnvexg 5101	The converse of a set is a set. Corollary 6.8(1) of [TakeutiZaring] p. 26. (Contributed by set.mm contributors, 17-Mar-1998.)
|- (A e. V -> `'A e. _V)
Theorem	cnvex 5102	The converse of a set is a set. Corollary 6.8(1) of [TakeutiZaring] p. 26. (Contributed by set.mm contributors, 19-Dec-2003.)
|- A e. _V   =>   |- `'A e. _V
Theorem	cnvexb 5103	A class is a set iff its converse is a set. (Contributed by FL, 3-Mar-2007.) (Revised by Scott Fenton, 18-Apr-2021.)
|- (R e. _V <-> `'R e. _V)
Theorem	rnexg 5104	The range of a set is a set. Corollary 6.8(3) of [TakeutiZaring] p. 26. Similar to Lemma 3D of [Enderton] p. 41. (Contributed by set.mm contributors, 8-Jan-2015.)
|- (A e. V -> ran A e. _V)
Theorem	dmexg 5105	The domain of a set is a set. Corollary 6.8(2) of [TakeutiZaring] p. 26. (Contributed by set.mm contributors, 8-Jan-2015.)
|- (A e. V -> dom A e. _V)
Theorem	dmex 5106	The domain of a set is a set. Corollary 6.8(2) of [TakeutiZaring] p. 26. (Contributed by set.mm contributors, 7-Jul-2008.)
|- A e. _V   =>   |- dom A e. _V
Theorem	rnex 5107	The range of a set is a set. Corollary 6.8(3) of [TakeutiZaring] p. 26. Similar to Lemma 3D of [Enderton] p. 41. (Contributed by set.mm contributors, 7-Jul-2008.)
|- A e. _V   =>   |- ran A e. _V
Theorem	elxp4 5108	Membership in a cross product. This version requires no quantifiers or dummy variables. (Contributed by set.mm contributors, 17-Feb-2004.)
|- (A e. (B X. C) <-> (A = <.U.dom {A}, U.ran {A}>. /\ (U.dom {A} e. B /\ U.ran {A} e. C)))
Theorem	xpexr 5109	If a cross product is a set, one of its components must be a set. (Contributed by set.mm contributors, 27-Aug-2006.)
|- ((A X. B) e. C -> (A e. _V \/ B e. _V))
Theorem	xpexr2 5110	If a nonempty cross product is a set, so are both of its components. (Contributed by set.mm contributors, 27-Aug-2006.) (Revised by set.mm contributors, 5-May-2007.)
|- (((A X. B) e. C /\ (A X. B) =/= (/)) -> (A e. _V /\ B e. _V))
Theorem	df2nd2 5111	Alternate definition of the 2nd function. (Contributed by SF, 8-Jan-2015.)
|- 2nd = (1st o. Swap )
Theorem	2ndex 5112	The 2nd function is a set. (Contributed by SF, 8-Jan-2015.)
|- 2nd e. _V
Theorem	dfxp2 5113	Define cross product via the set construction functions. (Contributed by SF, 8-Jan-2015.)
|- (A X. B) = ((`'1st"A) i^i (`'2nd"B))
Theorem	xpexg 5114	The cross product of two sets is a set. Proposition 6.2 of [TakeutiZaring] p. 23. (Contributed by set.mm contributors, 14-Aug-1994.)
|- ((A e. V /\ B e. W) -> (A X. B) e. _V)
Theorem	xpex 5115	The cross product of two sets is a set. Proposition 6.2 of [TakeutiZaring] p. 23. (Contributed by set.mm contributors, 14-Aug-1994.)
|- A e. _V   &   |- B e. _V   =>   |- (A X. B) e. _V
Theorem	resexg 5116	The restriction of a set to a set is a set. (Contributed by set.mm contributors, 8-Jan-2015.)
|- ((A e. V /\ B e. W) -> (A |` B) e. _V)
Theorem	resex 5117	The restriction of a set to a set is a set. (Contributed by set.mm contributors, 8-Jan-2015.)
|- A e. _V   &   |- B e. _V   =>   |- (A |` B) e. _V
Theorem	cnviin 5118*	The converse of an intersection is the intersection of the converse. (Contributed by FL, 15-Oct-2012.) (Revised by Scott Fenton, 18-Apr-2021.)
|- `'|^|_x e. A B = |^|_x e. A `'B
Theorem	dffun2 5119*	Alternate definition of a function. (Contributed by set.mm contributors, 29-Dec-1996.) (Revised by set.mm contributors, 23-Apr-2004.) (Revised by Scott Fenton, 16-Apr-2021.)
|- (Fun A <-> A.xA.yA.z((xAy /\ xAz) -> y = z))
Theorem	dffun3 5120*	Alternate definition of function. (Contributed by NM, 29-Dec-1996.) (Revised by Scott Fenton, 16-Apr-2021.)
|- (Fun A <-> A.xE.zA.y(xAy -> y = z))
Theorem	dffun4 5121*	Alternate definition of a function. Definition 6.4(4) of [TakeutiZaring] p. 24. (Contributed by set.mm contributors, 29-Dec-1996.) (Revised by Scott Fenton, 16-Apr-2021.)
|- (Fun A <-> A.xA.yA.z((<.x, y>. e. A /\ <.x, z>. e. A) -> y = z))
Theorem	dffun5 5122*	Alternate definition of function. (Contributed by set.mm contributors, 29-Dec-1996.) (Revised by Scott Fenton, 16-Apr-2021.)
|- (Fun A <-> A.xE.zA.y(<.x, y>. e. A -> y = z))
Theorem	dffun6f 5123*	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.) (Revised by Scott Fenton, 16-Apr-2021.)
|- F/_xA   &   |- F/_yA   =>   |- (Fun A <-> A.xE*y xAy)
Theorem	dffun6 5124*	Alternate definition of a function using "at most one" notation. (Contributed by NM, 9-Mar-1995.) (Revised by Scott Fenton, 16-Apr-2021.)
|- (Fun F <-> A.xE*y xFy)
Theorem	funmo 5125*	A function has at most one value for each argument. (Contributed by NM, 24-May-1998.)
|- (Fun F -> E*y AFy)
Theorem	funss 5126	Subclass theorem for function predicate. (The proof was shortened by Mario Carneiro, 24-Jun-2014.) (Contributed by set.mm contributors, 16-Aug-1994.) (Revised by set.mm contributors, 24-Jun-2014.)
|- (A C_ B -> (Fun B -> Fun A))
Theorem	funeq 5127	Equality theorem for function predicate. (Contributed by set.mm contributors, 16-Aug-1994.)
|- (A = B -> (Fun A <-> Fun B))
Theorem	funeqi 5128	Equality inference for the function predicate. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
|- A = B   =>   |- (Fun A <-> Fun B)
Theorem	funeqd 5129	Equality deduction for the function predicate. (Contributed by set.mm contributors, 23-Feb-2013.)
|- (ph -> A = B)   =>   |- (ph -> (Fun A <-> Fun B))
Theorem	nffun 5130	Bound-variable hypothesis builder for a function. (Contributed by NM, 30-Jan-2004.)
|- F/_xF   =>   |- F/xFun F
Theorem	funeu 5131*	There is exactly one value of a function. (Contributed by NM, 22-Apr-2004.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)
|- ((Fun F /\ AFB) -> E!y AFy)
Theorem	funeu2 5132*	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 5133*	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 5134 shows that it doesn't matter which meaning we pick.) (Contributed by set.mm contributors, 4-Nov-2002.) (Revised by Scott Fenton, 16-Apr-2021.)
|- (Fun A <-> A.x e. dom AE*y xAy)
Theorem	dffun8 5134*	Alternate definition of a function. One possibility for the definition of a function in [Enderton] p. 42. Compare dffun7 5133. (The proof was shortened by Andrew Salmon, 17-Sep-2011.) (Contributed by set.mm contributors, 4-Nov-2002.) (Revised by set.mm contributors, 18-Sep-2011.) (Revised by Scott Fenton, 16-Apr-2021.)
|- (Fun A <-> A.x e. dom AE!y xAy)
Theorem	dffun9 5135*	Alternate definition of a function. (Contributed by set.mm contributors, 28-Mar-2007.) (Revised by Scott Fenton, 16-Apr-2021.)
|- (Fun A <-> A.x e. dom AE*y(y e. ran A /\ xAy))
Theorem	funfn 5136	An equivalence for the function predicate. (Contributed by set.mm contributors, 13-Aug-2004.)
|- (Fun A <-> A Fn dom A)
Theorem	funi 5137	The identity relation is a function. Part of Theorem 10.4 of [Quine] p. 65. (Contributed by set.mm contributors, 30-Apr-1998.)
|- Fun _I
Theorem	nfunv 5138	The universe is not a function. (Contributed by Raph Levien, 27-Jan-2004.)
|- -. Fun _V
Theorem	funopab 5139*	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.xE*yph)
Theorem	funopabeq 5140*	A class of ordered pairs of values is a function. (Contributed by set.mm contributors, 14-Nov-1995.)
|- Fun {<.x, y>. | y = A}
Theorem	funopab4 5141*	A class of ordered pairs of values in the form used by fvopab4 5389 is a function. (Contributed by set.mm contributors, 17-Feb-2013.)
|- Fun {<.x, y>. | (ph /\ y = A)}
Theorem	funco 5142	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 5143	A restriction of a function is a function. Compare Exercise 18 of [TakeutiZaring] p. 25. (Contributed by set.mm contributors, 16-Aug-1994.)
|- (Fun F -> Fun (F |` A))
Theorem	funssres 5144	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 5145	Equality of restrictions of a function and a subclass. (Contributed by set.mm contributors, 16-Aug-1994.) (Revised by set.mm contributors, 2-Jun-2007.)
|- ((Fun F /\ G C_ F /\ A C_ dom G) -> (F |` A) = (G |` A))
Theorem	funun 5146	The union of functions with disjoint domains is a function. Theorem 4.6 of [Monk1] p. 43. (Contributed by set.mm contributors, 12-Aug-1994.)
|- (((Fun F /\ Fun G) /\ (dom F i^i dom G) = (/)) -> Fun (F u. G))
Theorem	funsn 5147	A singleton of an ordered pair is a function. Theorem 10.5 of [Quine] p. 65. (Contributed by NM, 12-Aug-1994.) (Revised by Scott Fenton, 16-Apr-2021.)
|- Fun {<.A, B>.}
Theorem	funsngOLD 5148	A singleton of an ordered pair is a function. Theorem 10.5 of [Quine] p. 65. (Contributed by set.mm contributors, 28-Jun-2011.) (Revised by set.mm contributors, 1-Oct-2013.)
|- ((A e. V /\ B e. W) -> Fun {<.A, B>.})
Theorem	funprg 5149	A set of two pairs is a function if their first members are different. (Contributed by FL, 26-Jun-2011.) (Revised by Scott Fenton, 16-Apr-2021.)
|- ((A =/= B /\ C e. V /\ D e. W) -> Fun {<.A, C>., <.B, D>.})
Theorem	funprgOLD 5150	A set of two pairs is a function if their first members are different. (Contributed by FL, 26-Jun-2011.)
|- ((A =/= B /\ (A e. V /\ B e. W) /\ (C e. T /\ D e. U)) -> Fun {<.A, C>., <.B, D>.})
Theorem	funpr 5151	A function with a domain of two elements. (Contributed by Jeff Madsen, 20-Jun-2010.)
|- C e. _V   &   |- D e. _V   =>   |- (A =/= B -> Fun {<.A, C>., <.B, D>.})
Theorem	fnsn 5152	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 5153	Domain of a function with a domain of two different values. (Contributed by FL, 26-Jun-2011.)
|- ((A =/= B /\ (A e. V /\ B e. W) /\ (C e. T /\ D e. U)) -> {<.A, C>., <.B, D>.} Fn {A, B})
Theorem	fun0 5154	The empty set is a function. Theorem 10.3 of [Quine] p. 65. (Contributed by set.mm contributors, 7-Apr-1998.)
|- Fun (/)
Theorem	funcnv2 5155*	A simpler equivalence for single-rooted (see funcnv 5156). (Contributed by set.mm contributors, 9-Aug-2004.)
|- (Fun `'A <-> A.yE*x xAy)
Theorem	funcnv 5156*	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 xAy. Definition of single-rooted in [Enderton] p. 43. See funcnv2 5155 for a simpler version. (Contributed by set.mm contributors, 13-Aug-2004.)
|- (Fun `'A <-> A.y e. ran AE*x xAy)
Theorem	funcnv3 5157*	A condition showing a class is single-rooted. (See funcnv 5156). (Contributed by set.mm contributors, 26-May-2006.)
|- (Fun `'A <-> A.y e. ran AE!x e. dom A xAy)
Theorem	fncnv 5158*	Single-rootedness (see funcnv 5156) 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 xRy)
Theorem	fun11 5159*	Two ways of stating that 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. (Contributed by NM, 17-Jan-2006.) (Revised by Scott Fenton, 18-Apr-2021.)
|- ((Fun A /\ Fun `'A) <-> A.xA.yA.zA.w((xAy /\ zAw) -> (x = z <-> y = w)))
Theorem	fununi 5160*	The union of a chain (with respect to inclusion) of functions is a function. (Contributed by set.mm contributors, 10-Aug-2004.)
|- (A.f e. A (Fun f /\ A.g e. A (f C_ g \/ g C_ f)) -> Fun U.A)
Theorem	funcnvuni 5161*	The union of a chain (with respect to inclusion) of single-rooted sets is single-rooted. (See funcnv 5156 for "single-rooted" definition.) (Contributed by set.mm contributors, 11-Aug-2004.)
|- (A.f e. A (Fun `'f /\ A.g e. A (f C_ g \/ g C_ f)) -> Fun `'U.A)
Theorem	fun11uni 5162*	The union of a chain (with respect to inclusion) of one-to-one functions is a one-to-one function. (Contributed by set.mm contributors, 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 5163	The intersection with a function is a function. Exercise 14(a) of [Enderton] p. 53. (The proof was shortened by Andrew Salmon, 17-Sep-2011.) (Contributed by set.mm contributors, 19-Mar-2004.) (Revised by set.mm contributors, 18-Sep-2011.)
|- (Fun F -> Fun (F i^i G))
Theorem	funres11 5164	The restriction of a one-to-one function is one-to-one. (Contributed by set.mm contributors, 25-Mar-1998.)
|- (Fun `'F -> Fun `'(F |` A))
Theorem	funcnvres 5165	The converse of a restricted function. (Contributed by set.mm contributors, 27-Mar-1998.)
|- (Fun `'F -> `'(F |` A) = (`'F |` (F"A)))
Theorem	cnvresid 5166	Converse of a restricted identity function. (Contributed by FL, 4-Mar-2007.)
|- `'( _I |` A) = ( _I |` A)
Theorem	funcnvres2 5167	The converse of a restriction of the converse of a function equals the function restricted to the image of its converse. (Contributed by set.mm contributors, 4-May-2005.)
|- (Fun F -> `'(`'F |` A) = (F |` (`'F"A)))
Theorem	funimacnv 5168	The image of the preimage of a function. (Contributed by set.mm contributors, 25-May-2004.)
|- (Fun F -> (F"(`'F"A)) = (A i^i ran F))
Theorem	funimass1 5169	A kind of contraposition law that infers a subclass of an image from a preimage subclass. (Contributed by set.mm contributors, 25-May-2004.)
|- ((Fun F /\ A C_ ran F) -> ((`'F"A) C_ B -> A C_ (F"B)))
Theorem	funimass2 5170	A kind of contraposition law that infers an image subclass from a subclass of a preimage. (Contributed by set.mm contributors, 25-May-2004.) (Revised by set.mm contributors, 4-May-2007.)
|- ((Fun F /\ A C_ (`'F"B)) -> (F"A) C_ B)
Theorem	imadif 5171	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	imain 5172	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	fneq1 5173	Equality theorem for function predicate with domain. (Contributed by set.mm contributors, 1-Aug-1994.)
|- (F = G -> (F Fn A <-> G Fn A))
Theorem	fneq2 5174	Equality theorem for function predicate with domain. (Contributed by set.mm contributors, 1-Aug-1994.)
|- (A = B -> (F Fn A <-> F Fn B))
Theorem	fneq1d 5175	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 5176	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 5177	Equality deduction for function predicate with domain. (Contributed by set.mm contributors, 26-Jun-2011.)
|- (ph -> F = G)   &   |- (ph -> A = B)   =>   |- (ph -> (F Fn A <-> G Fn B))
Theorem	fneq1i 5178	Equality inference for function predicate with domain. (Contributed by Paul Chapman, 22-Jun-2011.)
|- F = G   =>   |- (F Fn A <-> G Fn A)
Theorem	fneq2i 5179	Equality inference for function predicate with domain. (Contributed by set.mm contributors, 4-Sep-2011.)
|- A = B   =>   |- (F Fn A <-> F Fn B)
Theorem	nffn 5180	Bound-variable hypothesis builder for a function with domain. (Contributed by NM, 30-Jan-2004.)
|- F/_xF   &   |- F/_xA   =>   |- F/x F Fn A
Theorem	fnfun 5181	A function with domain is a function. (Contributed by set.mm contributors, 1-Aug-1994.)
|- (F Fn A -> Fun F)
Theorem	fndm 5182	The domain of a function. (Contributed by set.mm contributors, 2-Aug-1994.)
|- (F Fn A -> dom F = A)
Theorem	funfni 5183	Inference to convert a function and domain antecedent. (Contributed by set.mm contributors, 22-Apr-2004.)
|- ((Fun F /\ B e. dom F) -> ph)   =>   |- ((F Fn A /\ B e. A) -> ph)
Theorem	fndmu 5184	A function has a unique domain. (Contributed by set.mm contributors, 11-Aug-1994.)
|- ((F Fn A /\ F Fn B) -> A = B)
Theorem	fnbr 5185	The first argument of binary relation on a function belongs to the function's domain. (Contributed by set.mm contributors, 7-May-2004.)
|- ((F Fn A /\ BFC) -> B e. A)
Theorem	fnop 5186	The first argument of an ordered pair in a function belongs to the function's domain. (Contributed by set.mm contributors, 8-Aug-1994.) (Revised by set.mm contributors, 25-Mar-2007.)
|- ((F Fn A /\ <.B, C>. e. F) -> B e. A)
Theorem	fneu 5187*	There is exactly one value of a function. (The proof was shortened by Andrew Salmon, 17-Sep-2011.) (Contributed by set.mm contributors, 22-Apr-2004.) (Revised by set.mm contributors, 18-Sep-2011.)
|- ((F Fn A /\ B e. A) -> E!y BFy)
Theorem	fneu2 5188*	There is exactly one value of a function. (Contributed by set.mm contributors, 7-Nov-1995.)
|- ((F Fn A /\ B e. A) -> E!y<.B, y>. e. F)
Theorem	fnun 5189	The union of two functions with disjoint domains. (Contributed by set.mm contributors, 22-Sep-2004.)
|- (((F Fn A /\ G Fn B) /\ (A i^i B) = (/)) -> (F u. G) Fn (A u. B))
Theorem	fnunsn 5190	Extension of a function with a new ordered pair. (Contributed by NM, 28-Sep-2013.)
|- (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 5191	Composition of two functions. (Contributed by set.mm contributors, 22-May-2006.)
|- ((F Fn A /\ G Fn B /\ ran G C_ A) -> (F o. G) Fn B)
Theorem	fnresdm 5192	A function does not change when restricted to its domain. (Contributed by set.mm contributors, 5-Sep-2004.)
|- (F Fn A -> (F |` A) = F)
Theorem	fnresdisj 5193	A function restricted to a class disjoint with its domain is empty. (Contributed by set.mm contributors, 23-Sep-2004.)
|- (F Fn A -> ((A i^i B) = (/) <-> (F |` B) = (/)))
Theorem	2elresin 5194	Membership in two functions restricted by each other's domain. (Contributed by set.mm contributors, 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 5195	Restriction of a function with a subclass of its domain. (Contributed by set.mm contributors, 10-Oct-2007.)
|- (F Fn A -> ((F |` B) Fn B <-> B C_ A))
Theorem	fnssres 5196	Restriction of a function with a subclass of its domain. (Contributed by set.mm contributors, 2-Aug-1994.) (Revised by set.mm contributors, 25-Sep-2004.)
|- ((F Fn A /\ B C_ A) -> (F |` B) Fn B)
Theorem	fnresin1 5197	Restriction of a function's domain with an intersection. (Contributed by set.mm contributors, 9-Aug-1994.)
|- (F Fn A -> (F |` (A i^i B)) Fn (A i^i B))
Theorem	fnresin2 5198	Restriction of a function's domain with an intersection. (Contributed by set.mm contributors, 9-Aug-1994.)
|- (F Fn A -> (F |` (B i^i A)) Fn (B i^i A))
Theorem	fnres 5199*	An equivalence for functionality of a restriction. Compare dffun8 5134. (Contributed by Mario Carneiro, 20-May-2015.)
|- ((F |` A) Fn A <-> A.x e. A E!y xFy)
Theorem	fnresi 5200	Functionality and domain of restricted identity. (Contributed by set.mm contributors, 27-Aug-2004.)
|- ( _I |` A) Fn A