![]() |
Metamath
Proof Explorer Theorem List (p. 19 of 406) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-26564) |
![]() (26565-28087) |
![]() (28088-40527) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | sbequ8 1801 | Elimination of equality from antecedent after substitution. (Contributed by NM, 5-Aug-1993.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 28-Jul-2018.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | sbimi 1802 | Infer substitution into antecedent and consequent of an implication. (Contributed by NM, 25-Jun-1998.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | sbbii 1803 | Infer substitution into both sides of a logical equivalence. (Contributed by NM, 14-May-1993.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Axiom | ax-6 1804 |
Axiom of Existence. One of the equality and substitution axioms of
predicate calculus with equality. This axiom tells us is that at least
one thing exists. In this form (not requiring that ![]() ![]() Raph Levien proved the independence of this axiom from the other logical axioms on 12-Apr-2005. See item 16 at http://us.metamath.org/award2003.html. ax-6 1804 can be proved from the weaker version ax6v 1805 requiring that the variables be distinct; see theorem ax6 2094. ax-6 1804 can also be proved from the Axiom of Separation (in the form that we use that axiom, where free variables are not universally quantified). See theorem ax6vsep 4528. Except by ax6v 1805, this axiom should not be referenced directly. Instead, use theorem ax6 2094. (Contributed by NM, 10-Jan-1993.) (New usage is discouraged.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | ax6v 1805* |
Axiom B7 of [Tarski] p. 75, which requires that
![]() ![]()
Note: Introducing When possible, use of this theorem rather than ax6 2094 is preferred since its derivation is much shorter and requires fewer axioms. (Contributed by NM, 7-Aug-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | ax6ev 1806* | At least one individual exists. Weaker version of ax6e 2093. When possible, use of this theorem rather than ax6e 2093 is preferred since its derivation is much shorter and requires fewer axioms. (Contributed by NM, 3-Aug-2017.) |
![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | exiftru 1807 | Rule of existential generalization, similar to universal generalization ax-gen 1668, but valid only if an individual exists. Its proof requires ax-6 1804 but the equality predicate does not occur in its statement. Some fundamental theorems of predicate logic can be proven from ax-gen 1668, ax-4 1681 and this theorem alone, not requiring ax-7 1850 or excessive distinct variable conditions. (Contributed by Wolf Lammen, 12-Nov-2017.) (Proof shortened by Wolf Lammen, 9-Dec-2017.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 19.2 1808 | Theorem 19.2 of [Margaris] p. 89. This corresponds to the axiom (D) of modal logic. Note: This proof is very different from Margaris' because we only have Tarski's FOL axiom schemes available at this point. See the later 19.2g 1945 for a more conventional proof of a more general result, which uses additional axioms. (Contributed by NM, 2-Aug-2017.) Remove dependency on ax-7 1850. (Revised by Wolf Lammen, 4-Dec-2017.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 19.8w 1809 | Weak version of 19.8a 1934. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 1-Aug-2017.) (Proof shortened by Wolf Lammen, 4-Dec-2017.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 19.8v 1810* | Version of 19.8a 1934 with a dv condition, requiring fewer axioms. (Contributed by BJ, 12-Mar-2020.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 19.9v 1811* | Version of 19.9 1969 with a dv condition, requiring fewer axioms. Any formula can be existentially quantified using a variable which it does not contain. See also 19.3v 1812. (Contributed by NM, 28-May-1995.) Remove dependency on ax-7 1850. (Revised by Wolf Lammen, 4-Dec-2017.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 19.3v 1812* | Version of 19.3 1965 with a dv condition, requiring fewer axioms. Any formula can be universally quantified using a variable which it does not contain. See also 19.9v 1811. (Contributed by Anthony Hart, 13-Sep-2011.) Remove dependency on ax-7 1850. (Revised by Wolf Lammen, 4-Dec-2017.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | spvw 1813* |
Version of sp 1936 when ![]() ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 19.39 1814 | Theorem 19.39 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 19.24 1815 | Theorem 19.24 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 19.34 1816 | Theorem 19.34 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 19.23v 1817* | Version of 19.23 1992 with a dv condition instead of a non-freeness hypothesis. (Contributed by NM, 28-Jun-1998.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 11-Jan-2020.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 19.23vv 1818* | Theorem 19.23v 1817 extended to two variables. (Contributed by NM, 10-Aug-2004.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 19.36v 1819* | Version of 19.36 2043 with a dv condition instead of a non-freeness hypothesis. (Contributed by NM, 18-Aug-1993.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 17-Jan-2020.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 19.36iv 1820* | Inference associated with 19.36v 1819. Version of 19.36i 2044 with a dv condition. (Contributed by NM, 5-Aug-1993.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 17-Jan-2020.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | pm11.53v 1821* | Version of pm11.53 2072 with a dv condition, requiring fewer axioms. (Contributed by BJ, 7-Mar-2020.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 19.12vvv 1822* | Version of 19.12vv 2075 with a dv condition, requiring fewer axioms. See also 19.12 2032. (Contributed by BJ, 18-Mar-2020.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 19.27v 1823* | Version of 19.27 2005 with a dv condition, requiring fewer axioms. (Contributed by NM, 3-Jun-2004.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 19.28v 1824* | Version of 19.28 2006 with a dv condition, requiring fewer axioms. (Contributed by NM, 25-Mar-2004.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 19.37v 1825* | Version of 19.37 2045 with a dv condition, requiring fewer axioms. (Contributed by NM, 21-Jun-1993.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 19.37iv 1826* | Inference associated with 19.37v 1825. (Contributed by NM, 5-Aug-1993.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 19.44v 1827* | Version of 19.44 2048 with a dv condition, requiring fewer axioms. (Contributed by NM, 12-Mar-1993.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 19.45v 1828* | Version of 19.45 2049 with a dv condition, requiring fewer axioms. (Contributed by NM, 12-Mar-1993.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 19.41v 1829* | Version of 19.41 2050 with a dv condition, requiring fewer axioms. (Contributed by NM, 21-Jun-1993.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 19.41vv 1830* | Version of 19.41 2050 with two quantifiers and a dv condition requiring fewer axioms. (Contributed by NM, 30-Apr-1995.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 19.41vvv 1831* | Version of 19.41 2050 with three quantifiers and a dv condition requiring fewer axioms. (Contributed by NM, 30-Apr-1995.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 19.41vvvv 1832* | Version of 19.41 2050 with four quantifiers and a dv condition requiring fewer axioms. (Contributed by FL, 14-Jul-2007.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 19.42v 1833* | Version of 19.42 2051 with a dv condition requiring fewer axioms. (Contributed by NM, 21-Jun-1993.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | exdistr 1834* | Distribution of existential quantifiers. (Contributed by NM, 9-Mar-1995.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 19.42vv 1835* | Version of 19.42 2051 with two quantifiers and a dv condition requiring fewer axioms. (Contributed by NM, 16-Mar-1995.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 19.42vvv 1836* | Version of 19.42 2051 with three quantifiers and a dv condition requiring fewer axioms. (Contributed by NM, 21-Sep-2011.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | exdistr2 1837* | Distribution of existential quantifiers. (Contributed by NM, 17-Mar-1995.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 3exdistr 1838* | Distribution of existential quantifiers in a triple conjunction. (Contributed by NM, 9-Mar-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 4exdistr 1839* | Distribution of existential quantifiers in a quadruple conjunction. (Contributed by NM, 9-Mar-1995.) (Proof shortened by Wolf Lammen, 20-Jan-2018.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | spimeh 1840* | Existential introduction, using implicit substitution. Compare Lemma 14 of [Tarski] p. 70. (Contributed by NM, 7-Aug-1994.) (Proof shortened by Wolf Lammen, 10-Dec-2017.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | spimw 1841* | Specialization. Lemma 8 of [KalishMontague] p. 87. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 19-Apr-2017.) (Proof shortened by Wolf Lammen, 7-Aug-2017.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | spimvw 1842* | Specialization. Lemma 8 of [KalishMontague] p. 87. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 9-Apr-2017.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | spnfw 1843 | Weak version of sp 1936. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 1-Aug-2017.) (Proof shortened by Wolf Lammen, 13-Aug-2017.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | spfalw 1844 |
Version of sp 1936 when ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | equs4v 1845* | Version of equs4 2126 with a dv condition, which requires fewer axioms. (Contributed by BJ, 31-May-2019.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | equsalvw 1846* | Version of equsal 2127 with two dv conditions, which requires fewer axioms. (Contributed by BJ, 31-May-2019.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | equsexvw 1847* | Version of equsexv 2065 with a dv condition, which requires fewer axioms. See also equsex 2129. (Contributed by BJ, 31-May-2019.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | cbvaliw 1848* | Change bound variable. Uses only Tarski's FOL axiom schemes. Part of Lemma 7 of [KalishMontague] p. 86. (Contributed by NM, 19-Apr-2017.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | cbvalivw 1849* | Change bound variable. Uses only Tarski's FOL axiom schemes. Part of Lemma 7 of [KalishMontague] p. 86. (Contributed by NM, 9-Apr-2017.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Axiom | ax-7 1850 |
Axiom of Equality. One of the equality and substitution axioms of
predicate calculus with equality. It states that equality is
right-Euclidean (this is similar, but not identical, to being transitive,
which is proved as equtr 1864). This axiom scheme is a sub-scheme of Axiom
Scheme B8 of system S2 of [Tarski], p. 75,
whose general form cannot be
represented with our notation. Also appears as Axiom C7 of [Monk2] p. 105
and Axiom Scheme C8' in [Megill] p. 448
(p. 16 of the preprint).
The equality symbol was invented in 1527 by Robert Recorde. He chose a pair of parallel lines of the same length because "noe .2. thynges, can be moare equalle."
We prove in ax7 1859 that this axiom can be recovered from its
weakened
version ax7v 1851 where |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | ax7v 1851* |
Weakened version of ax-7 1850, with a dv condition on ![]() ![]() ![]()
In ax7v 1851, it is still allowed to substitute the same
variable for
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | ax7v1 1852* |
First of two weakened versions of ax7v 1851, with an extra dv condition on
![]() ![]() ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | ax7v2 1853* |
Second of two weakened versions of ax7v 1851, with an extra dv condition
on ![]() ![]() ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | equid 1854 | Identity law for equality. Lemma 2 of [KalishMontague] p. 85. See also Lemma 6 of [Tarski] p. 68. (Contributed by NM, 1-Apr-2005.) (Revised by NM, 9-Apr-2017.) (Proof shortened by Wolf Lammen, 5-Feb-2018.) (Proof shortened by Wolf Lammen, 22-Aug-2020.) |
![]() ![]() ![]() ![]() | ||
Theorem | equidOLD 1855 | Obsolete proof of equid 1854 as of 22-Aug-2020. (Contributed by NM, 1-Apr-2005.) (Revised by NM, 9-Apr-2017.) (Proof shortened by Wolf Lammen, 5-Feb-2018.) (Proof modification is discouraged.) (New usage is discouraged.) |
![]() ![]() ![]() ![]() | ||
Theorem | nfequid 1856 |
Bound-variable hypothesis builder for ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | equcomiv 1857* |
Weaker form of equcomi 1860 with a dv condition on ![]() ![]() ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | ax6evr 1858* | A commuted form of ax6ev 1806. (Contributed by BJ, 7-Dec-2020.) |
![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | ax7 1859 |
Proof of ax-7 1850 from ax7v1 1852 and ax7v2 1853, proving sufficiency of the
conjunction of the latter two weakened versions of ax7v 1851,
which is
itself a weakened version of ax-7 1850.
Note that the weakened version of ax-7 1850
obtained by adding a dv
condition on |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | equcomi 1860 | Commutative law for equality. Equality is a symmetric relation. Lemma 3 of [KalishMontague] p. 85. See also Lemma 7 of [Tarski] p. 69. (Contributed by NM, 10-Jan-1993.) (Revised by NM, 9-Apr-2017.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | equcom 1861 | Commutative law for equality. Equality is a symmetric relation. (Contributed by NM, 20-Aug-1993.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | equcomd 1862 | Deduction form of equcom 1861, symmetry of equality. For the versions for classes, see eqcom 2457 and eqcomd 2456. (Contributed by BJ, 6-Oct-2019.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | equcoms 1863 | An inference commuting equality in antecedent. Used to eliminate the need for a syllogism. (Contributed by NM, 10-Jan-1993.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | equtr 1864 | A transitive law for equality. (Contributed by NM, 23-Aug-1993.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | equtrr 1865 | A transitive law for equality. Lemma L17 in [Megill] p. 446 (p. 14 of the preprint). (Contributed by NM, 23-Aug-1993.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | equequ1 1866 | An equivalence law for equality. (Contributed by NM, 1-Aug-1993.) (Proof shortened by Wolf Lammen, 10-Dec-2017.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | equequ2 1867 | An equivalence law for equality. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Wolf Lammen, 4-Aug-2017.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | equtr2 1868 | Equality is left-Euclidean. (Contributed by NM, 12-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | stdpc6 1869 | One of the two equality axioms of standard predicate calculus, called reflexivity of equality. (The other one is stdpc7 1870.) 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 | stdpc7 1870 |
One of the two equality axioms of standard predicate calculus, called
substitutivity of equality. (The other one is stdpc6 1869.) Translated to
traditional notation, it can be
read: "![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | equviniv 1871* | A specialized version of equvini 2178 with a distinct variable restriction. (Contributed by Wolf Lammen, 8-Sep-2018.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | equvin 1872* | A variable introduction law for equality. Lemma 15 of [Monk2] p. 109. (Contributed by NM, 9-Jan-1993.) Remove dependencies on ax-10 1914, ax-13 2090. (Revised by Wolf Lammen, 10-Jun-2019.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | ax13b 1873 | An equivalence used to show two ways of expressing ax-13 2090. See the comment for ax-13 2090. (Contributed by NM, 2-May-2017.) (Proof shortened by Wolf Lammen, 26-Feb-2018.) (Revised by BJ, 15-Sep-2020.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | spfw 1874* | Weak version of sp 1936. Uses only Tarski's FOL axiom schemes. Lemma 9 of [KalishMontague] p. 87. This may be the best we can do with minimal distinct variable conditions. (Contributed by NM, 19-Apr-2017.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | spw 1875* |
Weak version of the specialization scheme sp 1936. Lemma 9 of
[KalishMontague] p. 87. While
it appears that sp 1936 in its general form
does not follow from Tarski's FOL axiom schemes, from this theorem we
can prove any instance of sp 1936 having mutually distinct setvar
variables and no wff metavariables (see ax12wdemo 1908 for an example of
the procedure to eliminate the hypothesis). Other approximations of
sp 1936 are spfw 1874 (minimal distinct variable
requirements), spnfw 1843 (when
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | cbvalw 1876* | Change bound variable. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 9-Apr-2017.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | cbvalvw 1877* | Change bound variable. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 9-Apr-2017.) (Proof shortened by Wolf Lammen, 28-Feb-2018.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | cbvexvw 1878* | Change bound variable. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 19-Apr-2017.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | alcomiw 1879* | Weak version of alcom 1922. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 10-Apr-2017.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | hbn1fw 1880* | Weak version of ax-10 1914 from which we can prove any ax-10 1914 instance not involving wff variables or bundling. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 19-Apr-2017.) (Proof shortened by Wolf Lammen, 28-Feb-2018.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | hbn1w 1881* | Weak version of hbn1 1915. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 9-Apr-2017.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | hba1w 1882* | Weak version of hba1 1977. See comments for ax10w 1902. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 9-Apr-2017.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | hbe1w 1883* | Weak version of hbe1 1916. See comments for ax10w 1902. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 19-Apr-2017.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | hbalw 1884* |
Weak version of hbal 1921. Uses only Tarski's FOL axiom schemes.
Unlike
hbal 1921, this theorem requires that ![]() ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | cbvaev 1885* | Change bound variable in an equality with a dv condition. (Contributed by NM, 22-Jul-2015.) (Revised by BJ, 18-Jun-2019.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Syntax | wcel 1886 |
Extend wff definition to include the membership connective between
classes.
For a general discussion of the theory of classes, see http://us.metamath.org/mpeuni/mmset.html#class.
(The purpose of introducing |
![]() ![]() ![]() ![]() | ||
Theorem | wel 1887 |
Extend wff definition to include atomic formulas with the epsilon
(membership) predicate. This is read "![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]()
This syntactic construction introduces a binary non-logical predicate
symbol
(Instead of introducing wel 1887 as an axiomatic statement, as was done in an
older version of this database, we introduce it by "proving" a
special
case of set theory's more general wcel 1886. This lets us avoid overloading
the |
![]() ![]() ![]() ![]() | ||
Axiom | ax-8 1888 |
Axiom of Left Equality for Binary Predicate. One of the equality and
substitution axioms for a non-logical predicate in our predicate calculus
with equality. It substitutes equal variables into the left-hand side of
an arbitrary binary predicate ![]()
We prove in ax8 1892 that this axiom can be recovered from its
weakened
version ax8v 1889 where |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | ax8v 1889* |
Weakened version of ax-8 1888, with a dv condition on ![]() ![]() ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | ax8v1 1890* |
First of two weakened versions of ax8v 1889, with an extra dv condition on
![]() ![]() ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | ax8v2 1891* |
Second of two weakened versions of ax8v 1889, with an extra dv condition
on ![]() ![]() ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | ax8 1892 | Proof of ax-8 1888 from ax8v1 1890 and ax8v2 1891, proving sufficiency of the conjunction of the latter two weakened versions of ax8v 1889, which is itself a weakened version of ax-8 1888. (Contributed by BJ, 7-Dec-2020.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | elequ1 1893 | An identity law for the non-logical predicate. (Contributed by NM, 30-Jun-1993.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | cleljust 1894* |
When the class variables in definition df-clel 2446 are replaced with
setvar variables, this theorem of predicate calculus is the result.
This theorem provides part of the justification for the consistency of
that definition, which "overloads" the setvar variables in wel 1887
with
the class variables in wcel 1886. (Contributed by NM, 28-Jan-2004.)
Revised to use equsexvw 1847 in order to remove dependencies on ax-10 1914,
ax-12 1932, ax-13 2090. Note that there is no DV condition
on ![]() ![]() ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Axiom | ax-9 1895 |
Axiom of Right Equality for Binary Predicate. One of the equality and
substitution axioms for a non-logical predicate in our predicate calculus
with equality. It substitutes equal variables into the right-hand side of
an arbitrary binary predicate ![]()
We prove in ax9 1899 that this axiom can be recovered from its
weakened
version ax9v 1896 where |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | ax9v 1896* |
Weakened version of ax-9 1895, with a dv condition on ![]() ![]() ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | ax9v1 1897* |
First of two weakened versions of ax9v 1896, with an extra dv condition on
![]() ![]() ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | ax9v2 1898* |
Second of two weakened versions of ax9v 1896, with an extra dv condition
on ![]() ![]() ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | ax9 1899 | Proof of ax-9 1895 from ax9v1 1897 and ax9v2 1898, proving sufficiency of the conjunction of the latter two weakened versions of ax9v 1896, which is itself a weakened version of ax-9 1895. (Contributed by BJ, 7-Dec-2020.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | elequ2 1900 | An identity law for the non-logical predicate. (Contributed by NM, 21-Jun-1993.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |