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	f1oiso2 5501*	Any one-to-one onto function determines an isomorphism with an induced relation S. (Contributed by Mario Carneiro, 9-Mar-2013.)
|- S = {<.x, y>. | ((x e. B /\ y e. B) /\ (`'H` x)R(`'H` y))}   =>   |- (H:A-1-1-onto->B -> H Isom R, S (A, B))
Theorem	opbr1st 5502	Binary relationship of an ordered pair over 1st. (Contributed by SF, 6-Feb-2015.)
|- A e. _V   &   |- B e. _V   =>   |- (<.A, B>.1stC <-> A = C)
Theorem	opbr2nd 5503	Binary relationship of an ordered pair over 2nd. (Contributed by SF, 6-Feb-2015.)
|- A e. _V   &   |- B e. _V   =>   |- (<.A, B>.2ndC <-> B = C)
Theorem	dfid4 5504	Alternate definition of the identity relationship. (Contributed by SF, 11-Feb-2015.)
|- _I = ( S i^i `' S )
Theorem	idex 5505	The identity relationship is a set. (Contributed by SF, 11-Feb-2015.)
|- _I e. _V
Theorem	1stfo 5506	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 5507	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 5508	Alternate definition of domain. (Contributed by SF, 23-Feb-2015.)
|- dom A = (1st"A)
Theorem	dfrn5 5509	Alternate definition of range. (Contributed by SF, 23-Feb-2015.)
|- ran A = (2nd"A)
Theorem	brswap 5510*	Binary relationship of Swap . (Contributed by SF, 23-Feb-2015.)
|- (A Swap B <-> E.xE.y(A = <.x, y>. /\ B = <.y, x>.))
Theorem	cnvswap 5511	The converse of Swap is Swap . (Contributed by SF, 23-Feb-2015.)
|- `' Swap = Swap
Theorem	swapf1o 5512	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 5513	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 5514	Cross products with non-equal singletons are disjoint. (Contributed by SF, 23-Feb-2015.)
|- C e. _V   &   |- C =/= D   =>   |- ((A X. {C}) i^i (B X. {D})) = (/)
Theorem	opfv1st 5515	The value of the 1st function on an ordered pair. (Contributed by SF, 23-Feb-2015.)
|- A e. _V   &   |- B e. _V   =>   |- (1st` <.A, B>.) = A
Theorem	opfv2nd 5516	The value of the 2nd function on an ordered pair. (Contributed by SF, 23-Feb-2015.)
|- A e. _V   &   |- B e. _V   =>   |- (2nd` <.A, B>.) = B
Theorem	1st2nd2 5517	Reconstruction of a member of a cross product in terms of its ordered pair components. (Contributed by SF, 20-Oct-2013.)
|- (A e. (B X. C) -> A = <.(1st` A), (2nd` A)>.)
Theorem	fununiq 5518	Implicational form of part of the definition of a function. (Contributed by SF, 24-Feb-2015.)
|- ((Fun F /\ AFB /\ AFC) -> B = C)
Theorem	cnvsi 5519	Calculate the converse of a singleton image. (Contributed by SF, 26-Feb-2015.)
|- `' SI R = SI `'R
Theorem	dmsi 5520	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 = ~P1 dom R
Theorem	funsi 5521	The singleton image of a function is a function. (Contributed by SF, 26-Feb-2015.)
|- (Fun F -> Fun SI F)
Theorem	rnsi 5522	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 = ~P1 ran R
Theorem	op1std 5523	Extract the first member of an ordered pair. (Contributed by Mario Carneiro, 31-Aug-2015.)
|- A e. _V   &   |- B e. _V   =>   |- (C = <.A, B>. -> (1st` C) = A)
Theorem	op2ndd 5524	Extract the second member of an ordered pair. (Contributed by Mario Carneiro, 31-Aug-2015.)
|- A e. _V   &   |- B e. _V   =>   |- (C = <.A, B>. -> (2nd` C) = B)
Theorem	dmep 5525	The domain of the epsilon relationship. (Contributed by Scott Fenton, 20-Apr-2021.)
|- dom _E = _V
2.3.8  Operations
Syntax	co 5526	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 5527	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 5529. (Contributed by SF, 5-Jan-2015.)
|- (AFB) = (F` <.A, B>.)
Syntax	coprab 5528	Extend class notation to include class abstraction (class builder) of nested ordered pairs.
class {<.<.x, y>., z>. | ph}
Definition	df-oprab 5529*	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 5527 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>. | ph} = {w | E.xE.yE.z(w = <.<.x, y>., z>. /\ ph)}
Theorem	oveq 5530	Equality theorem for operation value. (Contributed by set.mm contributors, 28-Feb-1995.)
|- (F = G -> (AFB) = (AGB))
Theorem	oveq1 5531	Equality theorem for operation value. (Contributed by set.mm contributors, 28-Feb-1995.)
|- (A = B -> (AFC) = (BFC))
Theorem	oveq2 5532	Equality theorem for operation value. (Contributed by set.mm contributors, 28-Feb-1995.)
|- (A = B -> (CFA) = (CFB))
Theorem	oveq12 5533	Equality theorem for operation value. (Contributed by set.mm contributors, 16-Jul-1995.)
|- ((A = B /\ C = D) -> (AFC) = (BFD))
Theorem	oveq1i 5534	Equality inference for operation value. (Contributed by set.mm contributors, 28-Feb-1995.)
|- A = B   =>   |- (AFC) = (BFC)
Theorem	oveq2i 5535	Equality inference for operation value. (Contributed by set.mm contributors, 28-Feb-1995.)
|- A = B   =>   |- (CFA) = (CFB)
Theorem	oveq12i 5536	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 5537	Equality inference for operation value. (Contributed by set.mm contributors, 24-Nov-2007.)
|- A = B   =>   |- (CAD) = (CBD)
Theorem	oveq1d 5538	Equality deduction for operation value. (Contributed by set.mm contributors, 13-Mar-1995.)
|- (ph -> A = B)   =>   |- (ph -> (AFC) = (BFC))
Theorem	oveq2d 5539	Equality deduction for operation value. (Contributed by set.mm contributors, 13-Mar-1995.)
|- (ph -> A = B)   =>   |- (ph -> (CFA) = (CFB))
Theorem	oveqd 5540	Equality deduction for operation value. (Contributed by set.mm contributors, 9-Sep-2006.)
|- (ph -> A = B)   =>   |- (ph -> (CAD) = (CBD))
Theorem	oveq12d 5541	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.)
|- (ph -> A = B)   &   |- (ph -> C = D)   =>   |- (ph -> (AFC) = (BFD))
Theorem	oveqan12d 5542	Equality deduction for operation value. (Contributed by set.mm contributors, 10-Aug-1995.)
|- (ph -> A = B)   &   |- (ps -> C = D)   =>   |- ((ph /\ ps) -> (AFC) = (BFD))
Theorem	oveqan12rd 5543	Equality deduction for operation value. (Contributed by set.mm contributors, 10-Aug-1995.)
|- (ph -> A = B)   &   |- (ps -> C = D)   =>   |- ((ps /\ ph) -> (AFC) = (BFD))
Theorem	oveq123d 5544	Equality deduction for operation value. (Contributed by FL, 22-Dec-2008.)
|- (ph -> F = G)   &   |- (ph -> A = B)   &   |- (ph -> C = D)   =>   |- (ph -> (AFC) = (BGD))
Theorem	nfovd 5545	Deduction version of bound-variable hypothesis builder nfov 5546. (Contributed by NM, 13-Dec-2005.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
|- (ph -> F/_xA)   &   |- (ph -> F/_xF)   &   |- (ph -> F/_xB)   =>   |- (ph -> F/_x(AFB))
Theorem	nfov 5546	Bound-variable hypothesis builder for operation value. (Contributed by NM, 4-May-2004.)
|- F/_xA   &   |- F/_xF   &   |- F/_xB   =>   |- F/_x(AFB)
Theorem	nfoprab1 5547	The abstraction variables in an operation class abstraction are not free. (Contributed by NM, 25-Apr-1995.) (Revised by David Abernethy, 19-Jun-2012.)
|- F/_x{<.<.x, y>., z>. | ph}
Theorem	nfoprab2 5548	The abstraction variables in an operation class abstraction are not free. (Contributed by NM, 25-Apr-1995.) (Revised by David Abernethy, 30-Jul-2012.)
|- F/_y{<.<.x, y>., z>. | ph}
Theorem	nfoprab3 5549	The abstraction variables in an operation class abstraction are not free. (Contributed by NM, 22-Aug-2013.)
|- F/_z{<.<.x, y>., z>. | ph}
Theorem	nfoprab 5550*	Bound-variable hypothesis builder for an operation class abstraction. (Contributed by NM, 22-Aug-2013.)
|- F/wph   =>   |- F/_w{<.<.x, y>., z>. | ph}
Theorem	oprabid 5551	The law of concretion. Special case of Theorem 9.5 of [Quine] p. 61. (Contributed by Mario Carneiro, 20-Mar-2013.)
|- (<.<.x, y>., z>. e. {<.<.x, y>., z>. | ph} <-> ph)
Theorem	ovex 5552	The result of an operation is a set. (Contributed by set.mm contributors, 13-Mar-1995.)
|- (AFB) e. _V
Theorem	csbovg 5553	Move class substitution in and out of an operation. (Contributed by NM, 12-Nov-2005.) (Proof shortened by Mario Carneiro, 5-Dec-2016.)
|- (A e. D -> [_A / x]_(BFC) = ([_A / x]_B[_A / x]_F[_A / x]_C))
Theorem	csbov12g 5554*	Move class substitution in and out of an operation. (Contributed by NM, 12-Nov-2005.)
|- (A e. D -> [_A / x]_(BFC) = ([_A / x]_BF[_A / x]_C))
Theorem	csbov1g 5555*	Move class substitution in and out of an operation. (Contributed by NM, 12-Nov-2005.)
|- (A e. D -> [_A / x]_(BFC) = ([_A / x]_BFC))
Theorem	csbov2g 5556*	Move class substitution in and out of an operation. (Contributed by NM, 12-Nov-2005.)
|- (A e. D -> [_A / x]_(BFC) = (BF[_A / x]_C))
Theorem	rspceov 5557*	A frequently used special case of rspc2ev 2964 for operation values. (Contributed by set.mm contributors, 21-Mar-2007.)
|- ((C e. A /\ D e. B /\ S = (CFD)) -> E.x e. A E.y e. B S = (xFy))
Theorem	fnopovb 5558	Equivalence of operation value and ordered triple membership, analogous to fnopfvb 5360. (Contributed by set.mm contributors, 17-Dec-2008.)
|- ((F Fn (A X. B) /\ C e. A /\ D e. B) -> ((CFD) = R <-> <.<.C, D>., R>. e. F))
Theorem	dfoprab2 5559*	Class abstraction for operations in terms of class abstraction of ordered pairs. (Contributed by set.mm contributors, 12-Mar-1995.)
|- {<.<.x, y>., z>. | ph} = {<.w, z>. | E.xE.y(w = <.x, y>. /\ ph)}
Theorem	hboprab1 5560*	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 e. {<.<.x, y>., z>. | ph} -> A.x w e. {<.<.x, y>., z>. | ph})
Theorem	hboprab2 5561*	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 e. {<.<.x, y>., z>. | ph} -> A.y w e. {<.<.x, y>., z>. | ph})
Theorem	hboprab3 5562*	The abstraction variables in an operation class abstraction are not free. (Contributed by set.mm contributors, 22-Aug-2013.)
|- (w e. {<.<.x, y>., z>. | ph} -> A.z w e. {<.<.x, y>., z>. | ph})
Theorem	hboprab 5563*	Bound-variable hypothesis builder for an operation class abstraction. (Contributed by set.mm contributors, 22-Aug-2013.)
|- (ph -> A.wph)   =>   |- (u e. {<.<.x, y>., z>. | ph} -> A.w u e. {<.<.x, y>., z>. | ph})
Theorem	oprabbid 5564*	Equivalent wff's yield equal operation class abstractions (deduction rule). (Contributed by NM, 21-Feb-2004.) (Revised by Mario Carneiro, 24-Jun-2014.)
|- F/xph   &   |- F/yph   &   |- F/zph   &   |- (ph -> (ps <-> ch))   =>   |- (ph -> {<.<.x, y>., z>. | ps} = {<.<.x, y>., z>. | ch})
Theorem	oprabbidv 5565*	Equivalent wff's yield equal operation class abstractions (deduction rule). (Contributed by NM, 21-Feb-2004.)
|- (ph -> (ps <-> ch))   =>   |- (ph -> {<.<.x, y>., z>. | ps} = {<.<.x, y>., z>. | ch})
Theorem	oprabbii 5566*	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.)
|- (ph <-> ps)   =>   |- {<.<.x, y>., z>. | ph} = {<.<.x, y>., z>. | ps}
Theorem	oprab4 5567*	Two ways to state the domain of an operation. (Contributed by FL, 24-Jan-2010.)
|- {<.<.x, y>., z>. | (<.x, y>. e. (A X. B) /\ ph)} = {<.<.x, y>., z>. | ((x e. A /\ y e. B) /\ ph)}
Theorem	cbvoprab1 5568*	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.)
|- F/wph   &   |- F/xps   &   |- (x = w -> (ph <-> ps))   =>   |- {<.<.x, y>., z>. | ph} = {<.<.w, y>., z>. | ps}
Theorem	cbvoprab2 5569*	Change the second bound variable in an operation abstraction. (Contributed by Jeff Madsen, 11-Jun-2010.) (Revised by Mario Carneiro, 11-Dec-2016.)
|- F/wph   &   |- F/yps   &   |- (y = w -> (ph <-> ps))   =>   |- {<.<.x, y>., z>. | ph} = {<.<.x, w>., z>. | ps}
Theorem	cbvoprab12 5570*	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.)
|- F/wph   &   |- F/vph   &   |- F/xps   &   |- F/yps   &   |- ((x = w /\ y = v) -> (ph <-> ps))   =>   |- {<.<.x, y>., z>. | ph} = {<.<.w, v>., z>. | ps}
Theorem	cbvoprab12v 5571*	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) -> (ph <-> ps))   =>   |- {<.<.x, y>., z>. | ph} = {<.<.w, v>., z>. | ps}
Theorem	cbvoprab3 5572*	Rule used to change the third bound variable in an operation abstraction, using implicit substitution. (Contributed by NM, 22-Aug-2013.)
|- F/wph   &   |- F/zps   &   |- (z = w -> (ph <-> ps))   =>   |- {<.<.x, y>., z>. | ph} = {<.<.x, y>., w>. | ps}
Theorem	cbvoprab3v 5573*	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 -> (ph <-> ps))   =>   |- {<.<.x, y>., z>. | ph} = {<.<.x, y>., w>. | ps}
Theorem	elimdelov 5574	Eliminate a hypothesis which is a predicate expressing membership in the result of an operator (deduction version). (Contributed by Paul Chapman, 25-Mar-2008.)
|- (ph -> C e. (AFB))   &   |- Z e. (XFY)   =>   |- if(ph, C, Z) e. (if(ph, A, X)Fif(ph, B, Y))
Theorem	dmoprab 5575*	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>. | ph} = {<.x, y>. | E.zph}
Theorem	dmoprabss 5576*	The domain of an operation class abstraction. (Contributed by set.mm contributors, 24-Aug-1995.)
|- dom {<.<.x, y>., z>. | ((x e. A /\ y e. B) /\ ph)} C_ (A X. B)
Theorem	rnoprab 5577*	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>. | ph} = {z | E.xE.yph}
Theorem	rnoprab2 5578*	The range of a restricted operation class abstraction. (Contributed by Scott Fenton, 21-Mar-2012.)
|- ran {<.<.x, y>., z>. | ((x e. A /\ y e. B) /\ ph)} = {z | E.x e. A E.y e. B ph}
Theorem	eloprabga 5579*	The law of concretion for operation class abstraction. Compare elopab 4697. (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) -> (ph <-> ps))   =>   |- ((A e. V /\ B e. W /\ C e. X) -> (<.<.A, B>., C>. e. {<.<.x, y>., z>. | ph} <-> ps))
Theorem	eloprabg 5580*	The law of concretion for operation class abstraction. Compare elopab 4697. (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 -> (ph <-> ps))   &   |- (y = B -> (ps <-> ch))   &   |- (z = C -> (ch <-> th))   =>   |- ((A e. V /\ B e. W /\ C e. X) -> (<.<.A, B>., C>. e. {<.<.x, y>., z>. | ph} <-> th))
Theorem	ssoprab2i 5581*	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.)
|- (ph -> ps)   =>   |- {<.<.x, y>., z>. | ph} C_ {<.<.x, y>., z>. | ps}
Theorem	resoprab 5582*	Restriction of an operation class abstraction. (Contributed by set.mm contributors, 10-Feb-2007.)
|- ({<.<.x, y>., z>. | ph} |` (A X. B)) = {<.<.x, y>., z>. | ((x e. A /\ y e. B) /\ ph)}
Theorem	resoprab2 5583*	Restriction of an operator abstraction. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ((C C_ A /\ D C_ B) -> ({<.<.x, y>., z>. | ((x e. A /\ y e. B) /\ ph)} |` (C X. D)) = {<.<.x, y>., z>. | ((x e. C /\ y e. D) /\ ph)})
Theorem	funoprabg 5584*	"At most one" is a sufficient condition for an operation class abstraction to be a function. (Contributed by set.mm contributors, 28-Aug-2007.)
|- (A.xA.yE*zph -> Fun {<.<.x, y>., z>. | ph})
Theorem	funoprab 5585*	"At most one" is a sufficient condition for an operation class abstraction to be a function. (Contributed by set.mm contributors, 17-Mar-1995.)
|- E*zph   =>   |- Fun {<.<.x, y>., z>. | ph}
Theorem	fnoprabg 5586*	Functionality and domain of an operation class abstraction. (Contributed by set.mm contributors, 28-Aug-2007.)
|- (A.xA.y(ph -> E!zps) -> {<.<.x, y>., z>. | (ph /\ ps)} Fn {<.x, y>. | ph})
Theorem	fnoprab 5587*	Functionality and domain of an operation class abstraction. (Contributed by set.mm contributors, 15-May-1995.)
|- (ph -> E!zps)   =>   |- {<.<.x, y>., z>. | (ph /\ ps)} Fn {<.x, y>. | ph}
Theorem	ffnov 5588*	An operation maps to a class to which all values belong. (Contributed by set.mm contributors, 7-Feb-2004.)
|- (F:(A X. B)-->C <-> (F Fn (A X. B) /\ A.x e. A A.y e. B (xFy) e. C))
Theorem	fovcl 5589	Closure law for an operation. (Contributed by set.mm contributors, 19-Apr-2007.)
|- F:(R X. S)-->C   =>   |- ((A e. R /\ B e. S) -> (AFB) e. C)
Theorem	eqfnov 5590*	Equality of two operations is determined by their values. (Contributed by set.mm contributors, 1-Sep-2005.)
|- ((F Fn (A X. B) /\ G Fn (C X. D)) -> (F = G <-> ((A X. B) = (C X. D) /\ A.x e. A A.y e. B (xFy) = (xGy))))
Theorem	eqfnov2 5591*	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 X. B) /\ G Fn (A X. B)) -> (F = G <-> A.x e. A A.y e. B (xFy) = (xGy)))
Theorem	fnov 5592*	Representation of an operation class abstraction in terms of its values. (Contributed by set.mm contributors, 7-Feb-2004.)
|- (F Fn (A X. B) <-> F = {<.<.x, y>., z>. | ((x e. A /\ y e. B) /\ z = (xFy))})
Theorem	fov 5593*	Representation of an operation class abstraction in terms of its values. (Contributed by set.mm contributors, 7-Feb-2004.)
|- (F:(A X. B)-->C <-> (F = {<.<.x, y>., z>. | ((x e. A /\ y e. B) /\ z = (xFy))} /\ A.x e. A A.y e. B (xFy) e. C))
Theorem	ovidig 5594*	The value of an operation class abstraction. Compare ovidi 5595. The condition (x e. R /\ y e. S) is been removed. (Contributed by Mario Carneiro, 29-Dec-2014.)
|- E*zph   &   |- F = {<.<.x, y>., z>. | ph}   =>   |- (ph -> (xFy) = z)
Theorem	ovidi 5595*	The value of an operation class abstraction (weak version). (Contributed by Mario Carneiro, 29-Dec-2014.)
|- ((x e. R /\ y e. S) -> E*zph)   &   |- F = {<.<.x, y>., z>. | ((x e. R /\ y e. S) /\ ph)}   =>   |- ((x e. R /\ y e. S) -> (ph -> (xFy) = z))
Theorem	ov 5596*	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 e. _V   &   |- (x = A -> (ph <-> ps))   &   |- (y = B -> (ps <-> ch))   &   |- (z = C -> (ch <-> th))   &   |- ((x e. R /\ y e. S) -> E!zph)   &   |- F = {<.<.x, y>., z>. | ((x e. R /\ y e. S) /\ ph)}   =>   |- ((A e. R /\ B e. S) -> ((AFB) = C <-> th))
Theorem	ovigg 5597*	The value of an operation class abstraction. Compare ovig 5598. The condition (x e. R /\ y e. S) is been removed. (Contributed by FL, 24-Mar-2007.)
|- ((x = A /\ y = B /\ z = C) -> (ph <-> ps))   &   |- E*zph   &   |- F = {<.<.x, y>., z>. | ph}   =>   |- ((A e. V /\ B e. W /\ C e. X) -> (ps -> (AFB) = C))
Theorem	ovig 5598*	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) -> (ph <-> ps))   &   |- ((x e. R /\ y e. S) -> E*zph)   &   |- F = {<.<.x, y>., z>. | ((x e. R /\ y e. S) /\ ph)}   =>   |- ((A e. R /\ B e. S /\ C e. D) -> (ps -> (AFB) = C))
Theorem	ov2ag 5599*	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 e. C /\ y e. D) /\ z = R)}   =>   |- ((A e. C /\ B e. D /\ S e. H) -> (AFB) = S)
Theorem	ov3 5600*	The value of an operation class abstraction. Special case. (Contributed by NM, 28-May-1995.) (Revised by Mario Carneiro, 29-Dec-2014.)
|- S e. _V   &   |- (((w = A /\ v = B) /\ (u = C /\ f = D)) -> R = S)   &   |- F = {<.<.x, y>., z>. | ((x e. (H X. H) /\ y e. (H X. H)) /\ E.wE.vE.uE.f((x = <.w, v>. /\ y = <.u, f>.) /\ z = R))}   =>   |- (((A e. H /\ B e. H) /\ (C e. H /\ D e. H)) -> (<.A, B>.F<.C, D>.) = S)