![]() |
Intuitionistic Logic Explorer Theorem List (p. 17 of 135) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | 19.29r 1601 | Variation of Theorem 19.29 of [Margaris] p. 90. (Contributed by NM, 18-Aug-1993.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 19.29r2 1602 | Variation of Theorem 19.29 of [Margaris] p. 90 with double quantification. (Contributed by NM, 3-Feb-2005.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 19.29x 1603 | Variation of Theorem 19.29 of [Margaris] p. 90 with mixed quantification. (Contributed by NM, 11-Feb-2005.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 19.35-1 1604 | Forward direction of Theorem 19.35 of [Margaris] p. 90. The converse holds for classical logic but not (for all propositions) in intuitionistic logic (Contributed by Mario Carneiro, 2-Feb-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 19.35i 1605 | Inference from Theorem 19.35 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 2-Feb-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 19.25 1606 | Theorem 19.25 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 2-Feb-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 19.30dc 1607 | Theorem 19.30 of [Margaris] p. 90, with an additional decidability condition. (Contributed by Jim Kingdon, 21-Jul-2018.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 19.43 1608 | Theorem 19.43 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Mario Carneiro, 2-Feb-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 19.33b2 1609 | The antecedent provides a condition implying the converse of 19.33 1461. Compare Theorem 19.33 of [Margaris] p. 90. This variation of 19.33bdc 1610 is intuitionistically valid without a decidability condition. (Contributed by Mario Carneiro, 2-Feb-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 19.33bdc 1610 |
Converse of 19.33 1461 given ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 19.40 1611 | Theorem 19.40 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 19.40-2 1612 | Theorem *11.42 in [WhiteheadRussell] p. 163. Theorem 19.40 of [Margaris] p. 90 with 2 quantifiers. (Contributed by Andrew Salmon, 24-May-2011.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | exintrbi 1613 | Add/remove a conjunct in the scope of an existential quantifier. (Contributed by Raph Levien, 3-Jul-2006.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | exintr 1614 | Introduce a conjunct in the scope of an existential quantifier. (Contributed by NM, 11-Aug-1993.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | alsyl 1615 | Theorem *10.3 in [WhiteheadRussell] p. 150. (Contributed by Andrew Salmon, 8-Jun-2011.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | hbex 1616 |
If ![]() ![]() ![]() ![]() ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | nfex 1617 |
If ![]() ![]() ![]() ![]() ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 19.2 1618 | Theorem 19.2 of [Margaris] p. 89, generalized to use two setvar variables. (Contributed by O'Cat, 31-Mar-2008.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | i19.24 1619 | Theorem 19.24 of [Margaris] p. 90, with an additional hypothesis. The hypothesis is the converse of 19.35-1 1604, and is a theorem of classical logic, but in intuitionistic logic it will only be provable for some propositions. (Contributed by Jim Kingdon, 22-Jul-2018.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | i19.39 1620 | Theorem 19.39 of [Margaris] p. 90, with an additional hypothesis. The hypothesis is the converse of 19.35-1 1604, and is a theorem of classical logic, but in intuitionistic logic it will only be provable for some propositions. (Contributed by Jim Kingdon, 22-Jul-2018.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 19.9ht 1621 | A closed version of one direction of 19.9 1624. (Contributed by NM, 5-Aug-1993.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 19.9t 1622 | A closed version of 19.9 1624. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof shortended by Wolf Lammen, 30-Dec-2017.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 19.9h 1623 | A wff may be existentially quantified with a variable not free in it. Theorem 19.9 of [Margaris] p. 89. (Contributed by FL, 24-Mar-2007.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 19.9 1624 | A wff may be existentially quantified with a variable not free in it. Theorem 19.9 of [Margaris] p. 89. (Contributed by FL, 24-Mar-2007.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | alexim 1625 | One direction of theorem 19.6 of [Margaris] p. 89. The converse holds given a decidability condition, as seen at alexdc 1599. (Contributed by Jim Kingdon, 2-Jul-2018.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | exnalim 1626 | One direction of Theorem 19.14 of [Margaris] p. 90. In classical logic the converse also holds. (Contributed by Jim Kingdon, 15-Jul-2018.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | exanaliim 1627 | A transformation of quantifiers and logical connectives. In classical logic the converse also holds. (Contributed by Jim Kingdon, 15-Jul-2018.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | alexnim 1628 | A relationship between two quantifiers and negation. (Contributed by Jim Kingdon, 27-Aug-2018.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | ax6blem 1629 |
If ![]() ![]() ![]() ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | ax6b 1630 |
Quantified Negation. Axiom C5-2 of [Monk2] p.
113.
(Contributed by GD, 27-Jan-2018.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | hbn1 1631 |
![]() ![]() ![]() ![]() ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | hbnt 1632 | Closed theorem version of bound-variable hypothesis builder hbn 1633. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 2-Feb-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | hbn 1633 |
If ![]() ![]() ![]() ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | hbnd 1634 | Deduction form of bound-variable hypothesis builder hbn 1633. (Contributed by NM, 3-Jan-2002.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | nfnt 1635 |
If ![]() ![]() ![]() ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | nfnd 1636 | Deduction associated with nfnt 1635. (Contributed by Mario Carneiro, 24-Sep-2016.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | nfn 1637 | Inference associated with nfnt 1635. (Contributed by Mario Carneiro, 11-Aug-2016.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | nfdc 1638 |
If ![]() ![]() ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | modal-5 1639 | The analog in our predicate calculus of axiom 5 of modal logic S5. (Contributed by NM, 5-Oct-2005.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 19.9d 1640 | A deduction version of one direction of 19.9 1624. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 19.9hd 1641 | A deduction version of one direction of 19.9 1624. This is an older variation of this theorem; new proofs should use 19.9d 1640. (Contributed by NM, 5-Aug-1993.) (New usage is discouraged.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | excomim 1642 | One direction of Theorem 19.11 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | excom 1643 | Theorem 19.11 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 19.12 1644 | Theorem 19.12 of [Margaris] p. 89. Assuming the converse is a mistake sometimes made by beginners! (Contributed by NM, 5-Aug-1993.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 19.19 1645 | Theorem 19.19 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 19.21-2 1646 | Theorem 19.21 of [Margaris] p. 90 but with 2 quantifiers. (Contributed by NM, 4-Feb-2005.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | nf2 1647 | An alternate definition of df-nf 1438, which does not involve nested quantifiers on the same variable. (Contributed by Mario Carneiro, 24-Sep-2016.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | nf3 1648 | An alternate definition of df-nf 1438. (Contributed by Mario Carneiro, 24-Sep-2016.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | nf4dc 1649 |
Variable ![]() ![]() ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | nf4r 1650 |
If ![]() ![]() ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 19.36i 1651 | Inference from Theorem 19.36 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 2-Feb-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 19.36-1 1652 | Closed form of 19.36i 1651. One direction of Theorem 19.36 of [Margaris] p. 90. The converse holds in classical logic, but does not hold (for all propositions) in intuitionistic logic. (Contributed by Jim Kingdon, 20-Jun-2018.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 19.37-1 1653 | One direction of Theorem 19.37 of [Margaris] p. 90. The converse holds in classical logic but not, in general, here. (Contributed by Jim Kingdon, 21-Jun-2018.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 19.37aiv 1654* | Inference from Theorem 19.37 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 19.38 1655 | Theorem 19.38 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 19.23t 1656 | Closed form of Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 7-Nov-2005.) (Proof shortened by Wolf Lammen, 2-Jan-2018.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 19.23 1657 | Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 19.32dc 1658 |
Theorem 19.32 of [Margaris] p. 90, where ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 19.32r 1659 |
One direction of Theorem 19.32 of [Margaris]
p. 90. The converse holds
if ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 19.31r 1660 | One direction of Theorem 19.31 of [Margaris] p. 90. The converse holds in classical logic, but not intuitionistic logic. (Contributed by Jim Kingdon, 28-Jul-2018.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 19.44 1661 | Theorem 19.44 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 19.45 1662 | Theorem 19.45 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 19.34 1663 | Theorem 19.34 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 19.41h 1664 | Theorem 19.41 of [Margaris] p. 90. New proofs should use 19.41 1665 instead. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (New usage is discouraged.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 19.41 1665 | Theorem 19.41 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 12-Jan-2018.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 19.42h 1666 | Theorem 19.42 of [Margaris] p. 90. New proofs should use 19.42 1667 instead. (Contributed by NM, 18-Aug-1993.) (New usage is discouraged.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 19.42 1667 | Theorem 19.42 of [Margaris] p. 90. (Contributed by NM, 18-Aug-1993.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | excom13 1668 | Swap 1st and 3rd existential quantifiers. (Contributed by NM, 9-Mar-1995.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | exrot3 1669 | Rotate existential quantifiers. (Contributed by NM, 17-Mar-1995.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | exrot4 1670 | Rotate existential quantifiers twice. (Contributed by NM, 9-Mar-1995.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | nexr 1671 | Inference from 19.8a 1570. (Contributed by Jeff Hankins, 26-Jul-2009.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | exan 1672 | Place a conjunct in the scope of an existential quantifier. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | hbexd 1673 | Deduction form of bound-variable hypothesis builder hbex 1616. (Contributed by NM, 2-Jan-2002.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | eeor 1674 | Rearrange existential quantifiers. (Contributed by NM, 8-Aug-1994.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | a9e 1675 | At least one individual exists. This is not a theorem of free logic, which is sound in empty domains. For such a logic, we would add this theorem as an axiom of set theory (Axiom 0 of [Kunen] p. 10). In the system consisting of ax-5 1424 through ax-14 1493 and ax-17 1507, all axioms other than ax-9 1512 are believed to be theorems of free logic, although the system without ax-9 1512 is probably not complete in free logic. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 3-Feb-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | a9ev 1676* | At least one individual exists. Weaker version of a9e 1675. (Contributed by NM, 3-Aug-2017.) |
![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | ax9o 1677 | An implication related to substitution. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 3-Feb-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | equid 1678 |
Identity law for equality (reflexivity). Lemma 6 of [Tarski] p. 68.
This is often an axiom of equality in textbook systems, but we don't
need it as an axiom since it can be proved from our other axioms.
This proof is similar to Tarski's and makes use of a dummy variable
|
![]() ![]() ![]() ![]() | ||
Theorem | nfequid 1679 |
Bound-variable hypothesis builder for ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | stdpc6 1680 | One of the two equality axioms of standard predicate calculus, called reflexivity of equality. (The other one is stdpc7 1744.) Axiom 6 of [Mendelson] p. 95. Mendelson doesn't say why he prepended the redundant quantifier, but it was probably to be compatible with free logic (which is valid in the empty domain). (Contributed by NM, 16-Feb-2005.) |
![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | equcomi 1681 | Commutative law for equality. Lemma 7 of [Tarski] p. 69. (Contributed by NM, 5-Aug-1993.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | ax6evr 1682* | A commuted form of a9ev 1676. The naming reflects how axioms were numbered in the Metamath Proof Explorer as of 2020 (a numbering which we eventually plan to adopt here too, but until this happens everywhere only some theorems will have it). (Contributed by BJ, 7-Dec-2020.) |
![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | equcom 1683 | Commutative law for equality. (Contributed by NM, 20-Aug-1993.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | equcomd 1684 | Deduction form of equcom 1683, symmetry of equality. For the versions for classes, see eqcom 2142 and eqcomd 2146. (Contributed by BJ, 6-Oct-2019.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | equcoms 1685 | An inference commuting equality in antecedent. Used to eliminate the need for a syllogism. (Contributed by NM, 5-Aug-1993.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | equtr 1686 | A transitive law for equality. (Contributed by NM, 23-Aug-1993.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | equtrr 1687 | A transitive law for equality. Lemma L17 in [Megill] p. 446 (p. 14 of the preprint). (Contributed by NM, 23-Aug-1993.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | equtr2 1688 | A transitive law for equality. (Contributed by NM, 12-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | equequ1 1689 | An equivalence law for equality. (Contributed by NM, 5-Aug-1993.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | equequ2 1690 | An equivalence law for equality. (Contributed by NM, 5-Aug-1993.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | elequ1 1691 | An identity law for the non-logical predicate. (Contributed by NM, 5-Aug-1993.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | elequ2 1692 | An identity law for the non-logical predicate. (Contributed by NM, 5-Aug-1993.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | ax11i 1693 |
Inference that has ax-11 1485 (without ![]() ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | ax10o 1694 |
Show that ax-10o 1695 can be derived from ax-10 1484. An open problem is
whether this theorem can be derived from ax-10 1484 and the others when
ax-11 1485 is replaced with ax-11o 1796. See theorem ax10 1696
for the
rederivation of ax-10 1484 from ax10o 1694.
Normally, ax10o 1694 should be used rather than ax-10o 1695, except by theorems specifically studying the latter's properties. (Contributed by NM, 16-May-2008.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Axiom | ax-10o 1695 |
Axiom ax-10o 1695 ("o" for "old") was the
original version of ax-10 1484,
before it was discovered (in May 2008) that the shorter ax-10 1484 could
replace it. It appears as Axiom scheme C11' in [Megill] p. 448 (p. 16 of
the preprint).
This axiom is redundant, as shown by theorem ax10o 1694. Normally, ax10o 1694 should be used rather than ax-10o 1695, except by theorems specifically studying the latter's properties. (Contributed by NM, 5-Aug-1993.) (New usage is discouraged.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | ax10 1696 |
Rederivation of ax-10 1484 from original version ax-10o 1695. See theorem
ax10o 1694 for the derivation of ax-10o 1695 from ax-10 1484.
This theorem should not be referenced in any proof. Instead, use ax-10 1484 above so that uses of ax-10 1484 can be more easily identified. (Contributed by NM, 16-May-2008.) (New usage is discouraged.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | hbae 1697 | All variables are effectively bound in an identical variable specifier. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 3-Feb-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | nfae 1698 | All variables are effectively bound in an identical variable specifier. (Contributed by Mario Carneiro, 11-Aug-2016.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | hbaes 1699 | Rule that applies hbae 1697 to antecedent. (Contributed by NM, 5-Aug-1993.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | hbnae 1700 | All variables are effectively bound in a distinct variable specifier. Lemma L19 in [Megill] p. 446 (p. 14 of the preprint). (Contributed by NM, 5-Aug-1993.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |