Home Intuitionistic Logic ExplorerTheorem List (p. 53 of 95) < Previous  Next > Bad symbols? Try the GIF version. Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Intuitionistic Logic Explorer - 5201-5300   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremfvmptdf 5201* Alternate deduction version of fvmpt 5192, suitable for iteration. (Contributed by Mario Carneiro, 7-Jan-2017.)
(φA 𝐷)    &   ((φ x = A) → B 𝑉)    &   ((φ x = A) → ((𝐹A) = Bψ))    &   x𝐹    &   xψ       (φ → (𝐹 = (x 𝐷B) → ψ))

Theoremfvmptdv 5202* Alternate deduction version of fvmpt 5192, suitable for iteration. (Contributed by Mario Carneiro, 7-Jan-2017.)
(φA 𝐷)    &   ((φ x = A) → B 𝑉)    &   ((φ x = A) → ((𝐹A) = Bψ))       (φ → (𝐹 = (x 𝐷B) → ψ))

Theoremfvmptdv2 5203* Alternate deduction version of fvmpt 5192, suitable for iteration. (Contributed by Mario Carneiro, 7-Jan-2017.)
(φA 𝐷)    &   ((φ x = A) → B 𝑉)    &   ((φ x = A) → B = 𝐶)       (φ → (𝐹 = (x 𝐷B) → (𝐹A) = 𝐶))

Theoremmpteqb 5204* Bidirectional equality theorem for a mapping abstraction. Equivalent to eqfnfv 5208. (Contributed by Mario Carneiro, 14-Nov-2014.)
(x A B 𝑉 → ((x AB) = (x A𝐶) ↔ x A B = 𝐶))

Theoremfvmptt 5205* Closed theorem form of fvmpt 5192. (Contributed by Scott Fenton, 21-Feb-2013.) (Revised by Mario Carneiro, 11-Sep-2015.)
((x(x = AB = 𝐶) 𝐹 = (x 𝐷B) (A 𝐷 𝐶 𝑉)) → (𝐹A) = 𝐶)

Theoremfvmptf 5206* Value of a function given by an ordered-pair class abstraction. This version of fvmptg 5191 uses bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 8-Nov-2005.) (Revised by Mario Carneiro, 15-Oct-2016.)
xA    &   x𝐶    &   (x = AB = 𝐶)    &   𝐹 = (x 𝐷B)       ((A 𝐷 𝐶 𝑉) → (𝐹A) = 𝐶)

Theoremfvopab6 5207* Value of a function given by ordered-pair class abstraction. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 11-Sep-2015.)
𝐹 = {⟨x, y⟩ ∣ (φ y = B)}    &   (x = A → (φψ))    &   (x = AB = 𝐶)       ((A 𝐷 𝐶 𝑅 ψ) → (𝐹A) = 𝐶)

Theoremeqfnfv 5208* Equality of functions is determined by their values. Special case of Exercise 4 of [TakeutiZaring] p. 28 (with domain equality omitted). (Contributed by NM, 3-Aug-1994.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) (Proof shortened by Mario Carneiro, 31-Aug-2015.)
((𝐹 Fn A 𝐺 Fn A) → (𝐹 = 𝐺x A (𝐹x) = (𝐺x)))

Theoremeqfnfv2 5209* Equality of functions is determined by their values. Exercise 4 of [TakeutiZaring] p. 28. (Contributed by NM, 3-Aug-1994.) (Revised by Mario Carneiro, 31-Aug-2015.)
((𝐹 Fn A 𝐺 Fn B) → (𝐹 = 𝐺 ↔ (A = B x A (𝐹x) = (𝐺x))))

Theoremeqfnfv3 5210* Derive equality of functions from equality of their values. (Contributed by Jeff Madsen, 2-Sep-2009.)
((𝐹 Fn A 𝐺 Fn B) → (𝐹 = 𝐺 ↔ (BA x A (x B (𝐹x) = (𝐺x)))))

Theoremeqfnfvd 5211* Deduction for equality of functions. (Contributed by Mario Carneiro, 24-Jul-2014.)
(φ𝐹 Fn A)    &   (φ𝐺 Fn A)    &   ((φ x A) → (𝐹x) = (𝐺x))       (φ𝐹 = 𝐺)

Theoremeqfnfv2f 5212* 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 5208 uses bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 29-Jan-2004.)
x𝐹    &   x𝐺       ((𝐹 Fn A 𝐺 Fn A) → (𝐹 = 𝐺x A (𝐹x) = (𝐺x)))

Theoremeqfunfv 5213* Equality of functions is determined by their values. (Contributed by Scott Fenton, 19-Jun-2011.)
((Fun 𝐹 Fun 𝐺) → (𝐹 = 𝐺 ↔ (dom 𝐹 = dom 𝐺 x dom 𝐹(𝐹x) = (𝐺x))))

Theoremfvreseq 5214* Equality of restricted functions is determined by their values. (Contributed by NM, 3-Aug-1994.)
(((𝐹 Fn A 𝐺 Fn A) BA) → ((𝐹B) = (𝐺B) ↔ x B (𝐹x) = (𝐺x)))

Theoremfndmdif 5215* Two ways to express the locus of differences between two functions. (Contributed by Stefan O'Rear, 17-Jan-2015.)
((𝐹 Fn A 𝐺 Fn A) → dom (𝐹𝐺) = {x A ∣ (𝐹x) ≠ (𝐺x)})

Theoremfndmdifcom 5216 The difference set between two functions is commutative. (Contributed by Stefan O'Rear, 17-Jan-2015.)
((𝐹 Fn A 𝐺 Fn A) → dom (𝐹𝐺) = dom (𝐺𝐹))

Theoremfndmin 5217* Two ways to express the locus of equality between two functions. (Contributed by Stefan O'Rear, 17-Jan-2015.)
((𝐹 Fn A 𝐺 Fn A) → dom (𝐹𝐺) = {x A ∣ (𝐹x) = (𝐺x)})

Theoremfneqeql 5218 Two functions are equal iff their equalizer is the whole domain. (Contributed by Stefan O'Rear, 7-Mar-2015.)
((𝐹 Fn A 𝐺 Fn A) → (𝐹 = 𝐺 ↔ dom (𝐹𝐺) = A))

Theoremfneqeql2 5219 Two functions are equal iff their equalizer contains the whole domain. (Contributed by Stefan O'Rear, 9-Mar-2015.)
((𝐹 Fn A 𝐺 Fn A) → (𝐹 = 𝐺A ⊆ dom (𝐹𝐺)))

Theoremfnreseql 5220 Two functions are equal on a subset iff their equalizer contains that subset. (Contributed by Stefan O'Rear, 7-Mar-2015.)
((𝐹 Fn A 𝐺 Fn A 𝑋A) → ((𝐹𝑋) = (𝐺𝑋) ↔ 𝑋 ⊆ dom (𝐹𝐺)))

Theoremchfnrn 5221* 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 NM, 31-Aug-1999.)
((𝐹 Fn A x A (𝐹x) x) → ran 𝐹 A)

Theoremfunfvop 5222 Ordered pair with function value. Part of Theorem 4.3(i) of [Monk1] p. 41. (Contributed by NM, 14-Oct-1996.)
((Fun 𝐹 A dom 𝐹) → ⟨A, (𝐹A)⟩ 𝐹)

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

Theoremfvimacnvi 5224 A member of a preimage is a function value argument. (Contributed by NM, 4-May-2007.)
((Fun 𝐹 A (𝐹B)) → (𝐹A) B)

Theoremfvimacnv 5225 The argument of a function value belongs to the preimage of any class containing the function value. Raph Levien remarks: "This proof is unsatisfying, because it seems to me that funimass2 4920 could probably be strengthened to a biconditional." (Contributed by Raph Levien, 20-Nov-2006.)
((Fun 𝐹 A dom 𝐹) → ((𝐹A) BA (𝐹B)))

Theoremfunimass3 5226 A kind of contraposition law that infers an image subclass from a subclass of a preimage. Raph Levien remarks: "Likely this could be proved directly, and fvimacnv 5225 would be the special case of A being a singleton, but it works this way round too." (Contributed by Raph Levien, 20-Nov-2006.)
((Fun 𝐹 A ⊆ dom 𝐹) → ((𝐹A) ⊆ BA ⊆ (𝐹B)))

Theoremfunimass5 5227* A subclass of a preimage in terms of function values. (Contributed by NM, 15-May-2007.)
((Fun 𝐹 A ⊆ dom 𝐹) → (A ⊆ (𝐹B) ↔ x A (𝐹x) B))

Theoremfunconstss 5228* Two ways of specifying that a function is constant on a subdomain. (Contributed by NM, 8-Mar-2007.)
((Fun 𝐹 A ⊆ dom 𝐹) → (x A (𝐹x) = BA ⊆ (𝐹 “ {B})))

Theoremelpreima 5229 Membership in the preimage of a set under a function. (Contributed by Jeff Madsen, 2-Sep-2009.)
(𝐹 Fn A → (B (𝐹𝐶) ↔ (B A (𝐹B) 𝐶)))

Theoremfniniseg 5230 Membership in the preimage of a singleton, under a function. (Contributed by Mario Carneiro, 12-May-2014.) (Proof shortened by Mario Carneiro, 28-Apr-2015.)
(𝐹 Fn A → (𝐶 (𝐹 “ {B}) ↔ (𝐶 A (𝐹𝐶) = B)))

Theoremfncnvima2 5231* Inverse images under functions expressed as abstractions. (Contributed by Stefan O'Rear, 1-Feb-2015.)
(𝐹 Fn A → (𝐹B) = {x A ∣ (𝐹x) B})

Theoremfniniseg2 5232* Inverse point images under functions expressed as abstractions. (Contributed by Stefan O'Rear, 1-Feb-2015.)
(𝐹 Fn A → (𝐹 “ {B}) = {x A ∣ (𝐹x) = B})

Theoremfnniniseg2 5233* Support sets of functions expressed as abstractions. (Contributed by Stefan O'Rear, 1-Feb-2015.)
(𝐹 Fn A → (𝐹 “ (V ∖ {B})) = {x A ∣ (𝐹x) ≠ B})

Theoremrexsupp 5234* Existential quantification restricted to a support. (Contributed by Stefan O'Rear, 23-Mar-2015.)
(𝐹 Fn A → (x (𝐹 “ (V ∖ {𝑍}))φx A ((𝐹x) ≠ 𝑍 φ)))

Theoremunpreima 5235 Preimage of a union. (Contributed by Jeff Madsen, 2-Sep-2009.)
(Fun 𝐹 → (𝐹 “ (AB)) = ((𝐹A) ∪ (𝐹B)))

Theoreminpreima 5236 Preimage of an intersection. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 14-Jun-2016.)
(Fun 𝐹 → (𝐹 “ (AB)) = ((𝐹A) ∩ (𝐹B)))

Theoremdifpreima 5237 Preimage of a difference. (Contributed by Mario Carneiro, 14-Jun-2016.)
(Fun 𝐹 → (𝐹 “ (AB)) = ((𝐹A) ∖ (𝐹B)))

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

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

Theoremfnopfv 5240 Ordered pair with function value. Part of Theorem 4.3(i) of [Monk1] p. 41. (Contributed by NM, 30-Sep-2004.)
((𝐹 Fn A B A) → ⟨B, (𝐹B)⟩ 𝐹)

Theoremfvelrn 5241 A function's value belongs to its range. (Contributed by NM, 14-Oct-1996.)
((Fun 𝐹 A dom 𝐹) → (𝐹A) ran 𝐹)

Theoremfnfvelrn 5242 A function's value belongs to its range. (Contributed by NM, 15-Oct-1996.)
((𝐹 Fn A B A) → (𝐹B) ran 𝐹)

Theoremffvelrn 5243 A function's value belongs to its codomain. (Contributed by NM, 12-Aug-1999.)
((𝐹:AB 𝐶 A) → (𝐹𝐶) B)

Theoremffvelrni 5244 A function's value belongs to its codomain. (Contributed by NM, 6-Apr-2005.)
𝐹:AB       (𝐶 A → (𝐹𝐶) B)

Theoremffvelrnda 5245 A function's value belongs to its codomain. (Contributed by Mario Carneiro, 29-Dec-2016.)
(φ𝐹:AB)       ((φ 𝐶 A) → (𝐹𝐶) B)

Theoremffvelrnd 5246 A function's value belongs to its codomain. (Contributed by Mario Carneiro, 29-Dec-2016.)
(φ𝐹:AB)    &   (φ𝐶 A)       (φ → (𝐹𝐶) B)

Theoremrexrn 5247* Restricted existential quantification over the range of a function. (Contributed by Mario Carneiro, 24-Dec-2013.) (Revised by Mario Carneiro, 20-Aug-2014.)
(x = (𝐹y) → (φψ))       (𝐹 Fn A → (x ran 𝐹φy A ψ))

Theoremralrn 5248* Restricted universal quantification over the range of a function. (Contributed by Mario Carneiro, 24-Dec-2013.) (Revised by Mario Carneiro, 20-Aug-2014.)
(x = (𝐹y) → (φψ))       (𝐹 Fn A → (x ran 𝐹φy A ψ))

Theoremelrnrexdm 5249* For any element in the range of a function there is an element in the domain of the function for which the function value is the element of the range. (Contributed by Alexander van der Vekens, 8-Dec-2017.)
(Fun 𝐹 → (𝑌 ran 𝐹x dom 𝐹 𝑌 = (𝐹x)))

Theoremelrnrexdmb 5250* For any element in the range of a function there is an element in the domain of the function for which the function value is the element of the range. (Contributed by Alexander van der Vekens, 17-Dec-2017.)
(Fun 𝐹 → (𝑌 ran 𝐹x dom 𝐹 𝑌 = (𝐹x)))

Theoremeldmrexrn 5251* For any element in the domain of a function there is an element in the range of the function which is the function value for the element of the domain. (Contributed by Alexander van der Vekens, 8-Dec-2017.)
(Fun 𝐹 → (𝑌 dom 𝐹x ran 𝐹 x = (𝐹𝑌)))

Theoremralrnmpt 5252* A restricted quantifier over an image set. (Contributed by Mario Carneiro, 20-Aug-2015.)
𝐹 = (x AB)    &   (y = B → (ψχ))       (x A B 𝑉 → (y ran 𝐹ψx A χ))

Theoremrexrnmpt 5253* A restricted quantifier over an image set. (Contributed by Mario Carneiro, 20-Aug-2015.)
𝐹 = (x AB)    &   (y = B → (ψχ))       (x A B 𝑉 → (y ran 𝐹ψx A χ))

Theoremdff2 5254 Alternate definition of a mapping. (Contributed by NM, 14-Nov-2007.)
(𝐹:AB ↔ (𝐹 Fn A 𝐹 ⊆ (A × B)))

Theoremdff3im 5255* Property of a mapping. (Contributed by Jim Kingdon, 4-Jan-2019.)
(𝐹:AB → (𝐹 ⊆ (A × B) x A ∃!y x𝐹y))

Theoremdff4im 5256* Property of a mapping. (Contributed by Jim Kingdon, 4-Jan-2019.)
(𝐹:AB → (𝐹 ⊆ (A × B) x A ∃!y B x𝐹y))

Theoremdffo3 5257* An onto mapping expressed in terms of function values. (Contributed by NM, 29-Oct-2006.)
(𝐹:AontoB ↔ (𝐹:AB y B x A y = (𝐹x)))

Theoremdffo4 5258* Alternate definition of an onto mapping. (Contributed by NM, 20-Mar-2007.)
(𝐹:AontoB ↔ (𝐹:AB y B x A x𝐹y))

Theoremdffo5 5259* Alternate definition of an onto mapping. (Contributed by NM, 20-Mar-2007.)
(𝐹:AontoB ↔ (𝐹:AB y B x x𝐹y))

Theoremfoelrn 5260* Property of a surjective function. (Contributed by Jeff Madsen, 4-Jan-2011.)
((𝐹:AontoB 𝐶 B) → x A 𝐶 = (𝐹x))

Theoremfoco2 5261 If a composition of two functions is surjective, then the function on the left is surjective. (Contributed by Jeff Madsen, 16-Jun-2011.)
((𝐹:B𝐶 𝐺:AB (𝐹𝐺):Aonto𝐶) → 𝐹:Bonto𝐶)

Theoremfmpt 5262* Functionality of the mapping operation. (Contributed by Mario Carneiro, 26-Jul-2013.) (Revised by Mario Carneiro, 31-Aug-2015.)
𝐹 = (x A𝐶)       (x A 𝐶 B𝐹:AB)

Theoremf1ompt 5263* Express bijection for a mapping operation. (Contributed by Mario Carneiro, 30-May-2015.) (Revised by Mario Carneiro, 4-Dec-2016.)
𝐹 = (x A𝐶)       (𝐹:A1-1-ontoB ↔ (x A 𝐶 B y B ∃!x A y = 𝐶))

Theoremfmpti 5264* Functionality of the mapping operation. (Contributed by NM, 19-Mar-2005.) (Revised by Mario Carneiro, 1-Sep-2015.)
𝐹 = (x A𝐶)    &   (x A𝐶 B)       𝐹:AB

Theoremfmptd 5265* Domain and codomain of the mapping operation; deduction form. (Contributed by Mario Carneiro, 13-Jan-2013.)
((φ x A) → B 𝐶)    &   𝐹 = (x AB)       (φ𝐹:A𝐶)

Theoremffnfv 5266* A function maps to a class to which all values belong. (Contributed by NM, 3-Dec-2003.)
(𝐹:AB ↔ (𝐹 Fn A x A (𝐹x) B))

Theoremffnfvf 5267 A function maps to a class to which all values belong. This version of ffnfv 5266 uses bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 28-Sep-2006.)
xA    &   xB    &   x𝐹       (𝐹:AB ↔ (𝐹 Fn A x A (𝐹x) B))

Theoremfnfvrnss 5268* An upper bound for range determined by function values. (Contributed by NM, 8-Oct-2004.)
((𝐹 Fn A x A (𝐹x) B) → ran 𝐹B)

Theoremrnmptss 5269* The range of an operation given by the "maps to" notation as a subset. (Contributed by Thierry Arnoux, 24-Sep-2017.)
𝐹 = (x AB)       (x A B 𝐶 → ran 𝐹𝐶)

Theoremfmpt2d 5270* Domain and codomain of the mapping operation; deduction form. (Contributed by NM, 27-Dec-2014.)
((φ x A) → B 𝑉)    &   (φ𝐹 = (x AB))    &   ((φ y A) → (𝐹y) 𝐶)       (φ𝐹:A𝐶)

Theoremffvresb 5271* A necessary and sufficient condition for a restricted function. (Contributed by Mario Carneiro, 14-Nov-2013.)
(Fun 𝐹 → ((𝐹A):ABx A (x dom 𝐹 (𝐹x) B)))

Theoremf1oresrab 5272* Build a bijection between restricted abstract builders, given a bijection between the base classes, deduction version. (Contributed by Thierry Arnoux, 17-Aug-2018.)
𝐹 = (x A𝐶)    &   (φ𝐹:A1-1-ontoB)    &   ((φ x A y = 𝐶) → (χψ))       (φ → (𝐹 ↾ {x Aψ}):{x Aψ}–1-1-onto→{y Bχ})

Theoremfmptco 5273* Composition of two functions expressed as ordered-pair class abstractions. If 𝐹 has the equation ( x + 2 ) and 𝐺 the equation ( 3 * z ) then (𝐺𝐹) has the equation ( 3 * ( x + 2 ) ) . (Contributed by FL, 21-Jun-2012.) (Revised by Mario Carneiro, 24-Jul-2014.)
((φ x A) → 𝑅 B)    &   (φ𝐹 = (x A𝑅))    &   (φ𝐺 = (y B𝑆))    &   (y = 𝑅𝑆 = 𝑇)       (φ → (𝐺𝐹) = (x A𝑇))

Theoremfmptcof 5274* Version of fmptco 5273 where φ needn't be distinct from x. (Contributed by NM, 27-Dec-2014.)
(φx A 𝑅 B)    &   (φ𝐹 = (x A𝑅))    &   (φ𝐺 = (y B𝑆))    &   (y = 𝑅𝑆 = 𝑇)       (φ → (𝐺𝐹) = (x A𝑇))

Theoremfmptcos 5275* Composition of two functions expressed as mapping abstractions. (Contributed by NM, 22-May-2006.) (Revised by Mario Carneiro, 31-Aug-2015.)
(φx A 𝑅 B)    &   (φ𝐹 = (x A𝑅))    &   (φ𝐺 = (y B𝑆))       (φ → (𝐺𝐹) = (x A𝑅 / y𝑆))

Theoremfcompt 5276* Express composition of two functions as a maps-to applying both in sequence. (Contributed by Stefan O'Rear, 5-Oct-2014.) (Proof shortened by Mario Carneiro, 27-Dec-2014.)
((A:𝐷𝐸 B:𝐶𝐷) → (AB) = (x 𝐶 ↦ (A‘(Bx))))

Theoremfcoconst 5277 Composition with a constant function. (Contributed by Stefan O'Rear, 11-Mar-2015.)
((𝐹 Fn 𝑋 𝑌 𝑋) → (𝐹 ∘ (𝐼 × {𝑌})) = (𝐼 × {(𝐹𝑌)}))

Theoremfsn 5278 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       (𝐹:{A}⟶{B} ↔ 𝐹 = {⟨A, B⟩})

Theoremfsng 5279 A function maps a singleton to a singleton iff it is the singleton of an ordered pair. (Contributed by NM, 26-Oct-2012.)
((A 𝐶 B 𝐷) → (𝐹:{A}⟶{B} ↔ 𝐹 = {⟨A, B⟩}))

Theoremfsn2 5280 A function that maps a singleton to a class is the singleton of an ordered pair. (Contributed by NM, 19-May-2004.)
A V       (𝐹:{A}⟶B ↔ ((𝐹A) B 𝐹 = {⟨A, (𝐹A)⟩}))

Theoremxpsng 5281 The cross product of two singletons. (Contributed by Mario Carneiro, 30-Apr-2015.)
((A 𝑉 B 𝑊) → ({A} × {B}) = {⟨A, B⟩})

Theoremxpsn 5282 The cross product of two singletons. (Contributed by NM, 4-Nov-2006.)
A V    &   B V       ({A} × {B}) = {⟨A, B⟩}

Theoremdfmpt 5283 Alternate definition for the "maps to" notation df-mpt 3811 (although it requires that B be a set). (Contributed by NM, 24-Aug-2010.) (Revised by Mario Carneiro, 30-Dec-2016.)
B V       (x AB) = x A {⟨x, B⟩}

Theoremfnasrn 5284 A function expressed as the range of another function. (Contributed by Mario Carneiro, 22-Jun-2013.) (Proof shortened by Mario Carneiro, 31-Aug-2015.)
B V       (x AB) = ran (x A ↦ ⟨x, B⟩)

Theoremdfmptg 5285 Alternate definition for the "maps to" notation df-mpt 3811 (which requires that B be a set). (Contributed by Jim Kingdon, 9-Jan-2019.)
(x A B 𝑉 → (x AB) = x A {⟨x, B⟩})

Theoremfnasrng 5286 A function expressed as the range of another function. (Contributed by Jim Kingdon, 9-Jan-2019.)
(x A B 𝑉 → (x AB) = ran (x A ↦ ⟨x, B⟩))

Theoremressnop0 5287 If A is not in 𝐶, then the restriction of a singleton of A, B to 𝐶 is null. (Contributed by Scott Fenton, 15-Apr-2011.)
A 𝐶 → ({⟨A, B⟩} ↾ 𝐶) = ∅)

Theoremfpr 5288 A function with a domain of two elements. (Contributed by Jeff Madsen, 20-Jun-2010.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
A V    &   B V    &   𝐶 V    &   𝐷 V       (AB → {⟨A, 𝐶⟩, ⟨B, 𝐷⟩}:{A, B}⟶{𝐶, 𝐷})

Theoremfprg 5289 A function with a domain of two elements. (Contributed by FL, 2-Feb-2014.)
(((A 𝐸 B 𝐹) (𝐶 𝐺 𝐷 𝐻) AB) → {⟨A, 𝐶⟩, ⟨B, 𝐷⟩}:{A, B}⟶{𝐶, 𝐷})

Theoremftpg 5290 A function with a domain of three elements. (Contributed by Alexander van der Vekens, 4-Dec-2017.)
(((𝑋 𝑈 𝑌 𝑉 𝑍 𝑊) (A 𝐹 B 𝐺 𝐶 𝐻) (𝑋𝑌 𝑋𝑍 𝑌𝑍)) → {⟨𝑋, A⟩, ⟨𝑌, B⟩, ⟨𝑍, 𝐶⟩}:{𝑋, 𝑌, 𝑍}⟶{A, B, 𝐶})

Theoremftp 5291 A function with a domain of three elements. (Contributed by Stefan O'Rear, 17-Oct-2014.) (Proof shortened by Alexander van der Vekens, 23-Jan-2018.)
A V    &   B V    &   𝐶 V    &   𝑋 V    &   𝑌 V    &   𝑍 V    &   AB    &   A𝐶    &   B𝐶       {⟨A, 𝑋⟩, ⟨B, 𝑌⟩, ⟨𝐶, 𝑍⟩}:{A, B, 𝐶}⟶{𝑋, 𝑌, 𝑍}

Theoremfnressn 5292 A function restricted to a singleton. (Contributed by NM, 9-Oct-2004.)
((𝐹 Fn A B A) → (𝐹 ↾ {B}) = {⟨B, (𝐹B)⟩})

Theoremfressnfv 5293 The value of a function restricted to a singleton. (Contributed by NM, 9-Oct-2004.)
((𝐹 Fn A B A) → ((𝐹 ↾ {B}):{B}⟶𝐶 ↔ (𝐹B) 𝐶))

Theoremfvconst 5294 The value of a constant function. (Contributed by NM, 30-May-1999.)
((𝐹:A⟶{B} 𝐶 A) → (𝐹𝐶) = B)

Theoremfmptsn 5295* Express a singleton function in maps-to notation. (Contributed by NM, 6-Jun-2006.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) (Revised by Stefan O'Rear, 28-Feb-2015.)
((A 𝑉 B 𝑊) → {⟨A, B⟩} = (x {A} ↦ B))

Theoremfmptap 5296* Append an additional value to a function. (Contributed by NM, 6-Jun-2006.) (Revised by Mario Carneiro, 31-Aug-2015.)
A V    &   B V    &   (𝑅 ∪ {A}) = 𝑆    &   (x = A𝐶 = B)       ((x 𝑅𝐶) ∪ {⟨A, B⟩}) = (x 𝑆𝐶)

Theoremfmptapd 5297* Append an additional value to a function. (Contributed by Thierry Arnoux, 3-Jan-2017.)
(φA V)    &   (φB V)    &   (φ → (𝑅 ∪ {A}) = 𝑆)    &   ((φ x = A) → 𝐶 = B)       (φ → ((x 𝑅𝐶) ∪ {⟨A, B⟩}) = (x 𝑆𝐶))

Theoremfmptpr 5298* Express a pair function in maps-to notation. (Contributed by Thierry Arnoux, 3-Jan-2017.)
(φA 𝑉)    &   (φB 𝑊)    &   (φ𝐶 𝑋)    &   (φ𝐷 𝑌)    &   ((φ x = A) → 𝐸 = 𝐶)    &   ((φ x = B) → 𝐸 = 𝐷)       (φ → {⟨A, 𝐶⟩, ⟨B, 𝐷⟩} = (x {A, B} ↦ 𝐸))

Theoremfvresi 5299 The value of a restricted identity function. (Contributed by NM, 19-May-2004.)
(B A → (( I ↾ A)‘B) = B)

Theoremfvunsng 5300 Remove an ordered pair not participating in a function value. (Contributed by Jim Kingdon, 7-Jan-2019.)
((𝐷 𝑉 B𝐷) → ((A ∪ {⟨B, 𝐶⟩})‘𝐷) = (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-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9447
 Copyright terms: Public domain < Previous  Next >