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	fnsnfv 6901	Singleton of function value. (Contributed by NM, 22-May-1998.) (Proof shortened by Scott Fenton, 8-Aug-2024.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → {(𝐹‘𝐵)} = (𝐹 “ {𝐵}))
Theorem	opabiotafun 6902*	Define a function whose value is "the unique 𝑦 such that 𝜑(𝑥, 𝑦)". (Contributed by NM, 19-May-2015.)
⊢ 𝐹 = {⟨𝑥, 𝑦⟩ ∣ {𝑦 ∣ 𝜑} = {𝑦}}    ⇒   ⊢ Fun 𝐹
Theorem	opabiotadm 6903*	Define a function whose value is "the unique 𝑦 such that 𝜑(𝑥, 𝑦)". (Contributed by NM, 16-Nov-2013.)
⊢ 𝐹 = {⟨𝑥, 𝑦⟩ ∣ {𝑦 ∣ 𝜑} = {𝑦}}    ⇒   ⊢ dom 𝐹 = {𝑥 ∣ ∃!𝑦𝜑}
Theorem	opabiota 6904*	Define a function whose value is "the unique 𝑦 such that 𝜑(𝑥, 𝑦)". (Contributed by NM, 16-Nov-2013.)
⊢ 𝐹 = {⟨𝑥, 𝑦⟩ ∣ {𝑦 ∣ 𝜑} = {𝑦}}    &   ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐵 ∈ dom 𝐹 → (𝐹‘𝐵) = (℩𝑦𝜓))
Theorem	fnimapr 6905	The image of a pair under a function. (Contributed by Jeff Madsen, 6-Jan-2011.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) → (𝐹 “ {𝐵, 𝐶}) = {(𝐹‘𝐵), (𝐹‘𝐶)})
Theorem	fnimatpd 6906	The image of an unordered triple under a function. (Contributed by Thierry Arnoux, 19-Sep-2023.)
⊢ (𝜑 → 𝐹 Fn 𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐷)    ⇒   ⊢ (𝜑 → (𝐹 “ {𝐴, 𝐵, 𝐶}) = {(𝐹‘𝐴), (𝐹‘𝐵), (𝐹‘𝐶)})
Theorem	ssimaex 6907*	The existence of a subimage. (Contributed by NM, 8-Apr-2007.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ((Fun 𝐹 ∧ 𝐵 ⊆ (𝐹 “ 𝐴)) → ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝐵 = (𝐹 “ 𝑥)))
Theorem	ssimaexg 6908*	The existence of a subimage. (Contributed by FL, 15-Apr-2007.)
⊢ ((𝐴 ∈ 𝐶 ∧ Fun 𝐹 ∧ 𝐵 ⊆ (𝐹 “ 𝐴)) → ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝐵 = (𝐹 “ 𝑥)))
Theorem	funfv 6909	A simplified expression for the value of a function when we know it is a function. (Contributed by NM, 22-May-1998.)
⊢ (Fun 𝐹 → (𝐹‘𝐴) = ∪ (𝐹 “ {𝐴}))
Theorem	funfv2 6910*	The value of a function. Definition of function value in [Enderton] p. 43. (Contributed by NM, 22-May-1998.)
⊢ (Fun 𝐹 → (𝐹‘𝐴) = ∪ {𝑦 ∣ 𝐴𝐹𝑦})
Theorem	funfv2f 6911	The value of a function. Version of funfv2 6910 using a bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 19-Feb-2006.)
⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑦𝐹    ⇒   ⊢ (Fun 𝐹 → (𝐹‘𝐴) = ∪ {𝑦 ∣ 𝐴𝐹𝑦})
Theorem	fvun 6912	Value of the union of two functions when the domains are separate. (Contributed by FL, 7-Nov-2011.)
⊢ (((Fun 𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 ∩ dom 𝐺) = ∅) → ((𝐹 ∪ 𝐺)‘𝐴) = ((𝐹‘𝐴) ∪ (𝐺‘𝐴)))
Theorem	fvun1 6913	The value of a union when the argument is in the first domain. (Contributed by Scott Fenton, 29-Jun-2013.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ((𝐴 ∩ 𝐵) = ∅ ∧ 𝑋 ∈ 𝐴)) → ((𝐹 ∪ 𝐺)‘𝑋) = (𝐹‘𝑋))
Theorem	fvun2 6914	The value of a union when the argument is in the second domain. (Contributed by Scott Fenton, 29-Jun-2013.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ((𝐴 ∩ 𝐵) = ∅ ∧ 𝑋 ∈ 𝐵)) → ((𝐹 ∪ 𝐺)‘𝑋) = (𝐺‘𝑋))
Theorem	fvun1d 6915	The value of a union when the argument is in the first domain, a deduction version. (Contributed by metakunt, 28-May-2024.)
⊢ (𝜑 → 𝐹 Fn 𝐴)    &   ⊢ (𝜑 → 𝐺 Fn 𝐵)    &   ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    ⇒   ⊢ (𝜑 → ((𝐹 ∪ 𝐺)‘𝑋) = (𝐹‘𝑋))
Theorem	fvun2d 6916	The value of a union when the argument is in the second domain, a deduction version. (Contributed by metakunt, 28-May-2024.)
⊢ (𝜑 → 𝐹 Fn 𝐴)    &   ⊢ (𝜑 → 𝐺 Fn 𝐵)    &   ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝐹 ∪ 𝐺)‘𝑋) = (𝐺‘𝑋))
Theorem	dffv2 6917	Alternate definition of function value df-fv 6489 that doesn't require dummy variables. (Contributed by NM, 4-Aug-2010.)
⊢ (𝐹‘𝐴) = ∪ ((𝐹 “ {𝐴}) ∖ ∪ ∪ (((𝐹 ↾ {𝐴}) ∘ ◡(𝐹 ↾ {𝐴})) ∖ I ))
Theorem	dmfco 6918	Domains of a function composition. (Contributed by NM, 27-Jan-1997.)
⊢ ((Fun 𝐺 ∧ 𝐴 ∈ dom 𝐺) → (𝐴 ∈ dom (𝐹 ∘ 𝐺) ↔ (𝐺‘𝐴) ∈ dom 𝐹))
Theorem	fvco2 6919	Value of a function composition. Similar to second part of Theorem 3H of [Enderton] p. 47. (Contributed by NM, 9-Oct-2004.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) (Revised by Stefan O'Rear, 16-Oct-2014.)
⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → ((𝐹 ∘ 𝐺)‘𝑋) = (𝐹‘(𝐺‘𝑋)))
Theorem	fvco 6920	Value of a function composition. Similar to Exercise 5 of [TakeutiZaring] p. 28. (Contributed by NM, 22-Apr-2006.) (Proof shortened by Mario Carneiro, 26-Dec-2014.)
⊢ ((Fun 𝐺 ∧ 𝐴 ∈ dom 𝐺) → ((𝐹 ∘ 𝐺)‘𝐴) = (𝐹‘(𝐺‘𝐴)))
Theorem	fvco3 6921	Value of a function composition. (Contributed by NM, 3-Jan-2004.) (Revised by Mario Carneiro, 26-Dec-2014.)
⊢ ((𝐺:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → ((𝐹 ∘ 𝐺)‘𝐶) = (𝐹‘(𝐺‘𝐶)))
Theorem	fvco3d 6922	Value of a function composition. Deduction form of fvco3 6921. (Contributed by Stanislas Polu, 9-Mar-2020.)
⊢ (𝜑 → 𝐺:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐴)    ⇒   ⊢ (𝜑 → ((𝐹 ∘ 𝐺)‘𝐶) = (𝐹‘(𝐺‘𝐶)))
Theorem	fvco4i 6923	Conditions for a composition to be expandable without conditions on the argument. (Contributed by Stefan O'Rear, 31-Mar-2015.)
⊢ ∅ = (𝐹‘∅)    &   ⊢ Fun 𝐺    ⇒   ⊢ ((𝐹 ∘ 𝐺)‘𝑋) = (𝐹‘(𝐺‘𝑋))
Theorem	fvopab3g 6924*	Value of a function given by ordered-pair class abstraction. (Contributed by NM, 6-Mar-1996.) (Revised by Mario Carneiro, 28-Apr-2015.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑥 ∈ 𝐶 → ∃!𝑦𝜑)    &   ⊢ 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐶 ∧ 𝜑)}    ⇒   ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ((𝐹‘𝐴) = 𝐵 ↔ 𝜒))
Theorem	fvopab3ig 6925*	Value of a function given by ordered-pair class abstraction. (Contributed by NM, 23-Oct-1999.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑥 ∈ 𝐶 → ∃*𝑦𝜑)    &   ⊢ 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐶 ∧ 𝜑)}    ⇒   ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝜒 → (𝐹‘𝐴) = 𝐵))
Theorem	brfvopabrbr 6926*	The binary relation of a function value which is an ordered-pair class abstraction of a restricted binary relation is the restricted binary relation. The first hypothesis can often be obtained by using fvmptopab 7401. (Contributed by AV, 29-Oct-2021.)
⊢ (𝐴‘𝑍) = {⟨𝑥, 𝑦⟩ ∣ (𝑥(𝐵‘𝑍)𝑦 ∧ 𝜑)}    &   ⊢ ((𝑥 = 𝑋 ∧ 𝑦 = 𝑌) → (𝜑 ↔ 𝜓))    &   ⊢ Rel (𝐵‘𝑍)    ⇒   ⊢ (𝑋(𝐴‘𝑍)𝑌 ↔ (𝑋(𝐵‘𝑍)𝑌 ∧ 𝜓))
Theorem	fvmptg 6927*	Value of a function given in maps-to notation. (Contributed by NM, 2-Oct-2007.) (Revised by Mario Carneiro, 31-Aug-2015.)
⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵)    ⇒   ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑅) → (𝐹‘𝐴) = 𝐶)
Theorem	fvmpti 6928*	Value of a function given in maps-to notation. (Contributed by Mario Carneiro, 23-Apr-2014.)
⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵)    ⇒   ⊢ (𝐴 ∈ 𝐷 → (𝐹‘𝐴) = ( I ‘𝐶))
Theorem	fvmpt 6929*	Value of a function given in maps-to notation. (Contributed by NM, 17-Aug-2011.)
⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵)    &   ⊢ 𝐶 ∈ V    ⇒   ⊢ (𝐴 ∈ 𝐷 → (𝐹‘𝐴) = 𝐶)
Theorem	fvmpt2f 6930	Value of a function given by the maps-to notation. (Contributed by Thierry Arnoux, 9-Mar-2017.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝐶) → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) = 𝐵)
Theorem	fvtresfn 6931*	Functionality of a tuple-restriction function. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝑥 ↾ 𝑉))    ⇒   ⊢ (𝑋 ∈ 𝐵 → (𝐹‘𝑋) = (𝑋 ↾ 𝑉))
Theorem	fvmpts 6932*	Value of a function given in maps-to notation, using explicit class substitution. (Contributed by Scott Fenton, 17-Jul-2013.) (Revised by Mario Carneiro, 31-Aug-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝐶 ↦ 𝐵)    ⇒   ⊢ ((𝐴 ∈ 𝐶 ∧ ⦋𝐴 / 𝑥⦌𝐵 ∈ 𝑉) → (𝐹‘𝐴) = ⦋𝐴 / 𝑥⦌𝐵)
Theorem	fvmpt3 6933*	Value of a function given in maps-to notation, with a slightly different sethood condition. (Contributed by Stefan O'Rear, 30-Jan-2015.)
⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵)    &   ⊢ (𝑥 ∈ 𝐷 → 𝐵 ∈ 𝑉)    ⇒   ⊢ (𝐴 ∈ 𝐷 → (𝐹‘𝐴) = 𝐶)
Theorem	fvmpt3i 6934*	Value of a function given in maps-to notation, with a slightly different sethood condition. (Contributed by Mario Carneiro, 11-Sep-2015.)
⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵)    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 ∈ 𝐷 → (𝐹‘𝐴) = 𝐶)
Theorem	fvmptdf 6935*	Deduction version of fvmptd 6936 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by AV, 29-Mar-2024.)
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵))    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 = 𝐶)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐶    ⇒   ⊢ (𝜑 → (𝐹‘𝐴) = 𝐶)
Theorem	fvmptd 6936*	Deduction version of fvmpt 6929. (Contributed by Scott Fenton, 18-Feb-2013.) (Revised by Mario Carneiro, 31-Aug-2015.) (Proof shortened by AV, 29-Mar-2024.)
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵))    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 = 𝐶)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐹‘𝐴) = 𝐶)
Theorem	fvmptd2 6937*	Deduction version of fvmpt 6929 (where the definition of the mapping does not depend on the common antecedent 𝜑). (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 = 𝐶)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐹‘𝐴) = 𝐶)
Theorem	mptrcl 6938*	Reverse closure for a mapping: If the function value of a mapping has a member, the argument belongs to the base class of the mapping. (Contributed by AV, 4-Apr-2020.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    ⇒   ⊢ (𝐼 ∈ (𝐹‘𝑋) → 𝑋 ∈ 𝐴)
Theorem	fvmpt2i 6939*	Value of a function given by the maps-to notation. (Contributed by Mario Carneiro, 23-Apr-2014.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    ⇒   ⊢ (𝑥 ∈ 𝐴 → (𝐹‘𝑥) = ( I ‘𝐵))
Theorem	fvmpt2 6940*	Value of a function given by the maps-to notation. (Contributed by FL, 21-Jun-2010.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    ⇒   ⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝐶) → (𝐹‘𝑥) = 𝐵)
Theorem	fvmptss 6941*	If all the values of the mapping are subsets of a class 𝐶, then so is any evaluation of the mapping, even if 𝐷 is not in the base set 𝐴. (Contributed by Mario Carneiro, 13-Feb-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → (𝐹‘𝐷) ⊆ 𝐶)
Theorem	fvmpt2d 6942*	Deduction version of fvmpt2 6940. (Contributed by Thierry Arnoux, 8-Dec-2016.)
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    ⇒   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 𝐵)
Theorem	fvmptex 6943*	Express a function 𝐹 whose value 𝐵 may not always be a set in terms of another function 𝐺 for which sethood is guaranteed. (Note that ( I ‘𝐵) is just shorthand for if(𝐵 ∈ V, 𝐵, ∅), and it is always a set by fvex 6835.) Note also that these functions are not the same; wherever 𝐵(𝐶) is not a set, 𝐶 is not in the domain of 𝐹 (so it evaluates to the empty set), but 𝐶 is in the domain of 𝐺, and 𝐺(𝐶) is defined to be the empty set. (Contributed by Mario Carneiro, 14-Jul-2013.) (Revised by Mario Carneiro, 23-Apr-2014.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    &   ⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ ( I ‘𝐵))    ⇒   ⊢ (𝐹‘𝐶) = (𝐺‘𝐶)
Theorem	fvmptd3f 6944*	Alternate deduction version of fvmpt 6929 with three nonfreeness hypotheses instead of distinct variable conditions. (Contributed by AV, 19-Jan-2022.)
⊢ (𝜑 → 𝐴 ∈ 𝐷)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → ((𝐹‘𝐴) = 𝐵 → 𝜓))    &   ⊢ Ⅎ𝑥𝐹    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (𝜑 → (𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵) → 𝜓))
Theorem	fvmptd2f 6945*	Alternate deduction version of fvmpt 6929, suitable for iteration. (Contributed by Mario Carneiro, 7-Jan-2017.) (Proof shortened by AV, 19-Jan-2022.)
⊢ (𝜑 → 𝐴 ∈ 𝐷)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → ((𝐹‘𝐴) = 𝐵 → 𝜓))    &   ⊢ Ⅎ𝑥𝐹    &   ⊢ Ⅎ𝑥𝜓    ⇒   ⊢ (𝜑 → (𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵) → 𝜓))
Theorem	fvmptdv 6946*	Alternate deduction version of fvmpt 6929, suitable for iteration. (Contributed by Mario Carneiro, 7-Jan-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝐷)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → ((𝐹‘𝐴) = 𝐵 → 𝜓))    ⇒   ⊢ (𝜑 → (𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵) → 𝜓))
Theorem	fvmptdv2 6947*	Alternate deduction version of fvmpt 6929, suitable for iteration. (Contributed by Mario Carneiro, 7-Jan-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝐷)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → (𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵) → (𝐹‘𝐴) = 𝐶))
Theorem	mpteqb 6948*	Bidirectional equality theorem for a mapping abstraction. Equivalent to eqfnfv 6964. (Contributed by Mario Carneiro, 14-Nov-2014.)
⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ((𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶) ↔ ∀𝑥 ∈ 𝐴 𝐵 = 𝐶))
Theorem	fvmptt 6949*	Closed theorem form of fvmpt 6929. (Contributed by Scott Fenton, 21-Feb-2013.) (Revised by Mario Carneiro, 11-Sep-2015.)
⊢ ((∀𝑥(𝑥 = 𝐴 → 𝐵 = 𝐶) ∧ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵) ∧ (𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑉)) → (𝐹‘𝐴) = 𝐶)
Theorem	fvmptf 6950*	Value of a function given by an ordered-pair class abstraction. This version of fvmptg 6927 uses bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 8-Nov-2005.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐶    &   ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵)    ⇒   ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑉) → (𝐹‘𝐴) = 𝐶)
Theorem	fvmptnf 6951*	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 6954 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 6952*	Deduction version of fvmpt 6929. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵)    &   ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐹‘𝐴) = 𝐶)
Theorem	fvmptd4 6953*	Deduction version of fvmpt 6929 (where the substitution hypothesis does not have the antecedent 𝜑). (Contributed by SN, 26-Jul-2024.)
⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵))    &   ⊢ (𝜑 → 𝐴 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐹‘𝐴) = 𝐶)
Theorem	fvmptn 6954*	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 6927. (Contributed by NM, 21-Oct-2003.) (Revised by Mario Carneiro, 9-Sep-2013.)
⊢ (𝑥 = 𝐷 → 𝐵 = 𝐶)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    ⇒   ⊢ (¬ 𝐶 ∈ V → (𝐹‘𝐷) = ∅)
Theorem	fvmptss2 6955*	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 6956*	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 6957 with a disjoint variable condition, which does not require ax-13 2372. (Contributed by Alexander van der Vekens, 15-Jul-2018.) Avoid ax-13 2372. (Revised by GG, 26-Jan-2024.)
⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ {𝑦 ∈ ⦋𝑥 / 𝑚⦌𝑀 ∣ 𝜑})    &   ⊢ (𝑋 ∈ 𝑉 → ⦋𝑋 / 𝑚⦌𝑀 ∈ V)    ⇒   ⊢ (𝑌 ∈ (𝐹‘𝑋) → (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ ⦋𝑋 / 𝑚⦌𝑀))
Theorem	elfvmptrab1 6957*	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 2372. Use the weaker elfvmptrab1w 6956 when possible. (Contributed by Alexander van der Vekens, 15-Jul-2018.) (New usage is discouraged.)
⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ {𝑦 ∈ ⦋𝑥 / 𝑚⦌𝑀 ∣ 𝜑})    &   ⊢ (𝑋 ∈ 𝑉 → ⦋𝑋 / 𝑚⦌𝑀 ∈ V)    ⇒   ⊢ (𝑌 ∈ (𝐹‘𝑋) → (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ ⦋𝑋 / 𝑚⦌𝑀))
Theorem	elfvmptrab 6958*	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 6959*	Value of a function given by an ordered-pair class abstraction, outside of its domain. (Contributed by NM, 28-Mar-2008.)
⊢ 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}    ⇒   ⊢ (¬ 𝐵 ∈ 𝐴 → (𝐹‘𝐵) = ∅)
Theorem	fvmptndm 6960*	Value of a function given by the maps-to notation, outside of its domain. (Contributed by AV, 31-Dec-2020.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    ⇒   ⊢ (¬ 𝑋 ∈ 𝐴 → (𝐹‘𝑋) = ∅)
Theorem	fvmptrabfv 6961*	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 6962*	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 6963*	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 6964*	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 6965*	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 6966*	Derive equality of functions from equality of their values. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) → (𝐹 = 𝐺 ↔ (𝐵 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝐵 ∧ (𝐹‘𝑥) = (𝐺‘𝑥)))))
Theorem	eqfnfvd 6967*	Deduction for equality of functions. (Contributed by Mario Carneiro, 24-Jul-2014.)
⊢ (𝜑 → 𝐹 Fn 𝐴)    &   ⊢ (𝜑 → 𝐺 Fn 𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = (𝐺‘𝑥))    ⇒   ⊢ (𝜑 → 𝐹 = 𝐺)
Theorem	eqfnfv2f 6968*	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 6964 uses bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 29-Jan-2004.)
⊢ Ⅎ𝑥𝐹    &   ⊢ Ⅎ𝑥𝐺    ⇒   ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥)))
Theorem	eqfunfv 6969*	Equality of functions is determined by their values. (Contributed by Scott Fenton, 19-Jun-2011.)
⊢ ((Fun 𝐹 ∧ Fun 𝐺) → (𝐹 = 𝐺 ↔ (dom 𝐹 = dom 𝐺 ∧ ∀𝑥 ∈ dom 𝐹(𝐹‘𝑥) = (𝐺‘𝑥))))
Theorem	eqfnun 6970	Two functions on 𝐴 ∪ 𝐵 are equal if and only if they have equal restrictions to both 𝐴 and 𝐵. (Contributed by Jeff Madsen, 19-Jun-2011.)
⊢ ((𝐹 Fn (𝐴 ∪ 𝐵) ∧ 𝐺 Fn (𝐴 ∪ 𝐵)) → (𝐹 = 𝐺 ↔ ((𝐹 ↾ 𝐴) = (𝐺 ↾ 𝐴) ∧ (𝐹 ↾ 𝐵) = (𝐺 ↾ 𝐵))))
Theorem	fvreseq0 6971*	Equality of restricted functions is determined by their values (for functions with different domains). (Contributed by AV, 6-Jan-2019.)
⊢ (((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐶) ∧ (𝐵 ⊆ 𝐴 ∧ 𝐵 ⊆ 𝐶)) → ((𝐹 ↾ 𝐵) = (𝐺 ↾ 𝐵) ↔ ∀𝑥 ∈ 𝐵 (𝐹‘𝑥) = (𝐺‘𝑥)))
Theorem	fvreseq1 6972*	Equality of a function restricted to the domain of another function. (Contributed by AV, 6-Jan-2019.)
⊢ (((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) ∧ 𝐵 ⊆ 𝐴) → ((𝐹 ↾ 𝐵) = 𝐺 ↔ ∀𝑥 ∈ 𝐵 (𝐹‘𝑥) = (𝐺‘𝑥)))
Theorem	fvreseq 6973*	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 6974*	A function with a given domain is a mapping defined by its function values. (Contributed by AV, 1-Mar-2019.)
⊢ (𝜑 → 𝑀 Fn 𝐴)    &   ⊢ (𝑖 = 𝑎 → 𝐷 = 𝐶)    &   ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → 𝐷 ∈ 𝑈)    &   ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → 𝐶 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑀 = (𝑎 ∈ 𝐴 ↦ 𝐶) ↔ ∀𝑖 ∈ 𝐴 (𝑀‘𝑖) = 𝐷))
Theorem	fndmdif 6975*	Two ways to express the locus of differences between two functions. (Contributed by Stefan O'Rear, 17-Jan-2015.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → dom (𝐹 ∖ 𝐺) = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) ≠ (𝐺‘𝑥)})
Theorem	fndmdifcom 6976	The difference set between two functions is commutative. (Contributed by Stefan O'Rear, 17-Jan-2015.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → dom (𝐹 ∖ 𝐺) = dom (𝐺 ∖ 𝐹))
Theorem	fndmdifeq0 6977	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 6978*	Two ways to express the locus of equality between two functions. (Contributed by Stefan O'Rear, 17-Jan-2015.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → dom (𝐹 ∩ 𝐺) = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) = (𝐺‘𝑥)})
Theorem	fneqeql 6979	Two functions are equal iff their equalizer is the whole domain. (Contributed by Stefan O'Rear, 7-Mar-2015.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ dom (𝐹 ∩ 𝐺) = 𝐴))
Theorem	fneqeql2 6980	Two functions are equal iff their equalizer contains the whole domain. (Contributed by Stefan O'Rear, 9-Mar-2015.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ 𝐴 ⊆ dom (𝐹 ∩ 𝐺)))
Theorem	fnreseql 6981	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 6982*	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 6983	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 6984	Two ways to say that 𝐴 is in the domain of 𝐹. (Contributed by Mario Carneiro, 1-May-2014.)
⊢ (Fun 𝐹 → (𝐴 ∈ dom 𝐹 ↔ 𝐴𝐹(𝐹‘𝐴)))
Theorem	fvimacnvi 6985	A member of a preimage is a function value argument. (Contributed by NM, 4-May-2007.)
⊢ ((Fun 𝐹 ∧ 𝐴 ∈ (◡𝐹 “ 𝐵)) → (𝐹‘𝐴) ∈ 𝐵)
Theorem	fvimacnv 6986	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 6564 could probably be strengthened to a biconditional." (Contributed by Raph Levien, 20-Nov-2006.)
⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → ((𝐹‘𝐴) ∈ 𝐵 ↔ 𝐴 ∈ (◡𝐹 “ 𝐵)))
Theorem	funimass3 6987	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 6986 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 6988*	A subclass of a preimage in terms of function values. (Contributed by NM, 15-May-2007.)
⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹) → (𝐴 ⊆ (◡𝐹 “ 𝐵) ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))
Theorem	funconstss 6989*	Two ways of specifying that a function is constant on a subdomain. (Contributed by NM, 8-Mar-2007.)
⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹) → (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵 ↔ 𝐴 ⊆ (◡𝐹 “ {𝐵})))
Theorem	fvimacnvALT 6990	Alternate proof of fvimacnv 6986, based on funimass3 6987. If funimass3 6987 is ever proved directly, as opposed to using funimacnv 6562 pointwise, then the proof of funimacnv 6562 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 6991	Membership in the preimage of a set under a function. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) ↔ (𝐵 ∈ 𝐴 ∧ (𝐹‘𝐵) ∈ 𝐶)))
Theorem	elpreimad 6992	Membership in the preimage of a set under a function. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝜑 → 𝐹 Fn 𝐴)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐴)    &   ⊢ (𝜑 → (𝐹‘𝐵) ∈ 𝐶)    ⇒   ⊢ (𝜑 → 𝐵 ∈ (◡𝐹 “ 𝐶))
Theorem	fniniseg 6993	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 6994*	Inverse images under functions expressed as abstractions. (Contributed by Stefan O'Rear, 1-Feb-2015.)
⊢ (𝐹 Fn 𝐴 → (◡𝐹 “ 𝐵) = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) ∈ 𝐵})
Theorem	fniniseg2 6995*	Inverse point images under functions expressed as abstractions. (Contributed by Stefan O'Rear, 1-Feb-2015.)
⊢ (𝐹 Fn 𝐴 → (◡𝐹 “ {𝐵}) = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) = 𝐵})
Theorem	unpreima 6996	Preimage of a union. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (Fun 𝐹 → (◡𝐹 “ (𝐴 ∪ 𝐵)) = ((◡𝐹 “ 𝐴) ∪ (◡𝐹 “ 𝐵)))
Theorem	inpreima 6997	Preimage of an intersection. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 14-Jun-2016.)
⊢ (Fun 𝐹 → (◡𝐹 “ (𝐴 ∩ 𝐵)) = ((◡𝐹 “ 𝐴) ∩ (◡𝐹 “ 𝐵)))
Theorem	difpreima 6998	Preimage of a difference. (Contributed by Mario Carneiro, 14-Jun-2016.)
⊢ (Fun 𝐹 → (◡𝐹 “ (𝐴 ∖ 𝐵)) = ((◡𝐹 “ 𝐴) ∖ (◡𝐹 “ 𝐵)))
Theorem	respreima 6999	The preimage of a restricted function. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (Fun 𝐹 → (◡(𝐹 ↾ 𝐵) “ 𝐴) = ((◡𝐹 “ 𝐴) ∩ 𝐵))
Theorem	cnvimainrn 7000	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 𝐹 ∩ 𝐴)) = (◡𝐹 “ 𝐴))