Type | Label | Description |
Statement |
|
Theorem | ovrspc2v 5901* |
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.)
|
    
         
  |
|
Theorem | oveqrspc2v 5902* |
Restricted specialization of operands, using implicit substitution.
(Contributed by Mario Carneiro, 6-Dec-2014.)
|
  
 
           
 
          |
|
Theorem | oveqdr 5903 |
Equality of two operations for any two operands. Useful in proofs using
*propd theorems. (Contributed by Mario Carneiro, 29-Jun-2015.)
|
               |
|
Theorem | nfovd 5904 |
Deduction version of bound-variable hypothesis builder nfov 5905.
(Contributed by NM, 13-Dec-2005.) (Proof shortened by Andrew Salmon,
22-Oct-2011.)
|
            
        |
|
Theorem | nfov 5905 |
Bound-variable hypothesis builder for operation value. (Contributed by
NM, 4-May-2004.)
|
             |
|
Theorem | oprabidlem 5906* |
Slight elaboration of exdistrfor 1800. A lemma for oprabid 5907.
(Contributed by Jim Kingdon, 15-Jan-2019.)
|
               |
|
Theorem | oprabid 5907 |
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 , , and , we use ax-bndl 1509 to eliminate that
constraint. (Contributed by Mario Carneiro, 20-Mar-2013.)
|
             
   |
|
Theorem | fnovex 5908 |
The result of an operation is a set. (Contributed by Jim Kingdon,
15-Jan-2019.)
|
  
     
  |
|
Theorem | ovexg 5909 |
Evaluating a set operation at two sets gives a set. (Contributed by Jim
Kingdon, 19-Aug-2021.)
|
      
  |
|
Theorem | ovprc 5910 |
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.)
|
         |
|
Theorem | ovprc1 5911 |
The value of an operation when the first argument is a proper class.
(Contributed by NM, 16-Jun-2004.)
|
    
  |
|
Theorem | ovprc2 5912 |
The value of an operation when the second argument is a proper class.
(Contributed by Mario Carneiro, 26-Apr-2015.)
|
    
  |
|
Theorem | csbov123g 5913 |
Move class substitution in and out of an operation. (Contributed by NM,
12-Nov-2005.) (Proof shortened by Mario Carneiro, 5-Dec-2016.)
|
   ![]_ ]_](_urbrack.gif)    
   ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)    |
|
Theorem | csbov12g 5914* |
Move class substitution in and out of an operation. (Contributed by NM,
12-Nov-2005.)
|
   ![]_ ]_](_urbrack.gif)    
   ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)    |
|
Theorem | csbov1g 5915* |
Move class substitution in and out of an operation. (Contributed by NM,
12-Nov-2005.)
|
   ![]_ ]_](_urbrack.gif)    
   ![]_ ]_](_urbrack.gif)      |
|
Theorem | csbov2g 5916* |
Move class substitution in and out of an operation. (Contributed by NM,
12-Nov-2005.)
|
   ![]_ ]_](_urbrack.gif)    
     ![]_ ]_](_urbrack.gif)    |
|
Theorem | rspceov 5917* |
A frequently used special case of rspc2ev 2857 for operation values.
(Contributed by NM, 21-Mar-2007.)
|
        
      |
|
Theorem | fnotovb 5918 |
Equivalence of operation value and ordered triple membership, analogous to
fnopfvb 5558. (Contributed by NM, 17-Dec-2008.) (Revised
by Mario
Carneiro, 28-Apr-2015.)
|
  
      
 
     |
|
Theorem | opabbrex 5919* |
A collection of ordered pairs with an extension of a binary relation is
a set. (Contributed by Alexander van der Vekens, 1-Nov-2017.)
|
         
        
        
           |
|
Theorem | 0neqopab 5920 |
The empty set is never an element in an ordered-pair class abstraction.
(Contributed by Alexander van der Vekens, 5-Nov-2017.)
|
      |
|
Theorem | brabvv 5921* |
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.)
|
       
    |
|
Theorem | dfoprab2 5922* |
Class abstraction for operations in terms of class abstraction of
ordered pairs. (Contributed by NM, 12-Mar-1995.)
|
                       |
|
Theorem | reloprab 5923* |
An operation class abstraction is a relation. (Contributed by NM,
16-Jun-2004.)
|
         |
|
Theorem | nfoprab1 5924 |
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 5925 |
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 5926 |
The abstraction variables in an operation class abstraction are not
free. (Contributed by NM, 22-Aug-2013.)
|
           |
|
Theorem | nfoprab 5927* |
Bound-variable hypothesis builder for an operation class abstraction.
(Contributed by NM, 22-Aug-2013.)
|
             |
|
Theorem | oprabbid 5928* |
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 5929* |
Equivalent wff's yield equal operation class abstractions (deduction
form). (Contributed by NM, 21-Feb-2004.)
|
                       |
|
Theorem | oprabbii 5930* |
Equivalent wff's yield equal operation class abstractions. (Contributed
by NM, 28-May-1995.) (Revised by David Abernethy, 19-Jun-2012.)
|
                   |
|
Theorem | ssoprab2 5931 |
Equivalence of ordered pair abstraction subclass and implication.
Compare ssopab2 4276. (Contributed by FL, 6-Nov-2013.) (Proof
shortened
by Mario Carneiro, 11-Dec-2016.)
|
            
  
           |
|
Theorem | ssoprab2b 5932 |
Equivalence of ordered pair abstraction subclass and implication. Compare
ssopab2b 4277. (Contributed by FL, 6-Nov-2013.) (Proof
shortened by Mario
Carneiro, 11-Dec-2016.)
|
        
   
  
           |
|
Theorem | eqoprab2b 5933 |
Equivalence of ordered pair abstraction subclass and biconditional.
Compare eqopab2b 4280. (Contributed by Mario Carneiro,
4-Jan-2017.)
|
        
      
           |
|
Theorem | mpoeq123 5934* |
An equality theorem for the maps-to notation. (Contributed by Mario
Carneiro, 16-Dec-2013.) (Revised by Mario Carneiro, 19-Mar-2015.)
|
      
    
   |
|
Theorem | mpoeq12 5935* |
An equality theorem for the maps-to notation. (Contributed by Mario
Carneiro, 16-Dec-2013.)
|
       
   |
|
Theorem | mpoeq123dva 5936* |
An equality deduction for the maps-to notation. (Contributed by Mario
Carneiro, 26-Jan-2017.)
|
        
 
  

      |
|
Theorem | mpoeq123dv 5937* |
An equality deduction for the maps-to notation. (Contributed by NM,
12-Sep-2011.)
|
       

      |
|
Theorem | mpoeq123i 5938 |
An equality inference for the maps-to notation. (Contributed by NM,
15-Jul-2013.)
|


     |
|
Theorem | mpoeq3dva 5939* |
Slightly more general equality inference for the maps-to notation.
(Contributed by NM, 17-Oct-2013.)
|
     

      |
|
Theorem | mpoeq3ia 5940 |
An equality inference for the maps-to notation. (Contributed by Mario
Carneiro, 16-Dec-2013.)
|
     



  |
|
Theorem | mpoeq3dv 5941* |
An equality deduction for the maps-to notation restricted to the value
of the operation. (Contributed by SO, 16-Jul-2018.)
|
   

      |
|
Theorem | nfmpo1 5942 |
Bound-variable hypothesis builder for an operation in maps-to notation.
(Contributed by NM, 27-Aug-2013.)
|
      |
|
Theorem | nfmpo2 5943 |
Bound-variable hypothesis builder for an operation in maps-to notation.
(Contributed by NM, 27-Aug-2013.)
|
      |
|
Theorem | nfmpo 5944* |
Bound-variable hypothesis builder for the maps-to notation.
(Contributed by NM, 20-Feb-2013.)
|
            |
|
Theorem | mpo0 5945 |
A mapping operation with empty domain. (Contributed by Stefan O'Rear,
29-Jan-2015.) (Revised by Mario Carneiro, 15-May-2015.)
|
    |
|
Theorem | oprab4 5946* |
Two ways to state the domain of an operation. (Contributed by FL,
24-Jan-2010.)
|
                       
    |
|
Theorem | cbvoprab1 5947* |
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 5948* |
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 5949* |
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 5950* |
Rule used to change first two bound variables in an operation
abstraction, using implicit substitution. (Contributed by NM,
8-Oct-2004.)
|
             
      
  |
|
Theorem | cbvoprab3 5951* |
Rule used to change the third bound variable in an operation
abstraction, using implicit substitution. (Contributed by NM,
22-Aug-2013.)
|
    
          
      
  |
|
Theorem | cbvoprab3v 5952* |
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 5953* |
Rule to change the bound variable in a maps-to function, using implicit
substitution. This version of cbvmpo 5954 allows to be a function of
. (Contributed
by NM, 29-Dec-2014.)
|
                   

 
  |
|
Theorem | cbvmpo 5954* |
Rule to change the bound variable in a maps-to function, using implicit
substitution. (Contributed by NM, 17-Dec-2013.)
|
             

 
  |
|
Theorem | cbvmpov 5955* |
Rule to change the bound variable in a maps-to function, using implicit
substitution. With a longer proof analogous to cbvmpt 4099, some distinct
variable requirements could be eliminated. (Contributed by NM,
11-Jun-2013.)
|
  
 


 
  |
|
Theorem | dmoprab 5956* |
The domain of an operation class abstraction. (Contributed by NM,
17-Mar-1995.) (Revised by David Abernethy, 19-Jun-2012.)
|
                |
|
Theorem | dmoprabss 5957* |
The domain of an operation class abstraction. (Contributed by NM,
24-Aug-1995.)
|
        
   
  |
|
Theorem | rnoprab 5958* |
The range of an operation class abstraction. (Contributed by NM,
30-Aug-2004.) (Revised by David Abernethy, 19-Apr-2013.)
|
               |
|
Theorem | rnoprab2 5959* |
The range of a restricted operation class abstraction. (Contributed by
Scott Fenton, 21-Mar-2012.)
|
        
   
    |
|
Theorem | reldmoprab 5960* |
The domain of an operation class abstraction is a relation.
(Contributed by NM, 17-Mar-1995.)
|
         |
|
Theorem | oprabss 5961* |
Structure of an operation class abstraction. (Contributed by NM,
28-Nov-2006.)
|
             |
|
Theorem | eloprabga 5962* |
The law of concretion for operation class abstraction. Compare
elopab 4259. (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 5963* |
The law of concretion for operation class abstraction. Compare
elopab 4259. (Contributed by NM, 14-Sep-1999.) (Revised
by David
Abernethy, 19-Jun-2012.)
|
              
   
  
   
  
    |
|
Theorem | ssoprab2i 5964* |
Inference of operation class abstraction subclass from implication.
(Contributed by NM, 11-Nov-1995.) (Revised by David Abernethy,
19-Jun-2012.)
|
     
  
          |
|
Theorem | mpov 5965* |
Operation with universal domain in maps-to notation. (Contributed by
NM, 16-Aug-2013.)
|
 

      
  |
|
Theorem | mpomptx 5966* |
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 5967* |
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 5968 |
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 5969 |
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 5970* |
Representation of a constant operation using the mapping operation.
(Contributed by SO, 11-Jul-2018.)
|
  
  


  |
|
Theorem | resoprab 5971* |
Restriction of an operation class abstraction. (Contributed by NM,
10-Feb-2007.)
|
        
                |
|
Theorem | resoprab2 5972* |
Restriction of an operator abstraction. (Contributed by Jeff Madsen,
2-Sep-2009.)
|
       
  
 
                    |
|
Theorem | resmpo 5973* |
Restriction of the mapping operation. (Contributed by Mario Carneiro,
17-Dec-2013.)
|
       
       |
|
Theorem | funoprabg 5974* |
"At most one" is a sufficient condition for an operation class
abstraction to be a function. (Contributed by NM, 28-Aug-2007.)
|
                 |
|
Theorem | funoprab 5975* |
"At most one" is a sufficient condition for an operation class
abstraction to be a function. (Contributed by NM, 17-Mar-1995.)
|
           |
|
Theorem | fnoprabg 5976* |
Functionality and domain of an operation class abstraction.
(Contributed by NM, 28-Aug-2007.)
|
                
         |
|
Theorem | mpofun 5977* |
The maps-to notation for an operation is always a function.
(Contributed by Scott Fenton, 21-Mar-2012.)
|
  
 |
|
Theorem | fnoprab 5978* |
Functionality and domain of an operation class abstraction.
(Contributed by NM, 15-May-1995.)
|
           
        |
|
Theorem | ffnov 5979* |
An operation maps to a class to which all values belong. (Contributed
by NM, 7-Feb-2004.)
|
        
          |
|
Theorem | fovcl 5980 |
Closure law for an operation. (Contributed by NM, 19-Apr-2007.)
|
               |
|
Theorem | eqfnov 5981* |
Equality of two operations is determined by their values. (Contributed
by NM, 1-Sep-2005.)
|
  
       
  
             |
|
Theorem | eqfnov2 5982* |
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 5983* |
Representation of a function in terms of its values. (Contributed by
Jim Kingdon, 16-Jan-2019.)
|
  
         |
|
Theorem | mpo2eqb 5984* |
Bidirectional equality theorem for a mapping abstraction. Equivalent to
eqfnov2 5982. (Contributed by Mario Carneiro,
4-Jan-2017.)
|
        

     |
|
Theorem | rnmpo 5985* |
The range of an operation given by the maps-to notation. (Contributed
by FL, 20-Jun-2011.)
|
  

    |
|
Theorem | reldmmpo 5986* |
The domain of an operation defined by maps-to notation is a relation.
(Contributed by Stefan O'Rear, 27-Nov-2014.)
|
  
 |
|
Theorem | elrnmpog 5987* |
Membership in the range of an operation class abstraction. (Contributed
by NM, 27-Aug-2007.) (Revised by Mario Carneiro, 31-Aug-2015.)
|
      
   |
|
Theorem | elrnmpo 5988* |
Membership in the range of an operation class abstraction.
(Contributed by NM, 1-Aug-2004.) (Revised by Mario Carneiro,
31-Aug-2015.)
|
    

  |
|
Theorem | ralrnmpo 5989* |
A restricted quantifier over an image set. (Contributed by Mario
Carneiro, 1-Sep-2015.)
|
                  |
|
Theorem | rexrnmpo 5990* |
A restricted quantifier over an image set. (Contributed by Mario
Carneiro, 1-Sep-2015.)
|
              
   |
|
Theorem | ovid 5991* |
The value of an operation class abstraction. (Contributed by NM,
16-May-1995.) (Revised by David Abernethy, 19-Jun-2012.)
|
            
 
              |
|
Theorem | ovidig 5992* |
The value of an operation class abstraction. Compare ovidi 5993. The
condition   is been
removed. (Contributed by
Mario Carneiro, 29-Dec-2014.)
|
        
        |
|
Theorem | ovidi 5993* |
The value of an operation class abstraction (weak version).
(Contributed by Mario Carneiro, 29-Dec-2014.)
|
            
 
              |
|
Theorem | ov 5994* |
The value of an operation class abstraction. (Contributed by NM,
16-May-1995.) (Revised by David Abernethy, 19-Jun-2012.)
|

            
       
  
 
          
   |
|
Theorem | ovigg 5995* |
The value of an operation class abstraction. Compare ovig 5996.
The
condition   is been
removed. (Contributed by FL,
24-Mar-2007.) (Revised by Mario Carneiro, 19-Dec-2013.)
|
              
   
    
   |
|
Theorem | ovig 5996* |
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 5997* |
Value of a function given by the maps-to notation. (This is the
operation analog of fvmpt2 5600.) (Contributed by NM, 21-Feb-2004.)
(Revised by Mario Carneiro, 1-Sep-2015.)
|
     
      |
|
Theorem | ovmpos 5998* |
Value of a function given by the maps-to notation, expressed using
explicit substitution. (Contributed by Mario Carneiro, 30-Apr-2015.)
|
       ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif) 
      ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   |
|
Theorem | ov2gf 5999* |
The value of an operation class abstraction. A version of ovmpog 6009
using bound-variable hypotheses. (Contributed by NM, 17-Aug-2006.)
(Revised by Mario Carneiro, 19-Dec-2013.)
|
          
    
       
  |
|
Theorem | ovmpodxf 6000* |
Value of an operation given by a maps-to rule, deduction form.
(Contributed by Mario Carneiro, 29-Dec-2014.)
|
  
   
  
  
                           |