P. 71 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 7001-7100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	fvmptd2f 7001*	Alternate deduction version of fvmpt 6985, suitable for iteration. (Contributed by Mario Carneiro, 7-Jan-2017.) (Proof shortened by AV, 19-Jan-2022.)
⊢ (𝜑 → 𝐴 ∈ 𝐷)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → ((𝐹‘𝐴) = 𝐵 → 𝜓))    &   ⊢ Ⅎ𝑥𝐹    &   ⊢ Ⅎ𝑥𝜓    ⇒   ⊢ (𝜑 → (𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵) → 𝜓))
Theorem	fvmptdv 7002*	Alternate deduction version of fvmpt 6985, suitable for iteration. (Contributed by Mario Carneiro, 7-Jan-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝐷)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → ((𝐹‘𝐴) = 𝐵 → 𝜓))    ⇒   ⊢ (𝜑 → (𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵) → 𝜓))
Theorem	fvmptdv2 7003*	Alternate deduction version of fvmpt 6985, suitable for iteration. (Contributed by Mario Carneiro, 7-Jan-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝐷)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → (𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵) → (𝐹‘𝐴) = 𝐶))
Theorem	mpteqb 7004*	Bidirectional equality theorem for a mapping abstraction. Equivalent to eqfnfv 7019. (Contributed by Mario Carneiro, 14-Nov-2014.)
⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ((𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶) ↔ ∀𝑥 ∈ 𝐴 𝐵 = 𝐶))
Theorem	fvmptt 7005*	Closed theorem form of fvmpt 6985. (Contributed by Scott Fenton, 21-Feb-2013.) (Revised by Mario Carneiro, 11-Sep-2015.)
⊢ ((∀𝑥(𝑥 = 𝐴 → 𝐵 = 𝐶) ∧ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵) ∧ (𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑉)) → (𝐹‘𝐴) = 𝐶)
Theorem	fvmptf 7006*	Value of a function given by an ordered-pair class abstraction. This version of fvmptg 6983 uses bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 8-Nov-2005.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐶    &   ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵)    ⇒   ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑉) → (𝐹‘𝐴) = 𝐶)
Theorem	fvmptnf 7007*	The value of a function given by an ordered-pair class abstraction is the empty set when the class it would otherwise map to is a proper class. This version of fvmptn 7009 uses bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 21-Oct-2003.) (Revised by Mario Carneiro, 11-Sep-2015.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐶    &   ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵)    ⇒   ⊢ (¬ 𝐶 ∈ V → (𝐹‘𝐴) = ∅)
Theorem	fvmptd3 7008*	Deduction version of fvmpt 6985. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵)    &   ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐹‘𝐴) = 𝐶)
Theorem	fvmptn 7009*	This somewhat non-intuitive theorem tells us the value of its function is the empty set when the class 𝐶 it would otherwise map to is a proper class. This is a technical lemma that can help eliminate redundant sethood antecedents otherwise required by fvmptg 6983. (Contributed by NM, 21-Oct-2003.) (Revised by Mario Carneiro, 9-Sep-2013.)
⊢ (𝑥 = 𝐷 → 𝐵 = 𝐶)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    ⇒   ⊢ (¬ 𝐶 ∈ V → (𝐹‘𝐷) = ∅)
Theorem	fvmptss2 7010*	A mapping always evaluates to a subset of the substituted expression in the mapping, even if this is a proper class, or we are out of the domain. (Contributed by Mario Carneiro, 13-Feb-2015.)
⊢ (𝑥 = 𝐷 → 𝐵 = 𝐶)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    ⇒   ⊢ (𝐹‘𝐷) ⊆ 𝐶
Theorem	elfvmptrab1w 7011*	Implications for the value of a function defined by the maps-to notation with a class abstraction as a result having an element. Here, the base set of the class abstraction depends on the argument of the function. Version of elfvmptrab1 7012 with a disjoint variable condition, which does not require ax-13 2371. (Contributed by Alexander van der Vekens, 15-Jul-2018.) Avoid ax-13 2371. (Revised by Gino Giotto, 26-Jan-2024.)
⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ {𝑦 ∈ ⦋𝑥 / 𝑚⦌𝑀 ∣ 𝜑})    &   ⊢ (𝑋 ∈ 𝑉 → ⦋𝑋 / 𝑚⦌𝑀 ∈ V)    ⇒   ⊢ (𝑌 ∈ (𝐹‘𝑋) → (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ ⦋𝑋 / 𝑚⦌𝑀))
Theorem	elfvmptrab1 7012*	Implications for the value of a function defined by the maps-to notation with a class abstraction as a result having an element. Here, the base set of the class abstraction depends on the argument of the function. Usage of this theorem is discouraged because it depends on ax-13 2371. Use the weaker elfvmptrab1w 7011 when possible. (Contributed by Alexander van der Vekens, 15-Jul-2018.) (New usage is discouraged.)
⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ {𝑦 ∈ ⦋𝑥 / 𝑚⦌𝑀 ∣ 𝜑})    &   ⊢ (𝑋 ∈ 𝑉 → ⦋𝑋 / 𝑚⦌𝑀 ∈ V)    ⇒   ⊢ (𝑌 ∈ (𝐹‘𝑋) → (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ ⦋𝑋 / 𝑚⦌𝑀))
Theorem	elfvmptrab 7013*	Implications for the value of a function defined by the maps-to notation with a class abstraction as a result having an element. (Contributed by Alexander van der Vekens, 15-Jul-2018.)
⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ {𝑦 ∈ 𝑀 ∣ 𝜑})    &   ⊢ (𝑋 ∈ 𝑉 → 𝑀 ∈ V)    ⇒   ⊢ (𝑌 ∈ (𝐹‘𝑋) → (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑀))
Theorem	fvopab4ndm 7014*	Value of a function given by an ordered-pair class abstraction, outside of its domain. (Contributed by NM, 28-Mar-2008.)
⊢ 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}    ⇒   ⊢ (¬ 𝐵 ∈ 𝐴 → (𝐹‘𝐵) = ∅)
Theorem	fvmptndm 7015*	Value of a function given by the maps-to notation, outside of its domain. (Contributed by AV, 31-Dec-2020.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    ⇒   ⊢ (¬ 𝑋 ∈ 𝐴 → (𝐹‘𝑋) = ∅)
Theorem	fvmptrabfv 7016*	Value of a function mapping a set to a class abstraction restricting the value of another function. (Contributed by AV, 18-Feb-2022.)
⊢ 𝐹 = (𝑥 ∈ V ↦ {𝑦 ∈ (𝐺‘𝑥) ∣ 𝜑})    &   ⊢ (𝑥 = 𝑋 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐹‘𝑋) = {𝑦 ∈ (𝐺‘𝑋) ∣ 𝜓}
Theorem	fvopab5 7017*	The value of a function that is expressed as an ordered pair abstraction. (Contributed by NM, 19-Feb-2006.) (Revised by Mario Carneiro, 11-Sep-2015.)
⊢ 𝐹 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ 𝑉 → (𝐹‘𝐴) = (℩𝑦𝜓))
Theorem	fvopab6 7018*	Value of a function given by ordered-pair class abstraction. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 11-Sep-2015.)
⊢ 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝜑 ∧ 𝑦 = 𝐵)}    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)    ⇒   ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑅 ∧ 𝜓) → (𝐹‘𝐴) = 𝐶)
Theorem	eqfnfv 7019*	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 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥)))
Theorem	eqfnfv2 7020*	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 𝐴 ∧ 𝐺 Fn 𝐵) → (𝐹 = 𝐺 ↔ (𝐴 = 𝐵 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥))))
Theorem	eqfnfv3 7021*	Derive equality of functions from equality of their values. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) → (𝐹 = 𝐺 ↔ (𝐵 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝐵 ∧ (𝐹‘𝑥) = (𝐺‘𝑥)))))
Theorem	eqfnfvd 7022*	Deduction for equality of functions. (Contributed by Mario Carneiro, 24-Jul-2014.)
⊢ (𝜑 → 𝐹 Fn 𝐴)    &   ⊢ (𝜑 → 𝐺 Fn 𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = (𝐺‘𝑥))    ⇒   ⊢ (𝜑 → 𝐹 = 𝐺)
Theorem	eqfnfv2f 7023*	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 7019 uses bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 29-Jan-2004.)
⊢ Ⅎ𝑥𝐹    &   ⊢ Ⅎ𝑥𝐺    ⇒   ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥)))
Theorem	eqfunfv 7024*	Equality of functions is determined by their values. (Contributed by Scott Fenton, 19-Jun-2011.)
⊢ ((Fun 𝐹 ∧ Fun 𝐺) → (𝐹 = 𝐺 ↔ (dom 𝐹 = dom 𝐺 ∧ ∀𝑥 ∈ dom 𝐹(𝐹‘𝑥) = (𝐺‘𝑥))))
Theorem	fvreseq0 7025*	Equality of restricted functions is determined by their values (for functions with different domains). (Contributed by AV, 6-Jan-2019.)
⊢ (((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐶) ∧ (𝐵 ⊆ 𝐴 ∧ 𝐵 ⊆ 𝐶)) → ((𝐹 ↾ 𝐵) = (𝐺 ↾ 𝐵) ↔ ∀𝑥 ∈ 𝐵 (𝐹‘𝑥) = (𝐺‘𝑥)))
Theorem	fvreseq1 7026*	Equality of a function restricted to the domain of another function. (Contributed by AV, 6-Jan-2019.)
⊢ (((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) ∧ 𝐵 ⊆ 𝐴) → ((𝐹 ↾ 𝐵) = 𝐺 ↔ ∀𝑥 ∈ 𝐵 (𝐹‘𝑥) = (𝐺‘𝑥)))
Theorem	fvreseq 7027*	Equality of restricted functions is determined by their values. (Contributed by NM, 3-Aug-1994.) (Proof shortened by AV, 4-Mar-2019.)
⊢ (((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) ∧ 𝐵 ⊆ 𝐴) → ((𝐹 ↾ 𝐵) = (𝐺 ↾ 𝐵) ↔ ∀𝑥 ∈ 𝐵 (𝐹‘𝑥) = (𝐺‘𝑥)))
Theorem	fnmptfvd 7028*	A function with a given domain is a mapping defined by its function values. (Contributed by AV, 1-Mar-2019.)
⊢ (𝜑 → 𝑀 Fn 𝐴)    &   ⊢ (𝑖 = 𝑎 → 𝐷 = 𝐶)    &   ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → 𝐷 ∈ 𝑈)    &   ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → 𝐶 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑀 = (𝑎 ∈ 𝐴 ↦ 𝐶) ↔ ∀𝑖 ∈ 𝐴 (𝑀‘𝑖) = 𝐷))
Theorem	fndmdif 7029*	Two ways to express the locus of differences between two functions. (Contributed by Stefan O'Rear, 17-Jan-2015.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → dom (𝐹 ∖ 𝐺) = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) ≠ (𝐺‘𝑥)})
Theorem	fndmdifcom 7030	The difference set between two functions is commutative. (Contributed by Stefan O'Rear, 17-Jan-2015.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → dom (𝐹 ∖ 𝐺) = dom (𝐺 ∖ 𝐹))
Theorem	fndmdifeq0 7031	The difference set of two functions is empty if and only if the functions are equal. (Contributed by Stefan O'Rear, 17-Jan-2015.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (dom (𝐹 ∖ 𝐺) = ∅ ↔ 𝐹 = 𝐺))
Theorem	fndmin 7032*	Two ways to express the locus of equality between two functions. (Contributed by Stefan O'Rear, 17-Jan-2015.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → dom (𝐹 ∩ 𝐺) = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) = (𝐺‘𝑥)})
Theorem	fneqeql 7033	Two functions are equal iff their equalizer is the whole domain. (Contributed by Stefan O'Rear, 7-Mar-2015.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ dom (𝐹 ∩ 𝐺) = 𝐴))
Theorem	fneqeql2 7034	Two functions are equal iff their equalizer contains the whole domain. (Contributed by Stefan O'Rear, 9-Mar-2015.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ 𝐴 ⊆ dom (𝐹 ∩ 𝐺)))
Theorem	fnreseql 7035	Two functions are equal on a subset iff their equalizer contains that subset. (Contributed by Stefan O'Rear, 7-Mar-2015.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ∧ 𝑋 ⊆ 𝐴) → ((𝐹 ↾ 𝑋) = (𝐺 ↾ 𝑋) ↔ 𝑋 ⊆ dom (𝐹 ∩ 𝐺)))
Theorem	chfnrn 7036*	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 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝑥) → ran 𝐹 ⊆ ∪ 𝐴)
Theorem	funfvop 7037	Ordered pair with function value. Part of Theorem 4.3(i) of [Monk1] p. 41. (Contributed by NM, 14-Oct-1996.)
⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → ⟨𝐴, (𝐹‘𝐴)⟩ ∈ 𝐹)
Theorem	funfvbrb 7038	Two ways to say that 𝐴 is in the domain of 𝐹. (Contributed by Mario Carneiro, 1-May-2014.)
⊢ (Fun 𝐹 → (𝐴 ∈ dom 𝐹 ↔ 𝐴𝐹(𝐹‘𝐴)))
Theorem	fvimacnvi 7039	A member of a preimage is a function value argument. (Contributed by NM, 4-May-2007.)
⊢ ((Fun 𝐹 ∧ 𝐴 ∈ (◡𝐹 “ 𝐵)) → (𝐹‘𝐴) ∈ 𝐵)
Theorem	fvimacnv 7040	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 6621 could probably be strengthened to a biconditional." (Contributed by Raph Levien, 20-Nov-2006.)
⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → ((𝐹‘𝐴) ∈ 𝐵 ↔ 𝐴 ∈ (◡𝐹 “ 𝐵)))
Theorem	funimass3 7041	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 7040 would be the special case of 𝐴 being a singleton, but it works this way round too." (Contributed by Raph Levien, 20-Nov-2006.)
⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹) → ((𝐹 “ 𝐴) ⊆ 𝐵 ↔ 𝐴 ⊆ (◡𝐹 “ 𝐵)))
Theorem	funimass5 7042*	A subclass of a preimage in terms of function values. (Contributed by NM, 15-May-2007.)
⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹) → (𝐴 ⊆ (◡𝐹 “ 𝐵) ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))
Theorem	funconstss 7043*	Two ways of specifying that a function is constant on a subdomain. (Contributed by NM, 8-Mar-2007.)
⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹) → (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵 ↔ 𝐴 ⊆ (◡𝐹 “ {𝐵})))
Theorem	fvimacnvALT 7044	Alternate proof of fvimacnv 7040, based on funimass3 7041. If funimass3 7041 is ever proved directly, as opposed to using funimacnv 6619 pointwise, then the proof of funimacnv 6619 should be replaced with this one. (Contributed by Raph Levien, 20-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → ((𝐹‘𝐴) ∈ 𝐵 ↔ 𝐴 ∈ (◡𝐹 “ 𝐵)))
Theorem	elpreima 7045	Membership in the preimage of a set under a function. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) ↔ (𝐵 ∈ 𝐴 ∧ (𝐹‘𝐵) ∈ 𝐶)))
Theorem	elpreimad 7046	Membership in the preimage of a set under a function. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝜑 → 𝐹 Fn 𝐴)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐴)    &   ⊢ (𝜑 → (𝐹‘𝐵) ∈ 𝐶)    ⇒   ⊢ (𝜑 → 𝐵 ∈ (◡𝐹 “ 𝐶))
Theorem	fniniseg 7047	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 𝐴 → (𝐶 ∈ (◡𝐹 “ {𝐵}) ↔ (𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) = 𝐵)))
Theorem	fncnvima2 7048*	Inverse images under functions expressed as abstractions. (Contributed by Stefan O'Rear, 1-Feb-2015.)
⊢ (𝐹 Fn 𝐴 → (◡𝐹 “ 𝐵) = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) ∈ 𝐵})
Theorem	fniniseg2 7049*	Inverse point images under functions expressed as abstractions. (Contributed by Stefan O'Rear, 1-Feb-2015.)
⊢ (𝐹 Fn 𝐴 → (◡𝐹 “ {𝐵}) = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) = 𝐵})
Theorem	unpreima 7050	Preimage of a union. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (Fun 𝐹 → (◡𝐹 “ (𝐴 ∪ 𝐵)) = ((◡𝐹 “ 𝐴) ∪ (◡𝐹 “ 𝐵)))
Theorem	inpreima 7051	Preimage of an intersection. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 14-Jun-2016.)
⊢ (Fun 𝐹 → (◡𝐹 “ (𝐴 ∩ 𝐵)) = ((◡𝐹 “ 𝐴) ∩ (◡𝐹 “ 𝐵)))
Theorem	difpreima 7052	Preimage of a difference. (Contributed by Mario Carneiro, 14-Jun-2016.)
⊢ (Fun 𝐹 → (◡𝐹 “ (𝐴 ∖ 𝐵)) = ((◡𝐹 “ 𝐴) ∖ (◡𝐹 “ 𝐵)))
Theorem	respreima 7053	The preimage of a restricted function. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (Fun 𝐹 → (◡(𝐹 ↾ 𝐵) “ 𝐴) = ((◡𝐹 “ 𝐴) ∩ 𝐵))
Theorem	cnvimainrn 7054	The preimage of the intersection of the range of a class and a class 𝐴 is the preimage of the class 𝐴. (Contributed by AV, 17-Sep-2024.)
⊢ (Fun 𝐹 → (◡𝐹 “ (ran 𝐹 ∩ 𝐴)) = (◡𝐹 “ 𝐴))
Theorem	sspreima 7055	The preimage of a subset is a subset of the preimage. (Contributed by Brendan Leahy, 23-Sep-2017.)
⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ 𝐵) → (◡𝐹 “ 𝐴) ⊆ (◡𝐹 “ 𝐵))
Theorem	iinpreima 7056*	Preimage of an intersection. (Contributed by FL, 16-Apr-2012.)
⊢ ((Fun 𝐹 ∧ 𝐴 ≠ ∅) → (◡𝐹 “ ∩ 𝑥 ∈ 𝐴 𝐵) = ∩ 𝑥 ∈ 𝐴 (◡𝐹 “ 𝐵))
Theorem	intpreima 7057*	Preimage of an intersection. (Contributed by FL, 28-Apr-2012.)
⊢ ((Fun 𝐹 ∧ 𝐴 ≠ ∅) → (◡𝐹 “ ∩ 𝐴) = ∩ 𝑥 ∈ 𝐴 (◡𝐹 “ 𝑥))
Theorem	fimacnvOLD 7058	Obsolete version of fimacnv 6727 as of 20-Sep-2024. (Contributed by FL, 25-Jan-2007.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (𝐹:𝐴⟶𝐵 → (◡𝐹 “ 𝐵) = 𝐴)
Theorem	fimacnvinrn 7059	Taking the converse image of a set can be limited to the range of the function used. (Contributed by Thierry Arnoux, 21-Jan-2017.)
⊢ (Fun 𝐹 → (◡𝐹 “ 𝐴) = (◡𝐹 “ (𝐴 ∩ ran 𝐹)))
Theorem	fimacnvinrn2 7060	Taking the converse image of a set can be limited to the range of the function used. (Contributed by Thierry Arnoux, 17-Feb-2017.)
⊢ ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝐵) → (◡𝐹 “ 𝐴) = (◡𝐹 “ (𝐴 ∩ 𝐵)))
Theorem	rescnvimafod 7061	The restriction of a function to a preimage of a class is a function onto the intersection of this class and the range of the function. (Contributed by AV, 13-Sep-2024.) (Revised by AV, 29-Sep-2024.)
⊢ (𝜑 → 𝐹 Fn 𝐴)    &   ⊢ (𝜑 → 𝐸 = (ran 𝐹 ∩ 𝐵))    &   ⊢ (𝜑 → 𝐷 = (◡𝐹 “ 𝐵))    ⇒   ⊢ (𝜑 → (𝐹 ↾ 𝐷):𝐷–onto→𝐸)
Theorem	fvn0ssdmfun 7062*	If a class' function values for certain arguments is not the empty set, the arguments are contained in the domain of the class, and the class restricted to the arguments is a function, analogous to fvfundmfvn0 6922. (Contributed by AV, 27-Jan-2020.) (Proof shortened by Peter Mazsa, 2-Oct-2022.)
⊢ (∀𝑎 ∈ 𝐷 (𝐹‘𝑎) ≠ ∅ → (𝐷 ⊆ dom 𝐹 ∧ Fun (𝐹 ↾ 𝐷)))
Theorem	fnopfv 7063	Ordered pair with function value. Part of Theorem 4.3(i) of [Monk1] p. 41. (Contributed by NM, 30-Sep-2004.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ⟨𝐵, (𝐹‘𝐵)⟩ ∈ 𝐹)
Theorem	fvelrn 7064	A function's value belongs to its range. (Contributed by NM, 14-Oct-1996.)
⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → (𝐹‘𝐴) ∈ ran 𝐹)
Theorem	nelrnfvne 7065	A function value cannot be any element not contained in the range of the function. (Contributed by AV, 28-Jan-2020.)
⊢ ((Fun 𝐹 ∧ 𝑋 ∈ dom 𝐹 ∧ 𝑌 ∉ ran 𝐹) → (𝐹‘𝑋) ≠ 𝑌)
Theorem	fveqdmss 7066*	If the empty set is not contained in the range of a function, and the function values of another class (not necessarily a function) are equal to the function values of the function for all elements of the domain of the function, then the domain of the function is contained in the domain of the class. (Contributed by AV, 28-Jan-2020.)
⊢ 𝐷 = dom 𝐵    ⇒   ⊢ ((Fun 𝐵 ∧ ∅ ∉ ran 𝐵 ∧ ∀𝑥 ∈ 𝐷 (𝐴‘𝑥) = (𝐵‘𝑥)) → 𝐷 ⊆ dom 𝐴)
Theorem	fveqressseq 7067*	If the empty set is not contained in the range of a function, and the function values of another class (not necessarily a function) are equal to the function values of the function for all elements of the domain of the function, then the class restricted to the domain of the function is the function itself. (Contributed by AV, 28-Jan-2020.)
⊢ 𝐷 = dom 𝐵    ⇒   ⊢ ((Fun 𝐵 ∧ ∅ ∉ ran 𝐵 ∧ ∀𝑥 ∈ 𝐷 (𝐴‘𝑥) = (𝐵‘𝑥)) → (𝐴 ↾ 𝐷) = 𝐵)
Theorem	fnfvelrn 7068	A function's value belongs to its range. (Contributed by NM, 15-Oct-1996.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → (𝐹‘𝐵) ∈ ran 𝐹)
Theorem	ffvelcdm 7069	A function's value belongs to its codomain. (Contributed by NM, 12-Aug-1999.)
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ 𝐵)
Theorem	fnfvelrnd 7070	A function's value belongs to its range. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝐹 Fn 𝐴)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐴)    ⇒   ⊢ (𝜑 → (𝐹‘𝐵) ∈ ran 𝐹)
Theorem	ffvelcdmi 7071	A function's value belongs to its codomain. (Contributed by NM, 6-Apr-2005.)
⊢ 𝐹:𝐴⟶𝐵    ⇒   ⊢ (𝐶 ∈ 𝐴 → (𝐹‘𝐶) ∈ 𝐵)
Theorem	ffvelcdmda 7072	A function's value belongs to its codomain. (Contributed by Mario Carneiro, 29-Dec-2016.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    ⇒   ⊢ ((𝜑 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ 𝐵)
Theorem	ffvelcdmd 7073	A function's value belongs to its codomain. (Contributed by Mario Carneiro, 29-Dec-2016.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐴)    ⇒   ⊢ (𝜑 → (𝐹‘𝐶) ∈ 𝐵)
Theorem	rexrn 7074*	Restricted existential quantification over the range of a function. (Contributed by Mario Carneiro, 24-Dec-2013.) (Revised by Mario Carneiro, 20-Aug-2014.)
⊢ (𝑥 = (𝐹‘𝑦) → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐹 Fn 𝐴 → (∃𝑥 ∈ ran 𝐹𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓))
Theorem	ralrn 7075*	Restricted universal quantification over the range of a function. (Contributed by Mario Carneiro, 24-Dec-2013.) (Revised by Mario Carneiro, 20-Aug-2014.)
⊢ (𝑥 = (𝐹‘𝑦) → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐹 Fn 𝐴 → (∀𝑥 ∈ ran 𝐹𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓))
Theorem	elrnrexdm 7076*	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 𝐹 → ∃𝑥 ∈ dom 𝐹 𝑌 = (𝐹‘𝑥)))
Theorem	elrnrexdmb 7077*	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 𝐹 ↔ ∃𝑥 ∈ dom 𝐹 𝑌 = (𝐹‘𝑥)))
Theorem	eldmrexrn 7078*	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 𝐹 → ∃𝑥 ∈ ran 𝐹 𝑥 = (𝐹‘𝑌)))
Theorem	eldmrexrnb 7079*	For any element in the domain of a function, there is an element in the range of the function which is the value of the function at that element. Because of the definition df-fv 6541 of the value of a function, the theorem is only valid in general if the empty set is not contained in the range of the function (the implication "to the right" is always valid). Indeed, with the definition df-fv 6541 of the value of a function, (𝐹‘𝑌) = ∅ may mean that the value of 𝐹 at 𝑌 is the empty set or that 𝐹 is not defined at 𝑌. (Contributed by Alexander van der Vekens, 17-Dec-2017.)
⊢ ((Fun 𝐹 ∧ ∅ ∉ ran 𝐹) → (𝑌 ∈ dom 𝐹 ↔ ∃𝑥 ∈ ran 𝐹 𝑥 = (𝐹‘𝑌)))
Theorem	fvcofneq 7080*	The values of two function compositions are equal if the values of the composed functions are pairwise equal. (Contributed by AV, 26-Jan-2019.)
⊢ ((𝐺 Fn 𝐴 ∧ 𝐾 Fn 𝐵) → ((𝑋 ∈ (𝐴 ∩ 𝐵) ∧ (𝐺‘𝑋) = (𝐾‘𝑋) ∧ ∀𝑥 ∈ (ran 𝐺 ∩ ran 𝐾)(𝐹‘𝑥) = (𝐻‘𝑥)) → ((𝐹 ∘ 𝐺)‘𝑋) = ((𝐻 ∘ 𝐾)‘𝑋)))
Theorem	ralrnmptw 7081*	A restricted quantifier over an image set. Version of ralrnmpt 7083 with a disjoint variable condition, which does not require ax-13 2371. (Contributed by Mario Carneiro, 20-Aug-2015.) Avoid ax-13 2371. (Revised by Gino Giotto, 26-Jan-2024.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    &   ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → (∀𝑦 ∈ ran 𝐹𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒))
Theorem	rexrnmptw 7082*	A restricted quantifier over an image set. Version of rexrnmpt 7084 with a disjoint variable condition, which does not require ax-13 2371. (Contributed by Mario Carneiro, 20-Aug-2015.) Avoid ax-13 2371. (Revised by Gino Giotto, 26-Jan-2024.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    &   ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → (∃𝑦 ∈ ran 𝐹𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒))
Theorem	ralrnmpt 7083*	A restricted quantifier over an image set. Usage of this theorem is discouraged because it depends on ax-13 2371. Use the weaker ralrnmptw 7081 when possible. (Contributed by Mario Carneiro, 20-Aug-2015.) (New usage is discouraged.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    &   ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → (∀𝑦 ∈ ran 𝐹𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒))
Theorem	rexrnmpt 7084*	A restricted quantifier over an image set. Usage of this theorem is discouraged because it depends on ax-13 2371. Use the weaker rexrnmptw 7082 when possible. (Contributed by Mario Carneiro, 20-Aug-2015.) (New usage is discouraged.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    &   ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → (∃𝑦 ∈ ran 𝐹𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒))
Theorem	f0cli 7085	Unconditional closure of a function when the codomain includes the empty set. (Contributed by Mario Carneiro, 12-Sep-2013.)
⊢ 𝐹:𝐴⟶𝐵    &   ⊢ ∅ ∈ 𝐵    ⇒   ⊢ (𝐹‘𝐶) ∈ 𝐵
Theorem	dff2 7086	Alternate definition of a mapping. (Contributed by NM, 14-Nov-2007.)
⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ 𝐹 ⊆ (𝐴 × 𝐵)))
Theorem	dff3 7087*	Alternate definition of a mapping. (Contributed by NM, 20-Mar-2007.)
⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 ⊆ (𝐴 × 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃!𝑦 𝑥𝐹𝑦))
Theorem	dff4 7088*	Alternate definition of a mapping. (Contributed by NM, 20-Mar-2007.)
⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 ⊆ (𝐴 × 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝑥𝐹𝑦))
Theorem	dffo3 7089*	An onto mapping expressed in terms of function values. (Contributed by NM, 29-Oct-2006.)
⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)))
Theorem	dffo4 7090*	Alternate definition of an onto mapping. (Contributed by NM, 20-Mar-2007.)
⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝑥𝐹𝑦))
Theorem	dffo5 7091*	Alternate definition of an onto mapping. (Contributed by NM, 20-Mar-2007.)
⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃𝑥 𝑥𝐹𝑦))
Theorem	exfo 7092*	A relation equivalent to the existence of an onto mapping. The right-hand 𝑓 is not necessarily a function. (Contributed by NM, 20-Mar-2007.)
⊢ (∃𝑓 𝑓:𝐴–onto→𝐵 ↔ ∃𝑓(∀𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝑥𝑓𝑦 ∧ ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐴 𝑦𝑓𝑥))
Theorem	foelrn 7093*	Property of a surjective function. (Contributed by Jeff Madsen, 4-Jan-2011.)
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐶 ∈ 𝐵) → ∃𝑥 ∈ 𝐴 𝐶 = (𝐹‘𝑥))
Theorem	foco2 7094	If a composition of two functions is surjective, then the function on the left is surjective. (Contributed by Jeff Madsen, 16-Jun-2011.) (Proof shortened by JJ, 14-Jul-2021.)
⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵 ∧ (𝐹 ∘ 𝐺):𝐴–onto→𝐶) → 𝐹:𝐵–onto→𝐶)
Theorem	fmpt 7095*	Functionality of the mapping operation. (Contributed by Mario Carneiro, 26-Jul-2013.) (Revised by Mario Carneiro, 31-Aug-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶)    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ↔ 𝐹:𝐴⟶𝐵)
Theorem	f1ompt 7096*	Express bijection for a mapping operation. (Contributed by Mario Carneiro, 30-May-2015.) (Revised by Mario Carneiro, 4-Dec-2016.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶)    ⇒   ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃!𝑥 ∈ 𝐴 𝑦 = 𝐶))
Theorem	fmpti 7097*	Functionality of the mapping operation. (Contributed by NM, 19-Mar-2005.) (Revised by Mario Carneiro, 1-Sep-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶)    &   ⊢ (𝑥 ∈ 𝐴 → 𝐶 ∈ 𝐵)    ⇒   ⊢ 𝐹:𝐴⟶𝐵
Theorem	fvmptelcdm 7098*	The value of a function at a point of its domain belongs to its codomain. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶𝐶)    ⇒   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶)
Theorem	fmptd 7099*	Domain and codomain of the mapping operation; deduction form. (Contributed by Mario Carneiro, 13-Jan-2013.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    ⇒   ⊢ (𝜑 → 𝐹:𝐴⟶𝐶)
Theorem	fmpttd 7100*	Version of fmptd 7099 with inlined definition. Domain and codomain of the mapping operation; deduction form. (Contributed by Glauco Siliprandi, 23-Oct-2021.) (Proof shortened by BJ, 16-Aug-2022.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶𝐶)