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.)
|
|
|
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.)
|
|
|
Theorem | dmoprabss 5935* |
The domain of an operation class abstraction. (Contributed by NM,
24-Aug-1995.)
|
|
|
Theorem | rnoprab 5936* |
The range of an operation class abstraction. (Contributed by NM,
30-Aug-2004.) (Revised by David Abernethy, 19-Apr-2013.)
|
|
|
Theorem | rnoprab2 5937* |
The range of a restricted operation class abstraction. (Contributed by
Scott Fenton, 21-Mar-2012.)
|
|
|
Theorem | reldmoprab 5938* |
The domain of an operation class abstraction is a relation.
(Contributed by NM, 17-Mar-1995.)
|
|
|
Theorem | oprabss 5939* |
Structure of an operation class abstraction. (Contributed by NM,
28-Nov-2006.)
|
|
|
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.)
|
|
|
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.)
|
|
|
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.)
|
|
|
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.)
|
|
|
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.)
|
|
|
Theorem | fnoprabg 5954* |
Functionality and domain of an operation class abstraction.
(Contributed by NM, 28-Aug-2007.)
|
|
|
Theorem | mpofun 5955* |
The maps-to notation for an operation is always a function.
(Contributed by Scott Fenton, 21-Mar-2012.)
|
|
|
Theorem | fnoprab 5956* |
Functionality and domain of an operation class abstraction.
(Contributed by NM, 15-May-1995.)
|
|
|
Theorem | ffnov 5957* |
An operation maps to a class to which all values belong. (Contributed
by NM, 7-Feb-2004.)
|
|
|
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.)
|
|
|
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.)
|
|
|
Theorem | fnovim 5961* |
Representation of a function in terms of its values. (Contributed by
Jim Kingdon, 16-Jan-2019.)
|
|
|
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.)
|
|
|
Theorem | reldmmpo 5964* |
The domain of an operation defined by maps-to notation is a relation.
(Contributed by Stefan O'Rear, 27-Nov-2014.)
|
|
|
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.)
|
|
|
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.)
|
|
|
Theorem | ralrnmpo 5967* |
A restricted quantifier over an image set. (Contributed by Mario
Carneiro, 1-Sep-2015.)
|
|
|
Theorem | rexrnmpo 5968* |
A restricted quantifier over an image set. (Contributed by Mario
Carneiro, 1-Sep-2015.)
|
|
|
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.)
|
|
|
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.)
|
|
|
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.)
|
|
|
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.)
|
|
|
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.)
|
|
|
Theorem | foov 5999* |
An onto mapping of an operation expressed in terms of operation values.
(Contributed by NM, 29-Oct-2006.)
|
|
|
Theorem | fnovrn 6000 |
An operation's value belongs to its range. (Contributed by NM,
10-Feb-2007.)
|
|