P. 61 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 6001-6100   *Has distinct variable group(s)

Type	Label	Description
Statement
2.6.9  Cantor's Theorem
Theorem	canth 6001	No set A is equinumerous to its power set (Cantor's theorem), i.e., no function can map A onto its power set. Compare Theorem 6B(b) of [Enderton] p. 132. (Use nex 1549 if you want the form -. E. f f : A -onto-> ~P A.) (Contributed by NM, 7-Aug-1994.) (Revised by Noah R Kingdon, 23-Jul-2024.)
|- A e. _V   =>    |- -. F : A -onto-> ~P A
2.6.10  Restricted iota (description binder)
Syntax	crio 6002	Extend class notation with restricted description binder.
class ( iota_ x e. A ph )
Definition	df-riota 6003	Define restricted description binder. In case there is no unique x such that ( x e. A /\ ph ) holds, it evaluates to the empty set. See also comments for df-iota 5312. (Contributed by NM, 15-Sep-2011.) (Revised by Mario Carneiro, 15-Oct-2016.) (Revised by NM, 2-Sep-2018.)
|- ( iota_ x e. A ph ) = ( iota x ( x e. A /\ ph ) )
Theorem	riotaeqdv 6004*	Formula-building deduction for iota. (Contributed by NM, 15-Sep-2011.)
|- ( ph -> A = B )   =>    |- ( ph -> ( iota_ x e. A ps ) = ( iota_ x e. B ps ) )
Theorem	riotabidv 6005*	Formula-building deduction for restricted iota. (Contributed by NM, 15-Sep-2011.)
|- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( iota_ x e. A ps ) = ( iota_ x e. A ch ) )
Theorem	riotaeqbidv 6006*	Equality deduction for restricted universal quantifier. (Contributed by NM, 15-Sep-2011.)
|- ( ph -> A = B )   &    |- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( iota_ x e. A ps ) = ( iota_ x e. B ch ) )
Theorem	riotaexg 6007*	Restricted iota is a set. (Contributed by Jim Kingdon, 15-Jun-2020.)
|- ( A e. V -> ( iota_ x e. A ps ) e. _V )
Theorem	iotaexel 6008*	Set existence of an iota expression in which all values are contained within a set. (Contributed by Jim Kingdon, 28-Jun-2025.)
|- ( ( A e. V /\ A. x ( ph -> x e. A ) ) -> ( iota x ph ) e. _V )
Theorem	riotav 6009	An iota restricted to the universe is unrestricted. (Contributed by NM, 18-Sep-2011.)
|- ( iota_ x e. _V ph ) = ( iota x ph )
Theorem	riotauni 6010	Restricted iota in terms of class union. (Contributed by NM, 11-Oct-2011.)
|- ( E! x e. A ph -> ( iota_ x e. A ph ) = U. { x e. A | ph } )
Theorem	nfriota1 6011*	The abstraction variable in a restricted iota descriptor isn't free. (Contributed by NM, 12-Oct-2011.) (Revised by Mario Carneiro, 15-Oct-2016.)
|- F/_ x ( iota_ x e. A ph )
Theorem	nfriotadxy 6012*	Deduction version of nfriota 6013. (Contributed by Jim Kingdon, 12-Jan-2019.)
|- F/ y ph   &    |- ( ph -> F/ x ps )   &    |- ( ph -> F/_ x A )   =>    |- ( ph -> F/_ x ( iota_ y e. A ps ) )
Theorem	nfriota 6013*	A variable not free in a wff remains so in a restricted iota descriptor. (Contributed by NM, 12-Oct-2011.)
|- F/ x ph   &    |- F/_ x A   =>    |- F/_ x ( iota_ y e. A ph )
Theorem	cbvriotavw 6014*	Change bound variable in a restricted description binder. Version of cbvriotav 6016 with a disjoint variable condition. (Contributed by NM, 18-Mar-2013.) (Revised by GG, 30-Sep-2024.)
|- ( x = y -> ( ph <-> ps ) )   =>    |- ( iota_ x e. A ph ) = ( iota_ y e. A ps )
Theorem	cbvriota 6015*	Change bound variable in a restricted description binder. (Contributed by NM, 18-Mar-2013.) (Revised by Mario Carneiro, 15-Oct-2016.)
|- F/ y ph   &    |- F/ x ps   &    |- ( x = y -> ( ph <-> ps ) )   =>    |- ( iota_ x e. A ph ) = ( iota_ y e. A ps )
Theorem	cbvriotav 6016*	Change bound variable in a restricted description binder. (Contributed by NM, 18-Mar-2013.) (Revised by Mario Carneiro, 15-Oct-2016.)
|- ( x = y -> ( ph <-> ps ) )   =>    |- ( iota_ x e. A ph ) = ( iota_ y e. A ps )
Theorem	csbriotag 6017*	Interchange class substitution and restricted description binder. (Contributed by NM, 24-Feb-2013.)
|- ( A e. V -> [_ A / x ]_ ( iota_ y e. B ph ) = ( iota_ y e. B [. A / x ]. ph ) )
Theorem	riotacl2 6018	Membership law for "the unique element in A such that ph." (Contributed by NM, 21-Aug-2011.) (Revised by Mario Carneiro, 23-Dec-2016.)
|- ( E! x e. A ph -> ( iota_ x e. A ph ) e. { x e. A | ph } )
Theorem	riotacl 6019*	Closure of restricted iota. (Contributed by NM, 21-Aug-2011.)
|- ( E! x e. A ph -> ( iota_ x e. A ph ) e. A )
Theorem	riotasbc 6020	Substitution law for descriptions. (Contributed by NM, 23-Aug-2011.) (Proof shortened by Mario Carneiro, 24-Dec-2016.)
|- ( E! x e. A ph -> [. ( iota_ x e. A ph ) / x ]. ph )
Theorem	riotabidva 6021*	Equivalent wff's yield equal restricted class abstractions (deduction form). (rabbidva 2801 analog.) (Contributed by NM, 17-Jan-2012.)
|- ( ( ph /\ x e. A ) -> ( ps <-> ch ) )   =>    |- ( ph -> ( iota_ x e. A ps ) = ( iota_ x e. A ch ) )
Theorem	riotabiia 6022	Equivalent wff's yield equal restricted iotas (inference form). (rabbiia 2799 analog.) (Contributed by NM, 16-Jan-2012.)
|- ( x e. A -> ( ph <-> ps ) )   =>    |- ( iota_ x e. A ph ) = ( iota_ x e. A ps )
Theorem	riota1 6023*	Property of restricted iota. Compare iota1 5327. (Contributed by Mario Carneiro, 15-Oct-2016.)
|- ( E! x e. A ph -> ( ( x e. A /\ ph ) <-> ( iota_ x e. A ph ) = x ) )
Theorem	riota1a 6024	Property of iota. (Contributed by NM, 23-Aug-2011.)
|- ( ( x e. A /\ E! x e. A ph ) -> ( ph <-> ( iota x ( x e. A /\ ph ) ) = x ) )
Theorem	riota2df 6025*	A deduction version of riota2f 6026. (Contributed by NM, 17-Feb-2013.) (Revised by Mario Carneiro, 15-Oct-2016.)
|- F/ x ph   &    |- ( ph -> F/_ x B )   &    |- ( ph -> F/ x ch )   &    |- ( ph -> B e. A )   &    |- ( ( ph /\ x = B ) -> ( ps <-> ch ) )   =>    |- ( ( ph /\ E! x e. A ps ) -> ( ch <-> ( iota_ x e. A ps ) = B ) )
Theorem	riota2f 6026*	This theorem shows a condition that allows us to represent a descriptor with a class expression B. (Contributed by NM, 23-Aug-2011.) (Revised by Mario Carneiro, 15-Oct-2016.)
|- F/_ x B   &    |- F/ x ps   &    |- ( x = B -> ( ph <-> ps ) )   =>    |- ( ( B e. A /\ E! x e. A ph ) -> ( ps <-> ( iota_ x e. A ph ) = B ) )
Theorem	riota2 6027*	This theorem shows a condition that allows us to represent a descriptor with a class expression B. (Contributed by NM, 23-Aug-2011.) (Revised by Mario Carneiro, 10-Dec-2016.)
|- ( x = B -> ( ph <-> ps ) )   =>    |- ( ( B e. A /\ E! x e. A ph ) -> ( ps <-> ( iota_ x e. A ph ) = B ) )
Theorem	riotaeqimp 6028*	If two restricted iota descriptors for an equality are equal, then the terms of the equality are equal. (Contributed by AV, 6-Dec-2020.)
|- I = ( iota_ a e. V X = A )   &    |- J = ( iota_ a e. V Y = A )   &    |- ( ph -> E! a e. V X = A )   &    |- ( ph -> E! a e. V Y = A )   =>    |- ( ( ph /\ I = J ) -> X = Y )
Theorem	riotaprop 6029*	Properties of a restricted definite description operator. Todo (df-riota 6003 update): can some uses of riota2f 6026 be shortened with this? (Contributed by NM, 23-Nov-2013.)
|- F/ x ps   &    |- B = ( iota_ x e. A ph )   &    |- ( x = B -> ( ph <-> ps ) )   =>    |- ( E! x e. A ph -> ( B e. A /\ ps ) )
Theorem	riota5f 6030*	A method for computing restricted iota. (Contributed by NM, 16-Apr-2013.) (Revised by Mario Carneiro, 15-Oct-2016.)
|- ( ph -> F/_ x B )   &    |- ( ph -> B e. A )   &    |- ( ( ph /\ x e. A ) -> ( ps <-> x = B ) )   =>    |- ( ph -> ( iota_ x e. A ps ) = B )
Theorem	riota5 6031*	A method for computing restricted iota. (Contributed by NM, 20-Oct-2011.) (Revised by Mario Carneiro, 6-Dec-2016.)
|- ( ph -> B e. A )   &    |- ( ( ph /\ x e. A ) -> ( ps <-> x = B ) )   =>    |- ( ph -> ( iota_ x e. A ps ) = B )
Theorem	riotass2 6032*	Restriction of a unique element to a smaller class. (Contributed by NM, 21-Aug-2011.) (Revised by NM, 22-Mar-2013.)
|- ( ( ( A C_ B /\ A. x e. A ( ph -> ps ) ) /\ ( E. x e. A ph /\ E! x e. B ps ) ) -> ( iota_ x e. A ph ) = ( iota_ x e. B ps ) )
Theorem	riotass 6033*	Restriction of a unique element to a smaller class. (Contributed by NM, 19-Oct-2005.) (Revised by Mario Carneiro, 24-Dec-2016.)
|- ( ( A C_ B /\ E. x e. A ph /\ E! x e. B ph ) -> ( iota_ x e. A ph ) = ( iota_ x e. B ph ) )
Theorem	moriotass 6034*	Restriction of a unique element to a smaller class. (Contributed by NM, 19-Feb-2006.) (Revised by NM, 16-Jun-2017.)
|- ( ( A C_ B /\ E. x e. A ph /\ E* x e. B ph ) -> ( iota_ x e. A ph ) = ( iota_ x e. B ph ) )
Theorem	snriota 6035	A restricted class abstraction with a unique member can be expressed as a singleton. (Contributed by NM, 30-May-2006.)
|- ( E! x e. A ph -> { x e. A | ph } = { ( iota_ x e. A ph ) } )
Theorem	eusvobj2 6036*	Specify the same property in two ways when class B ( y ) is single-valued. (Contributed by NM, 1-Nov-2010.) (Proof shortened by Mario Carneiro, 24-Dec-2016.)
|- B e. _V   =>    |- ( E! x E. y e. A x = B -> ( E. y e. A x = B <-> A. y e. A x = B ) )
Theorem	eusvobj1 6037*	Specify the same object in two ways when class B ( y ) is single-valued. (Contributed by NM, 1-Nov-2010.) (Proof shortened by Mario Carneiro, 19-Nov-2016.)
|- B e. _V   =>    |- ( E! x E. y e. A x = B -> ( iota x E. y e. A x = B ) = ( iota x A. y e. A x = B ) )
Theorem	f1ofveu 6038*	There is one domain element for each value of a one-to-one onto function. (Contributed by NM, 26-May-2006.)
|- ( ( F : A -1-1-onto-> B /\ C e. B ) -> E! x e. A ( F ` x ) = C )
Theorem	f1ocnvfv3 6039*	Value of the converse of a one-to-one onto function. (Contributed by NM, 26-May-2006.) (Proof shortened by Mario Carneiro, 24-Dec-2016.)
|- ( ( F : A -1-1-onto-> B /\ C e. B ) -> ( `' F ` C ) = ( iota_ x e. A ( F ` x ) = C ) )
Theorem	riotaund 6040*	Restricted iota equals the empty set when not meaningful. (Contributed by NM, 16-Jan-2012.) (Revised by Mario Carneiro, 15-Oct-2016.) (Revised by NM, 13-Sep-2018.)
|- ( -. E! x e. A ph -> ( iota_ x e. A ph ) = (/) )
Theorem	acexmidlema 6041*	Lemma for acexmid 6049. (Contributed by Jim Kingdon, 6-Aug-2019.)
|- A = { x e. { (/) , { (/) } } | ( x = (/) \/ ph ) }   &    |- B = { x e. { (/) , { (/) } } | ( x = { (/) } \/ ph ) }   &    |- C = { A , B }   =>    |- ( { (/) } e. A -> ph )
Theorem	acexmidlemb 6042*	Lemma for acexmid 6049. (Contributed by Jim Kingdon, 6-Aug-2019.)
|- A = { x e. { (/) , { (/) } } | ( x = (/) \/ ph ) }   &    |- B = { x e. { (/) , { (/) } } | ( x = { (/) } \/ ph ) }   &    |- C = { A , B }   =>    |- ( (/) e. B -> ph )
Theorem	acexmidlemph 6043*	Lemma for acexmid 6049. (Contributed by Jim Kingdon, 6-Aug-2019.)
|- A = { x e. { (/) , { (/) } } | ( x = (/) \/ ph ) }   &    |- B = { x e. { (/) , { (/) } } | ( x = { (/) } \/ ph ) }   &    |- C = { A , B }   =>    |- ( ph -> A = B )
Theorem	acexmidlemab 6044*	Lemma for acexmid 6049. (Contributed by Jim Kingdon, 6-Aug-2019.)
|- A = { x e. { (/) , { (/) } } | ( x = (/) \/ ph ) }   &    |- B = { x e. { (/) , { (/) } } | ( x = { (/) } \/ ph ) }   &    |- C = { A , B }   =>    |- ( ( ( iota_ v e. A E. u e. y ( A e. u /\ v e. u ) ) = (/) /\ ( iota_ v e. B E. u e. y ( B e. u /\ v e. u ) ) = { (/) } ) -> -. ph )
Theorem	acexmidlemcase 6045*	Lemma for acexmid 6049. Here we divide the proof into cases (based on the disjunction implicit in an unordered pair, not the sort of case elimination which relies on excluded middle). The cases are (1) the choice function evaluated at A equals { (/) }, (2) the choice function evaluated at B equals (/), and (3) the choice function evaluated at A equals (/) and the choice function evaluated at B equals { (/) }. Because of the way we represent the choice function y, the choice function evaluated at A is ( iota_ v e. A E. u e. y ( A e. u /\ v e. u ) ) and the choice function evaluated at B is ( iota_ v e. B E. u e. y ( B e. u /\ v e. u ) ). Other than the difference in notation these work just as ( y ` A ) and ( y ` B ) would if y were a function as defined by df-fun 5354. Although it isn't exactly about the division into cases, it is also convenient for this lemma to also include the step that if the choice function evaluated at A equals { (/) }, then { (/) } e. A and likewise for B. (Contributed by Jim Kingdon, 7-Aug-2019.)
|- A = { x e. { (/) , { (/) } } | ( x = (/) \/ ph ) }   &    |- B = { x e. { (/) , { (/) } } | ( x = { (/) } \/ ph ) }   &    |- C = { A , B }   =>    |- ( A. z e. C E! v e. z E. u e. y ( z e. u /\ v e. u ) -> ( { (/) } e. A \/ (/) e. B \/ ( ( iota_ v e. A E. u e. y ( A e. u /\ v e. u ) ) = (/) /\ ( iota_ v e. B E. u e. y ( B e. u /\ v e. u ) ) = { (/) } ) ) )
Theorem	acexmidlem1 6046*	Lemma for acexmid 6049. List the cases identified in acexmidlemcase 6045 and hook them up to the lemmas which handle each case. (Contributed by Jim Kingdon, 7-Aug-2019.)
|- A = { x e. { (/) , { (/) } } | ( x = (/) \/ ph ) }   &    |- B = { x e. { (/) , { (/) } } | ( x = { (/) } \/ ph ) }   &    |- C = { A , B }   =>    |- ( A. z e. C E! v e. z E. u e. y ( z e. u /\ v e. u ) -> ( ph \/ -. ph ) )
Theorem	acexmidlem2 6047*	Lemma for acexmid 6049. This builds on acexmidlem1 6046 by noting that every element of C is inhabited. (Note that y is not quite a function in the df-fun 5354 sense because it uses ordered pairs as described in opthreg 4678 rather than df-op 3698). The set A is also found in onsucelsucexmidlem 4651. (Contributed by Jim Kingdon, 5-Aug-2019.)
|- A = { x e. { (/) , { (/) } } | ( x = (/) \/ ph ) }   &    |- B = { x e. { (/) , { (/) } } | ( x = { (/) } \/ ph ) }   &    |- C = { A , B }   =>    |- ( A. z e. C A. w e. z E! v e. z E. u e. y ( z e. u /\ v e. u ) -> ( ph \/ -. ph ) )
Theorem	acexmidlemv 6048*	Lemma for acexmid 6049. This is acexmid 6049 with additional disjoint variable conditions, most notably between ph and x. (Contributed by Jim Kingdon, 6-Aug-2019.)
|- E. y A. z e. x A. w e. z E! v e. z E. u e. y ( z e. u /\ v e. u )   =>    |- ( ph \/ -. ph )
Theorem	acexmid 6049*	The axiom of choice implies excluded middle. Theorem 1.3 in [Bauer] p. 483. The statement of the axiom of choice given here is ac2 in the Metamath Proof Explorer (version of 3-Aug-2019). In particular, note that the choice function y provides a value when z is inhabited (as opposed to nonempty as in some statements of the axiom of choice). Essentially the same proof can also be found at "The axiom of choice implies instances of EM", [Crosilla], p. "Set-theoretic principles incompatible with intuitionistic logic". Often referred to as Diaconescu's theorem, or Diaconescu-Goodman-Myhill theorem, after Radu Diaconescu who discovered it in 1975 in the framework of topos theory and N. D. Goodman and John Myhill in 1978 in the framework of set theory (although it already appeared as an exercise in Errett Bishop's book Foundations of Constructive Analysis from 1967). For this theorem stated using the df-ac 7513 and df-exmid 4308 syntaxes, see exmidac 7516. (Contributed by Jim Kingdon, 4-Aug-2019.)
|- E. y A. z e. x A. w e. z E! v e. z E. u e. y ( z e. u /\ v e. u )   =>    |- ( ph \/ -. ph )
2.6.11  Operations
Syntax	co 6050	Extend class notation to include the value of an operation F (such as + ) 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 ( A F B )
Syntax	coprab 6051	Extend class notation to include class abstraction (class builder) of nested ordered pairs.
class { <. <. x , y >. , z >. | ph }
Syntax	cmpo 6052	Extend the definition of a class to include maps-to notation for defining an operation via a rule.
class ( x e. A , y e. B |-> C )
Definition	df-ov 6053	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. For example, if class F is the operation + and arguments A and B are 3 and 2 , the expression ( 3 + 2 ) can be proved to equal 5 . This definition is well-defined, although not very meaningful, when classes A and/or B are proper classes (i.e. are not sets); see ovprc1 6087 and ovprc2 6088. 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 6054. (Contributed by NM, 28-Feb-1995.)
|- ( A F B ) = ( F ` <. A , B >. )
Definition	df-oprab 6054*	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 6053 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 ovmpo 6189. (Contributed by NM, 12-Mar-1995.)
|- { <. <. x , y >. , z >. | ph } = { w | E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) }
Definition	df-mpo 6055*	Define maps-to notation for defining an operation via a rule. Read as "the operation defined by the map from x , y (in A X. B) to B ( x , y )". An extension of df-mpt 4173 for two arguments. (Contributed by NM, 17-Feb-2008.)
|- ( x e. A , y e. B |-> C ) = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) }
Theorem	oveq 6056	Equality theorem for operation value. (Contributed by NM, 28-Feb-1995.)
|- ( F = G -> ( A F B ) = ( A G B ) )
Theorem	oveq1 6057	Equality theorem for operation value. (Contributed by NM, 28-Feb-1995.)
|- ( A = B -> ( A F C ) = ( B F C ) )
Theorem	oveq2 6058	Equality theorem for operation value. (Contributed by NM, 28-Feb-1995.)
|- ( A = B -> ( C F A ) = ( C F B ) )
Theorem	oveq12 6059	Equality theorem for operation value. (Contributed by NM, 16-Jul-1995.)
|- ( ( A = B /\ C = D ) -> ( A F C ) = ( B F D ) )
Theorem	oveq1i 6060	Equality inference for operation value. (Contributed by NM, 28-Feb-1995.)
|- A = B   =>    |- ( A F C ) = ( B F C )
Theorem	oveq2i 6061	Equality inference for operation value. (Contributed by NM, 28-Feb-1995.)
|- A = B   =>    |- ( C F A ) = ( C F B )
Theorem	oveq12i 6062	Equality inference for operation value. (Contributed by NM, 28-Feb-1995.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
|- A = B   &    |- C = D   =>    |- ( A F C ) = ( B F D )
Theorem	oveqi 6063	Equality inference for operation value. (Contributed by NM, 24-Nov-2007.)
|- A = B   =>    |- ( C A D ) = ( C B D )
Theorem	oveq123i 6064	Equality inference for operation value. (Contributed by FL, 11-Jul-2010.)
|- A = C   &    |- B = D   &    |- F = G   =>    |- ( A F B ) = ( C G D )
Theorem	oveq1d 6065	Equality deduction for operation value. (Contributed by NM, 13-Mar-1995.)
|- ( ph -> A = B )   =>    |- ( ph -> ( A F C ) = ( B F C ) )
Theorem	oveq2d 6066	Equality deduction for operation value. (Contributed by NM, 13-Mar-1995.)
|- ( ph -> A = B )   =>    |- ( ph -> ( C F A ) = ( C F B ) )
Theorem	oveqd 6067	Equality deduction for operation value. (Contributed by NM, 9-Sep-2006.)
|- ( ph -> A = B )   =>    |- ( ph -> ( C A D ) = ( C B D ) )
Theorem	oveq12d 6068	Equality deduction for operation value. (Contributed by NM, 13-Mar-1995.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
|- ( ph -> A = B )   &    |- ( ph -> C = D )   =>    |- ( ph -> ( A F C ) = ( B F D ) )
Theorem	oveqan12d 6069	Equality deduction for operation value. (Contributed by NM, 10-Aug-1995.)
|- ( ph -> A = B )   &    |- ( ps -> C = D )   =>    |- ( ( ph /\ ps ) -> ( A F C ) = ( B F D ) )
Theorem	oveqan12rd 6070	Equality deduction for operation value. (Contributed by NM, 10-Aug-1995.)
|- ( ph -> A = B )   &    |- ( ps -> C = D )   =>    |- ( ( ps /\ ph ) -> ( A F C ) = ( B F D ) )
Theorem	oveq123d 6071	Equality deduction for operation value. (Contributed by FL, 22-Dec-2008.)
|- ( ph -> F = G )   &    |- ( ph -> A = B )   &    |- ( ph -> C = D )   =>    |- ( ph -> ( A F C ) = ( B G D ) )
Theorem	fvoveq1d 6072	Equality deduction for nested function and operation value. (Contributed by AV, 23-Jul-2022.)
|- ( ph -> A = B )   =>    |- ( ph -> ( F ` ( A O C ) ) = ( F ` ( B O C ) ) )
Theorem	fvoveq1 6073	Equality theorem for nested function and operation value. Closed form of fvoveq1d 6072. (Contributed by AV, 23-Jul-2022.)
|- ( A = B -> ( F ` ( A O C ) ) = ( F ` ( B O C ) ) )
Theorem	ovanraleqv 6074*	Equality theorem for a conjunction with an operation values within a restricted universal quantification. Technical theorem to be used to reduce the size of a significant number of proofs. (Contributed by AV, 13-Aug-2022.)
|- ( B = X -> ( ph <-> ps ) )   =>    |- ( B = X -> ( A. x e. V ( ph /\ ( A .x. B ) = C ) <-> A. x e. V ( ps /\ ( A .x. X ) = C ) ) )
Theorem	imbrov2fvoveq 6075	Equality theorem for nested function and operation value in an implication for a binary relation. Technical theorem to be used to reduce the size of a significant number of proofs. (Contributed by AV, 17-Aug-2022.)
|- ( X = Y -> ( ph <-> ps ) )   =>    |- ( X = Y -> ( ( ph -> ( F ` ( ( G ` X ) .x. O ) ) R A ) <-> ( ps -> ( F ` ( ( G ` Y ) .x. O ) ) R A ) ) )
Theorem	ovrspc2v 6076*	If an operation value is element of a class for all operands of two classes, then the operation value is an element of the class for specific operands of the two classes. (Contributed by Mario Carneiro, 6-Dec-2014.)
|- ( ( ( X e. A /\ Y e. B ) /\ A. x e. A A. y e. B ( x F y ) e. C ) -> ( X F Y ) e. C )
Theorem	oveqrspc2v 6077*	Restricted specialization of operands, using implicit substitution. (Contributed by Mario Carneiro, 6-Dec-2014.)
|- ( ( ph /\ ( x e. A /\ y e. B ) ) -> ( x F y ) = ( x G y ) )   =>    |- ( ( ph /\ ( X e. A /\ Y e. B ) ) -> ( X F Y ) = ( X G Y ) )
Theorem	oveqdr 6078	Equality of two operations for any two operands. Useful in proofs using *propd theorems. (Contributed by Mario Carneiro, 29-Jun-2015.)
|- ( ph -> F = G )   =>    |- ( ( ph /\ ps ) -> ( x F y ) = ( x G y ) )
Theorem	nfovd 6079	Deduction version of bound-variable hypothesis builder nfov 6080. (Contributed by NM, 13-Dec-2005.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
|- ( ph -> F/_ x A )   &    |- ( ph -> F/_ x F )   &    |- ( ph -> F/_ x B )   =>    |- ( ph -> F/_ x ( A F B ) )
Theorem	nfov 6080	Bound-variable hypothesis builder for operation value. (Contributed by NM, 4-May-2004.)
|- F/_ x A   &    |- F/_ x F   &    |- F/_ x B   =>    |- F/_ x ( A F B )
Theorem	oprabidlem 6081*	Slight elaboration of exdistrfor 1849. A lemma for oprabid 6082. (Contributed by Jim Kingdon, 15-Jan-2019.)
|- ( E. x E. y ( x = z /\ ps ) -> E. x ( x = z /\ E. y ps ) )
Theorem	oprabid 6082	The law of concretion. Special case of Theorem 9.5 of [Quine] p. 61. Although this theorem would be useful with a distinct variable condition between x, y, and z, we use ax-bndl 1558 to eliminate that constraint. (Contributed by Mario Carneiro, 20-Mar-2013.)
|- ( <. <. x , y >. , z >. e. { <. <. x , y >. , z >. | ph } <-> ph )
Theorem	fnovex 6083	The result of an operation is a set. (Contributed by Jim Kingdon, 15-Jan-2019.)
|- ( ( F Fn ( C X. D ) /\ A e. C /\ B e. D ) -> ( A F B ) e. _V )
Theorem	ovexg 6084	Evaluating a set operation at two sets gives a set. (Contributed by Jim Kingdon, 19-Aug-2021.)
|- ( ( A e. V /\ F e. W /\ B e. X ) -> ( A F B ) e. _V )
Theorem	ovssunirng 6085	The result of an operation value is always a subset of the union of the range. (Contributed by Mario Carneiro, 12-Jan-2017.)
|- ( ( X e. V /\ Y e. W ) -> ( X F Y ) C_ U. ran F )
Theorem	ovprc 6086	The value of an operation when the one of the arguments is a proper class. Note: this theorem is dependent on our particular definitions of operation value, function value, and ordered pair. (Contributed by Mario Carneiro, 26-Apr-2015.)
|- Rel dom F   =>    |- ( -. ( A e. _V /\ B e. _V ) -> ( A F B ) = (/) )
Theorem	ovprc1 6087	The value of an operation when the first argument is a proper class. (Contributed by NM, 16-Jun-2004.)
|- Rel dom F   =>    |- ( -. A e. _V -> ( A F B ) = (/) )
Theorem	ovprc2 6088	The value of an operation when the second argument is a proper class. (Contributed by Mario Carneiro, 26-Apr-2015.)
|- Rel dom F   =>    |- ( -. B e. _V -> ( A F B ) = (/) )
Theorem	csbov123g 6089	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 ]_ ( B F C ) = ( [_ A / x ]_ B [_ A / x ]_ F [_ A / x ]_ C ) )
Theorem	csbov12g 6090*	Move class substitution in and out of an operation. (Contributed by NM, 12-Nov-2005.)
|- ( A e. V -> [_ A / x ]_ ( B F C ) = ( [_ A / x ]_ B F [_ A / x ]_ C ) )
Theorem	csbov1g 6091*	Move class substitution in and out of an operation. (Contributed by NM, 12-Nov-2005.)
|- ( A e. V -> [_ A / x ]_ ( B F C ) = ( [_ A / x ]_ B F C ) )
Theorem	csbov2g 6092*	Move class substitution in and out of an operation. (Contributed by NM, 12-Nov-2005.)
|- ( A e. V -> [_ A / x ]_ ( B F C ) = ( B F [_ A / x ]_ C ) )
Theorem	rspceov 6093*	A frequently used special case of rspc2ev 2936 for operation values. (Contributed by NM, 21-Mar-2007.)
|- ( ( C e. A /\ D e. B /\ S = ( C F D ) ) -> E. x e. A E. y e. B S = ( x F y ) )
Theorem	elovimad 6094	Elementhood of the image set of an operation value. (Contributed by Thierry Arnoux, 13-Mar-2017.)
|- ( ph -> A e. C )   &    |- ( ph -> B e. D )   &    |- ( ph -> Fun F )   &    |- ( ph -> ( C X. D ) C_ dom F )   =>    |- ( ph -> ( A F B ) e. ( F " ( C X. D ) ) )
Theorem	fnbrovb 6095	Value of a binary operation expressed as a binary relation. See also fnbrfvb 5715 for functions on Cartesian products. (Contributed by BJ, 15-Feb-2022.)
|- ( ( F Fn ( V X. W ) /\ ( A e. V /\ B e. W ) ) -> ( ( A F B ) = C <-> <. A , B >. F C ) )
Theorem	fnotovb 6096	Equivalence of operation value and ordered triple membership, analogous to fnopfvb 5716. (Contributed by NM, 17-Dec-2008.) (Revised by Mario Carneiro, 28-Apr-2015.)
|- ( ( F Fn ( A X. B ) /\ C e. A /\ D e. B ) -> ( ( C F D ) = R <-> <. C , D , R >. e. F ) )
Theorem	opabbrex 6097*	A collection of ordered pairs with an extension of a binary relation is a set. (Contributed by Alexander van der Vekens, 1-Nov-2017.)
|- ( ( V e. _V /\ E e. _V ) -> ( f ( V W E ) p -> th ) )   &    |- ( ( V e. _V /\ E e. _V ) -> { <. f , p >. | th } e. _V )   =>    |- ( ( V e. _V /\ E e. _V ) -> { <. f , p >. | ( f ( V W E ) p /\ ps ) } e. _V )
Theorem	0neqopab 6098	The empty set is never an element in an ordered-pair class abstraction. (Contributed by Alexander van der Vekens, 5-Nov-2017.)
|- -. (/) e. { <. x , y >. | ph }
Theorem	brabvv 6099*	If two classes are in a relationship given by an ordered-pair class abstraction, the classes are sets. (Contributed by Jim Kingdon, 16-Jan-2019.)
|- ( X { <. x , y >. | ph } Y -> ( X e. _V /\ Y e. _V ) )
Theorem	dfoprab2 6100*	Class abstraction for operations in terms of class abstraction of ordered pairs. (Contributed by NM, 12-Mar-1995.)
|- { <. <. x , y >. , z >. | ph } = { <. w , z >. | E. x E. y ( w = <. x , y >. /\ ph ) }