P. 60 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 5901-6000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	reloprab 5901*	An operation class abstraction is a relation. (Contributed by NM, 16-Jun-2004.)
⊢ Rel {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}
Theorem	nfoprab1 5902	The abstraction variables in an operation class abstraction are not free. (Contributed by NM, 25-Apr-1995.) (Revised by David Abernethy, 19-Jun-2012.)
⊢ Ⅎ𝑥{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}
Theorem	nfoprab2 5903	The abstraction variables in an operation class abstraction are not free. (Contributed by NM, 25-Apr-1995.) (Revised by David Abernethy, 30-Jul-2012.)
⊢ Ⅎ𝑦{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}
Theorem	nfoprab3 5904	The abstraction variables in an operation class abstraction are not free. (Contributed by NM, 22-Aug-2013.)
⊢ Ⅎ𝑧{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}
Theorem	nfoprab 5905*	Bound-variable hypothesis builder for an operation class abstraction. (Contributed by NM, 22-Aug-2013.)
⊢ Ⅎ𝑤𝜑    ⇒   ⊢ Ⅎ𝑤{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}
Theorem	oprabbid 5906*	Equivalent wff's yield equal operation class abstractions (deduction form). (Contributed by NM, 21-Feb-2004.) (Revised by Mario Carneiro, 24-Jun-2014.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑧𝜑    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜒})
Theorem	oprabbidv 5907*	Equivalent wff's yield equal operation class abstractions (deduction form). (Contributed by NM, 21-Feb-2004.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜒})
Theorem	oprabbii 5908*	Equivalent wff's yield equal operation class abstractions. (Contributed by NM, 28-May-1995.) (Revised by David Abernethy, 19-Jun-2012.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓}
Theorem	ssoprab2 5909	Equivalence of ordered pair abstraction subclass and implication. Compare ssopab2 4260. (Contributed by FL, 6-Nov-2013.) (Proof shortened by Mario Carneiro, 11-Dec-2016.)
⊢ (∀𝑥∀𝑦∀𝑧(𝜑 → 𝜓) → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} ⊆ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓})
Theorem	ssoprab2b 5910	Equivalence of ordered pair abstraction subclass and implication. Compare ssopab2b 4261. (Contributed by FL, 6-Nov-2013.) (Proof shortened by Mario Carneiro, 11-Dec-2016.)
⊢ ({⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} ⊆ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} ↔ ∀𝑥∀𝑦∀𝑧(𝜑 → 𝜓))
Theorem	eqoprab2b 5911	Equivalence of ordered pair abstraction subclass and biconditional. Compare eqopab2b 4264. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ ({⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} ↔ ∀𝑥∀𝑦∀𝑧(𝜑 ↔ 𝜓))
Theorem	mpoeq123 5912*	An equality theorem for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.) (Revised by Mario Carneiro, 19-Mar-2015.)
⊢ ((𝐴 = 𝐷 ∧ ∀𝑥 ∈ 𝐴 (𝐵 = 𝐸 ∧ ∀𝑦 ∈ 𝐵 𝐶 = 𝐹)) → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐷, 𝑦 ∈ 𝐸 ↦ 𝐹))
Theorem	mpoeq12 5913*	An equality theorem for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐸) = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝐸))
Theorem	mpoeq123dva 5914*	An equality deduction for the maps-to notation. (Contributed by Mario Carneiro, 26-Jan-2017.)
⊢ (𝜑 → 𝐴 = 𝐷)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐸)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝐶 = 𝐹)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐷, 𝑦 ∈ 𝐸 ↦ 𝐹))
Theorem	mpoeq123dv 5915*	An equality deduction for the maps-to notation. (Contributed by NM, 12-Sep-2011.)
⊢ (𝜑 → 𝐴 = 𝐷)    &   ⊢ (𝜑 → 𝐵 = 𝐸)    &   ⊢ (𝜑 → 𝐶 = 𝐹)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐷, 𝑦 ∈ 𝐸 ↦ 𝐹))
Theorem	mpoeq123i 5916	An equality inference for the maps-to notation. (Contributed by NM, 15-Jul-2013.)
⊢ 𝐴 = 𝐷    &   ⊢ 𝐵 = 𝐸    &   ⊢ 𝐶 = 𝐹    ⇒   ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐷, 𝑦 ∈ 𝐸 ↦ 𝐹)
Theorem	mpoeq3dva 5917*	Slightly more general equality inference for the maps-to notation. (Contributed by NM, 17-Oct-2013.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷))
Theorem	mpoeq3ia 5918	An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐶 = 𝐷)    ⇒   ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷)
Theorem	mpoeq3dv 5919*	An equality deduction for the maps-to notation restricted to the value of the operation. (Contributed by SO, 16-Jul-2018.)
⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷))
Theorem	nfmpo1 5920	Bound-variable hypothesis builder for an operation in maps-to notation. (Contributed by NM, 27-Aug-2013.)
⊢ Ⅎ𝑥(𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)
Theorem	nfmpo2 5921	Bound-variable hypothesis builder for an operation in maps-to notation. (Contributed by NM, 27-Aug-2013.)
⊢ Ⅎ𝑦(𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)
Theorem	nfmpo 5922*	Bound-variable hypothesis builder for the maps-to notation. (Contributed by NM, 20-Feb-2013.)
⊢ Ⅎ𝑧𝐴    &   ⊢ Ⅎ𝑧𝐵    &   ⊢ Ⅎ𝑧𝐶    ⇒   ⊢ Ⅎ𝑧(𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)
Theorem	mpo0 5923	A mapping operation with empty domain. (Contributed by Stefan O'Rear, 29-Jan-2015.) (Revised by Mario Carneiro, 15-May-2015.)
⊢ (𝑥 ∈ ∅, 𝑦 ∈ 𝐵 ↦ 𝐶) = ∅
Theorem	oprab4 5924*	Two ways to state the domain of an operation. (Contributed by FL, 24-Jan-2010.)
⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ (⟨𝑥, 𝑦⟩ ∈ (𝐴 × 𝐵) ∧ 𝜑)} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)}
Theorem	cbvoprab1 5925*	Rule used to change first bound variable in an operation abstraction, using implicit substitution. (Contributed by NM, 20-Dec-2008.) (Revised by Mario Carneiro, 5-Dec-2016.)
⊢ Ⅎ𝑤𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑤 → (𝜑 ↔ 𝜓))    ⇒   ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {⟨⟨𝑤, 𝑦⟩, 𝑧⟩ ∣ 𝜓}
Theorem	cbvoprab2 5926*	Change the second bound variable in an operation abstraction. (Contributed by Jeff Madsen, 11-Jun-2010.) (Revised by Mario Carneiro, 11-Dec-2016.)
⊢ Ⅎ𝑤𝜑    &   ⊢ Ⅎ𝑦𝜓    &   ⊢ (𝑦 = 𝑤 → (𝜑 ↔ 𝜓))    ⇒   ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {⟨⟨𝑥, 𝑤⟩, 𝑧⟩ ∣ 𝜓}
Theorem	cbvoprab12 5927*	Rule used to change first two bound variables in an operation abstraction, using implicit substitution. (Contributed by NM, 21-Feb-2004.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
⊢ Ⅎ𝑤𝜑    &   ⊢ Ⅎ𝑣𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ Ⅎ𝑦𝜓    &   ⊢ ((𝑥 = 𝑤 ∧ 𝑦 = 𝑣) → (𝜑 ↔ 𝜓))    ⇒   ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {⟨⟨𝑤, 𝑣⟩, 𝑧⟩ ∣ 𝜓}
Theorem	cbvoprab12v 5928*	Rule used to change first two bound variables in an operation abstraction, using implicit substitution. (Contributed by NM, 8-Oct-2004.)
⊢ ((𝑥 = 𝑤 ∧ 𝑦 = 𝑣) → (𝜑 ↔ 𝜓))    ⇒   ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {⟨⟨𝑤, 𝑣⟩, 𝑧⟩ ∣ 𝜓}
Theorem	cbvoprab3 5929*	Rule used to change the third bound variable in an operation abstraction, using implicit substitution. (Contributed by NM, 22-Aug-2013.)
⊢ Ⅎ𝑤𝜑    &   ⊢ Ⅎ𝑧𝜓    &   ⊢ (𝑧 = 𝑤 → (𝜑 ↔ 𝜓))    ⇒   ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∣ 𝜓}
Theorem	cbvoprab3v 5930*	Rule used to change the third bound variable in an operation abstraction, using implicit substitution. (Contributed by NM, 8-Oct-2004.) (Revised by David Abernethy, 19-Jun-2012.)
⊢ (𝑧 = 𝑤 → (𝜑 ↔ 𝜓))    ⇒   ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∣ 𝜓}
Theorem	cbvmpox 5931*	Rule to change the bound variable in a maps-to function, using implicit substitution. This version of cbvmpo 5932 allows 𝐵 to be a function of 𝑥. (Contributed by NM, 29-Dec-2014.)
⊢ Ⅎ𝑧𝐵    &   ⊢ Ⅎ𝑥𝐷    &   ⊢ Ⅎ𝑧𝐶    &   ⊢ Ⅎ𝑤𝐶    &   ⊢ Ⅎ𝑥𝐸    &   ⊢ Ⅎ𝑦𝐸    &   ⊢ (𝑥 = 𝑧 → 𝐵 = 𝐷)    &   ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝐶 = 𝐸)    ⇒   ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑧 ∈ 𝐴, 𝑤 ∈ 𝐷 ↦ 𝐸)
Theorem	cbvmpo 5932*	Rule to change the bound variable in a maps-to function, using implicit substitution. (Contributed by NM, 17-Dec-2013.)
⊢ Ⅎ𝑧𝐶    &   ⊢ Ⅎ𝑤𝐶    &   ⊢ Ⅎ𝑥𝐷    &   ⊢ Ⅎ𝑦𝐷    &   ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝐶 = 𝐷)    ⇒   ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑧 ∈ 𝐴, 𝑤 ∈ 𝐵 ↦ 𝐷)
Theorem	cbvmpov 5933*	Rule to change the bound variable in a maps-to function, using implicit substitution. With a longer proof analogous to cbvmpt 4084, some distinct variable requirements could be eliminated. (Contributed by NM, 11-Jun-2013.)
⊢ (𝑥 = 𝑧 → 𝐶 = 𝐸)    &   ⊢ (𝑦 = 𝑤 → 𝐸 = 𝐷)    ⇒   ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑧 ∈ 𝐴, 𝑤 ∈ 𝐵 ↦ 𝐷)
Theorem	dmoprab 5934*	The domain of an operation class abstraction. (Contributed by NM, 17-Mar-1995.) (Revised by David Abernethy, 19-Jun-2012.)
⊢ dom {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧𝜑}
Theorem	dmoprabss 5935*	The domain of an operation class abstraction. (Contributed by NM, 24-Aug-1995.)
⊢ dom {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)} ⊆ (𝐴 × 𝐵)
Theorem	rnoprab 5936*	The range of an operation class abstraction. (Contributed by NM, 30-Aug-2004.) (Revised by David Abernethy, 19-Apr-2013.)
⊢ ran {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥∃𝑦𝜑}
Theorem	rnoprab2 5937*	The range of a restricted operation class abstraction. (Contributed by Scott Fenton, 21-Mar-2012.)
⊢ ran {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)} = {𝑧 ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑}
Theorem	reldmoprab 5938*	The domain of an operation class abstraction is a relation. (Contributed by NM, 17-Mar-1995.)
⊢ Rel dom {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}
Theorem	oprabss 5939*	Structure of an operation class abstraction. (Contributed by NM, 28-Nov-2006.)
⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} ⊆ ((V × V) × V)
Theorem	eloprabga 5940*	The law of concretion for operation class abstraction. Compare elopab 4243. (Contributed by NM, 14-Sep-1999.) (Unnecessary distinct variable restrictions were removed by David Abernethy, 19-Jun-2012.) (Revised by Mario Carneiro, 19-Dec-2013.)
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (⟨⟨𝐴, 𝐵⟩, 𝐶⟩ ∈ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} ↔ 𝜓))
Theorem	eloprabg 5941*	The law of concretion for operation class abstraction. Compare elopab 4243. (Contributed by NM, 14-Sep-1999.) (Revised by David Abernethy, 19-Jun-2012.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑧 = 𝐶 → (𝜒 ↔ 𝜃))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (⟨⟨𝐴, 𝐵⟩, 𝐶⟩ ∈ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} ↔ 𝜃))
Theorem	ssoprab2i 5942*	Inference of operation class abstraction subclass from implication. (Contributed by NM, 11-Nov-1995.) (Revised by David Abernethy, 19-Jun-2012.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} ⊆ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓}
Theorem	mpov 5943*	Operation with universal domain in maps-to notation. (Contributed by NM, 16-Aug-2013.)
⊢ (𝑥 ∈ V, 𝑦 ∈ V ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝑧 = 𝐶}
Theorem	mpomptx 5944*	Express a two-argument function as a one-argument function, or vice-versa. In this version 𝐵(𝑥) is not assumed to be constant w.r.t 𝑥. (Contributed by Mario Carneiro, 29-Dec-2014.)
⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → 𝐶 = 𝐷)    ⇒   ⊢ (𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷)
Theorem	mpompt 5945*	Express a two-argument function as a one-argument function, or vice-versa. (Contributed by Mario Carneiro, 17-Dec-2013.) (Revised by Mario Carneiro, 29-Dec-2014.)
⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → 𝐶 = 𝐷)    ⇒   ⊢ (𝑧 ∈ (𝐴 × 𝐵) ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷)
Theorem	mpodifsnif 5946	A mapping with two arguments with the first argument from a difference set with a singleton and a conditional as result. (Contributed by AV, 13-Feb-2019.)
⊢ (𝑖 ∈ (𝐴 ∖ {𝑋}), 𝑗 ∈ 𝐵 ↦ if(𝑖 = 𝑋, 𝐶, 𝐷)) = (𝑖 ∈ (𝐴 ∖ {𝑋}), 𝑗 ∈ 𝐵 ↦ 𝐷)
Theorem	mposnif 5947	A mapping with two arguments with the first argument from a singleton and a conditional as result. (Contributed by AV, 14-Feb-2019.)
⊢ (𝑖 ∈ {𝑋}, 𝑗 ∈ 𝐵 ↦ if(𝑖 = 𝑋, 𝐶, 𝐷)) = (𝑖 ∈ {𝑋}, 𝑗 ∈ 𝐵 ↦ 𝐶)
Theorem	fconstmpo 5948*	Representation of a constant operation using the mapping operation. (Contributed by SO, 11-Jul-2018.)
⊢ ((𝐴 × 𝐵) × {𝐶}) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)
Theorem	resoprab 5949*	Restriction of an operation class abstraction. (Contributed by NM, 10-Feb-2007.)
⊢ ({⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} ↾ (𝐴 × 𝐵)) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)}
Theorem	resoprab2 5950*	Restriction of an operator abstraction. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ ((𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐵) → ({⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)} ↾ (𝐶 × 𝐷)) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) ∧ 𝜑)})
Theorem	resmpo 5951*	Restriction of the mapping operation. (Contributed by Mario Carneiro, 17-Dec-2013.)
⊢ ((𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐵) → ((𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐸) ↾ (𝐶 × 𝐷)) = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝐸))
Theorem	funoprabg 5952*	"At most one" is a sufficient condition for an operation class abstraction to be a function. (Contributed by NM, 28-Aug-2007.)
⊢ (∀𝑥∀𝑦∃*𝑧𝜑 → Fun {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑})
Theorem	funoprab 5953*	"At most one" is a sufficient condition for an operation class abstraction to be a function. (Contributed by NM, 17-Mar-1995.)
⊢ ∃*𝑧𝜑    ⇒   ⊢ Fun {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}
Theorem	fnoprabg 5954*	Functionality and domain of an operation class abstraction. (Contributed by NM, 28-Aug-2007.)
⊢ (∀𝑥∀𝑦(𝜑 → ∃!𝑧𝜓) → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ (𝜑 ∧ 𝜓)} Fn {⟨𝑥, 𝑦⟩ ∣ 𝜑})
Theorem	mpofun 5955*	The maps-to notation for an operation is always a function. (Contributed by Scott Fenton, 21-Mar-2012.)
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)    ⇒   ⊢ Fun 𝐹
Theorem	fnoprab 5956*	Functionality and domain of an operation class abstraction. (Contributed by NM, 15-May-1995.)
⊢ (𝜑 → ∃!𝑧𝜓)    ⇒   ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ (𝜑 ∧ 𝜓)} Fn {⟨𝑥, 𝑦⟩ ∣ 𝜑}
Theorem	ffnov 5957*	An operation maps to a class to which all values belong. (Contributed by NM, 7-Feb-2004.)
⊢ (𝐹:(𝐴 × 𝐵)⟶𝐶 ↔ (𝐹 Fn (𝐴 × 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥𝐹𝑦) ∈ 𝐶))
Theorem	fovcl 5958	Closure law for an operation. (Contributed by NM, 19-Apr-2007.)
⊢ 𝐹:(𝑅 × 𝑆)⟶𝐶    ⇒   ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) → (𝐴𝐹𝐵) ∈ 𝐶)
Theorem	eqfnov 5959*	Equality of two operations is determined by their values. (Contributed by NM, 1-Sep-2005.)
⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐺 Fn (𝐶 × 𝐷)) → (𝐹 = 𝐺 ↔ ((𝐴 × 𝐵) = (𝐶 × 𝐷) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥𝐹𝑦) = (𝑥𝐺𝑦))))
Theorem	eqfnov2 5960*	Two operators with the same domain are equal iff their values at each point in the domain are equal. (Contributed by Jeff Madsen, 7-Jun-2010.)
⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐺 Fn (𝐴 × 𝐵)) → (𝐹 = 𝐺 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥𝐹𝑦) = (𝑥𝐺𝑦)))
Theorem	fnovim 5961*	Representation of a function in terms of its values. (Contributed by Jim Kingdon, 16-Jan-2019.)
⊢ (𝐹 Fn (𝐴 × 𝐵) → 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ (𝑥𝐹𝑦)))
Theorem	mpo2eqb 5962*	Bidirectional equality theorem for a mapping abstraction. Equivalent to eqfnov2 5960. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝑉 → ((𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 = 𝐷))
Theorem	rnmpo 5963*	The range of an operation given by the maps-to notation. (Contributed by FL, 20-Jun-2011.)
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)    ⇒   ⊢ ran 𝐹 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = 𝐶}
Theorem	reldmmpo 5964*	The domain of an operation defined by maps-to notation is a relation. (Contributed by Stefan O'Rear, 27-Nov-2014.)
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)    ⇒   ⊢ Rel dom 𝐹
Theorem	elrnmpog 5965*	Membership in the range of an operation class abstraction. (Contributed by NM, 27-Aug-2007.) (Revised by Mario Carneiro, 31-Aug-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)    ⇒   ⊢ (𝐷 ∈ 𝑉 → (𝐷 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝐷 = 𝐶))
Theorem	elrnmpo 5966*	Membership in the range of an operation class abstraction. (Contributed by NM, 1-Aug-2004.) (Revised by Mario Carneiro, 31-Aug-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)    &   ⊢ 𝐶 ∈ V    ⇒   ⊢ (𝐷 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝐷 = 𝐶)
Theorem	ralrnmpo 5967*	A restricted quantifier over an image set. (Contributed by Mario Carneiro, 1-Sep-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)    &   ⊢ (𝑧 = 𝐶 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝑉 → (∀𝑧 ∈ ran 𝐹𝜑 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓))
Theorem	rexrnmpo 5968*	A restricted quantifier over an image set. (Contributed by Mario Carneiro, 1-Sep-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)    &   ⊢ (𝑧 = 𝐶 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝑉 → (∃𝑧 ∈ ran 𝐹𝜑 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓))
Theorem	ovid 5969*	The value of an operation class abstraction. (Contributed by NM, 16-May-1995.) (Revised by David Abernethy, 19-Jun-2012.)
⊢ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) → ∃!𝑧𝜑)    &   ⊢ 𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) ∧ 𝜑)}    ⇒   ⊢ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) → ((𝑥𝐹𝑦) = 𝑧 ↔ 𝜑))
Theorem	ovidig 5970*	The value of an operation class abstraction. Compare ovidi 5971. The condition (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) is been removed. (Contributed by Mario Carneiro, 29-Dec-2014.)
⊢ ∃*𝑧𝜑    &   ⊢ 𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}    ⇒   ⊢ (𝜑 → (𝑥𝐹𝑦) = 𝑧)
Theorem	ovidi 5971*	The value of an operation class abstraction (weak version). (Contributed by Mario Carneiro, 29-Dec-2014.)
⊢ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) → ∃*𝑧𝜑)    &   ⊢ 𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) ∧ 𝜑)}    ⇒   ⊢ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) → (𝜑 → (𝑥𝐹𝑦) = 𝑧))
Theorem	ov 5972*	The value of an operation class abstraction. (Contributed by NM, 16-May-1995.) (Revised by David Abernethy, 19-Jun-2012.)
⊢ 𝐶 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑧 = 𝐶 → (𝜒 ↔ 𝜃))    &   ⊢ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) → ∃!𝑧𝜑)    &   ⊢ 𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) ∧ 𝜑)}    ⇒   ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) → ((𝐴𝐹𝐵) = 𝐶 ↔ 𝜃))
Theorem	ovigg 5973*	The value of an operation class abstraction. Compare ovig 5974. The condition (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) is been removed. (Contributed by FL, 24-Mar-2007.) (Revised by Mario Carneiro, 19-Dec-2013.)
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) → (𝜑 ↔ 𝜓))    &   ⊢ ∃*𝑧𝜑    &   ⊢ 𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝜓 → (𝐴𝐹𝐵) = 𝐶))
Theorem	ovig 5974*	The value of an operation class abstraction (weak version). (Unnecessary distinct variable restrictions were removed by David Abernethy, 19-Jun-2012.) (Contributed by NM, 14-Sep-1999.) (Revised by Mario Carneiro, 19-Dec-2013.)
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) → (𝜑 ↔ 𝜓))    &   ⊢ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) → ∃*𝑧𝜑)    &   ⊢ 𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) ∧ 𝜑)}    ⇒   ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝐷) → (𝜓 → (𝐴𝐹𝐵) = 𝐶))
Theorem	ovmpt4g 5975*	Value of a function given by the maps-to notation. (This is the operation analog of fvmpt2 5579.) (Contributed by NM, 21-Feb-2004.) (Revised by Mario Carneiro, 1-Sep-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)    ⇒   ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉) → (𝑥𝐹𝑦) = 𝐶)
Theorem	ovmpos 5976*	Value of a function given by the maps-to notation, expressed using explicit substitution. (Contributed by Mario Carneiro, 30-Apr-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)    ⇒   ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ ⦋𝐴 / 𝑥⦌⦋𝐵 / 𝑦⦌𝑅 ∈ 𝑉) → (𝐴𝐹𝐵) = ⦋𝐴 / 𝑥⦌⦋𝐵 / 𝑦⦌𝑅)
Theorem	ov2gf 5977*	The value of an operation class abstraction. A version of ovmpog 5987 using bound-variable hypotheses. (Contributed by NM, 17-Aug-2006.) (Revised by Mario Carneiro, 19-Dec-2013.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑦𝐵    &   ⊢ Ⅎ𝑥𝐺    &   ⊢ Ⅎ𝑦𝑆    &   ⊢ (𝑥 = 𝐴 → 𝑅 = 𝐺)    &   ⊢ (𝑦 = 𝐵 → 𝐺 = 𝑆)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)    ⇒   ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝑆 ∈ 𝐻) → (𝐴𝐹𝐵) = 𝑆)
Theorem	ovmpodxf 5978*	Value of an operation given by a maps-to rule, deduction form. (Contributed by Mario Carneiro, 29-Dec-2014.)
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅))    &   ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝑅 = 𝑆)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐷 = 𝐿)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐶)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐿)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑋)    &   ⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ Ⅎ𝑥𝑆    &   ⊢ Ⅎ𝑦𝑆    ⇒   ⊢ (𝜑 → (𝐴𝐹𝐵) = 𝑆)
Theorem	ovmpodx 5979*	Value of an operation given by a maps-to rule, deduction form. (Contributed by Mario Carneiro, 29-Dec-2014.)
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅))    &   ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝑅 = 𝑆)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐷 = 𝐿)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐶)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐿)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑋)    ⇒   ⊢ (𝜑 → (𝐴𝐹𝐵) = 𝑆)
Theorem	ovmpod 5980*	Value of an operation given by a maps-to rule, deduction form. (Contributed by Mario Carneiro, 7-Dec-2014.)
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅))    &   ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝑅 = 𝑆)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐶)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑋)    ⇒   ⊢ (𝜑 → (𝐴𝐹𝐵) = 𝑆)
Theorem	ovmpox 5981*	The value of an operation class abstraction. Variant of ovmpoga 5982 which does not require 𝐷 and 𝑥 to be distinct. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 20-Dec-2013.)
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → 𝑅 = 𝑆)    &   ⊢ (𝑥 = 𝐴 → 𝐷 = 𝐿)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)    ⇒   ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐿 ∧ 𝑆 ∈ 𝐻) → (𝐴𝐹𝐵) = 𝑆)
Theorem	ovmpoga 5982*	Value of an operation given by a maps-to rule. (Contributed by Mario Carneiro, 19-Dec-2013.)
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → 𝑅 = 𝑆)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)    ⇒   ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝑆 ∈ 𝐻) → (𝐴𝐹𝐵) = 𝑆)
Theorem	ovmpoa 5983*	Value of an operation given by a maps-to rule. (Contributed by NM, 19-Dec-2013.)
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → 𝑅 = 𝑆)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)    &   ⊢ 𝑆 ∈ V    ⇒   ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴𝐹𝐵) = 𝑆)
Theorem	ovmpodf 5984*	Alternate deduction version of ovmpo 5988, suitable for iteration. (Contributed by Mario Carneiro, 7-Jan-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝐶)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 ∈ 𝐷)    &   ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝑅 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → ((𝐴𝐹𝐵) = 𝑅 → 𝜓))    &   ⊢ Ⅎ𝑥𝐹    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ Ⅎ𝑦𝐹    &   ⊢ Ⅎ𝑦𝜓    ⇒   ⊢ (𝜑 → (𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) → 𝜓))
Theorem	ovmpodv 5985*	Alternate deduction version of ovmpo 5988, suitable for iteration. (Contributed by Mario Carneiro, 7-Jan-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝐶)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 ∈ 𝐷)    &   ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝑅 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → ((𝐴𝐹𝐵) = 𝑅 → 𝜓))    ⇒   ⊢ (𝜑 → (𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) → 𝜓))
Theorem	ovmpodv2 5986*	Alternate deduction version of ovmpo 5988, suitable for iteration. (Contributed by Mario Carneiro, 7-Jan-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝐶)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 ∈ 𝐷)    &   ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝑅 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝑅 = 𝑆)    ⇒   ⊢ (𝜑 → (𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) → (𝐴𝐹𝐵) = 𝑆))
Theorem	ovmpog 5987*	Value of an operation given by a maps-to rule. Special case. (Contributed by NM, 14-Sep-1999.) (Revised by David Abernethy, 19-Jun-2012.)
⊢ (𝑥 = 𝐴 → 𝑅 = 𝐺)    &   ⊢ (𝑦 = 𝐵 → 𝐺 = 𝑆)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)    ⇒   ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝑆 ∈ 𝐻) → (𝐴𝐹𝐵) = 𝑆)
Theorem	ovmpo 5988*	Value of an operation given by a maps-to rule. Special case. (Contributed by NM, 16-May-1995.) (Revised by David Abernethy, 19-Jun-2012.)
⊢ (𝑥 = 𝐴 → 𝑅 = 𝐺)    &   ⊢ (𝑦 = 𝐵 → 𝐺 = 𝑆)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)    &   ⊢ 𝑆 ∈ V    ⇒   ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴𝐹𝐵) = 𝑆)
Theorem	ovi3 5989*	The value of an operation class abstraction. Special case. (Contributed by NM, 28-May-1995.) (Revised by Mario Carneiro, 29-Dec-2014.)
⊢ (((𝐴 ∈ 𝐻 ∧ 𝐵 ∈ 𝐻) ∧ (𝐶 ∈ 𝐻 ∧ 𝐷 ∈ 𝐻)) → 𝑆 ∈ (𝐻 × 𝐻))    &   ⊢ (((𝑤 = 𝐴 ∧ 𝑣 = 𝐵) ∧ (𝑢 = 𝐶 ∧ 𝑓 = 𝐷)) → 𝑅 = 𝑆)    &   ⊢ 𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ (𝐻 × 𝐻) ∧ 𝑦 ∈ (𝐻 × 𝐻)) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = 𝑅))}    ⇒   ⊢ (((𝐴 ∈ 𝐻 ∧ 𝐵 ∈ 𝐻) ∧ (𝐶 ∈ 𝐻 ∧ 𝐷 ∈ 𝐻)) → (⟨𝐴, 𝐵⟩𝐹⟨𝐶, 𝐷⟩) = 𝑆)
Theorem	ov6g 5990*	The value of an operation class abstraction. Special case. (Contributed by NM, 13-Nov-2006.)
⊢ (⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝐵⟩ → 𝑅 = 𝑆)    &   ⊢ 𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ (⟨𝑥, 𝑦⟩ ∈ 𝐶 ∧ 𝑧 = 𝑅)}    ⇒   ⊢ (((𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐻 ∧ ⟨𝐴, 𝐵⟩ ∈ 𝐶) ∧ 𝑆 ∈ 𝐽) → (𝐴𝐹𝐵) = 𝑆)
Theorem	ovg 5991*	The value of an operation class abstraction. (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑧 = 𝐶 → (𝜒 ↔ 𝜃))    &   ⊢ ((𝜏 ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆)) → ∃!𝑧𝜑)    &   ⊢ 𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) ∧ 𝜑)}    ⇒   ⊢ ((𝜏 ∧ (𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝐷)) → ((𝐴𝐹𝐵) = 𝐶 ↔ 𝜃))
Theorem	ovres 5992	The value of a restricted operation. (Contributed by FL, 10-Nov-2006.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴(𝐹 ↾ (𝐶 × 𝐷))𝐵) = (𝐴𝐹𝐵))
Theorem	ovresd 5993	Lemma for converting metric theorems to metric space theorems. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑋)    ⇒   ⊢ (𝜑 → (𝐴(𝐷 ↾ (𝑋 × 𝑋))𝐵) = (𝐴𝐷𝐵))
Theorem	oprssov 5994	The value of a member of the domain of a subclass of an operation. (Contributed by NM, 23-Aug-2007.)
⊢ (((Fun 𝐹 ∧ 𝐺 Fn (𝐶 × 𝐷) ∧ 𝐺 ⊆ 𝐹) ∧ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)) → (𝐴𝐹𝐵) = (𝐴𝐺𝐵))
Theorem	fovrn 5995	An operation's value belongs to its codomain. (Contributed by NM, 27-Aug-2006.)
⊢ ((𝐹:(𝑅 × 𝑆)⟶𝐶 ∧ 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) → (𝐴𝐹𝐵) ∈ 𝐶)
Theorem	fovrnda 5996	An operation's value belongs to its codomain. (Contributed by Mario Carneiro, 29-Dec-2016.)
⊢ (𝜑 → 𝐹:(𝑅 × 𝑆)⟶𝐶)    ⇒   ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆)) → (𝐴𝐹𝐵) ∈ 𝐶)
Theorem	fovrnd 5997	An operation's value belongs to its codomain. (Contributed by Mario Carneiro, 29-Dec-2016.)
⊢ (𝜑 → 𝐹:(𝑅 × 𝑆)⟶𝐶)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑅)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝐴𝐹𝐵) ∈ 𝐶)
Theorem	fnrnov 5998*	The range of an operation expressed as a collection of the operation's values. (Contributed by NM, 29-Oct-2006.)
⊢ (𝐹 Fn (𝐴 × 𝐵) → ran 𝐹 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = (𝑥𝐹𝑦)})
Theorem	foov 5999*	An onto mapping of an operation expressed in terms of operation values. (Contributed by NM, 29-Oct-2006.)
⊢ (𝐹:(𝐴 × 𝐵)–onto→𝐶 ↔ (𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ ∀𝑧 ∈ 𝐶 ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = (𝑥𝐹𝑦)))
Theorem	fnovrn 6000	An operation's value belongs to its range. (Contributed by NM, 10-Feb-2007.)
⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵) → (𝐶𝐹𝐷) ∈ ran 𝐹)