Type | Label | Description |
Statement |
|
Theorem | f1ores 5301 |
The restriction of a one-to-one function maps one-to-one onto the image.
(Contributed by set.mm contributors, 25-Mar-1998.)
|
      
            |
|
Theorem | f1orescnv 5302 |
The converse of a one-to-one-onto restricted function. (Contributed by
Paul Chapman, 21-Apr-2008.)
|
                   |
|
Theorem | f1imacnv 5303 |
Preimage of an image. (Contributed by set.mm contributors,
30-Sep-2004.)
|
      
           |
|
Theorem | foimacnv 5304 |
A reverse version of f1imacnv 5303. (Contributed by Jeffrey Hankins,
16-Jul-2009.)
|
      
           |
|
Theorem | f1oun 5305 |
The union of two one-to-one onto functions with disjoint domains and
ranges. (Contributed by set.mm contributors, 26-Mar-1998.)
|
           
  
   
            |
|
Theorem | fun11iun 5306* |
The union of a chain (with respect to inclusion) of one-to-one functions
is a one-to-one function. (Contributed by Mario Carneiro, 20-May-2013.)
(Revised by Mario Carneiro, 24-Jun-2015.)
|
          
          |
|
Theorem | resdif 5307 |
The restriction of a one-to-one onto function to a difference maps onto
the difference of the images. (Contributed by Paul Chapman,
11-Apr-2009.)
|
         
            
       |
|
Theorem | resin 5308 |
The restriction of a one-to-one onto function to an intersection maps onto
the intersection of the images. (Contributed by Paul Chapman,
11-Apr-2009.)
|
         
            
       |
|
Theorem | f1oco 5309 |
Composition of one-to-one onto functions. (Contributed by set.mm
contributors, 19-Mar-1998.)
|
                   |
|
Theorem | f1ococnv2 5310 |
The composition of a one-to-one onto function and its converse equals the
identity relation restricted to the function's range. (Contributed by
set.mm contributors, 13-Dec-2003.)
|
       
   |
|
Theorem | f1ococnv1 5311 |
The composition of a one-to-one onto function's converse and itself equals
the identity relation restricted to the function's domain. (Contributed
by set.mm contributors, 13-Dec-2003.)
|
       
   |
|
Theorem | f1cnv 5312 |
The converse of an injective function is bijective. (Contributed by FL,
11-Nov-2011.)
|
            |
|
Theorem | f1cocnv1 5313 |
Composition of an injective function with its converse. (Contributed by
FL, 11-Nov-2011.)
|
           |
|
Theorem | f1cocnv2 5314 |
Composition of an injective function with its converse. (Contributed by
FL, 11-Nov-2011.)
|
           |
|
Theorem | ffoss 5315* |
Relationship between a mapping and an onto mapping. Figure 38 of
[Enderton] p. 145. (Contributed by
set.mm contributors,
10-May-1998.)
|
               |
|
Theorem | f11o 5316* |
Relationship between one-to-one and one-to-one onto function.
(Contributed by set.mm contributors, 4-Apr-1998.)
|
               |
|
Theorem | f10 5317 |
The empty set maps one-to-one into any class. (Contributed by set.mm
contributors, 7-Apr-1998.)
|
     |
|
Theorem | f1o00 5318 |
One-to-one onto mapping of the empty set. (Contributed by set.mm
contributors, 15-Apr-1998.)
|
     
   |
|
Theorem | fo00 5319 |
Onto mapping of the empty set. (Contributed by set.mm contributors,
22-Mar-2006.)
|
     
   |
|
Theorem | f1o0 5320 |
One-to-one onto mapping of the empty set. (Contributed by set.mm
contributors, 10-Feb-2004.) (Revised by set.mm contributors,
16-Feb-2004.)
|
     |
|
Theorem | f1oi 5321 |
A restriction of the identity relation is a one-to-one onto function.
(The proof was shortened by Andrew Salmon, 22-Oct-2011.) (Contributed by
set.mm contributors, 30-Apr-1998.) (Revised by set.mm contributors,
22-Oct-2011.)
|
      |
|
Theorem | f1ovi 5322 |
The identity relation is a one-to-one onto function on the universe.
(Contributed by set.mm contributors, 16-May-2004.)
|
    |
|
Theorem | f1osn 5323 |
A singleton of an ordered pair is one-to-one onto function. (The proof
was shortened by Andrew Salmon, 22-Oct-2011.) (Contributed by set.mm
contributors, 18-May-1998.) (Revised by set.mm contributors,
22-Oct-2011.)
|
              |
|
Theorem | f1osng 5324 |
A singleton of an ordered pair is one-to-one onto function.
(Contributed by Mario Carneiro, 12-Jan-2013.)
|
                  |
|
Theorem | fv2 5325* |
Alternate definition of function value. Definition 10.11 of [Quine]
p. 68. (The proof was shortened by Andrew Salmon, 17-Sep-2011.)
(Contributed by set.mm contributors, 30-Apr-2004.) (Revised by set.mm
contributors, 18-Sep-2011.)
|
   
          |
|
Theorem | fvprc 5326 |
A function's value at a proper class is the empty set. (Contributed by
set.mm contributors, 20-May-1998.)
|
    
  |
|
Theorem | elfv 5327* |
Membership in a function value. (Contributed by set.mm contributors,
30-Apr-2004.)
|
       
         |
|
Theorem | fveq1 5328 |
Equality theorem for function value. (Contributed by set.mm
contributors, 29-Dec-1996.)
|
    
      |
|
Theorem | fveq2 5329 |
Equality theorem for function value. (Contributed by set.mm
contributors, 29-Dec-1996.)
|
    
      |
|
Theorem | fveq1i 5330 |
Equality inference for function value. (Contributed by set.mm
contributors, 2-Sep-2003.)
|
   
     |
|
Theorem | fveq1d 5331 |
Equality deduction for function value. (Contributed by set.mm
contributors, 2-Sep-2003.)
|
             |
|
Theorem | fveq2i 5332 |
Equality inference for function value. (Contributed by set.mm
contributors, 28-Jul-1999.)
|
   
     |
|
Theorem | fveq2d 5333 |
Equality deduction for function value. (Contributed by set.mm
contributors, 29-May-1999.)
|
             |
|
Theorem | fveq12d 5334 |
Equality deduction for function value. (Contributed by FL,
22-Dec-2008.)
|
               |
|
Theorem | nffv 5335 |
Bound-variable hypothesis builder for function value. (Contributed by
NM, 14-Nov-1995.) (Revised by Mario Carneiro, 15-Oct-2016.)
|
           |
|
Theorem | nffvd 5336 |
Deduction version of bound-variable hypothesis builder nffv 5335.
(Contributed by NM, 10-Nov-2005.) (Revised by Mario Carneiro,
15-Oct-2016.)
|
                 |
|
Theorem | csbfv12g 5337 |
Move class substitution in and out of a function value. (Contributed by
NM, 11-Nov-2005.)
|
   ![]_](_urbrack.gif)    
   ![]_](_urbrack.gif)     ![]_](_urbrack.gif)    |
|
Theorem | csbfv2g 5338* |
Move class substitution in and out of a function value. (Contributed by
NM, 10-Nov-2005.)
|
   ![]_](_urbrack.gif)    
     ![]_](_urbrack.gif)    |
|
Theorem | csbfvg 5339* |
Substitution for a function value. (Contributed by NM, 1-Jan-2006.)
|
   ![]_](_urbrack.gif)    
      |
|
Theorem | fvex 5340 |
The value of a class exists. Corollary 6.13 of [TakeutiZaring] p. 27.
(Contributed by set.mm contributors, 30-Dec-1996.)
|
     |
|
Theorem | fvif 5341 |
Move a conditional outside of a function. (Contributed by Jeff Madsen,
2-Sep-2009.)
|
                       |
|
Theorem | fv3 5342* |
Alternate definition of the value of a function. Definition 6.11 of
[TakeutiZaring] p. 26.
(Contributed by NM, 30-Apr-2004.) (Revised by
Mario Carneiro, 31-Aug-2015.)
|
   
        
     |
|
Theorem | fvres 5343 |
The value of a restricted function. (Contributed by set.mm
contributors, 2-Aug-1994.) (Revised by set.mm contributors,
16-Feb-2004.)
|
             |
|
Theorem | funssfv 5344 |
The value of a member of the domain of a subclass of a function.
(Contributed by set.mm contributors, 15-Aug-1994.) (Revised by set.mm
contributors, 29-May-2007.)
|
             |
|
Theorem | tz6.12-1 5345* |
Function value. Theorem 6.12(1) of [TakeutiZaring] p. 27. (Contributed
by NM, 30-Apr-2004.)
|
              |
|
Theorem | tz6.12 5346* |
Function value. Theorem 6.12(1) of [TakeutiZaring] p. 27. (Contributed
by NM, 10-Jul-1994.)
|
    
         
  |
|
Theorem | tz6.12-2 5347* |
Function value when
is not a function. Theorem 6.12(2) of
[TakeutiZaring] p. 27.
(Contributed by set.mm contributors,
30-Apr-2004.)
|
          |
|
Theorem | tz6.12c 5348* |
Corollary of Theorem 6.12(1) of [TakeutiZaring] p. 27. (Contributed by
NM, 30-Apr-2004.)
|
   
          |
|
Theorem | tz6.12i 5349 |
Corollary of Theorem 6.12(2) of [TakeutiZaring] p. 27. (Contributed by
set.mm contributors, 30-Apr-2004.) (Revised by set.mm contributors,
6-Apr-2007.)
|
           |
|
Theorem | ndmfv 5350 |
The value of a class outside its domain is the empty set. (Contributed
by set.mm contributors, 24-Aug-1995.)
|
    
  |
|
Theorem | ndmfvrcl 5351 |
Reverse closure law for function with the empty set not in its domain.
(Contributed by set.mm contributors, 26-Apr-1996.)
|
    
  |
|
Theorem | elfvdm 5352 |
If a function value has a member, the argument belongs to the domain.
(Contributed by set.mm contributors, 12-Feb-2007.)
|
       |
|
Theorem | nfvres 5353 |
The value of a non-member of a restriction is the empty set. (Contributed
by set.mm contributors, 13-Nov-1995.)
|
      
  |
|
Theorem | nfunsn 5354 |
If the restriction of a class to a singleton is not a function, its
value is the empty set. (Contributed by NM, 8-Aug-2010.) (Proof
shortened by Andrew Salmon, 22-Oct-2011.)
|
        
  |
|
Theorem | fv01 5355 |
Function value of the empty set. (Contributed by Stefan O'Rear,
26-Nov-2014.)
|
     |
|
Theorem | fveqres 5356 |
Equal values imply equal values in a restriction. (Contributed by set.mm
contributors, 13-Nov-1995.)
|
    
                  |
|
Theorem | funbrfv 5357 |
The second argument of a binary relation on a function is the function's
value. (Contributed by NM, 30-Apr-2004.) (Revised by Mario Carneiro,
28-Apr-2015.)
|
           |
|
Theorem | funopfv 5358 |
The second element in an ordered pair member of a function is the
function's value. (Contributed by set.mm contributors, 19-Jul-1996.)
|
        
   |
|
Theorem | fnbrfvb 5359 |
Equivalence of function value and binary relation. (Contributed by NM,
19-Apr-2004.) (Revised by Mario Carneiro, 28-Apr-2015.)
|
             |
|
Theorem | fnopfvb 5360 |
Equivalence of function value and ordered pair membership. (Contributed
by set.mm contributors, 9-Jan-2015.)
|
              |
|
Theorem | funbrfvb 5361 |
Equivalence of function value and binary relation. (Contributed by set.mm
contributors, 9-Jan-2015.)
|
       
     |
|
Theorem | funopfvb 5362 |
Equivalence of function value and ordered pair membership. Theorem
4.3(ii) of [Monk1] p. 42. (Contributed by
set.mm contributors,
9-Jan-2015.)
|
       
      |
|
Theorem | funbrfv2b 5363 |
Function value in terms of a binary relation. (Contributed by Mario
Carneiro, 19-Mar-2014.)
|
             |
|
Theorem | dffn5 5364* |
Representation of a function in terms of its values. (Contributed by
set.mm contributors, 29-Jan-2004.)
|

   
         |
|
Theorem | fnrnfv 5365* |
The range of a function expressed as a collection of the function's
values. (Contributed by set.mm contributors, 20-Oct-2005.)
|
  
       |
|
Theorem | fvelrnb 5366* |
A member of a function's range is a value of the function. (Contributed
by set.mm contributors, 31-Oct-1995.)
|
  
       |
|
Theorem | dfimafn 5367* |
Alternate definition of the image of a function. (Contributed by Raph
Levien, 20-Nov-2006.)
|
      
         |
|
Theorem | dfimafn2 5368* |
Alternate definition of the image of a function as an indexed union of
singletons of function values. (Contributed by Raph Levien,
20-Nov-2006.)
|
      
         |
|
Theorem | funimass4 5369* |
Membership relation for the values of a function whose image is a
subclass. (Contributed by Raph Levien, 20-Nov-2006.)
|
       
    
   |
|
Theorem | fvelima 5370* |
Function value in an image. Part of Theorem 4.4(iii) of [Monk1] p. 42.
(The proof was shortened by Andrew Salmon, 22-Oct-2011.) (Contributed
by set.mm contributors, 29-Apr-2004.) (Revised by set.mm contributors,
22-Oct-2011.)
|
              |
|
Theorem | fvelimab 5371* |
Function value in an image. (The proof was shortened by Andrew Salmon,
22-Oct-2011.) (An unnecessary distinct variable restriction was removed
by David Abernethy, 17-Dec-2011.) (Contributed by set.mm contributors,
20-Jan-2007.) (Revised by set.mm contributors, 25-Dec-2011.)
|
        
       |
|
Theorem | fniniseg 5372 |
Membership in the preimage of a singleton, under a function. (Contributed
by Mario Carneiro, 12-May-2014.)
|
        
         |
|
Theorem | fniinfv 5373* |
The indexed intersection of a function's values is the intersection of
its range. (Contributed by set.mm contributors, 20-Oct-2005.)
|
         |
|
Theorem | fnsnfv 5374 |
Singleton of function value. (Contributed by set.mm contributors,
22-May-1998.)
|
                 |
|
Theorem | fnimapr 5375 |
The image of a pair under a function. (Contributed by Jeff Madsen,
6-Jan-2011.)
|
                       |
|
Theorem | funfv 5376 |
A simplified expression for the value of a function when we know it's a
function. (Contributed by NM, 22-May-1998.)
|
              |
|
Theorem | funfv2 5377* |
The value of a function. Definition of function value in [Enderton]
p. 43. (Contributed by set.mm contributors, 22-May-1998.) (Revised by
set.mm contributors, 11-May-2005.)
|
            |
|
Theorem | funfv2f 5378 |
The value of a function. Version of funfv2 5377 using a bound-variable
hypotheses instead of distinct variable conditions. (Contributed by NM,
19-Feb-2006.)
|
                |
|
Theorem | fvun 5379 |
Value of the union of two functions when the domains are separate.
(Contributed by FL, 7-Nov-2011.)
|
                 
       |
|
Theorem | fvun1 5380 |
The value of a union when the argument is in the first domain.
(Contributed by Scott Fenton, 29-Jun-2013.)
|
                   |
|
Theorem | fvun2 5381 |
The value of a union when the argument is in the second domain.
(Contributed by Scott Fenton, 29-Jun-2013.)
|
                   |
|
Theorem | dmfco 5382 |
Domains of a function composition. (Contributed by set.mm contributors,
27-Jan-1997.)
|
    
        |
|
Theorem | fvco2 5383 |
Value of a function composition. Similar to second part of Theorem 3H
of [Enderton] p. 47. (The proof was
shortened by Andrew Salmon,
22-Oct-2011.) (Contributed by set.mm contributors, 9-Oct-2004.)
(Revised by set.mm contributors, 22-Oct-2011.)
|
        
          |
|
Theorem | fvco 5384 |
Value of a function composition. Similar to Exercise 5 of [TakeutiZaring]
p. 28. (Contributed by set.mm contributors, 22-Apr-2006.)
|
                   |
|
Theorem | fvco3 5385 |
Value of a function composition. (Contributed by set.mm contributors,
3-Jan-2004.) (Revised by set.mm contributors, 21-Aug-2006.)
|
      
                |
|
Theorem | fvopab4t 5386* |
Closed theorem form of fvopab4 5390. (Contributed by set.mm contributors,
21-Feb-2013.)
|
                
     
  |
|
Theorem | fvopab3g 5387* |
Value of a function given by ordered-pair class abstraction.
(Contributed by set.mm contributors, 6-Mar-1996.)
|
                        
   |
|
Theorem | fvopab3ig 5388* |
Value of a function given by ordered-pair class abstraction.
(Contributed by set.mm contributors, 23-Oct-1999.)
|
                              |
|
Theorem | fvopab4g 5389* |
Value of a function given by ordered-pair class abstraction.
(Contributed by set.mm contributors, 23-Oct-1999.)
|
 
   
         
  |
|
Theorem | fvopab4 5390* |
Value of a function given by ordered-pair class abstraction.
(Contributed by set.mm contributors, 23-Oct-1999.)
|
 
   
       
  |
|
Theorem | fvopab4ndm 5391* |
Value of a function given by an ordered-pair class abstraction, outside
of its domain. (Contributed by set.mm contributors, 28-Mar-2008.)
|
   
       
  |
|
Theorem | fvopabg 5392* |
The value of a function given by ordered-pair class abstraction.
(Contributed by set.mm contributors, 2-Sep-2003.)
|
             
  |
|
Theorem | eqfnfv 5393* |
Equality of functions is determined by their values. Special case of
Exercise 4 of [TakeutiZaring] p.
28 (with domain equality omitted).
(The proof was shortened by Andrew Salmon, 22-Oct-2011.) (Contributed
by set.mm contributors, 3-Aug-1994.) (Revised by set.mm contributors,
22-Oct-2011.)
|
    
           |
|
Theorem | eqfnfv2 5394* |
Equality of functions is determined by their values. Exercise 4 of
[TakeutiZaring] p. 28.
(Contributed by set.mm contributors,
3-Aug-1994.) (Revised by set.mm contributors, 5-Feb-2004.)
|
     
            |
|
Theorem | eqfnfv3 5395* |
Derive equality of functions from equality of their values.
(Contributed by Jeff Madsen, 2-Sep-2009.)
|
     

   
         |
|
Theorem | eqfnfvd 5396* |
Deduction for equality of functions. (Contributed by Mario Carneiro,
24-Jul-2014.)
|
                   |
|
Theorem | eqfnfv2f 5397* |
Equality of functions is determined by their values. Special case of
Exercise 4 of [TakeutiZaring] p.
28 (with domain equality omitted).
This version of eqfnfv 5393 uses bound-variable hypotheses instead of
distinct variable conditions. (Contributed by NM, 29-Jan-2004.)
|
        
           |
|
Theorem | eqfunfv 5398* |
Equality of functions is determined by their values. (Contributed by
Scott Fenton, 19-Jun-2011.)
|
   
               |
|
Theorem | fvreseq 5399* |
Equality of restricted functions is determined by their values.
(Contributed by set.mm contributors, 3-Aug-1994.) (Revised by set.mm
contributors, 6-Feb-2004.)
|
   

 
               |
|
Theorem | chfnrn 5400* |
The range of a choice function (a function that chooses an element from
each member of its domain) is included in the union of its domain.
(Contributed by set.mm contributors, 31-Aug-1999.)
|
       
   |