Statement List for Metamath Proof Explorer - 3701-3800 - Page 38 of 107
| Type | Label | Description |
| Statement |
| |
| Theorem | f1ocnv 3701 |
The converse of a one-to-one onto function is also one-to-one onto.
|
    
       |
| |
| Theorem | f1ocnvb 3702 |
A relation is a one-to-one onto function iff its converse is a one-to-one
onto function with domain and range interchanged.
|
              |
| |
| Theorem | f1ores 3703 |
The restriction of a one-to-one function maps one-to-one onto the
image.
|
                   |
| |
| Theorem | f1orescnv 3704 |
The converse of a one-to-one-onto restricted function. (Contributed by
Paul Chapman, 21-Apr-2008.)
|
  
        
       |
| |
| Theorem | f1imacnv 3705 |
Pre-image of an image.
|
                  |
| |
| Theorem | f1oun 3706 |
The union of two one-to-one onto functions with disjoint domains and
ranges.
|
                   
           |
| |
| Theorem | f1oco 3707 |
Composition of one-to-one onto functions.
|
           
       |
| |
| Theorem | f1ococnv2 3708 |
The composition of a one-to-one onto function and its converse equals
the identity relation restricted to the function's range.
|
    
       |
| |
| Theorem | f1ococnv1 3709 |
The composition of a one-to-one onto function's converse and itself
equals the identity relation restricted to the function's domain.
|
    
 
     |
| |
| Theorem | f1dmex 3710 |
If the codomain of a one-to-one function exists, so does its domain.
This theorem is equivalent to the Axiom of Replacement ax-rep 2689.
|
         |
| |
| Theorem | ffoss 3711 |
Relationship between a mapping and an onto mapping. Figure 38 of
[Enderton] p. 145.
|
               |
| |
| Theorem | f11o 3712 |
Relationship between one-to-one and one-to-one onto function.
|
           
   |
| |
| Theorem | f10 3713 |
The empty set maps one-to-one into any class.
|
     |
| |
| Theorem | f1o00 3714 |
One-to-one onto mapping of the empty set.
|
         |
| |
| Theorem | fo00 3715 |
Onto mapping of the empty set.
|
         |
| |
| Theorem | f1o0 3716 |
One-to-one onto mapping of the empty set.
|
     |
| |
| Theorem | f1oi 3717 |
A restriction of the identity relation is a one-to-one onto function.
|
       |
| |
| Theorem | f1ovi 3718 |
The identity relation is a one-to-one onto function on the universe.
|
     |
| |
| Theorem | f1osn 3719 |
A singleton of an ordered pair is one-to-one onto function.
|
              |
| |
| Theorem | fv2 3720 |
Alternate definition of function value. Definition 10.11 of [Quine]
p. 68.
|
              |
| |
| Theorem | fvprc 3721 |
A function's value at a proper class is the empty set.
|
       |
| |
| Theorem | elfv 3722 |
Membership in a function value.
|
                 |
| |
| Theorem | fveq1 3723 |
Equality theorem for function value.
|
           |
| |
| Theorem | fveq2 3724 |
Equality theorem for function value.
|
           |
| |
| Theorem | fveq1i 3725 |
Equality inference for function value.
|
         |
| |
| Theorem | fveq1d 3726 |
Equality deduction for function value.
|
             |
| |
| Theorem | fveq2i 3727 |
Equality inference for function value.
|
         |
| |
| Theorem | fveq2d 3728 |
Equality deduction for function value.
|
             |
| |
| Theorem | hbfv 3729 |
Bound-variable hypothesis builder for function value.
|
    
 
           |
| |
| Theorem | hbfvd 3730 |
Deduction version of bound-variable hypothesis builder hbfv 3729.
If a closed theorem version is desired, see hbfvd2 3731.
|
           
   
            |
| |
| Theorem | hbfvd2 3731 |
Deduction version of bound-variable hypothesis builder hbfv 3729.
This variant of hbfvd 3730 allows us to create a closed theorem form
by replacing the uncommitted antecedent with an appropriate
substitution instance.
|
        
   
    
            |
| |
| Theorem | fvex 3732 |
The value of a class exists. Corollary 6.13 of [TakeutiZaring]
p. 27.
|
   
 |
| |
| Theorem | fv3 3733 |
Alternate definition of the value of a function. Definition 6.11 of
[TakeutiZaring] p. 26.
|
    
             |
| |
| Theorem | fvres 3734 |
The value of a restricted function.
|
      
      |
| |
| Theorem | funssfv 3735 |
The value of a member of the domain of a subclass of a function.
|
 

          |
| |
| Theorem | tz6.12-1 3736 |
Function value. Theorem 6.12(1) of [TakeutiZaring] p. 27.
|
              |
| |
| Theorem | tz6.12 3737 |
Function value. Theorem 6.12(1) of [TakeutiZaring] p. 27.
|
              
  |
| |
| Theorem | tz6.12f 3738 |
Function value, using bound-variable hypotheses instead of distinct
variable conditions.
|
       
         
  |
| |
| Theorem | tz6.12-2 3739 |
Function value when is
not a function. Theorem 6.12(2) of
[TakeutiZaring] p. 27.
|
       
  |
| |
| Theorem | tz6.12c 3740 |
Corollary of Theorem 6.12(1) of [TakeutiZaring] p. 27.
|
              |
| |
| Theorem | tz6.12i 3741 |
Corollary of Theorem 6.12(2) of [TakeutiZaring] p. 27.
|
           |
| |
| Theorem | csbfv12g 3742 |
Move class substitution in and out of a function value.
|
   ![]_](_urbrack.gif)        ![]_](_urbrack.gif)     ![]_](_urbrack.gif)    |
| |
| Theorem | csbfv2g 3743 |
Move class substitution in and out of a function value.
|
   ![]_](_urbrack.gif)          ![]_](_urbrack.gif)    |
| |
| Theorem | csbfvg 3744 |
Substitution for a function value.
|
   ![]_](_urbrack.gif)           |
| |
| Theorem | ndmfv 3745 |
The value of a class outside its domain is the empty set.
|
       |
| |
| Theorem | ndmfvrcl 3746 |
Reverse closure law for function with the empty set not in its
domain.
|
       |
| |
| Theorem | elfvdm 3747 |
If a function value has a member, the argument belongs to the domain.
|
       |
| |
| Theorem | nfvres 3748 |
A non-element of a restriction has empty value.
|
  
      |
| |
| Theorem | fveqres 3749 |
Equal values imply equal values in a restriction.
|
              
        |
| |
| Theorem | funbrfv 3750 |
The second argument of a binary relation on a function is the function's
value.
|
           |
| |
| Theorem | funopfv 3751 |
The second element in an ordered pair member of a function is the
function's value.
|
        
   |
| |
| Theorem | funopfvg 3752 |
The second element in an ordered pair member of a function is the
function's value.
|
  
  

       |
| |
| Theorem | fnbrfvb 3753 |
Equivalence of function value and binary relation.
|
       
     |
| |
| Theorem | fnopfvb 3754 |
Equivalence of function value and ordered pair membership.
|
       
      |
| |
| Theorem | funbrfvb 3755 |
Equivalence of function value and binary relation.
|
             |
| |
| Theorem | funopfvb 3756 |
Equivalence of function value and ordered pair membership. Theorem
4.3(ii) of [Monk1] p. 42.
|
              |
| |
| Theorem | funbrfvbg 3757 |
Function value in terms of a binary relation.
|
 
     
     |
| |
| Theorem | fnopabfv 3758 |
Representation of a function in terms of its values.
|

    
        |
| |
| Theorem | fnrnfv 3759 |
The range of a function expressed as a collection of the function's
values.
|
 

       |
| |
| Theorem | fvelrnb |