Home New Foundations ExplorerTheorem List (p. 55 of 64) < Previous  Next > Bad symbols? Use Firefox (or GIF version for IE).

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

Theoremfunopfvb 5401 Equivalence of function value and ordered pair membership. Theorem 4.3(ii) of [Monk1] p. 42. (Contributed by set.mm contributors, 9-Jan-2015.)
((Fun F A dom F) → ((FA) = BA, B F))

Theoremfunbrfv2b 5402 Function value in terms of a binary relation. (Contributed by Mario Carneiro, 19-Mar-2014.)
(Fun F → (AFB ↔ (A dom F (FA) = B)))

Theoremdffn5 5403* Representation of a function in terms of its values. (Contributed by set.mm contributors, 29-Jan-2004.)
(F Fn AF = {x, y (x A y = (Fx))})

Theoremfnrnfv 5404* The range of a function expressed as a collection of the function's values. (Contributed by set.mm contributors, 20-Oct-2005.)
(F Fn A → ran F = {y x A y = (Fx)})

Theoremfvelrnb 5405* A member of a function's range is a value of the function. (Contributed by set.mm contributors, 31-Oct-1995.)
(F Fn A → (B ran Fx A (Fx) = B))

Theoremdfimafn 5406* Alternate definition of the image of a function. (Contributed by Raph Levien, 20-Nov-2006.)
((Fun F A dom F) → (FA) = {y x A (Fx) = y})

Theoremdfimafn2 5407* Alternate definition of the image of a function as an indexed union of singletons of function values. (Contributed by Raph Levien, 20-Nov-2006.)
((Fun F A dom F) → (FA) = x A {(Fx)})

Theoremfunimass4 5408* Membership relation for the values of a function whose image is a subclass. (Contributed by Raph Levien, 20-Nov-2006.)
((Fun F A dom F) → ((FA) Bx A (Fx) B))

Theoremfvelima 5409* Function value in an image. Part of Theorem 4.4(iii) of [Monk1] p. 42. (The proof was shortened by Andrew Salmon, 22-Oct-2011.) (Contributed by set.mm contributors, 29-Apr-2004.) (Revised by set.mm contributors, 22-Oct-2011.)
((Fun F A (FB)) → x B (Fx) = A)

Theoremfvelimab 5410* Function value in an image. (The proof was shortened by Andrew Salmon, 22-Oct-2011.) (An unnecessary distinct variable restriction was removed by David Abernethy, 17-Dec-2011.) (Contributed by set.mm contributors, 20-Jan-2007.) (Revised by set.mm contributors, 25-Dec-2011.)
((F Fn A B A) → (C (FB) ↔ x B (Fx) = C))

Theoremfniniseg 5411 Membership in the preimage of a singleton, under a function. (Contributed by Mario Carneiro, 12-May-2014.)
(F Fn A → (C (F “ {B}) ↔ (C A (FC) = B)))

Theoremfniinfv 5412* The indexed intersection of a function's values is the intersection of its range. (Contributed by set.mm contributors, 20-Oct-2005.)
(F Fn Ax A (Fx) = ran F)

Theoremfnsnfv 5413 Singleton of function value. (Contributed by set.mm contributors, 22-May-1998.)
((F Fn A B A) → {(FB)} = (F “ {B}))

Theoremfnimapr 5414 The image of a pair under a funtion. (Contributed by Jeff Madsen, 6-Jan-2011.)
((F Fn A B A C A) → (F “ {B, C}) = {(FB), (FC)})

Theoremfunfv 5415 A simplified expression for the value of a function when we know it's a function. (Contributed by NM, 22-May-1998.)
(Fun F → (FA) = (F “ {A}))

Theoremfunfv2 5416* The value of a function. Definition of function value in [Enderton] p. 43. (Contributed by set.mm contributors, 22-May-1998.) (Revised by set.mm contributors, 11-May-2005.)
(Fun F → (FA) = {y AFy})

Theoremfunfv2f 5417 The value of a function. Version of funfv2 5416 using a bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 19-Feb-2006.)
F/_yA    &   F/_yF       (Fun F → (FA) = {y AFy})

Theoremfvun 5418 Value of the union of two functions when the domains are separate. (Contributed by FL, 7-Nov-2011.)
(((Fun F Fun G) (dom F ∩ dom G) = ) → ((FG) ‘A) = ((FA) ∪ (GA)))

Theoremfvun1 5419 The value of a union when the argument is in the first domain. (Contributed by Scott Fenton, 29-Jun-2013.)
((F Fn A G Fn B ((AB) = X A)) → ((FG) ‘X) = (FX))

Theoremfvun2 5420 The value of a union when the argument is in the second domain. (Contributed by Scott Fenton, 29-Jun-2013.)
((F Fn A G Fn B ((AB) = X B)) → ((FG) ‘X) = (GX))

Theoremdmfco 5421 Domains of a function composition. (Contributed by set.mm contributors, 27-Jan-1997.)
((Fun G A dom G) → (A dom (F G) ↔ (GA) dom F))

Theoremfvco2 5422 Value of a function composition. Similar to second part of Theorem 3H of [Enderton] p. 47. (The proof was shortened by Andrew Salmon, 22-Oct-2011.) (Contributed by set.mm contributors, 9-Oct-2004.) (Revised by set.mm contributors, 22-Oct-2011.)
((G Fn A C A) → ((F G) ‘C) = (F ‘(GC)))

Theoremfvco 5423 Value of a function composition. Similar to Exercise 5 of [TakeutiZaring] p. 28. (Contributed by set.mm contributors, 22-Apr-2006.)
((Fun G A dom G) → ((F G) ‘A) = (F ‘(GA)))

Theoremfvco3 5424 Value of a function composition. (Contributed by set.mm contributors, 3-Jan-2004.) (Revised by set.mm contributors, 21-Aug-2006.)
((G:A–→B C A) → ((F G) ‘C) = (F ‘(GC)))

Theoremfvopab4t 5425* Closed theorem form of fvopab4 5429. (Contributed by set.mm contributors, 21-Feb-2013.)
((xy(x = AB = C) x F = {x, y (x D y = B)} (A D C V)) → (FA) = C)

Theoremfvopab3g 5426* Value of a function given by ordered-pair class abstraction. (Contributed by set.mm contributors, 6-Mar-1996.)
B V    &   (x = A → (φψ))    &   (y = B → (ψχ))    &   (x C∃!yφ)    &   F = {x, y (x C φ)}       (A C → ((FA) = Bχ))

Theoremfvopab3ig 5427* Value of a function given by ordered-pair class abstraction. (Contributed by set.mm contributors, 23-Oct-1999.)
(x = A → (φψ))    &   (y = B → (ψχ))    &   (x C∃*yφ)    &   F = {x, y (x C φ)}       ((A C B D) → (χ → (FA) = B))

Theoremfvopab4g 5428* Value of a function given by ordered-pair class abstraction. (Contributed by set.mm contributors, 23-Oct-1999.)
(x = AB = C)    &   F = {x, y (x D y = B)}       ((A D C R) → (FA) = C)

Theoremfvopab4 5429* Value of a function given by ordered-pair class abstraction. (Contributed by set.mm contributors, 23-Oct-1999.)
(x = AB = C)    &   F = {x, y (x D y = B)}    &   C V       (A D → (FA) = C)

Theoremfvopab4ndm 5430* Value of a function given by an ordered-pair class abstraction, outside of its domain. (Contributed by set.mm contributors, 28-Mar-2008.)
F = {x, y (x A φ)}       B A → (FB) = )

Theoremfvopabg 5431* The value of a function given by ordered-pair class abstraction. (Contributed by set.mm contributors, 2-Sep-2003.)
(x = AB = C)       ((A V C W) → ({x, y y = B} ‘A) = C)

Theoremeqfnfv2 5432* Equality of functions is determined by their values. Exercise 4 of [TakeutiZaring] p. 28. (Contributed by set.mm contributors, 3-Aug-1994.) (Revised by set.mm contributors, 5-Feb-2004.)
((F Fn A G Fn B) → (F = G ↔ (A = B x A (Fx) = (Gx))))

Theoremeqfnfv 5433* Equality of functions is determined by their values. Special case of Exercise 4 of [TakeutiZaring] p. 28 (with domain equality omitted). (The proof was shortened by Andrew Salmon, 22-Oct-2011.) (Contributed by set.mm contributors, 3-Aug-1994.) (Revised by set.mm contributors, 22-Oct-2011.)
((F Fn A G Fn A) → (F = Gx A (Fx) = (Gx)))

Theoremeqfnfv3 5434* Derive equality of functions from equality of their values. (Contributed by Jeff Madsen, 2-Sep-2009.)
((F Fn A G Fn B) → (F = G ↔ (B A x A (x B (Fx) = (Gx)))))

Theoremeqfnfvd 5435* Deduction for equality of functions. (Contributed by Mario Carneiro, 24-Jul-2014.)
(φF Fn A)    &   (φG Fn A)    &   ((φ x A) → (Fx) = (Gx))       (φF = G)

Theoremeqfnfv2f 5436* Equality of functions is determined by their values. Special case of Exercise 4 of [TakeutiZaring] p. 28 (with domain equality omitted). This version of eqfnfv 5433 uses bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 29-Jan-2004.)
F/_xF    &   F/_xG       ((F Fn A G Fn A) → (F = Gx A (Fx) = (Gx)))

Theoremeqfunfv 5437* Equality of functions is determined by their values. (Contributed by Scott Fenton, 19-Jun-2011.)
((Fun F Fun G) → (F = G ↔ (dom F = dom G x dom F(Fx) = (Gx))))

Theoremfvreseq 5438* Equality of restricted functions is determined by their values. (Contributed by set.mm contributors, 3-Aug-1994.) (Revised by set.mm contributors, 6-Feb-2004.)
(((F Fn A G Fn A) B A) → ((F B) = (G B) ↔ x B (Fx) = (Gx)))

Theoremchfnrn 5439* The range of a choice function (a function that chooses an element from each member of its domain) is included in the union of its domain. (Contributed by set.mm contributors, 31-Aug-1999.)
((F Fn A x A (Fx) x) → ran F A)

Theoremfunfvop 5440 Ordered pair with function value. Part of Theorem 4.3(i) of [Monk1] p. 41. (Contributed by set.mm contributors, 14-Oct-1996.)
((Fun F A dom F) → A, (FA) F)

Theoremfunfvbrb 5441 Two ways to say that A is in the domain of F. (Contributed by Mario Carneiro, 1-May-2014.)
(Fun F → (A dom FAF(FA)))

Theoremfvimacnvi 5442 A member of a preimage is a function value argument. (Contributed by set.mm contributors, 4-May-2007.)
((Fun F A (FB)) → (FA) B)

Theoremfvimacnv 5443 The argument of a function value belongs to the preimage of any class containing the function value. (Contributed by Raph Levien, 20-Nov-2006. He remarks: "This proof is unsatisfying, because it seems to me that funimass2 5206 could probably be strengthened to a biconditional.") (Contributed by set.mm contributors, 20-Nov-2006.)
((Fun F A dom F) → ((FA) BA (FB)))

Theoremfunimass3 5444 A kind of contraposition law that infers an image subclass from a subclass of a preimage. (Contributed by Raph Levien, 20-Nov-2006. He remarks: "Likely this could be proved directly, and fvimacnv 5443 would be the special case of A being a singleton, but it works this way round too.") (Contributed by set.mm contributors, 20-Nov-2006.)
((Fun F A dom F) → ((FA) BA (FB)))

Theoremfunimass5 5445* A subclass of a preimage in terms of function values. (Contributed by set.mm contributors, 15-May-2007.)
((Fun F A dom F) → (A (FB) ↔ x A (Fx) B))

Theoremfunconstss 5446* Two ways of specifying that a function is constant on a subdomain. (Contributed by set.mm contributors, 8-Mar-2007.)
((Fun F A dom F) → (x A (Fx) = BA (F “ {B})))

Theoremelpreima 5447 Membership in the preimage of a set under a function. (Contributed by Jeff Madsen, 2-Sep-2009.)
(F Fn A → (B (FC) ↔ (B A (FB) C)))

Theoremunpreima 5448 Preimage of a union. (Contributed by Jeff Madsen, 2-Sep-2009.)
(Fun F → (F “ (AB)) = ((FA) ∪ (FB)))

Theoreminpreima 5449 Preimage of an intersection. (Contributed by Jeff Madsen, 2-Sep-2009.)
(Fun F → (F “ (AB)) = ((FA) ∩ (FB)))

Theoremrespreima 5450 The preimage of a restricted function. (Contributed by Jeff Madsen, 2-Sep-2009.)
(Fun F → ((F B) “ A) = ((FA) ∩ B))

Theoremfimacnv 5451 The preimage of the codomain of a mapping is the mapping's domain. (Contributed by FL, 25-Jan-2007.)
(F:A–→B → (FB) = A)

Theoremfnopfv 5452 Ordered pair with function value. Part of Theorem 4.3(i) of [Monk1] p. 41. (Contributed by set.mm contributors, 30-Sep-2004.)
((F Fn A B A) → B, (FB) F)

Theoremfvelrn 5453 A function's value belongs to its range. (Contributed by set.mm contributors, 14-Oct-1996.)
((Fun F A dom F) → (FA) ran F)

Theoremfnfvelrn 5454 A function's value belongs to its range. (Contributed by set.mm contributors, 15-Oct-1996.)
((F Fn A B A) → (FB) ran F)

Theoremffvelrn 5455 A function's value belongs to its codomain. (Contributed by set.mm contributors, 12-Aug-1999.)
((F:A–→B C A) → (FC) B)

Theoremffvelrni 5456 A function's value belongs to its codomain. (Contributed by set.mm contributors, 6-Apr-2005.)
F:A–→B       (C A → (FC) B)

Theoremfnasrn 5457* A function expressed as the range of another function. (Contributed by Mario Carneiro, 22-Jun-2013.)
(F Fn AF = ran {x, y (x A y = x, (Fx))})

Theoremf0cli 5458 Unconditional closure of a function when the range includes the empty set. (Contributed by Mario Carneiro, 12-Sep-2013.)
F:A–→B    &    B       (FC) B

Theoremdff2 5459 Alternate definition of a mapping. (Contributed by set.mm contributors, 14-Nov-2007.)
(F:A–→B ↔ (F Fn A F (A × B)))

Theoremdff3 5460* Alternate definition of a mapping. (Contributed by set.mm contributors, 20-Mar-2007.)
(F:A–→B ↔ (F (A × B) x A ∃!y xFy))

Theoremdff4 5461* Alternate definition of a mapping. (Contributed by set.mm contributors, 20-Mar-2007.)
(F:A–→B ↔ (F (A × B) x A ∃!y B xFy))

Theoremdffo3 5462* An onto mapping expressed in terms of function values. (Contributed by set.mm contributors, 29-Oct-2006.)
(F:AontoB ↔ (F:A–→B y B x A y = (Fx)))

Theoremdffo4 5463* Alternate definition of an onto mapping. (Contributed by set.mm contributors, 20-Mar-2007.)
(F:AontoB ↔ (F:A–→B y B x A xFy))

Theoremdffo5 5464* Alternate definition of an onto mapping. (Contributed by set.mm contributors, 20-Mar-2007.)
(F:AontoB ↔ (F:A–→B y B x xFy))

Theoremfoelrn 5465* Property of a surjective function. (Contributed by Jeff Madsen, 4-Jan-2011.)
((F:AontoB C B) → x A C = (Fx))

Theoremfoco2 5466 If a composition of two functions is surjective, then the function on the left is surjective. (Contributed by Jeff Madsen, 16-Jun-2011.)
((F:B–→C G:A–→B (F G):AontoC) → F:BontoC)

Theoremffnfv 5467* A function maps to a class to which all values belong. (Contributed by NM, 3-Dec-2003.)
(F:A–→B ↔ (F Fn A x A (Fx) B))

Theoremffnfvf 5468 A function maps to a class to which all values belong. This version of ffnfv 5467 uses bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 28-Sep-2006.)
F/_xA    &   F/_xB    &   F/_xF       (F:A–→B ↔ (F Fn A x A (Fx) B))

Theoremfnfvrnss 5469* An upper bound for range determined by function values. (Contributed by set.mm contributors, 8-Oct-2004.)
((F Fn A x A (Fx) B) → ran F B)

Theoremfopabfv 5470* Representation of a mapping in terms of its values. (Contributed by set.mm contributors, 21-Feb-2004.)
(F:A–→B ↔ (F = {x, y (x A y = (Fx))} x A (Fx) B))

Theoremffvresb 5471* A necessary and sufficient condition for a restricted function. (Contributed by Mario Carneiro, 14-Nov-2013.)
(Fun F → ((F A):A–→Bx A (x dom F (Fx) B)))

Theoremfsn 5472 A function maps a singleton to a singleton iff it is the singleton of an ordered pair. (Contributed by NM, 10-Dec-2003.)
A V    &   B V       (F:{A}–→{B} ↔ F = {A, B})

Theoremfsng 5473 A function maps a singleton to a singleton iff it is the singleton of an ordered pair. (Contributed by set.mm contributors, 26-Oct-2012.)
((A C B D) → (F:{A}–→{B} ↔ F = {A, B}))

Theoremfsn2 5474 A function that maps a singleton to a class is the singleton of an ordered pair. (Contributed by set.mm contributors, 19-May-2004.)
A V       (F:{A}–→B ↔ ((FA) B F = {A, (FA)}))

Theoremxpsn 5475 The cross product of two singletons. (Contributed by set.mm contributors, 4-Nov-2006.)
A V    &   B V       ({A} × {B}) = {A, B}

Theoremressnop0 5476 If A is not in C, then the restriction of a singleton of A, B to C is null. (Contributed by Scott Fenton, 15-Apr-2011.)
A C → ({A, B} C) = )

Theoremfpr 5477 A function with a domain of two elements. (Contributed by Jeff Madsen, 20-Jun-2010.) (The proof was shortened by Andrew Salmon, 22-Oct-2011.)
A V    &   B V    &   C V    &   D V       (AB → {A, C, B, D}:{A, B}–→{C, D})

Theoremfnressn 5478 A function restricted to a singleton. (Contributed by set.mm contributors, 9-Oct-2004.)
((F Fn A B A) → (F {B}) = {B, (FB)})

Theoremfressnfv 5479 The value of a function restricted to a singleton. (Contributed by set.mm contributors, 9-Oct-2004.)
((F Fn A B A) → ((F {B}):{B}–→C ↔ (FB) C))

Theoremfvconst 5480 The value of a constant function. (Contributed by set.mm contributors, 30-May-1999.)
((F:A–→{B} C A) → (FC) = B)

Theoremfopabsn 5481* The singleton of an ordered pair expressed as an ordered pair class abstraction. (The proof was shortened by Andrew Salmon, 22-Oct-2011.) (Contributed by set.mm contributors, 6-Jun-2006.) (Revised by set.mm contributors, 22-Oct-2011.)
A V    &   B V       {A, B} = {x, y (x {A} y = B)}

Theoremfvi 5482 The value of the identity function. (Contributed by set.mm contributors, 1-May-2004.)
(A V → ( I ‘A) = A)

Theoremfvresi 5483 The value of a restricted identity function. (Contributed by set.mm contributors, 19-May-2004.)
(B A → (( I A) ‘B) = B)

Theoremfvunsn 5484 Remove an ordered pair not participating in a function value. (Revised by Mario Carneiro, 28-May-2014.) (Contributed by set.mm contributors, 1-Oct-2013.) (Revised by set.mm contributors, 28-May-2014.)
(BD → ((A ∪ {B, C}) ‘D) = (AD))

Theoremfvsn 5485 The value of a singleton of an ordered pair is the second member. (Contributed by set.mm contributors, 12-Aug-1994.)
A V    &   B V       ({A, B} ‘A) = B

Theoremfvsng 5486 The value of a singleton of an ordered pair is the second member. (Contributed by set.mm contributors, 26-Oct-2012.)
((A V B W) → ({A, B} ‘A) = B)

Theoremfvsnun1 5487 The value of a function with one of its ordered pairs replaced, at the replaced ordered pair. See also fvsnun2 5488. (Contributed by set.mm contributors, 23-Sep-2007.)
A V    &   B V    &   G = ({A, B} ∪ (F (C {A})))       (GA) = B

Theoremfvsnun2 5488 The value of a function with one of its ordered pairs replaced, at arguments other than the replaced one. See also fvsnun1 5487. (Contributed by set.mm contributors, 23-Sep-2007.)
A V    &   B V    &   G = ({A, B} ∪ (F (C {A})))       (D (C {A}) → (GD) = (FD))

Theoremfvpr1 5489 The value of a function with a domain of two elements. (Contributed by Jeff Madsen, 20-Jun-2010.)
A V    &   C V       (AB → ({A, C, B, D} ‘A) = C)

Theoremfvpr2 5490 The value of a function with a domain of two elements. (Contributed by Jeff Madsen, 20-Jun-2010.)
B V    &   D V       (AB → ({A, C, B, D} ‘B) = D)

Theoremfvconst2g 5491 The value of a constant function. (Contributed by set.mm contributors, 20-Aug-2005.)
((B D C A) → ((A × {B}) ‘C) = B)

Theoremfconst2g 5492 A constant function expressed as a cross product. (Contributed by set.mm contributors, 27-Nov-2007.)
(B C → (F:A–→{B} ↔ F = (A × {B})))

Theoremfvconst2 5493 The value of a constant function. (Contributed by set.mm contributors, 16-Apr-2005.)
B V       (C A → ((A × {B}) ‘C) = B)

Theoremfconst2 5494 A constant function expressed as a cross product. (Contributed by set.mm contributors, 20-Aug-1999.)
B V       (F:A–→{B} ↔ F = (A × {B}))

Theoremfconst5 5495 Two ways to express that a function is constant. (Contributed by set.mm contributors, 27-Nov-2007.)
((F Fn A A) → (F = (A × {B}) ↔ ran F = {B}))

Theoremfconstfv 5496* A constant function expressed in terms of its functionality, domain, and value. See also fconst2 5494. (Contributed by NM, 27-Aug-2004.)
(F:A–→{B} ↔ (F Fn A x A (Fx) = B))

Theoremfconst3 5497 Two ways to express a constant function. (Contributed by set.mm contributors, 15-Mar-2007.)
(F:A–→{B} ↔ (F Fn A A (F “ {B})))

Theoremfconst4 5498 Two ways to express a constant function. (Contributed by set.mm contributors, 8-Mar-2007.)
(F:A–→{B} ↔ (F Fn A (F “ {B}) = A))

Theoremfunfvima 5499 A function's value in a preimage belongs to the image. (Contributed by set.mm contributors, 23-Sep-2003.)
((Fun F B dom F) → (B A → (FB) (FA)))

Theoremfunfvima2 5500 A function's value in an included preimage belongs to the image. (Contributed by set.mm contributors, 3-Feb-1997.)
((Fun F A dom F) → (B A → (FB) (FA)))

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-6308
 Copyright terms: Public domain < Previous  Next >