P. 56 of Theorem List - New Foundations Explorer

Theorem List for New Foundations Explorer - 5501-5600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	opbr1st 5501	Binary relationship of an ordered pair over 1st. (Contributed by SF, 6-Feb-2015.)
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ (⟨A, B⟩1st C ↔ A = C)
Theorem	opbr2nd 5502	Binary relationship of an ordered pair over 2nd. (Contributed by SF, 6-Feb-2015.)
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ (⟨A, B⟩2nd C ↔ B = C)
Theorem	dfid4 5503	Alternate definition of the identity relationship. (Contributed by SF, 11-Feb-2015.)
⊢ I = ( S ∩ ◡ S )
Theorem	idex 5504	The identity relationship is a set. (Contributed by SF, 11-Feb-2015.)
⊢ I ∈ V
Theorem	1stfo 5505	1st is a mapping from the universe onto the universe. (Contributed by SF, 12-Feb-2015.) (Revised by Scott Fenton, 17-Apr-2021.)
⊢ 1st :V–onto→V
Theorem	2ndfo 5506	2nd is a mapping from the universe onto the universe. (Contributed by SF, 12-Feb-2015.) (Revised by Scott Fenton, 17-Apr-2021.)
⊢ 2nd :V–onto→V
Theorem	dfdm4 5507	Alternate definition of domain. (Contributed by SF, 23-Feb-2015.)
⊢ dom A = (1st “ A)
Theorem	dfrn5 5508	Alternate definition of range. (Contributed by SF, 23-Feb-2015.)
⊢ ran A = (2nd “ A)
Theorem	brswap 5509*	Binary relationship of Swap . (Contributed by SF, 23-Feb-2015.)
⊢ (A Swap B ↔ ∃x∃y(A = ⟨x, y⟩ ∧ B = ⟨y, x⟩))
Theorem	cnvswap 5510	The converse of Swap is Swap . (Contributed by SF, 23-Feb-2015.)
⊢ ◡ Swap = Swap
Theorem	swapf1o 5511	Swap is a bijection over the universe. (Contributed by SF, 23-Feb-2015.) (Revised by Scott Fenton, 17-Apr-2021.)
⊢ Swap :V–1-1-onto→V
Theorem	swapres 5512	Bijection law for restrictions of Swap . (Contributed by SF, 23-Feb-2015.) (Modified by Scott Fenton, 17-Apr-2021.)
⊢ ( Swap ↾ A):A–1-1-onto→◡A
Theorem	xpnedisj 5513	Cross products with non-equal singletons are disjoint. (Contributed by SF, 23-Feb-2015.)
⊢ C ∈ V    &   ⊢ C ≠ D    ⇒   ⊢ ((A × {C}) ∩ (B × {D})) = ∅
Theorem	opfv1st 5514	The value of the 1st function on an ordered pair. (Contributed by SF, 23-Feb-2015.)
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ (1st ‘⟨A, B⟩) = A
Theorem	opfv2nd 5515	The value of the 2nd function on an ordered pair. (Contributed by SF, 23-Feb-2015.)
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ (2nd ‘⟨A, B⟩) = B
Theorem	1st2nd2 5516	Reconstruction of a member of a cross product in terms of its ordered pair components. (Contributed by SF, 20-Oct-2013.)
⊢ (A ∈ (B × C) → A = ⟨(1st ‘A), (2nd ‘A)⟩)
Theorem	fununiq 5517	Implicational form of part of the definition of a function. (Contributed by SF, 24-Feb-2015.)
⊢ ((Fun F ∧ AFB ∧ AFC) → B = C)
Theorem	cnvsi 5518	Calculate the converse of a singleton image. (Contributed by SF, 26-Feb-2015.)
⊢ ◡ SI R = SI ◡R
Theorem	dmsi 5519	Calculate the domain of a singleton image. Theorem X.4.29.I of [Rosser] p. 301. (Contributed by SF, 26-Feb-2015.)
⊢ dom SI R = ℘1dom R
Theorem	funsi 5520	The singleton image of a function is a function. (Contributed by SF, 26-Feb-2015.)
⊢ (Fun F → Fun SI F)
Theorem	rnsi 5521	Calculate the range of a singleton image. Theorem X.4.29.II of [Rosser] p. 302. (Contributed by SF, 26-Feb-2015.)
⊢ ran SI R = ℘1ran R
Theorem	op1std 5522	Extract the first member of an ordered pair. (Contributed by Mario Carneiro, 31-Aug-2015.)
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ (C = ⟨A, B⟩ → (1st ‘C) = A)
Theorem	op2ndd 5523	Extract the second member of an ordered pair. (Contributed by Mario Carneiro, 31-Aug-2015.)
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ (C = ⟨A, B⟩ → (2nd ‘C) = B)
Theorem	dmep 5524	The domain of the epsilon relationship. (Contributed by Scott Fenton, 20-Apr-2021.)
⊢ dom E = V
2.3.8  Operations
Syntax	co 5525	Extend class notation to include the value of an operation F for two arguments A and B. Note that the syntax is simply three class symbols in a row surrounded by parentheses. Since operation values are the only possible class expressions consisting of three class expressions in a row surrounded by parentheses, the syntax is unambiguous.
class (AFB)
Definition	df-ov 5526	Define the value of an operation. Definition of operation value in [Enderton] p. 79. Note that the syntax is simply three class expressions in a row bracketed by parentheses. There are no restrictions of any kind on what those class expressions may be, although only certain kinds of class expressions - a binary operation F and its arguments A and B- will be useful for proving meaningful theorems. This definition is well-defined, although not very meaningful, when classes A and/or B are proper classes (i.e. are not sets). On the other hand, we often find uses for this definition when F is a proper class. F is normally equal to a class of nested ordered pairs of the form defined by df-oprab 5528. (Contributed by SF, 5-Jan-2015.)
⊢ (AFB) = (F ‘⟨A, B⟩)
Syntax	coprab 5527	Extend class notation to include class abstraction (class builder) of nested ordered pairs.
class {⟨⟨x, y⟩, z⟩ ∣ φ}
Definition	df-oprab 5528*	Define the class abstraction (class builder) of a collection of nested ordered pairs (for use in defining operations). This is a special case of Definition 4.16 of [TakeutiZaring] p. 14. Normally x, y, and z are distinct, although the definition doesn't strictly require it. See df-ov 5526 for the value of an operation. The brace notation is called "class abstraction" by Quine; it is also called a "class builder" in the literature. The value of the most common operation class builder is given by ov2 in set.mm. (Contributed by SF, 5-Jan-2015.)
⊢ {⟨⟨x, y⟩, z⟩ ∣ φ} = {w ∣ ∃x∃y∃z(w = ⟨⟨x, y⟩, z⟩ ∧ φ)}
Theorem	oveq 5529	Equality theorem for operation value. (Contributed by set.mm contributors, 28-Feb-1995.)
⊢ (F = G → (AFB) = (AGB))
Theorem	oveq1 5530	Equality theorem for operation value. (Contributed by set.mm contributors, 28-Feb-1995.)
⊢ (A = B → (AFC) = (BFC))
Theorem	oveq2 5531	Equality theorem for operation value. (Contributed by set.mm contributors, 28-Feb-1995.)
⊢ (A = B → (CFA) = (CFB))
Theorem	oveq12 5532	Equality theorem for operation value. (Contributed by set.mm contributors, 16-Jul-1995.)
⊢ ((A = B ∧ C = D) → (AFC) = (BFD))
Theorem	oveq1i 5533	Equality inference for operation value. (Contributed by set.mm contributors, 28-Feb-1995.)
⊢ A = B    ⇒   ⊢ (AFC) = (BFC)
Theorem	oveq2i 5534	Equality inference for operation value. (Contributed by set.mm contributors, 28-Feb-1995.)
⊢ A = B    ⇒   ⊢ (CFA) = (CFB)
Theorem	oveq12i 5535	Equality inference for operation value. (The proof was shortened by Andrew Salmon, 22-Oct-2011.) (Contributed by set.mm contributors, 28-Feb-1995.) (Revised by set.mm contributors, 22-Oct-2011.)
⊢ A = B    &   ⊢ C = D    ⇒   ⊢ (AFC) = (BFD)
Theorem	oveqi 5536	Equality inference for operation value. (Contributed by set.mm contributors, 24-Nov-2007.)
⊢ A = B    ⇒   ⊢ (CAD) = (CBD)
Theorem	oveq1d 5537	Equality deduction for operation value. (Contributed by set.mm contributors, 13-Mar-1995.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → (AFC) = (BFC))
Theorem	oveq2d 5538	Equality deduction for operation value. (Contributed by set.mm contributors, 13-Mar-1995.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → (CFA) = (CFB))
Theorem	oveqd 5539	Equality deduction for operation value. (Contributed by set.mm contributors, 9-Sep-2006.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → (CAD) = (CBD))
Theorem	oveq12d 5540	Equality deduction for operation value. (The proof was shortened by Andrew Salmon, 22-Oct-2011.) (Contributed by set.mm contributors, 13-Mar-1995.) (Revised by set.mm contributors, 22-Oct-2011.)
⊢ (φ → A = B)    &   ⊢ (φ → C = D)    ⇒   ⊢ (φ → (AFC) = (BFD))
Theorem	oveqan12d 5541	Equality deduction for operation value. (Contributed by set.mm contributors, 10-Aug-1995.)
⊢ (φ → A = B)    &   ⊢ (ψ → C = D)    ⇒   ⊢ ((φ ∧ ψ) → (AFC) = (BFD))
Theorem	oveqan12rd 5542	Equality deduction for operation value. (Contributed by set.mm contributors, 10-Aug-1995.)
⊢ (φ → A = B)    &   ⊢ (ψ → C = D)    ⇒   ⊢ ((ψ ∧ φ) → (AFC) = (BFD))
Theorem	oveq123d 5543	Equality deduction for operation value. (Contributed by FL, 22-Dec-2008.)
⊢ (φ → F = G)    &   ⊢ (φ → A = B)    &   ⊢ (φ → C = D)    ⇒   ⊢ (φ → (AFC) = (BGD))
Theorem	nfovd 5544	Deduction version of bound-variable hypothesis builder nfov 5545. (Contributed by NM, 13-Dec-2005.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
⊢ (φ → ℲxA)    &   ⊢ (φ → ℲxF)    &   ⊢ (φ → ℲxB)    ⇒   ⊢ (φ → Ⅎx(AFB))
Theorem	nfov 5545	Bound-variable hypothesis builder for operation value. (Contributed by NM, 4-May-2004.)
⊢ ℲxA    &   ⊢ ℲxF    &   ⊢ ℲxB    ⇒   ⊢ Ⅎx(AFB)
Theorem	nfoprab1 5546	The abstraction variables in an operation class abstraction are not free. (Contributed by NM, 25-Apr-1995.) (Revised by David Abernethy, 19-Jun-2012.)
⊢ Ⅎx{⟨⟨x, y⟩, z⟩ ∣ φ}
Theorem	nfoprab2 5547	The abstraction variables in an operation class abstraction are not free. (Contributed by NM, 25-Apr-1995.) (Revised by David Abernethy, 30-Jul-2012.)
⊢ Ⅎy{⟨⟨x, y⟩, z⟩ ∣ φ}
Theorem	nfoprab3 5548	The abstraction variables in an operation class abstraction are not free. (Contributed by NM, 22-Aug-2013.)
⊢ Ⅎz{⟨⟨x, y⟩, z⟩ ∣ φ}
Theorem	nfoprab 5549*	Bound-variable hypothesis builder for an operation class abstraction. (Contributed by NM, 22-Aug-2013.)
⊢ Ⅎwφ    ⇒   ⊢ Ⅎw{⟨⟨x, y⟩, z⟩ ∣ φ}
Theorem	oprabid 5550	The law of concretion. Special case of Theorem 9.5 of [Quine] p. 61. (Contributed by Mario Carneiro, 20-Mar-2013.)
⊢ (⟨⟨x, y⟩, z⟩ ∈ {⟨⟨x, y⟩, z⟩ ∣ φ} ↔ φ)
Theorem	ovex 5551	The result of an operation is a set. (Contributed by set.mm contributors, 13-Mar-1995.)
⊢ (AFB) ∈ V
Theorem	csbovg 5552	Move class substitution in and out of an operation. (Contributed by NM, 12-Nov-2005.) (Proof shortened by Mario Carneiro, 5-Dec-2016.)
⊢ (A ∈ D → [A / x](BFC) = ([A / x]B[A / x]F[A / x]C))
Theorem	csbov12g 5553*	Move class substitution in and out of an operation. (Contributed by NM, 12-Nov-2005.)
⊢ (A ∈ D → [A / x](BFC) = ([A / x]BF[A / x]C))
Theorem	csbov1g 5554*	Move class substitution in and out of an operation. (Contributed by NM, 12-Nov-2005.)
⊢ (A ∈ D → [A / x](BFC) = ([A / x]BFC))
Theorem	csbov2g 5555*	Move class substitution in and out of an operation. (Contributed by NM, 12-Nov-2005.)
⊢ (A ∈ D → [A / x](BFC) = (BF[A / x]C))
Theorem	rspceov 5556*	A frequently used special case of rspc2ev 2963 for operation values. (Contributed by set.mm contributors, 21-Mar-2007.)
⊢ ((C ∈ A ∧ D ∈ B ∧ S = (CFD)) → ∃x ∈ A ∃y ∈ B S = (xFy))
Theorem	fnopovb 5557	Equivalence of operation value and ordered triple membership, analogous to fnopfvb 5359. (Contributed by set.mm contributors, 17-Dec-2008.)
⊢ ((F Fn (A × B) ∧ C ∈ A ∧ D ∈ B) → ((CFD) = R ↔ ⟨⟨C, D⟩, R⟩ ∈ F))
Theorem	dfoprab2 5558*	Class abstraction for operations in terms of class abstraction of ordered pairs. (Contributed by set.mm contributors, 12-Mar-1995.)
⊢ {⟨⟨x, y⟩, z⟩ ∣ φ} = {⟨w, z⟩ ∣ ∃x∃y(w = ⟨x, y⟩ ∧ φ)}
Theorem	hboprab1 5559*	The abstraction variables in an operation class abstraction are not free. (Unnecessary distinct variable restrictions were removed by David Abernethy, 19-Jun-2012.) (Contributed by set.mm contributors, 25-Apr-1995.) (Revised by set.mm contributors, 24-Jul-2012.)
⊢ (w ∈ {⟨⟨x, y⟩, z⟩ ∣ φ} → ∀x w ∈ {⟨⟨x, y⟩, z⟩ ∣ φ})
Theorem	hboprab2 5560*	The abstraction variables in an operation class abstraction are not free. (Unnecessary distinct variable restrictions were removed by David Abernethy, 30-Jul-2012.) (Contributed by set.mm contributors, 25-Apr-1995.) (Revised by set.mm contributors, 31-Jul-2012.)
⊢ (w ∈ {⟨⟨x, y⟩, z⟩ ∣ φ} → ∀y w ∈ {⟨⟨x, y⟩, z⟩ ∣ φ})
Theorem	hboprab3 5561*	The abstraction variables in an operation class abstraction are not free. (Contributed by set.mm contributors, 22-Aug-2013.)
⊢ (w ∈ {⟨⟨x, y⟩, z⟩ ∣ φ} → ∀z w ∈ {⟨⟨x, y⟩, z⟩ ∣ φ})
Theorem	hboprab 5562*	Bound-variable hypothesis builder for an operation class abstraction. (Contributed by set.mm contributors, 22-Aug-2013.)
⊢ (φ → ∀wφ)    ⇒   ⊢ (u ∈ {⟨⟨x, y⟩, z⟩ ∣ φ} → ∀w u ∈ {⟨⟨x, y⟩, z⟩ ∣ φ})
Theorem	oprabbid 5563*	Equivalent wff's yield equal operation class abstractions (deduction rule). (Contributed by NM, 21-Feb-2004.) (Revised by Mario Carneiro, 24-Jun-2014.)
⊢ Ⅎxφ    &   ⊢ Ⅎyφ    &   ⊢ Ⅎzφ    &   ⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (φ → {⟨⟨x, y⟩, z⟩ ∣ ψ} = {⟨⟨x, y⟩, z⟩ ∣ χ})
Theorem	oprabbidv 5564*	Equivalent wff's yield equal operation class abstractions (deduction rule). (Contributed by NM, 21-Feb-2004.)
⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (φ → {⟨⟨x, y⟩, z⟩ ∣ ψ} = {⟨⟨x, y⟩, z⟩ ∣ χ})
Theorem	oprabbii 5565*	Equivalent wff's yield equal operation class abstractions. (Unnecessary distinct variable restrictions were removed by David Abernethy, 19-Jun-2012.) (Contributed by set.mm contributors, 28-May-1995.) (Revised by set.mm contributors, 24-Jul-2012.)
⊢ (φ ↔ ψ)    ⇒   ⊢ {⟨⟨x, y⟩, z⟩ ∣ φ} = {⟨⟨x, y⟩, z⟩ ∣ ψ}
Theorem	oprab4 5566*	Two ways to state the domain of an operation. (Contributed by FL, 24-Jan-2010.)
⊢ {⟨⟨x, y⟩, z⟩ ∣ (⟨x, y⟩ ∈ (A × B) ∧ φ)} = {⟨⟨x, y⟩, z⟩ ∣ ((x ∈ A ∧ y ∈ B) ∧ φ)}
Theorem	cbvoprab1 5567*	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.)
⊢ Ⅎwφ    &   ⊢ Ⅎxψ    &   ⊢ (x = w → (φ ↔ ψ))    ⇒   ⊢ {⟨⟨x, y⟩, z⟩ ∣ φ} = {⟨⟨w, y⟩, z⟩ ∣ ψ}
Theorem	cbvoprab2 5568*	Change the second bound variable in an operation abstraction. (Contributed by Jeff Madsen, 11-Jun-2010.) (Revised by Mario Carneiro, 11-Dec-2016.)
⊢ Ⅎwφ    &   ⊢ Ⅎyψ    &   ⊢ (y = w → (φ ↔ ψ))    ⇒   ⊢ {⟨⟨x, y⟩, z⟩ ∣ φ} = {⟨⟨x, w⟩, z⟩ ∣ ψ}
Theorem	cbvoprab12 5569*	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.)
⊢ Ⅎwφ    &   ⊢ Ⅎvφ    &   ⊢ Ⅎxψ    &   ⊢ Ⅎyψ    &   ⊢ ((x = w ∧ y = v) → (φ ↔ ψ))    ⇒   ⊢ {⟨⟨x, y⟩, z⟩ ∣ φ} = {⟨⟨w, v⟩, z⟩ ∣ ψ}
Theorem	cbvoprab12v 5570*	Rule used to change first two bound variables in an operation abstraction, using implicit substitution. (Contributed by set.mm contributors, 8-Oct-2004.)
⊢ ((x = w ∧ y = v) → (φ ↔ ψ))    ⇒   ⊢ {⟨⟨x, y⟩, z⟩ ∣ φ} = {⟨⟨w, v⟩, z⟩ ∣ ψ}
Theorem	cbvoprab3 5571*	Rule used to change the third bound variable in an operation abstraction, using implicit substitution. (Contributed by NM, 22-Aug-2013.)
⊢ Ⅎwφ    &   ⊢ Ⅎzψ    &   ⊢ (z = w → (φ ↔ ψ))    ⇒   ⊢ {⟨⟨x, y⟩, z⟩ ∣ φ} = {⟨⟨x, y⟩, w⟩ ∣ ψ}
Theorem	cbvoprab3v 5572*	Rule used to change the third bound variable in an operation abstraction, using implicit substitution. (Unnecessary distinct variable restrictions were removed by David Abernethy, 19-Jun-2012.) (Contributed by set.mm contributors, 8-Oct-2004.) (Revised by set.mm contributors, 24-Jul-2012.)
⊢ (z = w → (φ ↔ ψ))    ⇒   ⊢ {⟨⟨x, y⟩, z⟩ ∣ φ} = {⟨⟨x, y⟩, w⟩ ∣ ψ}
Theorem	elimdelov 5573	Eliminate a hypothesis which is a predicate expressing membership in the result of an operator (deduction version). (Contributed by Paul Chapman, 25-Mar-2008.)
⊢ (φ → C ∈ (AFB))    &   ⊢ Z ∈ (XFY)    ⇒   ⊢ if(φ, C, Z) ∈ ( if(φ, A, X)F if(φ, B, Y))
Theorem	dmoprab 5574*	The domain of an operation class abstraction. (Unnecessary distinct variable restrictions were removed by David Abernethy, 19-Jun-2012.) (Contributed by set.mm contributors, 17-Mar-1995.) (Revised by set.mm contributors, 24-Jul-2012.)
⊢ dom {⟨⟨x, y⟩, z⟩ ∣ φ} = {⟨x, y⟩ ∣ ∃zφ}
Theorem	dmoprabss 5575*	The domain of an operation class abstraction. (Contributed by set.mm contributors, 24-Aug-1995.)
⊢ dom {⟨⟨x, y⟩, z⟩ ∣ ((x ∈ A ∧ y ∈ B) ∧ φ)} ⊆ (A × B)
Theorem	rnoprab 5576*	The range of an operation class abstraction. (Unnecessary distinct variable restrictions were removed by David Abernethy, 19-Apr-2013.) (Contributed by set.mm contributors, 30-Aug-2004.) (Revised by set.mm contributors, 19-Apr-2013.)
⊢ ran {⟨⟨x, y⟩, z⟩ ∣ φ} = {z ∣ ∃x∃yφ}
Theorem	rnoprab2 5577*	The range of a restricted operation class abstraction. (Contributed by Scott Fenton, 21-Mar-2012.)
⊢ ran {⟨⟨x, y⟩, z⟩ ∣ ((x ∈ A ∧ y ∈ B) ∧ φ)} = {z ∣ ∃x ∈ A ∃y ∈ B φ}
Theorem	eloprabga 5578*	The law of concretion for operation class abstraction. Compare elopab 4696. (Contributed by NM, 14-Sep-1999.) (Revised by David Abernethy, 18-Jun-2012.) Removed unnecessary distinct variable requirements. (Revised by Mario Carneiro, 19-Dec-2013.)
⊢ ((x = A ∧ y = B ∧ z = C) → (φ ↔ ψ))    ⇒   ⊢ ((A ∈ V ∧ B ∈ W ∧ C ∈ X) → (⟨⟨A, B⟩, C⟩ ∈ {⟨⟨x, y⟩, z⟩ ∣ φ} ↔ ψ))
Theorem	eloprabg 5579*	The law of concretion for operation class abstraction. Compare elopab 4696. (Contributed by set.mm contributors, 14-Sep-1999.) (Revised by David Abernethy, 19-Jun-2012.) Removed unnecessary distinct variable requirements. (Revised by set.mm contributors, 19-Dec-2013.)
⊢ (x = A → (φ ↔ ψ))    &   ⊢ (y = B → (ψ ↔ χ))    &   ⊢ (z = C → (χ ↔ θ))    ⇒   ⊢ ((A ∈ V ∧ B ∈ W ∧ C ∈ X) → (⟨⟨A, B⟩, C⟩ ∈ {⟨⟨x, y⟩, z⟩ ∣ φ} ↔ θ))
Theorem	ssoprab2i 5580*	Inference of operation class abstraction subclass from implication. (Unnecessary distinct variable restrictions were removed by David Abernethy, 19-Jun-2012.) (Contributed by set.mm contributors, 11-Nov-1995.) (Revised by set.mm contributors, 24-Jul-2012.)
⊢ (φ → ψ)    ⇒   ⊢ {⟨⟨x, y⟩, z⟩ ∣ φ} ⊆ {⟨⟨x, y⟩, z⟩ ∣ ψ}
Theorem	resoprab 5581*	Restriction of an operation class abstraction. (Contributed by set.mm contributors, 10-Feb-2007.)
⊢ ({⟨⟨x, y⟩, z⟩ ∣ φ} ↾ (A × B)) = {⟨⟨x, y⟩, z⟩ ∣ ((x ∈ A ∧ y ∈ B) ∧ φ)}
Theorem	resoprab2 5582*	Restriction of an operator abstraction. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ ((C ⊆ A ∧ D ⊆ B) → ({⟨⟨x, y⟩, z⟩ ∣ ((x ∈ A ∧ y ∈ B) ∧ φ)} ↾ (C × D)) = {⟨⟨x, y⟩, z⟩ ∣ ((x ∈ C ∧ y ∈ D) ∧ φ)})
Theorem	funoprabg 5583*	"At most one" is a sufficient condition for an operation class abstraction to be a function. (Contributed by set.mm contributors, 28-Aug-2007.)
⊢ (∀x∀y∃*zφ → Fun {⟨⟨x, y⟩, z⟩ ∣ φ})
Theorem	funoprab 5584*	"At most one" is a sufficient condition for an operation class abstraction to be a function. (Contributed by set.mm contributors, 17-Mar-1995.)
⊢ ∃*zφ    ⇒   ⊢ Fun {⟨⟨x, y⟩, z⟩ ∣ φ}
Theorem	fnoprabg 5585*	Functionality and domain of an operation class abstraction. (Contributed by set.mm contributors, 28-Aug-2007.)
⊢ (∀x∀y(φ → ∃!zψ) → {⟨⟨x, y⟩, z⟩ ∣ (φ ∧ ψ)} Fn {⟨x, y⟩ ∣ φ})
Theorem	fnoprab 5586*	Functionality and domain of an operation class abstraction. (Contributed by set.mm contributors, 15-May-1995.)
⊢ (φ → ∃!zψ)    ⇒   ⊢ {⟨⟨x, y⟩, z⟩ ∣ (φ ∧ ψ)} Fn {⟨x, y⟩ ∣ φ}
Theorem	ffnov 5587*	An operation maps to a class to which all values belong. (Contributed by set.mm contributors, 7-Feb-2004.)
⊢ (F:(A × B)–→C ↔ (F Fn (A × B) ∧ ∀x ∈ A ∀y ∈ B (xFy) ∈ C))
Theorem	fovcl 5588	Closure law for an operation. (Contributed by set.mm contributors, 19-Apr-2007.)
⊢ F:(R × S)–→C    ⇒   ⊢ ((A ∈ R ∧ B ∈ S) → (AFB) ∈ C)
Theorem	eqfnov 5589*	Equality of two operations is determined by their values. (Contributed by set.mm contributors, 1-Sep-2005.)
⊢ ((F Fn (A × B) ∧ G Fn (C × D)) → (F = G ↔ ((A × B) = (C × D) ∧ ∀x ∈ A ∀y ∈ B (xFy) = (xGy))))
Theorem	eqfnov2 5590*	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.)
⊢ ((F Fn (A × B) ∧ G Fn (A × B)) → (F = G ↔ ∀x ∈ A ∀y ∈ B (xFy) = (xGy)))
Theorem	fnov 5591*	Representation of an operation class abstraction in terms of its values. (Contributed by set.mm contributors, 7-Feb-2004.)
⊢ (F Fn (A × B) ↔ F = {⟨⟨x, y⟩, z⟩ ∣ ((x ∈ A ∧ y ∈ B) ∧ z = (xFy))})
Theorem	fov 5592*	Representation of an operation class abstraction in terms of its values. (Contributed by set.mm contributors, 7-Feb-2004.)
⊢ (F:(A × B)–→C ↔ (F = {⟨⟨x, y⟩, z⟩ ∣ ((x ∈ A ∧ y ∈ B) ∧ z = (xFy))} ∧ ∀x ∈ A ∀y ∈ B (xFy) ∈ C))
Theorem	ovidig 5593*	The value of an operation class abstraction. Compare ovidi 5594. The condition (x ∈ R ∧ y ∈ S) is been removed. (Contributed by Mario Carneiro, 29-Dec-2014.)
⊢ ∃*zφ    &   ⊢ F = {⟨⟨x, y⟩, z⟩ ∣ φ}    ⇒   ⊢ (φ → (xFy) = z)
Theorem	ovidi 5594*	The value of an operation class abstraction (weak version). (Contributed by Mario Carneiro, 29-Dec-2014.)
⊢ ((x ∈ R ∧ y ∈ S) → ∃*zφ)    &   ⊢ F = {⟨⟨x, y⟩, z⟩ ∣ ((x ∈ R ∧ y ∈ S) ∧ φ)}    ⇒   ⊢ ((x ∈ R ∧ y ∈ S) → (φ → (xFy) = z))
Theorem	ov 5595*	The value of an operation class abstraction. (Unnecessary distinct variable restrictions were removed by David Abernethy, 19-Jun-2012.) (Contributed by set.mm contributors, 16-May-1995.) (Revised by set.mm contributors, 24-Jul-2012.)
⊢ C ∈ V    &   ⊢ (x = A → (φ ↔ ψ))    &   ⊢ (y = B → (ψ ↔ χ))    &   ⊢ (z = C → (χ ↔ θ))    &   ⊢ ((x ∈ R ∧ y ∈ S) → ∃!zφ)    &   ⊢ F = {⟨⟨x, y⟩, z⟩ ∣ ((x ∈ R ∧ y ∈ S) ∧ φ)}    ⇒   ⊢ ((A ∈ R ∧ B ∈ S) → ((AFB) = C ↔ θ))
Theorem	ovigg 5596*	The value of an operation class abstraction. Compare ovig 5597. The condition (x ∈ R ∧ y ∈ S) is been removed. (Contributed by FL, 24-Mar-2007.)
⊢ ((x = A ∧ y = B ∧ z = C) → (φ ↔ ψ))    &   ⊢ ∃*zφ    &   ⊢ F = {⟨⟨x, y⟩, z⟩ ∣ φ}    ⇒   ⊢ ((A ∈ V ∧ B ∈ W ∧ C ∈ X) → (ψ → (AFB) = C))
Theorem	ovig 5597*	The value of an operation class abstraction (weak version). (Contributed by set.mm contributors, 14-Sep-1999.) (Unnecessary distinct variable restrictions were removed by David Abernethy, 19-Jun-2012.) (Revised by Mario Carneiro, 19-Dec-2013.)
⊢ ((x = A ∧ y = B ∧ z = C) → (φ ↔ ψ))    &   ⊢ ((x ∈ R ∧ y ∈ S) → ∃*zφ)    &   ⊢ F = {⟨⟨x, y⟩, z⟩ ∣ ((x ∈ R ∧ y ∈ S) ∧ φ)}    ⇒   ⊢ ((A ∈ R ∧ B ∈ S ∧ C ∈ D) → (ψ → (AFB) = C))
Theorem	ov2ag 5598*	The value of an operation class abstraction. Special case. (Contributed by Mario Carneiro, 19-Dec-2013.)
⊢ ((x = A ∧ y = B) → R = S)    &   ⊢ F = {⟨⟨x, y⟩, z⟩ ∣ ((x ∈ C ∧ y ∈ D) ∧ z = R)}    ⇒   ⊢ ((A ∈ C ∧ B ∈ D ∧ S ∈ H) → (AFB) = S)
Theorem	ov3 5599*	The value of an operation class abstraction. Special case. (Contributed by NM, 28-May-1995.) (Revised by Mario Carneiro, 29-Dec-2014.)
⊢ S ∈ V    &   ⊢ (((w = A ∧ v = B) ∧ (u = C ∧ f = D)) → R = S)    &   ⊢ F = {⟨⟨x, y⟩, z⟩ ∣ ((x ∈ (H × H) ∧ y ∈ (H × H)) ∧ ∃w∃v∃u∃f((x = ⟨w, v⟩ ∧ y = ⟨u, f⟩) ∧ z = R))}    ⇒   ⊢ (((A ∈ H ∧ B ∈ H) ∧ (C ∈ H ∧ D ∈ H)) → (⟨A, B⟩F⟨C, D⟩) = S)
Theorem	ov6g 5600*	The value of an operation class abstraction. Special case. (Contributed by set.mm contributors, 13-Nov-2006.)
⊢ (⟨x, y⟩ = ⟨A, B⟩ → R = S)    &   ⊢ F = {⟨⟨x, y⟩, z⟩ ∣ (⟨x, y⟩ ∈ C ∧ z = R)}    ⇒   ⊢ (((A ∈ G ∧ B ∈ H ∧ ⟨A, B⟩ ∈ C) ∧ S ∈ J) → (AFB) = S)