P. 53 of Theorem List - Intuitionistic Logic Explorer

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

Type	Label	Description
Statement
Theorem	fvmptdf 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) → ψ))
Theorem	fvmptdv 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) → ψ))
Theorem	fvmptdv2 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) = 𝐶))
Theorem	mpteqb 5204*	Bidirectional equality theorem for a mapping abstraction. Equivalent to eqfnfv 5208. (Contributed by Mario Carneiro, 14-Nov-2014.)
⊢ (∀x ∈ A B ∈ 𝑉 → ((x ∈ A ↦ B) = (x ∈ A ↦ 𝐶) ↔ ∀x ∈ A B = 𝐶))
Theorem	fvmptt 5205*	Closed theorem form of fvmpt 5192. (Contributed by Scott Fenton, 21-Feb-2013.) (Revised by Mario Carneiro, 11-Sep-2015.)
⊢ ((∀x(x = A → B = 𝐶) ∧ 𝐹 = (x ∈ 𝐷 ↦ B) ∧ (A ∈ 𝐷 ∧ 𝐶 ∈ 𝑉)) → (𝐹‘A) = 𝐶)
Theorem	fvmptf 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 = A → B = 𝐶)    &   ⊢ 𝐹 = (x ∈ 𝐷 ↦ B)    ⇒   ⊢ ((A ∈ 𝐷 ∧ 𝐶 ∈ 𝑉) → (𝐹‘A) = 𝐶)
Theorem	fvopab6 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 = A → B = 𝐶)    ⇒   ⊢ ((A ∈ 𝐷 ∧ 𝐶 ∈ 𝑅 ∧ ψ) → (𝐹‘A) = 𝐶)
Theorem	eqfnfv 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)))
Theorem	eqfnfv2 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))))
Theorem	eqfnfv3 5210*	Derive equality of functions from equality of their values. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ ((𝐹 Fn A ∧ 𝐺 Fn B) → (𝐹 = 𝐺 ↔ (B ⊆ A ∧ ∀x ∈ A (x ∈ B ∧ (𝐹‘x) = (𝐺‘x)))))
Theorem	eqfnfvd 5211*	Deduction for equality of functions. (Contributed by Mario Carneiro, 24-Jul-2014.)
⊢ (φ → 𝐹 Fn A)    &   ⊢ (φ → 𝐺 Fn A)    &   ⊢ ((φ ∧ x ∈ A) → (𝐹‘x) = (𝐺‘x))    ⇒   ⊢ (φ → 𝐹 = 𝐺)
Theorem	eqfnfv2f 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)))
Theorem	eqfunfv 5213*	Equality of functions is determined by their values. (Contributed by Scott Fenton, 19-Jun-2011.)
⊢ ((Fun 𝐹 ∧ Fun 𝐺) → (𝐹 = 𝐺 ↔ (dom 𝐹 = dom 𝐺 ∧ ∀x ∈ dom 𝐹(𝐹‘x) = (𝐺‘x))))
Theorem	fvreseq 5214*	Equality of restricted functions is determined by their values. (Contributed by NM, 3-Aug-1994.)
⊢ (((𝐹 Fn A ∧ 𝐺 Fn A) ∧ B ⊆ A) → ((𝐹 ↾ B) = (𝐺 ↾ B) ↔ ∀x ∈ B (𝐹‘x) = (𝐺‘x)))
Theorem	fndmdif 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)})
Theorem	fndmdifcom 5216	The difference set between two functions is commutative. (Contributed by Stefan O'Rear, 17-Jan-2015.)
⊢ ((𝐹 Fn A ∧ 𝐺 Fn A) → dom (𝐹 ∖ 𝐺) = dom (𝐺 ∖ 𝐹))
Theorem	fndmin 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)})
Theorem	fneqeql 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))
Theorem	fneqeql2 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 (𝐹 ∩ 𝐺)))
Theorem	fnreseql 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 (𝐹 ∩ 𝐺)))
Theorem	chfnrn 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)
Theorem	funfvop 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)⟩ ∈ 𝐹)
Theorem	funfvbrb 5223	Two ways to say that A is in the domain of 𝐹. (Contributed by Mario Carneiro, 1-May-2014.)
⊢ (Fun 𝐹 → (A ∈ dom 𝐹 ↔ A𝐹(𝐹‘A)))
Theorem	fvimacnvi 5224	A member of a preimage is a function value argument. (Contributed by NM, 4-May-2007.)
⊢ ((Fun 𝐹 ∧ A ∈ (◡𝐹 “ B)) → (𝐹‘A) ∈ B)
Theorem	fvimacnv 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) ∈ B ↔ A ∈ (◡𝐹 “ B)))
Theorem	funimass3 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) ⊆ B ↔ A ⊆ (◡𝐹 “ B)))
Theorem	funimass5 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))
Theorem	funconstss 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) = B ↔ A ⊆ (◡𝐹 “ {B})))
Theorem	elpreima 5229	Membership in the preimage of a set under a function. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (𝐹 Fn A → (B ∈ (◡𝐹 “ 𝐶) ↔ (B ∈ A ∧ (𝐹‘B) ∈ 𝐶)))
Theorem	fniniseg 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)))
Theorem	fncnvima2 5231*	Inverse images under functions expressed as abstractions. (Contributed by Stefan O'Rear, 1-Feb-2015.)
⊢ (𝐹 Fn A → (◡𝐹 “ B) = {x ∈ A ∣ (𝐹‘x) ∈ B})
Theorem	fniniseg2 5232*	Inverse point images under functions expressed as abstractions. (Contributed by Stefan O'Rear, 1-Feb-2015.)
⊢ (𝐹 Fn A → (◡𝐹 “ {B}) = {x ∈ A ∣ (𝐹‘x) = B})
Theorem	fnniniseg2 5233*	Support sets of functions expressed as abstractions. (Contributed by Stefan O'Rear, 1-Feb-2015.)
⊢ (𝐹 Fn A → (◡𝐹 “ (V ∖ {B})) = {x ∈ A ∣ (𝐹‘x) ≠ B})
Theorem	rexsupp 5234*	Existential quantification restricted to a support. (Contributed by Stefan O'Rear, 23-Mar-2015.)
⊢ (𝐹 Fn A → (∃x ∈ (◡𝐹 “ (V ∖ {𝑍}))φ ↔ ∃x ∈ A ((𝐹‘x) ≠ 𝑍 ∧ φ)))
Theorem	unpreima 5235	Preimage of a union. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (Fun 𝐹 → (◡𝐹 “ (A ∪ B)) = ((◡𝐹 “ A) ∪ (◡𝐹 “ B)))
Theorem	inpreima 5236	Preimage of an intersection. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 14-Jun-2016.)
⊢ (Fun 𝐹 → (◡𝐹 “ (A ∩ B)) = ((◡𝐹 “ A) ∩ (◡𝐹 “ B)))
Theorem	difpreima 5237	Preimage of a difference. (Contributed by Mario Carneiro, 14-Jun-2016.)
⊢ (Fun 𝐹 → (◡𝐹 “ (A ∖ B)) = ((◡𝐹 “ A) ∖ (◡𝐹 “ B)))
Theorem	respreima 5238	The preimage of a restricted function. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (Fun 𝐹 → (◡(𝐹 ↾ B) “ A) = ((◡𝐹 “ A) ∩ B))
Theorem	fimacnv 5239	The preimage of the codomain of a mapping is the mapping's domain. (Contributed by FL, 25-Jan-2007.)
⊢ (𝐹:A⟶B → (◡𝐹 “ B) = A)
Theorem	fnopfv 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)⟩ ∈ 𝐹)
Theorem	fvelrn 5241	A function's value belongs to its range. (Contributed by NM, 14-Oct-1996.)
⊢ ((Fun 𝐹 ∧ A ∈ dom 𝐹) → (𝐹‘A) ∈ ran 𝐹)
Theorem	fnfvelrn 5242	A function's value belongs to its range. (Contributed by NM, 15-Oct-1996.)
⊢ ((𝐹 Fn A ∧ B ∈ A) → (𝐹‘B) ∈ ran 𝐹)
Theorem	ffvelrn 5243	A function's value belongs to its codomain. (Contributed by NM, 12-Aug-1999.)
⊢ ((𝐹:A⟶B ∧ 𝐶 ∈ A) → (𝐹‘𝐶) ∈ B)
Theorem	ffvelrni 5244	A function's value belongs to its codomain. (Contributed by NM, 6-Apr-2005.)
⊢ 𝐹:A⟶B    ⇒   ⊢ (𝐶 ∈ A → (𝐹‘𝐶) ∈ B)
Theorem	ffvelrnda 5245	A function's value belongs to its codomain. (Contributed by Mario Carneiro, 29-Dec-2016.)
⊢ (φ → 𝐹:A⟶B)    ⇒   ⊢ ((φ ∧ 𝐶 ∈ A) → (𝐹‘𝐶) ∈ B)
Theorem	ffvelrnd 5246	A function's value belongs to its codomain. (Contributed by Mario Carneiro, 29-Dec-2016.)
⊢ (φ → 𝐹:A⟶B)    &   ⊢ (φ → 𝐶 ∈ A)    ⇒   ⊢ (φ → (𝐹‘𝐶) ∈ B)
Theorem	rexrn 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 ψ))
Theorem	ralrn 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 ψ))
Theorem	elrnrexdm 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)))
Theorem	elrnrexdmb 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)))
Theorem	eldmrexrn 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 = (𝐹‘𝑌)))
Theorem	ralrnmpt 5252*	A restricted quantifier over an image set. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ 𝐹 = (x ∈ A ↦ B)    &   ⊢ (y = B → (ψ ↔ χ))    ⇒   ⊢ (∀x ∈ A B ∈ 𝑉 → (∀y ∈ ran 𝐹ψ ↔ ∀x ∈ A χ))
Theorem	rexrnmpt 5253*	A restricted quantifier over an image set. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ 𝐹 = (x ∈ A ↦ B)    &   ⊢ (y = B → (ψ ↔ χ))    ⇒   ⊢ (∀x ∈ A B ∈ 𝑉 → (∃y ∈ ran 𝐹ψ ↔ ∃x ∈ A χ))
Theorem	dff2 5254	Alternate definition of a mapping. (Contributed by NM, 14-Nov-2007.)
⊢ (𝐹:A⟶B ↔ (𝐹 Fn A ∧ 𝐹 ⊆ (A × B)))
Theorem	dff3im 5255*	Property of a mapping. (Contributed by Jim Kingdon, 4-Jan-2019.)
⊢ (𝐹:A⟶B → (𝐹 ⊆ (A × B) ∧ ∀x ∈ A ∃!y x𝐹y))
Theorem	dff4im 5256*	Property of a mapping. (Contributed by Jim Kingdon, 4-Jan-2019.)
⊢ (𝐹:A⟶B → (𝐹 ⊆ (A × B) ∧ ∀x ∈ A ∃!y ∈ B x𝐹y))
Theorem	dffo3 5257*	An onto mapping expressed in terms of function values. (Contributed by NM, 29-Oct-2006.)
⊢ (𝐹:A–onto→B ↔ (𝐹:A⟶B ∧ ∀y ∈ B ∃x ∈ A y = (𝐹‘x)))
Theorem	dffo4 5258*	Alternate definition of an onto mapping. (Contributed by NM, 20-Mar-2007.)
⊢ (𝐹:A–onto→B ↔ (𝐹:A⟶B ∧ ∀y ∈ B ∃x ∈ A x𝐹y))
Theorem	dffo5 5259*	Alternate definition of an onto mapping. (Contributed by NM, 20-Mar-2007.)
⊢ (𝐹:A–onto→B ↔ (𝐹:A⟶B ∧ ∀y ∈ B ∃x x𝐹y))
Theorem	foelrn 5260*	Property of a surjective function. (Contributed by Jeff Madsen, 4-Jan-2011.)
⊢ ((𝐹:A–onto→B ∧ 𝐶 ∈ B) → ∃x ∈ A 𝐶 = (𝐹‘x))
Theorem	foco2 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⟶𝐶 ∧ 𝐺:A⟶B ∧ (𝐹 ∘ 𝐺):A–onto→𝐶) → 𝐹:B–onto→𝐶)
Theorem	fmpt 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 ↔ 𝐹:A⟶B)
Theorem	f1ompt 5263*	Express bijection for a mapping operation. (Contributed by Mario Carneiro, 30-May-2015.) (Revised by Mario Carneiro, 4-Dec-2016.)
⊢ 𝐹 = (x ∈ A ↦ 𝐶)    ⇒   ⊢ (𝐹:A–1-1-onto→B ↔ (∀x ∈ A 𝐶 ∈ B ∧ ∀y ∈ B ∃!x ∈ A y = 𝐶))
Theorem	fmpti 5264*	Functionality of the mapping operation. (Contributed by NM, 19-Mar-2005.) (Revised by Mario Carneiro, 1-Sep-2015.)
⊢ 𝐹 = (x ∈ A ↦ 𝐶)    &   ⊢ (x ∈ A → 𝐶 ∈ B)    ⇒   ⊢ 𝐹:A⟶B
Theorem	fmptd 5265*	Domain and codomain of the mapping operation; deduction form. (Contributed by Mario Carneiro, 13-Jan-2013.)
⊢ ((φ ∧ x ∈ A) → B ∈ 𝐶)    &   ⊢ 𝐹 = (x ∈ A ↦ B)    ⇒   ⊢ (φ → 𝐹:A⟶𝐶)
Theorem	ffnfv 5266*	A function maps to a class to which all values belong. (Contributed by NM, 3-Dec-2003.)
⊢ (𝐹:A⟶B ↔ (𝐹 Fn A ∧ ∀x ∈ A (𝐹‘x) ∈ B))
Theorem	ffnfvf 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𝐹    ⇒   ⊢ (𝐹:A⟶B ↔ (𝐹 Fn A ∧ ∀x ∈ A (𝐹‘x) ∈ B))
Theorem	fnfvrnss 5268*	An upper bound for range determined by function values. (Contributed by NM, 8-Oct-2004.)
⊢ ((𝐹 Fn A ∧ ∀x ∈ A (𝐹‘x) ∈ B) → ran 𝐹 ⊆ B)
Theorem	rnmptss 5269*	The range of an operation given by the "maps to" notation as a subset. (Contributed by Thierry Arnoux, 24-Sep-2017.)
⊢ 𝐹 = (x ∈ A ↦ B)    ⇒   ⊢ (∀x ∈ A B ∈ 𝐶 → ran 𝐹 ⊆ 𝐶)
Theorem	fmpt2d 5270*	Domain and codomain of the mapping operation; deduction form. (Contributed by NM, 27-Dec-2014.)
⊢ ((φ ∧ x ∈ A) → B ∈ 𝑉)    &   ⊢ (φ → 𝐹 = (x ∈ A ↦ B))    &   ⊢ ((φ ∧ y ∈ A) → (𝐹‘y) ∈ 𝐶)    ⇒   ⊢ (φ → 𝐹:A⟶𝐶)
Theorem	ffvresb 5271*	A necessary and sufficient condition for a restricted function. (Contributed by Mario Carneiro, 14-Nov-2013.)
⊢ (Fun 𝐹 → ((𝐹 ↾ A):A⟶B ↔ ∀x ∈ A (x ∈ dom 𝐹 ∧ (𝐹‘x) ∈ B)))
Theorem	f1oresrab 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 ↦ 𝐶)    &   ⊢ (φ → 𝐹:A–1-1-onto→B)    &   ⊢ ((φ ∧ x ∈ A ∧ y = 𝐶) → (χ ↔ ψ))    ⇒   ⊢ (φ → (𝐹 ↾ {x ∈ A ∣ ψ}):{x ∈ A ∣ ψ}–1-1-onto→{y ∈ B ∣ χ})
Theorem	fmptco 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 ↦ 𝑇))
Theorem	fmptcof 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 ↦ 𝑇))
Theorem	fmptcos 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⦌𝑆))
Theorem	fcompt 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:𝐶⟶𝐷) → (A ∘ B) = (x ∈ 𝐶 ↦ (A‘(B‘x))))
Theorem	fcoconst 5277	Composition with a constant function. (Contributed by Stefan O'Rear, 11-Mar-2015.)
⊢ ((𝐹 Fn 𝑋 ∧ 𝑌 ∈ 𝑋) → (𝐹 ∘ (𝐼 × {𝑌})) = (𝐼 × {(𝐹‘𝑌)}))
Theorem	fsn 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⟩})
Theorem	fsng 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⟩}))
Theorem	fsn2 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)⟩}))
Theorem	xpsng 5281	The cross product of two singletons. (Contributed by Mario Carneiro, 30-Apr-2015.)
⊢ ((A ∈ 𝑉 ∧ B ∈ 𝑊) → ({A} × {B}) = {⟨A, B⟩})
Theorem	xpsn 5282	The cross product of two singletons. (Contributed by NM, 4-Nov-2006.)
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ ({A} × {B}) = {⟨A, B⟩}
Theorem	dfmpt 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 ∈ A ↦ B) = ∪ x ∈ A {⟨x, B⟩}
Theorem	fnasrn 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 ∈ A ↦ B) = ran (x ∈ A ↦ ⟨x, B⟩)
Theorem	dfmptg 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 ∈ A ↦ B) = ∪ x ∈ A {⟨x, B⟩})
Theorem	fnasrng 5286	A function expressed as the range of another function. (Contributed by Jim Kingdon, 9-Jan-2019.)
⊢ (∀x ∈ A B ∈ 𝑉 → (x ∈ A ↦ B) = ran (x ∈ A ↦ ⟨x, B⟩))
Theorem	ressnop0 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⟩} ↾ 𝐶) = ∅)
Theorem	fpr 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    ⇒   ⊢ (A ≠ B → {⟨A, 𝐶⟩, ⟨B, 𝐷⟩}:{A, B}⟶{𝐶, 𝐷})
Theorem	fprg 5289	A function with a domain of two elements. (Contributed by FL, 2-Feb-2014.)
⊢ (((A ∈ 𝐸 ∧ B ∈ 𝐹) ∧ (𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐻) ∧ A ≠ B) → {⟨A, 𝐶⟩, ⟨B, 𝐷⟩}:{A, B}⟶{𝐶, 𝐷})
Theorem	ftpg 5290	A function with a domain of three elements. (Contributed by Alexander van der Vekens, 4-Dec-2017.)
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (A ∈ 𝐹 ∧ B ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → {⟨𝑋, A⟩, ⟨𝑌, B⟩, ⟨𝑍, 𝐶⟩}:{𝑋, 𝑌, 𝑍}⟶{A, B, 𝐶})
Theorem	ftp 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    &   ⊢ A ≠ B    &   ⊢ A ≠ 𝐶    &   ⊢ B ≠ 𝐶    ⇒   ⊢ {⟨A, 𝑋⟩, ⟨B, 𝑌⟩, ⟨𝐶, 𝑍⟩}:{A, B, 𝐶}⟶{𝑋, 𝑌, 𝑍}
Theorem	fnressn 5292	A function restricted to a singleton. (Contributed by NM, 9-Oct-2004.)
⊢ ((𝐹 Fn A ∧ B ∈ A) → (𝐹 ↾ {B}) = {⟨B, (𝐹‘B)⟩})
Theorem	fressnfv 5293	The value of a function restricted to a singleton. (Contributed by NM, 9-Oct-2004.)
⊢ ((𝐹 Fn A ∧ B ∈ A) → ((𝐹 ↾ {B}):{B}⟶𝐶 ↔ (𝐹‘B) ∈ 𝐶))
Theorem	fvconst 5294	The value of a constant function. (Contributed by NM, 30-May-1999.)
⊢ ((𝐹:A⟶{B} ∧ 𝐶 ∈ A) → (𝐹‘𝐶) = B)
Theorem	fmptsn 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))
Theorem	fmptap 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 ∈ 𝑆 ↦ 𝐶)
Theorem	fmptapd 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 ∈ 𝑆 ↦ 𝐶))
Theorem	fmptpr 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} ↦ 𝐸))
Theorem	fvresi 5299	The value of a restricted identity function. (Contributed by NM, 19-May-2004.)
⊢ (B ∈ A → (( I ↾ A)‘B) = B)
Theorem	fvunsng 5300	Remove an ordered pair not participating in a function value. (Contributed by Jim Kingdon, 7-Jan-2019.)
⊢ ((𝐷 ∈ 𝑉 ∧ B ≠ 𝐷) → ((A ∪ {⟨B, 𝐶⟩})‘𝐷) = (A‘𝐷))