Statement List for Metamath Proof Explorer - 1601-1700 - Page 17 of 107
| Type | Label | Description |
| Statement |
| |
| Theorem | necon3bd 1601 |
Contrapositive law deduction for inequality.
|
 
   
   |
| |
| Theorem | necon3d 1602 |
Contrapositive law deduction for inequality.
|
 
       |
| |
| Theorem | necon3i 1603 |
Contrapositive inference for inequality.
|
     |
| |
| Theorem | necon3ai 1604 |
Contrapositive inference for inequality.
|
     |
| |
| Theorem | necon3bi 1605 |
Contrapositive inference for inequality.
|
     |
| |
| Theorem | necon1ai 1606 |
Contrapositive inference for inequality.
|
     |
| |
| Theorem | necon1bi 1607 |
Contrapositive inference for inequality.
|
     |
| |
| Theorem | necon1i 1608 |
Contrapositive inference for inequality.
|
  
  |
| |
| Theorem | necon2ai 1609 |
Contrapositive inference for inequality.
|
     |
| |
| Theorem | necon2bi 1610 |
Contrapositive inference for inequality.
|
     |
| |
| Theorem | necon2i 1611 |
Contrapositive inference for inequality.
|
     |
| |
| Theorem | necon2ad 1612 |
Contrapositive inference for inequality.
|
 
   
   |
| |
| Theorem | necon2bd 1613 |
Contrapositive inference for inequality.
|
     
   |
| |
| Theorem | necon1abii 1614 |
Contrapositive inference for inequality.
|
     |
| |
| Theorem | necon1bbii 1615 |
Contrapositive inference for inequality.
|
     |
| |
| Theorem | necon1abid 1616 |
Contrapositive deduction for inequality.
|
 
   
   |
| |
| Theorem | necon1bbid 1617 |
Contrapositive inference for inequality.
|
 
   
   |
| |
| Theorem | necon2abii 1618 |
Contrapositive inference for inequality.
|
     |
| |
| Theorem | necon2bbii 1619 |
Contrapositive inference for inequality.
|
     |
| |
| Theorem | necon2abid 1620 |
Contrapositive deduction for inequality.
|
 
       |
| |
| Theorem | necon2bbid 1621 |
Contrapositive deduction for inequality.
|
     
   |
| |
| Theorem | necon4ai 1622 |
Contrapositive inference for inequality.
|
     |
| |
| Theorem | necon4i 1623 |
Contrapositive inference for inequality.
|
  
  |
| |
| Theorem | necon4ad 1624 |
Contrapositive inference for inequality.
|
 
   
   |
| |
| Theorem | necon4bd 1625 |
Contrapositive inference for inequality.
|
 
   
   |
| |
| Theorem | necon4d 1626 |
Contrapositive inference for inequality.
|
 
       |
| |
| Theorem | necon4abid 1627 |
Contrapositive law deduction for inequality.
|
 
   
   |
| |
| Theorem | necon4bid 1628 |
Contrapositive law deduction for inequality.
|
 
   
   |
| |
| Theorem | necon1ad 1629 |
Contrapositive deduction for inequality.
|
 
   
   |
| |
| Theorem | necon1bd 1630 |
Contrapositive deduction for inequality.
|
 
   
   |
| |
| Theorem | pm2.61ne 1631 |
Deduction eliminating an inequality in an antecedent.
|
     

      |
| |
| Theorem | pm2.61ine 1632 |
Inference eliminating an inequality in an antecedent.
|
  
  |
| |
| Theorem | pm2.61dne 1633 |
Deduction eliminating an inequality in an antecedent.
|
 
   
     |
| |
| Theorem | necom 1634 |
Commutation of inequality.
|

  |
| |
| Theorem | necomd 1635 |
Deduction from commutative law for inequality.
|
     |
| |
| Theorem | neor 1636 |
Logical OR with an equality.
|
       |
| |
| Theorem | neanior 1637 |
A DeMorgan's law for inequality.
|
   
   |
| |
| Theorem | neorian 1638 |
A DeMorgan's law for inequality.
|
   
   |
| |
| Theorem | nemtbir 1639 |
An inference from an inequality, related to modus tollens.
|
   |
| |
| Theorem | neleq1 1640 |
Equality theorem for negated membership.
|
     |
| |
| Theorem | neleq2 1641 |
Equality theorem for negated membership.
|
     |
| |
| Theorem | hbne 1642 |
Bound-variable hypothesis builder for inequality.
|
    
 
   |
| |
| Restricted quantification |
| |
| Syntax | wral 1643 |
Extend wff notation to include restricted universal quantification.
|
  |
| |
| Syntax | wrex 1644 |
Extend wff notation to include restricted existential quantification.
|
  |
| |
| Syntax | wreu 1645 |
Extend wff notation to include restricted existential uniqueness.
|
  |
| |
| Syntax | crab 1646 |
Extend class notation to include the restricted class abstraction
(class builder).
|
   |
| |
| Definition | df-ral 1647 |
Define restricted universal quantification. Special case of Definition
4.15(3) of [TakeutiZaring] p. 22.
|
        |
| |
| Definition | df-rex 1648 |
Define restricted existential quantification. Special case of Definition
4.15(4) of [TakeutiZaring] p. 22.
|
        |
| |
| Definition | df-reu 1649 |
Define restricted existential uniqueness.
|
        |
| |
| Definition | df-rab 1650 |
Define a restricted class abstraction (class builder), which is the class
of all in such that is true. Definition
of
[TakeutiZaring] p. 20.
|
  

   |
| |
| Theorem | ralnex 1651 |
Relationship between restricted universal and existential quantifiers.
|
  
  |
| |
| Theorem | rexnal 1652 |
Relationship between restricted universal and existential quantifiers.
|
  
  |
| |
| Theorem | dfral2 1653 |
Relationship between restricted universal and existential quantifiers.
|
  
  |
| |
| Theorem | dfrex2 1654 |
Relationship between restricted universal and existential quantifiers.
|
  
  |
| |
| Theorem | ralbida 1655 |
Formula-building rule for restricted universal quantifier (deduction
rule).
|
     

          |
| |
| Theorem | rexbida 1656 |
Formula-building rule for restricted existential quantifier (deduction
rule).
|
     

          |
| |
| Theorem | ralbidva 1657 |
Formula-building rule for restricted universal quantifier (deduction
rule).
|
 
      
    |
| |
| Theorem | rexbidva 1658 |
Formula-building rule for restricted existential quantifier (deduction
rule).
|
 
      
    |
| |
| Theorem | ralbid 1659 |
Formula-building rule for restricted universal quantifier (deduction
rule).
|
     
    
    |
| |
| Theorem | rexbid 1660 |
Formula-building rule for restricted existential quantifier (deduction
rule).
|
     
    
    |
| |
| Theorem | ralbidv 1661 |
Formula-building rule for restricted universal quantifier (deduction
rule).
|
           |
| |
| Theorem | rexbidv 1662 |
Formula-building rule for restricted existential quantifier (deduction
rule).
|
           |
| |
| Theorem | ralbidv2 1663 |
Formula-building rule for restricted universal quantifier (deduction
rule).
|
               |
| |
| Theorem | rexbidv2 1664 |
Formula-building rule for restricted existential quantifier (deduction
rule).
|
               |
| |
| Theorem | ralbii 1665 |
Inference adding restricted universal quantifier to both sides of an
equivalence.
|
 |