Home | Metamath
Proof Explorer Theorem List (p. 20 of 426) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | 19.34 1901 | Theorem 19.34 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.) |
⊢ ((∀𝑥𝜑 ∨ ∃𝑥𝜓) → ∃𝑥(𝜑 ∨ 𝜓)) | ||
Theorem | 19.23v 1902* | Version of 19.23 2080 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 1903* | Theorem 19.23v 1902 extended to two variables. (Contributed by NM, 10-Aug-2004.) |
⊢ (∀𝑥∀𝑦(𝜑 → 𝜓) ↔ (∃𝑥∃𝑦𝜑 → 𝜓)) | ||
Theorem | 19.36v 1904* | Version of 19.36 2098 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 1905* | Inference associated with 19.36v 1904. Version of 19.36i 2099 with a dv condition. (Contributed by NM, 5-Aug-1993.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 17-Jan-2020.) |
⊢ ∃𝑥(𝜑 → 𝜓) ⇒ ⊢ (∀𝑥𝜑 → 𝜓) | ||
Theorem | pm11.53v 1906* | Version of pm11.53 2179 with a dv condition, requiring fewer axioms. (Contributed by BJ, 7-Mar-2020.) |
⊢ (∀𝑥∀𝑦(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → ∀𝑦𝜓)) | ||
Theorem | 19.12vvv 1907* | Version of 19.12vv 2180 with a dv condition, requiring fewer axioms. See also 19.12 2164. (Contributed by BJ, 18-Mar-2020.) |
⊢ (∃𝑥∀𝑦(𝜑 → 𝜓) ↔ ∀𝑦∃𝑥(𝜑 → 𝜓)) | ||
Theorem | 19.27v 1908* | Version of 19.27 2095 with a dv condition, requiring fewer axioms. (Contributed by NM, 3-Jun-2004.) |
⊢ (∀𝑥(𝜑 ∧ 𝜓) ↔ (∀𝑥𝜑 ∧ 𝜓)) | ||
Theorem | 19.28v 1909* | Version of 19.28 2096 with a dv condition, requiring fewer axioms. (Contributed by NM, 25-Mar-2004.) |
⊢ (∀𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∀𝑥𝜓)) | ||
Theorem | 19.37v 1910* | Version of 19.37 2100 with a dv condition, requiring fewer axioms. (Contributed by NM, 21-Jun-1993.) |
⊢ (∃𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∃𝑥𝜓)) | ||
Theorem | 19.37iv 1911* | Inference associated with 19.37v 1910. (Contributed by NM, 5-Aug-1993.) |
⊢ ∃𝑥(𝜑 → 𝜓) ⇒ ⊢ (𝜑 → ∃𝑥𝜓) | ||
Theorem | 19.44v 1912* | Version of 19.44 2106 with a dv condition, requiring fewer axioms. (Contributed by NM, 12-Mar-1993.) |
⊢ (∃𝑥(𝜑 ∨ 𝜓) ↔ (∃𝑥𝜑 ∨ 𝜓)) | ||
Theorem | 19.45v 1913* | Version of 19.45 2107 with a dv condition, requiring fewer axioms. (Contributed by NM, 12-Mar-1993.) |
⊢ (∃𝑥(𝜑 ∨ 𝜓) ↔ (𝜑 ∨ ∃𝑥𝜓)) | ||
Theorem | 19.41v 1914* | Version of 19.41 2103 with a dv condition, requiring fewer axioms. (Contributed by NM, 21-Jun-1993.) |
⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ 𝜓)) | ||
Theorem | 19.41vv 1915* | Version of 19.41 2103 with two quantifiers and a dv condition requiring fewer axioms. (Contributed by NM, 30-Apr-1995.) |
⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (∃𝑥∃𝑦𝜑 ∧ 𝜓)) | ||
Theorem | 19.41vvv 1916* | Version of 19.41 2103 with three quantifiers and a dv condition requiring fewer axioms. (Contributed by NM, 30-Apr-1995.) |
⊢ (∃𝑥∃𝑦∃𝑧(𝜑 ∧ 𝜓) ↔ (∃𝑥∃𝑦∃𝑧𝜑 ∧ 𝜓)) | ||
Theorem | 19.41vvvv 1917* | Version of 19.41 2103 with four quantifiers and a dv condition requiring fewer axioms. (Contributed by FL, 14-Jul-2007.) |
⊢ (∃𝑤∃𝑥∃𝑦∃𝑧(𝜑 ∧ 𝜓) ↔ (∃𝑤∃𝑥∃𝑦∃𝑧𝜑 ∧ 𝜓)) | ||
Theorem | 19.42v 1918* | Version of 19.42 2105 with a dv condition requiring fewer axioms. (Contributed by NM, 21-Jun-1993.) |
⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥𝜓)) | ||
Theorem | exdistr 1919* | Distribution of existential quantifiers. (Contributed by NM, 9-Mar-1995.) |
⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ ∃𝑥(𝜑 ∧ ∃𝑦𝜓)) | ||
Theorem | 19.42vv 1920* | Version of 19.42 2105 with two quantifiers and a dv condition requiring fewer axioms. (Contributed by NM, 16-Mar-1995.) |
⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥∃𝑦𝜓)) | ||
Theorem | 19.42vvv 1921* | Version of 19.42 2105 with three quantifiers and a dv condition requiring fewer axioms. (Contributed by NM, 21-Sep-2011.) |
⊢ (∃𝑥∃𝑦∃𝑧(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥∃𝑦∃𝑧𝜓)) | ||
Theorem | exdistr2 1922* | Distribution of existential quantifiers. (Contributed by NM, 17-Mar-1995.) |
⊢ (∃𝑥∃𝑦∃𝑧(𝜑 ∧ 𝜓) ↔ ∃𝑥(𝜑 ∧ ∃𝑦∃𝑧𝜓)) | ||
Theorem | 3exdistr 1923* | Distribution of existential quantifiers in a triple conjunction. (Contributed by NM, 9-Mar-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
⊢ (∃𝑥∃𝑦∃𝑧(𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ∃𝑥(𝜑 ∧ ∃𝑦(𝜓 ∧ ∃𝑧𝜒))) | ||
Theorem | 4exdistr 1924* | Distribution of existential quantifiers in a quadruple conjunction. (Contributed by NM, 9-Mar-1995.) (Proof shortened by Wolf Lammen, 20-Jan-2018.) |
⊢ (∃𝑥∃𝑦∃𝑧∃𝑤((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ↔ ∃𝑥(𝜑 ∧ ∃𝑦(𝜓 ∧ ∃𝑧(𝜒 ∧ ∃𝑤𝜃)))) | ||
Theorem | spimeh 1925* | 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 1926* | 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 1927* | Specialization. Lemma 8 of [KalishMontague] p. 87. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 9-Apr-2017.) |
⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) ⇒ ⊢ (∀𝑥𝜑 → 𝜓) | ||
Theorem | spnfw 1928 | Weak version of sp 2053. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 1-Aug-2017.) (Proof shortened by Wolf Lammen, 13-Aug-2017.) |
⊢ (¬ 𝜑 → ∀𝑥 ¬ 𝜑) ⇒ ⊢ (∀𝑥𝜑 → 𝜑) | ||
Theorem | spfalw 1929 | Version of sp 2053 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 1930* | Version of equs4 2290 with a dv condition, which requires fewer axioms. (Contributed by BJ, 31-May-2019.) |
⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) | ||
Theorem | equsalvw 1931* | Version of equsalv 2108 with a dv condition, and of equsal 2291 with two dv conditions, which requires fewer axioms. See also the dual form equsexvw 1932. (Contributed by BJ, 31-May-2019.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜓) | ||
Theorem | equsexvw 1932* | Version of equsexv 2109 with a dv condition, and of equsex 2292 with two dv conditions, which requires fewer axioms. See also the dual form equsalvw 1931. (Contributed by BJ, 31-May-2019.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ 𝜓) | ||
Theorem | cbvaliw 1933* | 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 1934* | 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 1935 |
Axiom of Equality. One of the equality and substitution axioms of
predicate calculus with equality. It states that equality is a
right-Euclidean binary relation (this is similar, but not identical, to
being transitive, which is proved as equtr 1948). 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 1557 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 1943 that this axiom can be recovered from its weakened version ax7v 1936 where 𝑥 and 𝑦 are assumed to be disjoint variables. In particular, the only theorem referencing ax-7 1935 should be ax7v 1936. See the comment of ax7v 1936 for more details on these matters. (Contributed by NM, 10-Jan-1993.) (Revised by BJ, 7-Dec-2020.) Use ax7 1943 instead. (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧)) | ||
Theorem | ax7v 1936* |
Weakened version of ax-7 1935, with a dv condition on 𝑥, 𝑦. This
should be the only proof referencing ax-7 1935,
and it should be
referenced only by its two weakened versions ax7v1 1937 and ax7v2 1938, from
which ax-7 1935 is then rederived as ax7 1943,
which shows that either ax7v 1936
or the conjunction of ax7v1 1937 and ax7v2 1938 is sufficient.
In ax7v 1936, it is still allowed to substitute the same variable for 𝑥 and 𝑧, or the same variable for 𝑦 and 𝑧. Therefore, ax7v 1936 "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 1941 and equid 1939 respectively. (Contributed by BJ, 7-Dec-2020.) Use ax7 1943 instead. (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧)) | ||
Theorem | ax7v1 1937* | First of two weakened versions of ax7v 1936, with an extra dv condition on 𝑥, 𝑧, see comments there. (Contributed by BJ, 7-Dec-2020.) |
⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧)) | ||
Theorem | ax7v2 1938* | Second of two weakened versions of ax7v 1936, with an extra dv condition on 𝑦, 𝑧, see comments there. (Contributed by BJ, 7-Dec-2020.) |
⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧)) | ||
Theorem | equid 1939 | 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 | nfequid 1940 | 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 1941* | Weaker form of equcomi 1944 with a dv condition on 𝑥, 𝑦. This is an intermediate step and equcomi 1944 is fully recovered later. (Contributed by BJ, 7-Dec-2020.) |
⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥) | ||
Theorem | ax6evr 1942* | A commuted form of ax6ev 1890. (Contributed by BJ, 7-Dec-2020.) |
⊢ ∃𝑥 𝑦 = 𝑥 | ||
Theorem | ax7 1943 |
Proof of ax-7 1935 from ax7v1 1937 and ax7v2 1938, proving sufficiency of the
conjunction of the latter two weakened versions of ax7v 1936,
which is
itself a weakened version of ax-7 1935.
Note that the weakened version of ax-7 1935 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 1944 | 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 1945 | Commutative law for equality. Equality is a symmetric relation. (Contributed by NM, 20-Aug-1993.) |
⊢ (𝑥 = 𝑦 ↔ 𝑦 = 𝑥) | ||
Theorem | equcomd 1946 | Deduction form of equcom 1945, symmetry of equality. For the versions for classes, see eqcom 2629 and eqcomd 2628. (Contributed by BJ, 6-Oct-2019.) |
⊢ (𝜑 → 𝑥 = 𝑦) ⇒ ⊢ (𝜑 → 𝑦 = 𝑥) | ||
Theorem | equcoms 1947 | An inference commuting equality in antecedent. Used to eliminate the need for a syllogism. (Contributed by NM, 10-Jan-1993.) |
⊢ (𝑥 = 𝑦 → 𝜑) ⇒ ⊢ (𝑦 = 𝑥 → 𝜑) | ||
Theorem | equtr 1948 | A transitive law for equality. (Contributed by NM, 23-Aug-1993.) |
⊢ (𝑥 = 𝑦 → (𝑦 = 𝑧 → 𝑥 = 𝑧)) | ||
Theorem | equtrr 1949 | A transitive law for equality. Lemma L17 in [Megill] p. 446 (p. 14 of the preprint). (Contributed by NM, 23-Aug-1993.) |
⊢ (𝑥 = 𝑦 → (𝑧 = 𝑥 → 𝑧 = 𝑦)) | ||
Theorem | equeuclr 1950 | Commuted version of equeucl 1951 (equality is left-Euclidean). (Contributed by BJ, 12-Apr-2021.) |
⊢ (𝑥 = 𝑧 → (𝑦 = 𝑧 → 𝑦 = 𝑥)) | ||
Theorem | equeucl 1951 | Equality is a left-Euclidean binary relation. (Right-Euclideanness is stated in ax-7 1935.) Curried (exported) form of equtr2 1954. (Contributed by BJ, 11-Apr-2021.) |
⊢ (𝑥 = 𝑧 → (𝑦 = 𝑧 → 𝑥 = 𝑦)) | ||
Theorem | equequ1 1952 | An equivalence law for equality. (Contributed by NM, 1-Aug-1993.) (Proof shortened by Wolf Lammen, 10-Dec-2017.) |
⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 ↔ 𝑦 = 𝑧)) | ||
Theorem | equequ2 1953 | An equivalence law for equality. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Wolf Lammen, 4-Aug-2017.) (Proof shortened by BJ, 12-Apr-2021.) |
⊢ (𝑥 = 𝑦 → (𝑧 = 𝑥 ↔ 𝑧 = 𝑦)) | ||
Theorem | equtr2 1954 | Equality is a left-Euclidean binary relation. Uncurried (imported) form of equeucl 1951. (Contributed by NM, 12-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by BJ, 11-Apr-2021.) |
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑧) → 𝑥 = 𝑦) | ||
Theorem | equequ2OLD 1955 | Obsolete proof of equequ2 1953 as of 12-Apr-2021. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Wolf Lammen, 4-Aug-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝑧 = 𝑥 ↔ 𝑧 = 𝑦)) | ||
Theorem | equtr2OLD 1956 | Obsolete proof of equtr2 1954 as of 11-Apr-2021. (Contributed by NM, 12-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑧) → 𝑥 = 𝑦) | ||
Theorem | stdpc6 1957 | One of the two equality axioms of standard predicate calculus, called reflexivity of equality. (The other one is stdpc7 1958.) 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 1958 | One of the two equality axioms of standard predicate calculus, called substitutivity of equality. (The other one is stdpc6 1957.) 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 | equvinv 1959* | A variable introduction law for equality. Lemma 15 of [Monk2] p. 109. (Contributed by NM, 9-Jan-1993.) Remove dependencies on ax-10 2019, ax-13 2246. (Revised by Wolf Lammen, 10-Jun-2019.) Move the quantified variable (𝑧) to the left of the equality signs. (Revised by Wolf Lammen, 11-Apr-2021.) |
⊢ (𝑥 = 𝑦 ↔ ∃𝑧(𝑧 = 𝑥 ∧ 𝑧 = 𝑦)) | ||
Theorem | equviniva 1960* | A modified version of the forward implication of equvinv 1959 adapted to common usage. (Contributed by Wolf Lammen, 8-Sep-2018.) |
⊢ (𝑥 = 𝑦 → ∃𝑧(𝑥 = 𝑧 ∧ 𝑦 = 𝑧)) | ||
Theorem | equvinivOLD 1961* | The forward implication of equvinv 1959. Obsolete as of 11-Apr-2021. Use equvinv 1959 instead. (Contributed by Wolf Lammen, 11-Apr-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → ∃𝑧(𝑧 = 𝑥 ∧ 𝑧 = 𝑦)) | ||
Theorem | equvinvOLD 1962* | Obsolete version of equvinv 1959 as of 11-Apr-2021. (Contributed by NM, 9-Jan-1993.) Remove dependencies on ax-10 2019, ax-13 2246. (Revised by Wolf Lammen, 10-Jun-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 ↔ ∃𝑧(𝑥 = 𝑧 ∧ 𝑦 = 𝑧)) | ||
Theorem | equvelv 1963* | A specialized version of equvel 2347 with distinct variable restrictions and fewer axiom usage. (Contributed by Wolf Lammen, 10-Apr-2021.) |
⊢ (𝑥 = 𝑦 ↔ ∀𝑧(𝑧 = 𝑥 → 𝑧 = 𝑦)) | ||
Theorem | ax13b 1964 | An equivalence between two ways of expressing ax-13 2246. See the comment for ax-13 2246. (Contributed by NM, 2-May-2017.) (Proof shortened by Wolf Lammen, 26-Feb-2018.) (Revised by BJ, 15-Sep-2020.) |
⊢ ((¬ 𝑥 = 𝑦 → (𝑦 = 𝑧 → 𝜑)) ↔ (¬ 𝑥 = 𝑦 → (¬ 𝑥 = 𝑧 → (𝑦 = 𝑧 → 𝜑)))) | ||
Theorem | spfw 1965* | Weak version of sp 2053. 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.) (Proof shortened by Wolf Lammen, 10-Oct-2021.) |
⊢ (¬ 𝜓 → ∀𝑥 ¬ 𝜓) & ⊢ (∀𝑥𝜑 → ∀𝑦∀𝑥𝜑) & ⊢ (¬ 𝜑 → ∀𝑦 ¬ 𝜑) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥𝜑 → 𝜑) | ||
Theorem | spfwOLD 1966* | Obsolete proof of spfw 1965 as of 10-Oct-2021. (Contributed by NM, 19-Apr-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ 𝜓 → ∀𝑥 ¬ 𝜓) & ⊢ (∀𝑥𝜑 → ∀𝑦∀𝑥𝜑) & ⊢ (¬ 𝜑 → ∀𝑦 ¬ 𝜑) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥𝜑 → 𝜑) | ||
Theorem | spw 1967* | Weak version of the specialization scheme sp 2053. Lemma 9 of [KalishMontague] p. 87. While it appears that sp 2053 in its general form does not follow from Tarski's FOL axiom schemes, from this theorem we can prove any instance of sp 2053 having mutually distinct setvar variables and no wff metavariables (see ax12wdemo 2012 for an example of the procedure to eliminate the hypothesis). Other approximations of sp 2053 are spfw 1965 (minimal distinct variable requirements), spnfw 1928 (when 𝑥 is not free in ¬ 𝜑), spvw 1898 (when 𝑥 does not appear in 𝜑), sptruw 1733 (when 𝜑 is true), and spfalw 1929 (when 𝜑 is false). (Contributed by NM, 9-Apr-2017.) (Proof shortened by Wolf Lammen, 27-Feb-2018.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥𝜑 → 𝜑) | ||
Theorem | cbvalw 1968* | Change bound variable. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 9-Apr-2017.) |
⊢ (∀𝑥𝜑 → ∀𝑦∀𝑥𝜑) & ⊢ (¬ 𝜓 → ∀𝑥 ¬ 𝜓) & ⊢ (∀𝑦𝜓 → ∀𝑥∀𝑦𝜓) & ⊢ (¬ 𝜑 → ∀𝑦 ¬ 𝜑) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓) | ||
Theorem | cbvalvw 1969* | 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 1970* | Change bound variable. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 19-Apr-2017.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓) | ||
Theorem | alcomiw 1971* | Weak version of alcom 2037. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 10-Apr-2017.) |
⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑) | ||
Theorem | hbn1fw 1972* | Weak version of ax-10 2019 from which we can prove any ax-10 2019 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 1973* | Weak version of hbn1 2020. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 9-Apr-2017.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (¬ ∀𝑥𝜑 → ∀𝑥 ¬ ∀𝑥𝜑) | ||
Theorem | hba1w 1974* | Weak version of hba1 2151. See comments for ax10w 2006. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 9-Apr-2017.) (Proof shortened by Wolf Lammen, 10-Oct-2021.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥𝜑 → ∀𝑥∀𝑥𝜑) | ||
Theorem | hba1wOLD 1975* | Obsolete proof of hba1w 1974 as of 10-Oct-2021. (Contributed by NM, 9-Apr-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥𝜑 → ∀𝑥∀𝑥𝜑) | ||
Theorem | hbe1w 1976* | Weak version of hbe1 2021. See comments for ax10w 2006. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 19-Apr-2017.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥𝜑 → ∀𝑥∃𝑥𝜑) | ||
Theorem | hbalw 1977* | Weak version of hbal 2036. Uses only Tarski's FOL axiom schemes. Unlike hbal 2036, this theorem requires that 𝑥 and 𝑦 be distinct, i.e. not be bundled. (Contributed by NM, 19-Apr-2017.) |
⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜓)) & ⊢ (𝜑 → ∀𝑥𝜑) ⇒ ⊢ (∀𝑦𝜑 → ∀𝑥∀𝑦𝜑) | ||
Theorem | spaev 1978* |
A special instance of sp 2053 applied to an equality with a dv condition.
Unlike the more general sp 2053, we can prove this without ax-12 2047.
Instance of aeveq 1982.
The antecedent ∀𝑥𝑥 = 𝑦 with distinct 𝑥 and 𝑦 is a characteristic of a degenerate universe, in which just one object exists. Actually more than one object may still exist, but if so, we give up on equality as a discriminating term. Separating this degenerate case from a richer universe, where inequality is possible, is a common proof idea. The name of this theorem follows a convention, where the condition ∀𝑥𝑥 = 𝑦 is denoted by 'aev', a shorthand for 'all equal, with a distinct variable condition'. (Contributed by Wolf Lammen, 14-Mar-2021.) |
⊢ (∀𝑥 𝑥 = 𝑦 → 𝑥 = 𝑦) | ||
Theorem | cbvaev 1979* | Change bound variable in an equality with a dv condition. Instance of aev 1983. (Contributed by NM, 22-Jul-2015.) (Revised by BJ, 18-Jun-2019.) |
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧 𝑧 = 𝑦) | ||
Theorem | aevlem0 1980* | Lemma for aevlem 1981. Instance of aev 1983. (Contributed by NM, 8-Jul-2016.) (Proof shortened by Wolf Lammen, 17-Feb-2018.) Remove dependency on ax-12 2047. (Revised by Wolf Lammen, 14-Mar-2021.) (Revised by BJ, 29-Mar-2021.) (Proof shortened by Wolf Lammen, 30-Mar-2021.) |
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧 𝑧 = 𝑥) | ||
Theorem | aevlem 1981* | Lemma for aev 1983 and axc16g 2134. Change free and bound variables. Instance of aev 1983. (Contributed by NM, 22-Jul-2015.) (Proof shortened by Wolf Lammen, 17-Feb-2018.) Remove dependency on ax-13 2246, along an idea of BJ. (Revised by Wolf Lammen, 30-Nov-2019.) (Revised by BJ, 29-Mar-2021.) |
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧 𝑧 = 𝑡) | ||
Theorem | aeveq 1982* | The antecedent ∀𝑥𝑥 = 𝑦 with a dv condition (typical of a one-object universe) forces equality of everything. (Contributed by Wolf Lammen, 19-Mar-2021.) |
⊢ (∀𝑥 𝑥 = 𝑦 → 𝑧 = 𝑡) | ||
Theorem | aev 1983* | A "distinctor elimination" lemma with no restrictions on variables in the consequent. (Contributed by NM, 8-Nov-2006.) Remove dependency on ax-11 2034. (Revised by Wolf Lammen, 7-Sep-2018.) Remove dependency on ax-13 2246, inspired by an idea of BJ. (Revised by Wolf Lammen, 30-Nov-2019.) Remove dependency on ax-12 2047. (Revised by Wolf Lammen, 19-Mar-2021.) |
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧 𝑡 = 𝑢) | ||
Theorem | hbaevg 1984* | Generalization of hbaev 1985, proved at no extra cost. Instance of aev2 1986. (Contributed by Wolf Lammen, 22-Mar-2021.) (Revised by BJ, 29-Mar-2021.) |
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧∀𝑡 𝑡 = 𝑢) | ||
Theorem | hbaev 1985* | Version of hbae 2315 with a DV condition, requiring fewer axioms. Instance of hbaevg 1984 and aev2 1986. (Contributed by Wolf Lammen, 22-Mar-2021.) |
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧∀𝑥 𝑥 = 𝑦) | ||
Theorem | aev2 1986* |
A version of aev 1983 with two universal quantifiers in the
consequent, and
a generalization of hbaevg 1984. One can prove similar statements with
arbitrary numbers of universal quantifiers in the consequent (the series
begins with aeveq 1982, aev 1983, aev2 1986).
Using aev 1983 and alrimiv 1855 (as in aev2ALT 1987), one can actually prove (with no more axioms) any scheme of the form (∀𝑥𝑥 = 𝑦 → PHI) , DV (𝑥, 𝑦) where PHI involves only setvar variables and the connectors →, ↔, ∧, ∨, ⊤, =, ∀, ∃, ∃*, ∃!, Ⅎ. An example is given by aevdemo 27317. This list cannot be extended to ¬ or ⊥ since the scheme ∀𝑥𝑥 = 𝑦 is consistent with ax-mp 5, ax-gen 1722, ax-1 6-- ax-13 2246 (as the one-element universe shows). (Contributed by BJ, 29-Mar-2021.) |
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧∀𝑡 𝑢 = 𝑣) | ||
Theorem | aev2ALT 1987* | Alternate proof of aev2 1986, bypassing hbaevg 1984. (Contributed by BJ, 23-Mar-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧∀𝑡 𝑢 = 𝑣) | ||
Theorem | axc11nlemOLD2 1988* | Lemma for axc11n 2307. Change bound variable in an equality. Obsolete as of 29-Mar-2021. Use aev 1983 instead. (Contributed by NM, 8-Jul-2016.) (Proof shortened by Wolf Lammen, 17-Feb-2018.) Restructure to ease either bundling, or reducing dependencies on axioms. (Revised by Wolf Lammen, 30-Nov-2019.) Remove dependency on ax-12 2047. (Revised by Wolf Lammen, 14-Mar-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑦 𝑦 = 𝑥 → (𝑥 = 𝑧 → ∀𝑦 𝑥 = 𝑧)) ⇒ ⊢ (∀𝑥 𝑥 = 𝑧 → ∀𝑦 𝑦 = 𝑥) | ||
Theorem | aevlemOLD 1989* | Old proof of aevlem 1981. Obsolete as of 29-Mar-2021. (Contributed by NM, 22-Jul-2015.) (Proof shortened by Wolf Lammen, 17-Feb-2018.) Remove dependency on ax-13 2246, along an idea of BJ. (Revised by Wolf Lammen, 30-Nov-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑧 𝑧 = 𝑤 → ∀𝑦 𝑦 = 𝑥) | ||
Syntax | wcel 1990 |
Extend wff definition to include the membership connective between
classes.
For a general discussion of the theory of classes, see mmset.html#class. (The purpose of introducing wff 𝐴 ∈ 𝐵 here is to allow us to express i.e. "prove" the wel 1991 of predicate calculus in terms of the wcel 1990 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 2609 for more information on the set theory usage of wcel 1990.) |
wff 𝐴 ∈ 𝐵 | ||
Theorem | wel 1991 |
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 1991 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 1990. This lets us avoid overloading the ∈ connective, thus preventing ambiguity that would complicate certain Metamath parsers. However, logically wel 1991 is considered to be a primitive syntax, even though here it is artificially "derived" from wcel 1990. 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.) |
wff 𝑥 ∈ 𝑦 | ||
Axiom | ax-8 1992 |
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 1996 that this axiom can be recovered from its weakened version ax8v 1993 where 𝑥 and 𝑦 are assumed to be disjoint variables. In particular, the only theorem referencing ax-8 1992 should be ax8v 1993. See the comment of ax8v 1993 for more details on these matters. (Contributed by NM, 30-Jun-1993.) (Revised by BJ, 7-Dec-2020.) Use ax8 1996 instead. (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧)) | ||
Theorem | ax8v 1993* | Weakened version of ax-8 1992, with a dv condition on 𝑥, 𝑦. This should be the only proof referencing ax-8 1992, and it should be referenced only by its two weakened versions ax8v1 1994 and ax8v2 1995, from which ax-8 1992 is then rederived as ax8 1996, which shows that either ax8v 1993 or the conjunction of ax8v1 1994 and ax8v2 1995 is sufficient. (Contributed by BJ, 7-Dec-2020.) Use ax8 1996 instead. (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧)) | ||
Theorem | ax8v1 1994* | First of two weakened versions of ax8v 1993, with an extra dv condition on 𝑥, 𝑧, see comments there. (Contributed by BJ, 7-Dec-2020.) |
⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧)) | ||
Theorem | ax8v2 1995* | Second of two weakened versions of ax8v 1993, with an extra dv condition on 𝑦, 𝑧 see comments there. (Contributed by BJ, 7-Dec-2020.) |
⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧)) | ||
Theorem | ax8 1996 | Proof of ax-8 1992 from ax8v1 1994 and ax8v2 1995, proving sufficiency of the conjunction of the latter two weakened versions of ax8v 1993, which is itself a weakened version of ax-8 1992. (Contributed by BJ, 7-Dec-2020.) (Proof shortened by Wolf Lammen, 11-Apr-2021.) |
⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧)) | ||
Theorem | elequ1 1997 | An identity law for the non-logical predicate. (Contributed by NM, 30-Jun-1993.) |
⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑧 ↔ 𝑦 ∈ 𝑧)) | ||
Theorem | cleljust 1998* | When the class variables in definition df-clel 2618 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 1991 with the class variables in wcel 1990. (Contributed by NM, 28-Jan-2004.) Revised to use equsexvw 1932 in order to remove dependencies on ax-10 2019, ax-12 2047, ax-13 2246. 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 1999 |
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 2003 that this axiom can be recovered from its weakened version ax9v 2000 where 𝑥 and 𝑦 are assumed to be disjoint variables. In particular, the only theorem referencing ax-9 1999 should be ax9v 2000. See the comment of ax9v 2000 for more details on these matters. (Contributed by NM, 21-Jun-1993.) (Revised by BJ, 7-Dec-2020.) Use ax9 2003 instead. (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦)) | ||
Theorem | ax9v 2000* | Weakened version of ax-9 1999, with a dv condition on 𝑥, 𝑦. This should be the only proof referencing ax-9 1999, and it should be referenced only by its two weakened versions ax9v1 2001 and ax9v2 2002, from which ax-9 1999 is then rederived as ax9 2003, which shows that either ax9v 2000 or the conjunction of ax9v1 2001 and ax9v2 2002 is sufficient. (Contributed by BJ, 7-Dec-2020.) Use ax9 2003 instead. (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |