Home | 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: | Metamath Proof Explorer
(1-26564) |
Hilbert Space Explorer
(26565-28087) |
Users' Mathboxes
(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 and be
distinct) it was used in an axiom system of Tarski (see Axiom B7' in
footnote 1 of [KalishMontague] p.
81.) It is equivalent to axiom scheme
C10' in [Megill] p. 448 (p. 16 of the
preprint); the equivalence is
established by axc10 2095 and ax6fromc10 32462. A more convenient form of this
axiom is ax6e 2093, which has additional remarks.
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
and be
distinct. This trivial proof is intended merely to weaken axiom ax-6 1804
by adding a distinct variable restriction. From here on, ax-6 1804
should
not be referenced directly by any other proof, so that theorem ax6 2094
will show that we can recover ax-6 1804 from this weaker version if it were
an axiom (as it is in the case of Tarski).
Note: Introducing as a distinct variable group "out of the blue" with no apparent justification has puzzled some people, but it is perfectly sound. All we are doing is adding an additional redundant requirement, no different from adding a redundant logical hypothesis, that results in a weakening of the theorem. This means that any future theorem that references ax6v 1805 must have a $d specified for the two variables that get substituted for and . The $d does not propagate "backwards" i.e. it does not impose a requirement on ax-6 1804. 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 does not occur in . Converse of ax-5 1757. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 10-Apr-2017.) (Proof shortened by Wolf Lammen, 4-Dec-2017.) |
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 is false. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 23-Apr-2017.) (Proof shortened by Wolf Lammen, 25-Dec-2017.) |
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 and are assumed to be disjoint variables. In particular, the only theorem referencing ax-7 1850 should be ax7v 1851. See the comment of ax7v 1851 for more details on these matters. (Contributed by NM, 10-Jan-1993.) (Revised by BJ, 7-Dec-2020.) Use ax7 1859 instead. (New usage is discouraged.) |
Theorem | ax7v 1851* |
Weakened version of ax-7 1850, with a dv condition on .
This
should be the only proof referencing ax-7 1850,
and it should be
referenced only by its two weakened versions ax7v1 1852 and ax7v2 1853, from
which ax-7 1850 is then rederived as ax7 1859,
which shows that either ax7v 1851
or the conjunction of ax7v1 1852 and ax7v2 1853 is sufficient.
In ax7v 1851, it is still allowed to substitute the same variable for and , or the same variable for and . Therefore, ax7v 1851 "bundles" (a term coined by Raph Levien) its "principal instance" with distinct, and its "degenerate instances" and with distinct. These degenerate instances are for instance used in the proofs of equcomiv 1857 and equid 1854 respectively. (Contributed by BJ, 7-Dec-2020.) Use ax7 1859 instead. (New usage is discouraged.) |
Theorem | ax7v1 1852* | First of two weakened versions of ax7v 1851, with an extra dv condition on , see comments there. (Contributed by BJ, 7-Dec-2020.) |
Theorem | ax7v2 1853* | Second of two weakened versions of ax7v 1851, with an extra dv condition on , see comments there. (Contributed by BJ, 7-Dec-2020.) |
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 . This theorem tells us that any variable, including , is effectively not free in , even though is technically free according to the traditional definition of free variable. (Contributed by NM, 13-Jan-2011.) (Revised by NM, 21-Aug-2017.) |
Theorem | equcomiv 1857* | Weaker form of equcomi 1860 with a dv condition on . This is an intermediate step and equcomi 1860 is fully recovered later. (Contributed by BJ, 7-Dec-2020.) |
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 (resp. on ) does not permit, together with the other axioms, to prove reflexivity (resp. symmetry). (Contributed by BJ, 7-Dec-2020.) |
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: " , provided that is free for in ." Axiom 7 of [Mendelson] p. 95. (Contributed by NM, 15-Feb-2005.) |
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 is not free in ), spvw 1813 (when does not appear in ), sptruw 1680 (when is true), and spfalw 1844 (when is false). (Contributed by NM, 9-Apr-2017.) (Proof shortened by Wolf Lammen, 27-Feb-2018.) |
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 and be distinct i.e. are not bundled. (Contributed by NM, 19-Apr-2017.) |
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 here is to allow us to express i.e. "prove" the wel 1887 of predicate calculus in terms of the wcel 1886 of set theory, so that we don't "overload" the connective with two syntax definitions. This is done to prevent ambiguity that would complicate some Metamath parsers. The class variables and are introduced temporarily for the purpose of this definition but otherwise not used in predicate calculus. See df-clab 2437 for more information on the set theory usage of wcel 1886.) |
Theorem | wel 1887 |
Extend wff definition to include atomic formulas with the epsilon
(membership) predicate. This is read " is an element of
," " is a member of ," " belongs to ,"
or " contains
." Note: The
phrase " includes
" means
" is a subset of
;" to use it also
for
, as some authors occasionally do, is poor form and causes
confusion, according to George Boolos (1992 lecture at MIT).
This syntactic construction introduces a binary non-logical predicate symbol (epsilon) into our predicate calculus. We will eventually use it for the membership predicate of set theory, but that is irrelevant at this point: the predicate calculus axioms for apply to any arbitrary binary predicate symbol. "Non-logical" means that the predicate is presumed to have additional properties beyond the realm of predicate calculus, although these additional properties are not specified by predicate calculus itself but rather by the axioms of a theory (in our case set theory) added to predicate calculus. "Binary" means that the predicate has two arguments. (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 connective, thus preventing ambiguity that would complicate certain Metamath parsers. However, logically wel 1887 is considered to be a primitive syntax, even though here it is artificially "derived" from wcel 1886. Note: To see the proof steps of this syntax proof, type "show proof wel /all" in the Metamath program.) (Contributed by NM, 24-Jan-2006.) |
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 , which we will use for the set
membership relation when set theory is introduced. 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 scheme C12' in [Megill] p. 448 (p.
16 of the preprint).
"Non-logical" means that the predicate is not a primitive of
predicate
calculus proper but instead is an extension to it. "Binary"
means that
the predicate has two arguments. In a system of predicate calculus with
equality, like ours, equality is not usually considered to be a
non-logical predicate. In systems of predicate calculus without equality,
it typically would be.
We prove in ax8 1892 that this axiom can be recovered from its weakened version ax8v 1889 where and are assumed to be disjoint variables. In particular, the only theorem referencing ax-8 1888 should be ax8v 1889. See the comment of ax8v 1889 for more details on these matters. (Contributed by NM, 30-Jun-1993.) (Revised by BJ, 7-Dec-2020.) Use ax8 1892 instead. (New usage is discouraged.) |
Theorem | ax8v 1889* | Weakened version of ax-8 1888, with a dv condition on . This should be the only proof referencing ax-8 1888, and it should be referenced only by its two weakened versions ax8v1 1890 and ax8v2 1891, from which ax-8 1888 is then rederived as ax8 1892, which shows that either ax8v 1889 or the conjunction of ax8v1 1890 and ax8v2 1891 is sufficient. (Contributed by BJ, 7-Dec-2020.) Use ax8 1892 instead. (New usage is discouraged.) |
Theorem | ax8v1 1890* | First of two weakened versions of ax8v 1889, with an extra dv condition on , see comments there. (Contributed by BJ, 7-Dec-2020.) |
Theorem | ax8v2 1891* | Second of two weakened versions of ax8v 1889, with an extra dv condition on see comments there. (Contributed by BJ, 7-Dec-2020.) |
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 , that is, on the variables of the left-hand side. (Revised by BJ, 29-Dec-2020.) |
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 , which we will use for the set
membership relation when set theory is introduced. 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 scheme C13' in [Megill] p. 448 (p.
16 of the preprint).
We prove in ax9 1899 that this axiom can be recovered from its weakened version ax9v 1896 where and are assumed to be disjoint variables. In particular, the only theorem referencing ax-9 1895 should be ax9v 1896. See the comment of ax9v 1896 for more details on these matters. (Contributed by NM, 21-Jun-1993.) (Revised by BJ, 7-Dec-2020.) Use ax9 1899 instead. (New usage is discouraged.) |
Theorem | ax9v 1896* | Weakened version of ax-9 1895, with a dv condition on . This should be the only proof referencing ax-9 1895, and it should be referenced only by its two weakened versions ax9v1 1897 and ax9v2 1898, from which ax-9 1895 is then rederived as ax9 1899, which shows that either ax9v 1896 or the conjunction of ax9v1 1897 and ax9v2 1898 is sufficient. (Contributed by BJ, 7-Dec-2020.) Use ax9 1899 instead. (New usage is discouraged.) |
Theorem | ax9v1 1897* | First of two weakened versions of ax9v 1896, with an extra dv condition on , see comments there. (Contributed by BJ, 7-Dec-2020.) |
Theorem | ax9v2 1898* | Second of two weakened versions of ax9v 1896, with an extra dv condition on see comments there. (Contributed by BJ, 7-Dec-2020.) |
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 > |