P. 70 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 6901-7000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	fvmptdv 6901*	Alternate deduction version of fvmpt 6884, suitable for iteration. (Contributed by Mario Carneiro, 7-Jan-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝐷)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → ((𝐹‘𝐴) = 𝐵 → 𝜓))    ⇒   ⊢ (𝜑 → (𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵) → 𝜓))
Theorem	fvmptdv2 6902*	Alternate deduction version of fvmpt 6884, suitable for iteration. (Contributed by Mario Carneiro, 7-Jan-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝐷)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → (𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵) → (𝐹‘𝐴) = 𝐶))
Theorem	mpteqb 6903*	Bidirectional equality theorem for a mapping abstraction. Equivalent to eqfnfv 6918. (Contributed by Mario Carneiro, 14-Nov-2014.)
⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ((𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶) ↔ ∀𝑥 ∈ 𝐴 𝐵 = 𝐶))
Theorem	fvmptt 6904*	Closed theorem form of fvmpt 6884. (Contributed by Scott Fenton, 21-Feb-2013.) (Revised by Mario Carneiro, 11-Sep-2015.)
⊢ ((∀𝑥(𝑥 = 𝐴 → 𝐵 = 𝐶) ∧ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵) ∧ (𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑉)) → (𝐹‘𝐴) = 𝐶)
Theorem	fvmptf 6905*	Value of a function given by an ordered-pair class abstraction. This version of fvmptg 6882 uses bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 8-Nov-2005.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐶    &   ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵)    ⇒   ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑉) → (𝐹‘𝐴) = 𝐶)
Theorem	fvmptnf 6906*	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 6908 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 6907*	Deduction version of fvmpt 6884. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵)    &   ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐹‘𝐴) = 𝐶)
Theorem	fvmptn 6908*	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 6882. (Contributed by NM, 21-Oct-2003.) (Revised by Mario Carneiro, 9-Sep-2013.)
⊢ (𝑥 = 𝐷 → 𝐵 = 𝐶)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    ⇒   ⊢ (¬ 𝐶 ∈ V → (𝐹‘𝐷) = ∅)
Theorem	fvmptss2 6909*	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 6910*	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 6911 with a disjoint variable condition, which does not require ax-13 2373. (Contributed by Alexander van der Vekens, 15-Jul-2018.) (Revised by Gino Giotto, 26-Jan-2024.)
⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ {𝑦 ∈ ⦋𝑥 / 𝑚⦌𝑀 ∣ 𝜑})    &   ⊢ (𝑋 ∈ 𝑉 → ⦋𝑋 / 𝑚⦌𝑀 ∈ V)    ⇒   ⊢ (𝑌 ∈ (𝐹‘𝑋) → (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ ⦋𝑋 / 𝑚⦌𝑀))
Theorem	elfvmptrab1 6911*	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 2373. Use the weaker elfvmptrab1w 6910 when possible. (Contributed by Alexander van der Vekens, 15-Jul-2018.) (New usage is discouraged.)
⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ {𝑦 ∈ ⦋𝑥 / 𝑚⦌𝑀 ∣ 𝜑})    &   ⊢ (𝑋 ∈ 𝑉 → ⦋𝑋 / 𝑚⦌𝑀 ∈ V)    ⇒   ⊢ (𝑌 ∈ (𝐹‘𝑋) → (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ ⦋𝑋 / 𝑚⦌𝑀))
Theorem	elfvmptrab 6912*	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 6913*	Value of a function given by an ordered-pair class abstraction, outside of its domain. (Contributed by NM, 28-Mar-2008.)
⊢ 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}    ⇒   ⊢ (¬ 𝐵 ∈ 𝐴 → (𝐹‘𝐵) = ∅)
Theorem	fvmptndm 6914*	Value of a function given by the maps-to notation, outside of its domain. (Contributed by AV, 31-Dec-2020.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    ⇒   ⊢ (¬ 𝑋 ∈ 𝐴 → (𝐹‘𝑋) = ∅)
Theorem	fvmptrabfv 6915*	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 6916*	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 6917*	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 6918*	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 6919*	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 6920*	Derive equality of functions from equality of their values. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) → (𝐹 = 𝐺 ↔ (𝐵 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝐵 ∧ (𝐹‘𝑥) = (𝐺‘𝑥)))))
Theorem	eqfnfvd 6921*	Deduction for equality of functions. (Contributed by Mario Carneiro, 24-Jul-2014.)
⊢ (𝜑 → 𝐹 Fn 𝐴)    &   ⊢ (𝜑 → 𝐺 Fn 𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = (𝐺‘𝑥))    ⇒   ⊢ (𝜑 → 𝐹 = 𝐺)
Theorem	eqfnfv2f 6922*	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 6918 uses bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 29-Jan-2004.)
⊢ Ⅎ𝑥𝐹    &   ⊢ Ⅎ𝑥𝐺    ⇒   ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥)))
Theorem	eqfunfv 6923*	Equality of functions is determined by their values. (Contributed by Scott Fenton, 19-Jun-2011.)
⊢ ((Fun 𝐹 ∧ Fun 𝐺) → (𝐹 = 𝐺 ↔ (dom 𝐹 = dom 𝐺 ∧ ∀𝑥 ∈ dom 𝐹(𝐹‘𝑥) = (𝐺‘𝑥))))
Theorem	fvreseq0 6924*	Equality of restricted functions is determined by their values (for functions with different domains). (Contributed by AV, 6-Jan-2019.)
⊢ (((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐶) ∧ (𝐵 ⊆ 𝐴 ∧ 𝐵 ⊆ 𝐶)) → ((𝐹 ↾ 𝐵) = (𝐺 ↾ 𝐵) ↔ ∀𝑥 ∈ 𝐵 (𝐹‘𝑥) = (𝐺‘𝑥)))
Theorem	fvreseq1 6925*	Equality of a function restricted to the domain of another function. (Contributed by AV, 6-Jan-2019.)
⊢ (((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) ∧ 𝐵 ⊆ 𝐴) → ((𝐹 ↾ 𝐵) = 𝐺 ↔ ∀𝑥 ∈ 𝐵 (𝐹‘𝑥) = (𝐺‘𝑥)))
Theorem	fvreseq 6926*	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 6927*	A function with a given domain is a mapping defined by its function values. (Contributed by AV, 1-Mar-2019.)
⊢ (𝜑 → 𝑀 Fn 𝐴)    &   ⊢ (𝑖 = 𝑎 → 𝐷 = 𝐶)    &   ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → 𝐷 ∈ 𝑈)    &   ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → 𝐶 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑀 = (𝑎 ∈ 𝐴 ↦ 𝐶) ↔ ∀𝑖 ∈ 𝐴 (𝑀‘𝑖) = 𝐷))
Theorem	fndmdif 6928*	Two ways to express the locus of differences between two functions. (Contributed by Stefan O'Rear, 17-Jan-2015.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → dom (𝐹 ∖ 𝐺) = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) ≠ (𝐺‘𝑥)})
Theorem	fndmdifcom 6929	The difference set between two functions is commutative. (Contributed by Stefan O'Rear, 17-Jan-2015.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → dom (𝐹 ∖ 𝐺) = dom (𝐺 ∖ 𝐹))
Theorem	fndmdifeq0 6930	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 6931*	Two ways to express the locus of equality between two functions. (Contributed by Stefan O'Rear, 17-Jan-2015.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → dom (𝐹 ∩ 𝐺) = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) = (𝐺‘𝑥)})
Theorem	fneqeql 6932	Two functions are equal iff their equalizer is the whole domain. (Contributed by Stefan O'Rear, 7-Mar-2015.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ dom (𝐹 ∩ 𝐺) = 𝐴))
Theorem	fneqeql2 6933	Two functions are equal iff their equalizer contains the whole domain. (Contributed by Stefan O'Rear, 9-Mar-2015.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ 𝐴 ⊆ dom (𝐹 ∩ 𝐺)))
Theorem	fnreseql 6934	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 6935*	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 6936	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 6937	Two ways to say that 𝐴 is in the domain of 𝐹. (Contributed by Mario Carneiro, 1-May-2014.)
⊢ (Fun 𝐹 → (𝐴 ∈ dom 𝐹 ↔ 𝐴𝐹(𝐹‘𝐴)))
Theorem	fvimacnvi 6938	A member of a preimage is a function value argument. (Contributed by NM, 4-May-2007.)
⊢ ((Fun 𝐹 ∧ 𝐴 ∈ (◡𝐹 “ 𝐵)) → (𝐹‘𝐴) ∈ 𝐵)
Theorem	fvimacnv 6939	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 6524 could probably be strengthened to a biconditional." (Contributed by Raph Levien, 20-Nov-2006.)
⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → ((𝐹‘𝐴) ∈ 𝐵 ↔ 𝐴 ∈ (◡𝐹 “ 𝐵)))
Theorem	funimass3 6940	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 6939 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 6941*	A subclass of a preimage in terms of function values. (Contributed by NM, 15-May-2007.)
⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹) → (𝐴 ⊆ (◡𝐹 “ 𝐵) ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))
Theorem	funconstss 6942*	Two ways of specifying that a function is constant on a subdomain. (Contributed by NM, 8-Mar-2007.)
⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹) → (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵 ↔ 𝐴 ⊆ (◡𝐹 “ {𝐵})))
Theorem	fvimacnvALT 6943	Alternate proof of fvimacnv 6939, based on funimass3 6940. If funimass3 6940 is ever proved directly, as opposed to using funimacnv 6522 pointwise, then the proof of funimacnv 6522 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 6944	Membership in the preimage of a set under a function. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) ↔ (𝐵 ∈ 𝐴 ∧ (𝐹‘𝐵) ∈ 𝐶)))
Theorem	elpreimad 6945	Membership in the preimage of a set under a function. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝜑 → 𝐹 Fn 𝐴)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐴)    &   ⊢ (𝜑 → (𝐹‘𝐵) ∈ 𝐶)    ⇒   ⊢ (𝜑 → 𝐵 ∈ (◡𝐹 “ 𝐶))
Theorem	fniniseg 6946	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 6947*	Inverse images under functions expressed as abstractions. (Contributed by Stefan O'Rear, 1-Feb-2015.)
⊢ (𝐹 Fn 𝐴 → (◡𝐹 “ 𝐵) = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) ∈ 𝐵})
Theorem	fniniseg2 6948*	Inverse point images under functions expressed as abstractions. (Contributed by Stefan O'Rear, 1-Feb-2015.)
⊢ (𝐹 Fn 𝐴 → (◡𝐹 “ {𝐵}) = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) = 𝐵})
Theorem	unpreima 6949	Preimage of a union. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (Fun 𝐹 → (◡𝐹 “ (𝐴 ∪ 𝐵)) = ((◡𝐹 “ 𝐴) ∪ (◡𝐹 “ 𝐵)))
Theorem	inpreima 6950	Preimage of an intersection. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 14-Jun-2016.)
⊢ (Fun 𝐹 → (◡𝐹 “ (𝐴 ∩ 𝐵)) = ((◡𝐹 “ 𝐴) ∩ (◡𝐹 “ 𝐵)))
Theorem	difpreima 6951	Preimage of a difference. (Contributed by Mario Carneiro, 14-Jun-2016.)
⊢ (Fun 𝐹 → (◡𝐹 “ (𝐴 ∖ 𝐵)) = ((◡𝐹 “ 𝐴) ∖ (◡𝐹 “ 𝐵)))
Theorem	respreima 6952	The preimage of a restricted function. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (Fun 𝐹 → (◡(𝐹 ↾ 𝐵) “ 𝐴) = ((◡𝐹 “ 𝐴) ∩ 𝐵))
Theorem	cnvimainrn 6953	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 6954	The preimage of a subset is a subset of the preimage. (Contributed by Brendan Leahy, 23-Sep-2017.)
⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ 𝐵) → (◡𝐹 “ 𝐴) ⊆ (◡𝐹 “ 𝐵))
Theorem	iinpreima 6955*	Preimage of an intersection. (Contributed by FL, 16-Apr-2012.)
⊢ ((Fun 𝐹 ∧ 𝐴 ≠ ∅) → (◡𝐹 “ ∩ 𝑥 ∈ 𝐴 𝐵) = ∩ 𝑥 ∈ 𝐴 (◡𝐹 “ 𝐵))
Theorem	intpreima 6956*	Preimage of an intersection. (Contributed by FL, 28-Apr-2012.)
⊢ ((Fun 𝐹 ∧ 𝐴 ≠ ∅) → (◡𝐹 “ ∩ 𝐴) = ∩ 𝑥 ∈ 𝐴 (◡𝐹 “ 𝑥))
Theorem	fimacnvOLD 6957	Obsolete version of fimacnv 6631 as of 20-Sep-2024. (Contributed by FL, 25-Jan-2007.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (𝐹:𝐴⟶𝐵 → (◡𝐹 “ 𝐵) = 𝐴)
Theorem	fimacnvinrn 6958	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 6959	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 6960	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 6961*	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 6821. (Contributed by AV, 27-Jan-2020.) (Proof shortened by Peter Mazsa, 2-Oct-2022.)
⊢ (∀𝑎 ∈ 𝐷 (𝐹‘𝑎) ≠ ∅ → (𝐷 ⊆ dom 𝐹 ∧ Fun (𝐹 ↾ 𝐷)))
Theorem	fnopfv 6962	Ordered pair with function value. Part of Theorem 4.3(i) of [Monk1] p. 41. (Contributed by NM, 30-Sep-2004.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ⟨𝐵, (𝐹‘𝐵)⟩ ∈ 𝐹)
Theorem	fvelrn 6963	A function's value belongs to its range. (Contributed by NM, 14-Oct-1996.)
⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → (𝐹‘𝐴) ∈ ran 𝐹)
Theorem	nelrnfvne 6964	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 6965*	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 6966*	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 6967	A function's value belongs to its range. (Contributed by NM, 15-Oct-1996.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → (𝐹‘𝐵) ∈ ran 𝐹)
Theorem	ffvelrn 6968	A function's value belongs to its codomain. (Contributed by NM, 12-Aug-1999.)
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ 𝐵)
Theorem	ffvelrni 6969	A function's value belongs to its codomain. (Contributed by NM, 6-Apr-2005.)
⊢ 𝐹:𝐴⟶𝐵    ⇒   ⊢ (𝐶 ∈ 𝐴 → (𝐹‘𝐶) ∈ 𝐵)
Theorem	ffvelrnda 6970	A function's value belongs to its codomain. (Contributed by Mario Carneiro, 29-Dec-2016.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    ⇒   ⊢ ((𝜑 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ 𝐵)
Theorem	ffvelrnd 6971	A function's value belongs to its codomain. (Contributed by Mario Carneiro, 29-Dec-2016.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐴)    ⇒   ⊢ (𝜑 → (𝐹‘𝐶) ∈ 𝐵)
Theorem	rexrn 6972*	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 6973*	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 6974*	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 6975*	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 6976*	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 6977*	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 6445 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 6445 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 6978*	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 6979*	A restricted quantifier over an image set. Version of ralrnmpt 6981 with a disjoint variable condition, which does not require ax-13 2373. (Contributed by Mario Carneiro, 20-Aug-2015.) (Revised by Gino Giotto, 26-Jan-2024.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    &   ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → (∀𝑦 ∈ ran 𝐹𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒))
Theorem	rexrnmptw 6980*	A restricted quantifier over an image set. Version of rexrnmpt 6982 with a disjoint variable condition, which does not require ax-13 2373. (Contributed by Mario Carneiro, 20-Aug-2015.) (Revised by Gino Giotto, 26-Jan-2024.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    &   ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → (∃𝑦 ∈ ran 𝐹𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒))
Theorem	ralrnmpt 6981*	A restricted quantifier over an image set. Usage of this theorem is discouraged because it depends on ax-13 2373. Use the weaker ralrnmptw 6979 when possible. (Contributed by Mario Carneiro, 20-Aug-2015.) (New usage is discouraged.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    &   ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → (∀𝑦 ∈ ran 𝐹𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒))
Theorem	rexrnmpt 6982*	A restricted quantifier over an image set. Usage of this theorem is discouraged because it depends on ax-13 2373. Use the weaker rexrnmptw 6980 when possible. (Contributed by Mario Carneiro, 20-Aug-2015.) (New usage is discouraged.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    &   ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → (∃𝑦 ∈ ran 𝐹𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒))
Theorem	f0cli 6983	Unconditional closure of a function when the range includes the empty set. (Contributed by Mario Carneiro, 12-Sep-2013.)
⊢ 𝐹:𝐴⟶𝐵    &   ⊢ ∅ ∈ 𝐵    ⇒   ⊢ (𝐹‘𝐶) ∈ 𝐵
Theorem	dff2 6984	Alternate definition of a mapping. (Contributed by NM, 14-Nov-2007.)
⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ 𝐹 ⊆ (𝐴 × 𝐵)))
Theorem	dff3 6985*	Alternate definition of a mapping. (Contributed by NM, 20-Mar-2007.)
⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 ⊆ (𝐴 × 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃!𝑦 𝑥𝐹𝑦))
Theorem	dff4 6986*	Alternate definition of a mapping. (Contributed by NM, 20-Mar-2007.)
⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 ⊆ (𝐴 × 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝑥𝐹𝑦))
Theorem	dffo3 6987*	An onto mapping expressed in terms of function values. (Contributed by NM, 29-Oct-2006.)
⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)))
Theorem	dffo4 6988*	Alternate definition of an onto mapping. (Contributed by NM, 20-Mar-2007.)
⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝑥𝐹𝑦))
Theorem	dffo5 6989*	Alternate definition of an onto mapping. (Contributed by NM, 20-Mar-2007.)
⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃𝑥 𝑥𝐹𝑦))
Theorem	exfo 6990*	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 6991*	Property of a surjective function. (Contributed by Jeff Madsen, 4-Jan-2011.)
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐶 ∈ 𝐵) → ∃𝑥 ∈ 𝐴 𝐶 = (𝐹‘𝑥))
Theorem	foco2 6992	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 6993*	Functionality of the mapping operation. (Contributed by Mario Carneiro, 26-Jul-2013.) (Revised by Mario Carneiro, 31-Aug-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶)    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ↔ 𝐹:𝐴⟶𝐵)
Theorem	f1ompt 6994*	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 6995*	Functionality of the mapping operation. (Contributed by NM, 19-Mar-2005.) (Revised by Mario Carneiro, 1-Sep-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶)    &   ⊢ (𝑥 ∈ 𝐴 → 𝐶 ∈ 𝐵)    ⇒   ⊢ 𝐹:𝐴⟶𝐵
Theorem	fvmptelrn 6996*	The value of a function at a point of its domain belongs to its codomain. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶𝐶)    ⇒   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶)
Theorem	fmptd 6997*	Domain and codomain of the mapping operation; deduction form. (Contributed by Mario Carneiro, 13-Jan-2013.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    ⇒   ⊢ (𝜑 → 𝐹:𝐴⟶𝐶)
Theorem	fmpttd 6998*	Version of fmptd 6997 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.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶𝐶)
Theorem	fmpt3d 6999*	Domain and codomain of the mapping operation; deduction form. (Contributed by Thierry Arnoux, 4-Jun-2017.)
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶)    ⇒   ⊢ (𝜑 → 𝐹:𝐴⟶𝐶)
Theorem	fmptdf 7000*	A version of fmptd 6997 using bound-variable hypothesis instead of a distinct variable condition for 𝜑. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ Ⅎ𝑥𝜑    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    ⇒   ⊢ (𝜑 → 𝐹:𝐴⟶𝐶)