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

Theoremcnvexg 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 VA V)

Theoremcnvex 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 V       A V

Theoremcnvexb 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 V ↔ R V)

Theoremrnexg 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 V → ran A V)

Theoremdmexg 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 V → dom A V)

Theoremdmex 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 V       dom A V

Theoremrnex 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 V       ran A V

Theoremelxp4 5108 Membership in a cross product. This version requires no quantifiers or dummy variables. (Contributed by set.mm contributors, 17-Feb-2004.)
(A (B × C) ↔ (A = dom {A}, ran {A} (dom {A} B ran {A} C)))

Theoremxpexr 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 × B) C → (A V B V))

Theoremxpexr2 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 × B) C (A × B) ≠ ) → (A V B V))

Theoremdf2nd2 5111 Alternate definition of the 2nd function. (Contributed by SF, 8-Jan-2015.)
2nd = (1st Swap )

Theorem2ndex 5112 The 2nd function is a set. (Contributed by SF, 8-Jan-2015.)
2nd V

Theoremdfxp2 5113 Define cross product via the set construction functions. (Contributed by SF, 8-Jan-2015.)
(A × B) = ((1stA) ∩ (2ndB))

Theoremxpexg 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 V B W) → (A × B) V)

Theoremxpex 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 V    &   B V       (A × B) V

Theoremresexg 5116 The restriction of a set to a set is a set. (Contributed by set.mm contributors, 8-Jan-2015.)
((A V B W) → (A B) V)

Theoremresex 5117 The restriction of a set to a set is a set. (Contributed by set.mm contributors, 8-Jan-2015.)
A V    &   B V       (A B) V

Theoremcnviin 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 A B = x A B

Theoremdffun2 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 Axyz((xAy xAz) → y = z))

Theoremdffun3 5120* Alternate definition of function. (Contributed by NM, 29-Dec-1996.) (Revised by Scott Fenton, 16-Apr-2021.)
(Fun Axzy(xAyy = z))

Theoremdffun4 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 Axyz((x, y A x, z A) → y = z))

Theoremdffun5 5122* Alternate definition of function. (Contributed by set.mm contributors, 29-Dec-1996.) (Revised by Scott Fenton, 16-Apr-2021.)
(Fun Axzy(x, y Ay = z))

Theoremdffun6f 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.)
xA    &   yA       (Fun Ax∃*y xAy)

Theoremdffun6 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 Fx∃*y xFy)

Theoremfunmo 5125* A function has at most one value for each argument. (Contributed by NM, 24-May-1998.)
(Fun F∃*y AFy)

Theoremfunss 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 B → (Fun B → Fun A))

Theoremfuneq 5127 Equality theorem for function predicate. (Contributed by set.mm contributors, 16-Aug-1994.)
(A = B → (Fun A ↔ Fun B))

Theoremfuneqi 5128 Equality inference for the function predicate. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
A = B       (Fun A ↔ Fun B)

Theoremfuneqd 5129 Equality deduction for the function predicate. (Contributed by set.mm contributors, 23-Feb-2013.)
(φA = B)       (φ → (Fun A ↔ Fun B))

Theoremnffun 5130 Bound-variable hypothesis builder for a function. (Contributed by NM, 30-Jan-2004.)
xF       xFun F

Theoremfuneu 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) → ∃!y AFy)

Theoremfuneu2 5132* There is exactly one value of a function. (Contributed by NM, 3-Aug-1994.)
((Fun F A, B F) → ∃!yA, y F)

Theoremdffun7 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 Ax dom A∃*y xAy)

Theoremdffun8 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 Ax dom A∃!y xAy)

Theoremdffun9 5135* Alternate definition of a function. (Contributed by set.mm contributors, 28-Mar-2007.) (Revised by Scott Fenton, 16-Apr-2021.)
(Fun Ax dom A∃*y(y ran A xAy))

Theoremfunfn 5136 An equivalence for the function predicate. (Contributed by set.mm contributors, 13-Aug-2004.)
(Fun AA Fn dom A)

Theoremfuni 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

Theoremnfunv 5138 The universe is not a function. (Contributed by Raph Levien, 27-Jan-2004.)
¬ Fun V

Theoremfunopab 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 φ} ↔ x∃*yφ)

Theoremfunopabeq 5140* A class of ordered pairs of values is a function. (Contributed by set.mm contributors, 14-Nov-1995.)
Fun {x, y y = A}

Theoremfunopab4 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 (φ y = A)}

Theoremfunco 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 G))

Theoremfunres 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))

Theoremfunssres 5144 The restriction of a function to the domain of a subclass equals the subclass. (Contributed by NM, 15-Aug-1994.)
((Fun F G F) → (F dom G) = G)

Theoremfun2ssres 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 F A dom G) → (F A) = (G A))

Theoremfunun 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 ∩ dom G) = ) → Fun (FG))

Theoremfunsn 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}

TheoremfunsngOLD 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 V B W) → Fun {A, B})

Theoremfunprg 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.)
((AB C V D W) → Fun {A, C, B, D})

TheoremfunprgOLD 5150 A set of two pairs is a function if their first members are different. (Contributed by FL, 26-Jun-2011.)
((AB (A V B W) (C T D U)) → Fun {A, C, B, D})

Theoremfunpr 5151 A function with a domain of two elements. (Contributed by Jeff Madsen, 20-Jun-2010.)
C V    &   D V       (AB → Fun {A, C, B, D})

Theoremfnsn 5152 Functionality and domain of the singleton of an ordered pair. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
A V    &   B V       {A, B} Fn {A}

Theoremfnprg 5153 Domain of a function with a domain of two different values. (Contributed by FL, 26-Jun-2011.)
((AB (A V B W) (C T D U)) → {A, C, B, D} Fn {A, B})

Theoremfun0 5154 The empty set is a function. Theorem 10.3 of [Quine] p. 65. (Contributed by set.mm contributors, 7-Apr-1998.)
Fun

Theoremfuncnv2 5155* A simpler equivalence for single-rooted (see funcnv 5156). (Contributed by set.mm contributors, 9-Aug-2004.)
(Fun Ay∃*x xAy)

Theoremfuncnv 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 Ay ran A∃*x xAy)

Theoremfuncnv3 5157* A condition showing a class is single-rooted. (See funcnv 5156). (Contributed by set.mm contributors, 26-May-2006.)
(Fun Ay ran A∃!x dom A xAy)

Theoremfncnv 5158* Single-rootedness (see funcnv 5156) of a class cut down by a cross product. (Contributed by NM, 5-Mar-2007.)
((R ∩ (A × B)) Fn By B ∃!x A xRy)

Theoremfun11 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) ↔ xyzw((xAy zAw) → (x = zy = w)))

Theoremfununi 5160* The union of a chain (with respect to inclusion) of functions is a function. (Contributed by set.mm contributors, 10-Aug-2004.)
(f A (Fun f g A (f g g f)) → Fun A)

Theoremfuncnvuni 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.)
(f A (Fun f g A (f g g f)) → Fun A)

Theoremfun11uni 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.)
(f A ((Fun f Fun f) g A (f g g f)) → (Fun A Fun A))

Theoremfunin 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 (FG))

Theoremfunres11 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))

Theoremfuncnvres 5165 The converse of a restricted function. (Contributed by set.mm contributors, 27-Mar-1998.)
(Fun F(F A) = (F (FA)))

Theoremcnvresid 5166 Converse of a restricted identity function. (Contributed by FL, 4-Mar-2007.)
( I A) = ( I A)

Theoremfuncnvres2 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 (FA)))

Theoremfunimacnv 5168 The image of the preimage of a function. (Contributed by set.mm contributors, 25-May-2004.)
(Fun F → (F “ (FA)) = (A ∩ ran F))

Theoremfunimass1 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 ran F) → ((FA) BA (FB)))

Theoremfunimass2 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 (FB)) → (FA) B)

Theoremimadif 5171 The image of a difference is the difference of images. (Contributed by NM, 24-May-1998.)
(Fun F → (F “ (A B)) = ((FA) (FB)))

Theoremimain 5172 The image of an intersection is the intersection of images. (Contributed by Paul Chapman, 11-Apr-2009.)
(Fun F → (F “ (AB)) = ((FA) ∩ (FB)))

Theoremfneq1 5173 Equality theorem for function predicate with domain. (Contributed by set.mm contributors, 1-Aug-1994.)
(F = G → (F Fn AG Fn A))

Theoremfneq2 5174 Equality theorem for function predicate with domain. (Contributed by set.mm contributors, 1-Aug-1994.)
(A = B → (F Fn AF Fn B))

Theoremfneq1d 5175 Equality deduction for function predicate with domain. (Contributed by Paul Chapman, 22-Jun-2011.)
(φF = G)       (φ → (F Fn AG Fn A))

Theoremfneq2d 5176 Equality deduction for function predicate with domain. (Contributed by Paul Chapman, 22-Jun-2011.)
(φA = B)       (φ → (F Fn AF Fn B))

Theoremfneq12d 5177 Equality deduction for function predicate with domain. (Contributed by set.mm contributors, 26-Jun-2011.)
(φF = G)    &   (φA = B)       (φ → (F Fn AG Fn B))

Theoremfneq1i 5178 Equality inference for function predicate with domain. (Contributed by Paul Chapman, 22-Jun-2011.)
F = G       (F Fn AG Fn A)

Theoremfneq2i 5179 Equality inference for function predicate with domain. (Contributed by set.mm contributors, 4-Sep-2011.)
A = B       (F Fn AF Fn B)

Theoremnffn 5180 Bound-variable hypothesis builder for a function with domain. (Contributed by NM, 30-Jan-2004.)
xF    &   xA       x F Fn A

Theoremfnfun 5181 A function with domain is a function. (Contributed by set.mm contributors, 1-Aug-1994.)
(F Fn A → Fun F)

Theoremfndm 5182 The domain of a function. (Contributed by set.mm contributors, 2-Aug-1994.)
(F Fn A → dom F = A)

Theoremfunfni 5183 Inference to convert a function and domain antecedent. (Contributed by set.mm contributors, 22-Apr-2004.)
((Fun F B dom F) → φ)       ((F Fn A B A) → φ)

Theoremfndmu 5184 A function has a unique domain. (Contributed by set.mm contributors, 11-Aug-1994.)
((F Fn A F Fn B) → A = B)

Theoremfnbr 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 A)

Theoremfnop 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 F) → B A)

Theoremfneu 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 A) → ∃!y BFy)

Theoremfneu2 5188* There is exactly one value of a function. (Contributed by set.mm contributors, 7-Nov-1995.)
((F Fn A B A) → ∃!yB, y F)

Theoremfnun 5189 The union of two functions with disjoint domains. (Contributed by set.mm contributors, 22-Sep-2004.)
(((F Fn A G Fn B) (AB) = ) → (FG) Fn (AB))

Theoremfnunsn 5190 Extension of a function with a new ordered pair. (Contributed by NM, 28-Sep-2013.)
(φX V)    &   (φY V)    &   (φF Fn D)    &   G = (F ∪ {X, Y})    &   E = (D ∪ {X})    &   (φ → ¬ X D)       (φG Fn E)

Theoremfnco 5191 Composition of two functions. (Contributed by set.mm contributors, 22-May-2006.)
((F Fn A G Fn B ran G A) → (F G) Fn B)

Theoremfnresdm 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)

Theoremfnresdisj 5193 A function restricted to a class disjoint with its domain is empty. (Contributed by set.mm contributors, 23-Sep-2004.)
(F Fn A → ((AB) = ↔ (F B) = ))

Theorem2elresin 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 F x, z G) ↔ (x, y (F (AB)) x, z (G (AB)))))

Theoremfnssresb 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 BB A))

Theoremfnssres 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 A) → (F B) Fn B)

Theoremfnresin1 5197 Restriction of a function's domain with an intersection. (Contributed by set.mm contributors, 9-Aug-1994.)
(F Fn A → (F (AB)) Fn (AB))

Theoremfnresin2 5198 Restriction of a function's domain with an intersection. (Contributed by set.mm contributors, 9-Aug-1994.)
(F Fn A → (F (BA)) Fn (BA))

Theoremfnres 5199* An equivalence for functionality of a restriction. Compare dffun8 5134. (Contributed by Mario Carneiro, 20-May-2015.)
((F A) Fn Ax A ∃!y xFy)

Theoremfnresi 5200 Functionality and domain of restricted identity. (Contributed by set.mm contributors, 27-Aug-2004.)
( I A) Fn A

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6337
 Copyright terms: Public domain < Previous  Next >