P. 20 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 1901-2000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	19.36v 1901*	Version of 19.36 2096 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 1902*	Inference associated with 19.36v 1901. Version of 19.36i 2097 with a dv condition. (Contributed by NM, 5-Aug-1993.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 17-Jan-2020.)
⊢ ∃𝑥(𝜑 → 𝜓)    ⇒   ⊢ (∀𝑥𝜑 → 𝜓)
Theorem	pm11.53v 1903*	Version of pm11.53 2178 with a dv condition, requiring fewer axioms. (Contributed by BJ, 7-Mar-2020.)
⊢ (∀𝑥∀𝑦(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → ∀𝑦𝜓))
Theorem	19.12vvv 1904*	Version of 19.12vv 2179 with a dv condition, requiring fewer axioms. See also 19.12 2161. (Contributed by BJ, 18-Mar-2020.)
⊢ (∃𝑥∀𝑦(𝜑 → 𝜓) ↔ ∀𝑦∃𝑥(𝜑 → 𝜓))
Theorem	19.27v 1905*	Version of 19.27 2093 with a dv condition, requiring fewer axioms. (Contributed by NM, 3-Jun-2004.)
⊢ (∀𝑥(𝜑 ∧ 𝜓) ↔ (∀𝑥𝜑 ∧ 𝜓))
Theorem	19.28v 1906*	Version of 19.28 2094 with a dv condition, requiring fewer axioms. (Contributed by NM, 25-Mar-2004.)
⊢ (∀𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∀𝑥𝜓))
Theorem	19.37v 1907*	Version of 19.37 2098 with a dv condition, requiring fewer axioms. (Contributed by NM, 21-Jun-1993.)
⊢ (∃𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∃𝑥𝜓))
Theorem	19.37iv 1908*	Inference associated with 19.37v 1907. (Contributed by NM, 5-Aug-1993.)
⊢ ∃𝑥(𝜑 → 𝜓)    ⇒   ⊢ (𝜑 → ∃𝑥𝜓)
Theorem	19.44v 1909*	Version of 19.44 2104 with a dv condition, requiring fewer axioms. (Contributed by NM, 12-Mar-1993.)
⊢ (∃𝑥(𝜑 ∨ 𝜓) ↔ (∃𝑥𝜑 ∨ 𝜓))
Theorem	19.45v 1910*	Version of 19.45 2105 with a dv condition, requiring fewer axioms. (Contributed by NM, 12-Mar-1993.)
⊢ (∃𝑥(𝜑 ∨ 𝜓) ↔ (𝜑 ∨ ∃𝑥𝜓))
Theorem	19.41v 1911*	Version of 19.41 2101 with a dv condition, requiring fewer axioms. (Contributed by NM, 21-Jun-1993.)
⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ 𝜓))
Theorem	19.41vv 1912*	Version of 19.41 2101 with two quantifiers and a dv condition requiring fewer axioms. (Contributed by NM, 30-Apr-1995.)
⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (∃𝑥∃𝑦𝜑 ∧ 𝜓))
Theorem	19.41vvv 1913*	Version of 19.41 2101 with three quantifiers and a dv condition requiring fewer axioms. (Contributed by NM, 30-Apr-1995.)
⊢ (∃𝑥∃𝑦∃𝑧(𝜑 ∧ 𝜓) ↔ (∃𝑥∃𝑦∃𝑧𝜑 ∧ 𝜓))
Theorem	19.41vvvv 1914*	Version of 19.41 2101 with four quantifiers and a dv condition requiring fewer axioms. (Contributed by FL, 14-Jul-2007.)
⊢ (∃𝑤∃𝑥∃𝑦∃𝑧(𝜑 ∧ 𝜓) ↔ (∃𝑤∃𝑥∃𝑦∃𝑧𝜑 ∧ 𝜓))
Theorem	19.42v 1915*	Version of 19.42 2103 with a dv condition requiring fewer axioms. (Contributed by NM, 21-Jun-1993.)
⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥𝜓))
Theorem	exdistr 1916*	Distribution of existential quantifiers. (Contributed by NM, 9-Mar-1995.)
⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ ∃𝑥(𝜑 ∧ ∃𝑦𝜓))
Theorem	19.42vv 1917*	Version of 19.42 2103 with two quantifiers and a dv condition requiring fewer axioms. (Contributed by NM, 16-Mar-1995.)
⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥∃𝑦𝜓))
Theorem	19.42vvv 1918*	Version of 19.42 2103 with three quantifiers and a dv condition requiring fewer axioms. (Contributed by NM, 21-Sep-2011.)
⊢ (∃𝑥∃𝑦∃𝑧(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥∃𝑦∃𝑧𝜓))
Theorem	exdistr2 1919*	Distribution of existential quantifiers. (Contributed by NM, 17-Mar-1995.)
⊢ (∃𝑥∃𝑦∃𝑧(𝜑 ∧ 𝜓) ↔ ∃𝑥(𝜑 ∧ ∃𝑦∃𝑧𝜓))
Theorem	3exdistr 1920*	Distribution of existential quantifiers in a triple conjunction. (Contributed by NM, 9-Mar-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ (∃𝑥∃𝑦∃𝑧(𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ∃𝑥(𝜑 ∧ ∃𝑦(𝜓 ∧ ∃𝑧𝜒)))
Theorem	4exdistr 1921*	Distribution of existential quantifiers in a quadruple conjunction. (Contributed by NM, 9-Mar-1995.) (Proof shortened by Wolf Lammen, 20-Jan-2018.)
⊢ (∃𝑥∃𝑦∃𝑧∃𝑤((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ↔ ∃𝑥(𝜑 ∧ ∃𝑦(𝜓 ∧ ∃𝑧(𝜒 ∧ ∃𝑤𝜃))))
Theorem	spimeh 1922*	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 1923*	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 1924*	Specialization. Lemma 8 of [KalishMontague] p. 87. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 9-Apr-2017.)
⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))    ⇒   ⊢ (∀𝑥𝜑 → 𝜓)
Theorem	spnfw 1925	Weak version of sp 2051. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 1-Aug-2017.) (Proof shortened by Wolf Lammen, 13-Aug-2017.)
⊢ (¬ 𝜑 → ∀𝑥 ¬ 𝜑)    ⇒   ⊢ (∀𝑥𝜑 → 𝜑)
Theorem	spfalw 1926	Version of sp 2051 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 1927*	Version of equs4 2289 with a dv condition, which requires fewer axioms. (Contributed by BJ, 31-May-2019.)
⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))
Theorem	equsalvw 1928*	Version of equsal 2290 with two dv conditions, which requires fewer axioms. (Contributed by BJ, 31-May-2019.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜓)
Theorem	equsexvw 1929*	Version of equsexv 2106 with a dv condition, which requires fewer axioms. See also equsex 2292. (Contributed by BJ, 31-May-2019.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ 𝜓)
Theorem	cbvaliw 1930*	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 1931*	Change bound variable. Uses only Tarski's FOL axiom schemes. Part of Lemma 7 of [KalishMontague] p. 86. (Contributed by NM, 9-Apr-2017.)
⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))    ⇒   ⊢ (∀𝑥𝜑 → ∀𝑦𝜓)
1.4.8  Axiom scheme ax-7 (Equality)
Axiom	ax-7 1932	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 1945). 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 1940 that this axiom can be recovered from its weakened version ax7v 1933 where 𝑥 and 𝑦 are assumed to be disjoint variables. In particular, the only theorem referencing ax-7 1932 should be ax7v 1933. See the comment of ax7v 1933 for more details on these matters. (Contributed by NM, 10-Jan-1993.) (Revised by BJ, 7-Dec-2020.) Use ax7 1940 instead. (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧))
Theorem	ax7v 1933*	Weakened version of ax-7 1932, with a dv condition on 𝑥, 𝑦. This should be the only proof referencing ax-7 1932, and it should be referenced only by its two weakened versions ax7v1 1934 and ax7v2 1935, from which ax-7 1932 is then rederived as ax7 1940, which shows that either ax7v 1933 or the conjunction of ax7v1 1934 and ax7v2 1935 is sufficient. In ax7v 1933, it is still allowed to substitute the same variable for 𝑥 and 𝑧, or the same variable for 𝑦 and 𝑧. Therefore, ax7v 1933 "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 1938 and equid 1936 respectively. (Contributed by BJ, 7-Dec-2020.) Use ax7 1940 instead. (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧))
Theorem	ax7v1 1934*	First of two weakened versions of ax7v 1933, with an extra dv condition on 𝑥, 𝑧, see comments there. (Contributed by BJ, 7-Dec-2020.)
⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧))
Theorem	ax7v2 1935*	Second of two weakened versions of ax7v 1933, with an extra dv condition on 𝑦, 𝑧, see comments there. (Contributed by BJ, 7-Dec-2020.)
⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧))
Theorem	equid 1936	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 1937	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 1938*	Weaker form of equcomi 1941 with a dv condition on 𝑥, 𝑦. This is an intermediate step and equcomi 1941 is fully recovered later. (Contributed by BJ, 7-Dec-2020.)
⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥)
Theorem	ax6evr 1939*	A commuted form of ax6ev 1887. (Contributed by BJ, 7-Dec-2020.)
⊢ ∃𝑥 𝑦 = 𝑥
Theorem	ax7 1940	Proof of ax-7 1932 from ax7v1 1934 and ax7v2 1935, proving sufficiency of the conjunction of the latter two weakened versions of ax7v 1933, which is itself a weakened version of ax-7 1932. Note that the weakened version of ax-7 1932 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 1941	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 1942	Commutative law for equality. Equality is a symmetric relation. (Contributed by NM, 20-Aug-1993.)
⊢ (𝑥 = 𝑦 ↔ 𝑦 = 𝑥)
Theorem	equcomd 1943	Deduction form of equcom 1942, symmetry of equality. For the versions for classes, see eqcom 2628 and eqcomd 2627. (Contributed by BJ, 6-Oct-2019.)
⊢ (𝜑 → 𝑥 = 𝑦)    ⇒   ⊢ (𝜑 → 𝑦 = 𝑥)
Theorem	equcoms 1944	An inference commuting equality in antecedent. Used to eliminate the need for a syllogism. (Contributed by NM, 10-Jan-1993.)
⊢ (𝑥 = 𝑦 → 𝜑)    ⇒   ⊢ (𝑦 = 𝑥 → 𝜑)
Theorem	equtr 1945	A transitive law for equality. (Contributed by NM, 23-Aug-1993.)
⊢ (𝑥 = 𝑦 → (𝑦 = 𝑧 → 𝑥 = 𝑧))
Theorem	equtrr 1946	A transitive law for equality. Lemma L17 in [Megill] p. 446 (p. 14 of the preprint). (Contributed by NM, 23-Aug-1993.)
⊢ (𝑥 = 𝑦 → (𝑧 = 𝑥 → 𝑧 = 𝑦))
Theorem	equeuclr 1947	Commuted version of equeucl 1948 (equality is left-Euclidean). (Contributed by BJ, 12-Apr-2021.)
⊢ (𝑥 = 𝑧 → (𝑦 = 𝑧 → 𝑦 = 𝑥))
Theorem	equeucl 1948	Equality is a left-Euclidean binary relation. (Right-Euclideanness is stated in ax-7 1932.) Curried (exported) form of equtr2 1951. (Contributed by BJ, 11-Apr-2021.)
⊢ (𝑥 = 𝑧 → (𝑦 = 𝑧 → 𝑥 = 𝑦))
Theorem	equequ1 1949	An equivalence law for equality. (Contributed by NM, 1-Aug-1993.) (Proof shortened by Wolf Lammen, 10-Dec-2017.)
⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 ↔ 𝑦 = 𝑧))
Theorem	equequ2 1950	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 1951	Equality is a left-Euclidean binary relation. Uncurried (imported) form of equeucl 1948. (Contributed by NM, 12-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by BJ, 11-Apr-2021.)
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑧) → 𝑥 = 𝑦)
Theorem	equequ2OLD 1952	Obsolete proof of equequ2 1950 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 1953	Obsolete proof of equtr2 1951 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 1954	One of the two equality axioms of standard predicate calculus, called reflexivity of equality. (The other one is stdpc7 1955.) 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 1955	One of the two equality axioms of standard predicate calculus, called substitutivity of equality. (The other one is stdpc6 1954.) 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 1956*	A variable introduction law for equality. Lemma 15 of [Monk2] p. 109. (Contributed by NM, 9-Jan-1993.) Remove dependencies on ax-10 2016, ax-13 2245. (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 1957*	A modified version of the forward implication of equvinv 1956 adapted to common usage. (Contributed by Wolf Lammen, 8-Sep-2018.)
⊢ (𝑥 = 𝑦 → ∃𝑧(𝑥 = 𝑧 ∧ 𝑦 = 𝑧))
Theorem	equvinivOLD 1958*	The forward implication of equvinv 1956. Obsolete as of 11-Apr-2021. Use equvinv 1956 instead. (Contributed by Wolf Lammen, 11-Apr-2021.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → ∃𝑧(𝑧 = 𝑥 ∧ 𝑧 = 𝑦))
Theorem	equvinvOLD 1959*	Obsolete version of equvinv 1956 as of 11-Apr-2021. (Contributed by NM, 9-Jan-1993.) Remove dependencies on ax-10 2016, ax-13 2245. (Revised by Wolf Lammen, 10-Jun-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 ↔ ∃𝑧(𝑥 = 𝑧 ∧ 𝑦 = 𝑧))
Theorem	equvelv 1960*	A specialized version of equvel 2346 with distinct variable restrictions and fewer axiom usage. (Contributed by Wolf Lammen, 10-Apr-2021.)
⊢ (𝑥 = 𝑦 ↔ ∀𝑧(𝑧 = 𝑥 → 𝑧 = 𝑦))
Theorem	ax13b 1961	An equivalence between two ways of expressing ax-13 2245. See the comment for ax-13 2245. (Contributed by NM, 2-May-2017.) (Proof shortened by Wolf Lammen, 26-Feb-2018.) (Revised by BJ, 15-Sep-2020.)
⊢ ((¬ 𝑥 = 𝑦 → (𝑦 = 𝑧 → 𝜑)) ↔ (¬ 𝑥 = 𝑦 → (¬ 𝑥 = 𝑧 → (𝑦 = 𝑧 → 𝜑))))
Theorem	spfw 1962*	Weak version of sp 2051. 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 1963*	Obsolete proof of spfw 1962 as of 10-Oct-2021. (Contributed by NM, 19-Apr-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ 𝜓 → ∀𝑥 ¬ 𝜓)    &   ⊢ (∀𝑥𝜑 → ∀𝑦∀𝑥𝜑)    &   ⊢ (¬ 𝜑 → ∀𝑦 ¬ 𝜑)    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥𝜑 → 𝜑)
Theorem	spw 1964*	Weak version of the specialization scheme sp 2051. Lemma 9 of [KalishMontague] p. 87. While it appears that sp 2051 in its general form does not follow from Tarski's FOL axiom schemes, from this theorem we can prove any instance of sp 2051 having mutually distinct setvar variables and no wff metavariables (see ax12wdemo 2009 for an example of the procedure to eliminate the hypothesis). Other approximations of sp 2051 are spfw 1962 (minimal distinct variable requirements), spnfw 1925 (when 𝑥 is not free in ¬ 𝜑), spvw 1895 (when 𝑥 does not appear in 𝜑), sptruw 1730 (when 𝜑 is true), and spfalw 1926 (when 𝜑 is false). (Contributed by NM, 9-Apr-2017.) (Proof shortened by Wolf Lammen, 27-Feb-2018.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥𝜑 → 𝜑)
Theorem	cbvalw 1965*	Change bound variable. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 9-Apr-2017.)
⊢ (∀𝑥𝜑 → ∀𝑦∀𝑥𝜑)    &   ⊢ (¬ 𝜓 → ∀𝑥 ¬ 𝜓)    &   ⊢ (∀𝑦𝜓 → ∀𝑥∀𝑦𝜓)    &   ⊢ (¬ 𝜑 → ∀𝑦 ¬ 𝜑)    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓)
Theorem	cbvalvw 1966*	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 1967*	Change bound variable. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 19-Apr-2017.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓)
Theorem	alcomiw 1968*	Weak version of alcom 2034. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 10-Apr-2017.)
⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑)
Theorem	hbn1fw 1969*	Weak version of ax-10 2016 from which we can prove any ax-10 2016 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 1970*	Weak version of hbn1 2017. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 9-Apr-2017.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (¬ ∀𝑥𝜑 → ∀𝑥 ¬ ∀𝑥𝜑)
Theorem	hba1w 1971*	Weak version of hba1 2148. See comments for ax10w 2003. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 9-Apr-2017.) (Proof shortened by Wolf Lammen, 10-Oct-2021.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥𝜑 → ∀𝑥∀𝑥𝜑)
Theorem	hba1wOLD 1972*	Obsolete proof of hba1w 1971 as of 10-Oct-2021. (Contributed by NM, 9-Apr-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥𝜑 → ∀𝑥∀𝑥𝜑)
Theorem	hbe1w 1973*	Weak version of hbe1 2018. See comments for ax10w 2003. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 19-Apr-2017.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥𝜑 → ∀𝑥∃𝑥𝜑)
Theorem	hbalw 1974*	Weak version of hbal 2033. Uses only Tarski's FOL axiom schemes. Unlike hbal 2033, this theorem requires that 𝑥 and 𝑦 be distinct, i.e. not be bundled. (Contributed by NM, 19-Apr-2017.)
⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜓))    &   ⊢ (𝜑 → ∀𝑥𝜑)    ⇒   ⊢ (∀𝑦𝜑 → ∀𝑥∀𝑦𝜑)
Theorem	spaev 1975*	A special instance of sp 2051 applied to an equality with a dv condition. Unlike the more general sp 2051, we can prove this without ax-12 2044. Instance of aeveq 1979. 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 1976*	Change bound variable in an equality with a dv condition. Instance of aev 1980. (Contributed by NM, 22-Jul-2015.) (Revised by BJ, 18-Jun-2019.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧 𝑧 = 𝑦)
Theorem	aevlem0 1977*	Lemma for aevlem 1978. Instance of aev 1980. (Contributed by NM, 8-Jul-2016.) (Proof shortened by Wolf Lammen, 17-Feb-2018.) Remove dependency on ax-12 2044. (Revised by Wolf Lammen, 14-Mar-2021.) (Revised by BJ, 29-Mar-2021.) (Proof shortened by Wolf Lammen, 30-Mar-2021.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧 𝑧 = 𝑥)
Theorem	aevlem 1978*	Lemma for aev 1980 and axc16g 2130. Change free and bound variables. Instance of aev 1980. (Contributed by NM, 22-Jul-2015.) (Proof shortened by Wolf Lammen, 17-Feb-2018.) Remove dependency on ax-13 2245, along an idea of BJ. (Revised by Wolf Lammen, 30-Nov-2019.) (Revised by BJ, 29-Mar-2021.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧 𝑧 = 𝑡)
Theorem	aeveq 1979*	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 1980*	A "distinctor elimination" lemma with no restrictions on variables in the consequent. (Contributed by NM, 8-Nov-2006.) Remove dependency on ax-11 2031. (Revised by Wolf Lammen, 7-Sep-2018.) Remove dependency on ax-13 2245, inspired by an idea of BJ. (Revised by Wolf Lammen, 30-Nov-2019.) Remove dependency on ax-12 2044. (Revised by Wolf Lammen, 19-Mar-2021.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧 𝑡 = 𝑢)
Theorem	hbaevg 1981*	Generalization of hbaev 1982, proved at no extra cost. Instance of aev2 1983. (Contributed by Wolf Lammen, 22-Mar-2021.) (Revised by BJ, 29-Mar-2021.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧∀𝑡 𝑡 = 𝑢)
Theorem	hbaev 1982*	Version of hbae 2314 with a DV condition, requiring fewer axioms. Instance of hbaevg 1981 and aev2 1983. (Contributed by Wolf Lammen, 22-Mar-2021.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧∀𝑥 𝑥 = 𝑦)
Theorem	aev2 1983*	A version of aev 1980 with two universal quantifiers in the consequent, and a generalization of hbaevg 1981. One can prove similar statements with arbitrary numbers of universal quantifiers in the consequent (the series begins with aeveq 1979, aev 1980, aev2 1983). Using aev 1980 and alrimiv 1852 (as in aev2ALT 1984), 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 27205. This list cannot be extended to ¬ or ⊥ since the scheme ∀𝑥𝑥 = 𝑦 is consistent with ax-mp 5, ax-gen 1719, ax-1 6-- ax-13 2245 (as the one-element universe shows). (Contributed by BJ, 29-Mar-2021.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧∀𝑡 𝑢 = 𝑣)
Theorem	aev2ALT 1984*	Alternate proof of aev2 1983, bypassing hbaevg 1981. (Contributed by BJ, 23-Mar-2021.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧∀𝑡 𝑢 = 𝑣)
Theorem	axc11nlemOLD2 1985*	Lemma for axc11n 2306. Change bound variable in an equality. Obsolete as of 29-Mar-2021. Use aev 1980 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 2044. (Revised by Wolf Lammen, 14-Mar-2021.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑦 𝑦 = 𝑥 → (𝑥 = 𝑧 → ∀𝑦 𝑥 = 𝑧))    ⇒   ⊢ (∀𝑥 𝑥 = 𝑧 → ∀𝑦 𝑦 = 𝑥)
Theorem	aevlemOLD 1986*	Old proof of aevlem 1978. 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 2245, along an idea of BJ. (Revised by Wolf Lammen, 30-Nov-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑧 𝑧 = 𝑤 → ∀𝑦 𝑦 = 𝑥)
1.4.9  Membership predicate
Syntax	wcel 1987	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 1988 of predicate calculus in terms of the wcel 1987 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 2608 for more information on the set theory usage of wcel 1987.)
wff 𝐴 ∈ 𝐵
Theorem	wel 1988	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 1988 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 1987. This lets us avoid overloading the ∈ connective, thus preventing ambiguity that would complicate certain Metamath parsers. However, logically wel 1988 is considered to be a primitive syntax, even though here it is artificially "derived" from wcel 1987. 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 𝑥 ∈ 𝑦
1.4.10  Axiom scheme ax-8 (Left Equality for Binary Predicate)
Axiom	ax-8 1989	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 1993 that this axiom can be recovered from its weakened version ax8v 1990 where 𝑥 and 𝑦 are assumed to be disjoint variables. In particular, the only theorem referencing ax-8 1989 should be ax8v 1990. See the comment of ax8v 1990 for more details on these matters. (Contributed by NM, 30-Jun-1993.) (Revised by BJ, 7-Dec-2020.) Use ax8 1993 instead. (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧))
Theorem	ax8v 1990*	Weakened version of ax-8 1989, with a dv condition on 𝑥, 𝑦. This should be the only proof referencing ax-8 1989, and it should be referenced only by its two weakened versions ax8v1 1991 and ax8v2 1992, from which ax-8 1989 is then rederived as ax8 1993, which shows that either ax8v 1990 or the conjunction of ax8v1 1991 and ax8v2 1992 is sufficient. (Contributed by BJ, 7-Dec-2020.) Use ax8 1993 instead. (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧))
Theorem	ax8v1 1991*	First of two weakened versions of ax8v 1990, with an extra dv condition on 𝑥, 𝑧, see comments there. (Contributed by BJ, 7-Dec-2020.)
⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧))
Theorem	ax8v2 1992*	Second of two weakened versions of ax8v 1990, with an extra dv condition on 𝑦, 𝑧 see comments there. (Contributed by BJ, 7-Dec-2020.)
⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧))
Theorem	ax8 1993	Proof of ax-8 1989 from ax8v1 1991 and ax8v2 1992, proving sufficiency of the conjunction of the latter two weakened versions of ax8v 1990, which is itself a weakened version of ax-8 1989. (Contributed by BJ, 7-Dec-2020.) (Proof shortened by Wolf Lammen, 11-Apr-2021.)
⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧))
Theorem	elequ1 1994	An identity law for the non-logical predicate. (Contributed by NM, 30-Jun-1993.)
⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑧 ↔ 𝑦 ∈ 𝑧))
Theorem	cleljust 1995*	When the class variables in definition df-clel 2617 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 1988 with the class variables in wcel 1987. (Contributed by NM, 28-Jan-2004.) Revised to use equsexvw 1929 in order to remove dependencies on ax-10 2016, ax-12 2044, ax-13 2245. Note that there is no DV condition on 𝑥, 𝑦, that is, on the variables of the left-hand side. (Revised by BJ, 29-Dec-2020.)
⊢ (𝑥 ∈ 𝑦 ↔ ∃𝑧(𝑧 = 𝑥 ∧ 𝑧 ∈ 𝑦))
1.4.11  Axiom scheme ax-9 (Right Equality for Binary Predicate)
Axiom	ax-9 1996	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 2000 that this axiom can be recovered from its weakened version ax9v 1997 where 𝑥 and 𝑦 are assumed to be disjoint variables. In particular, the only theorem referencing ax-9 1996 should be ax9v 1997. See the comment of ax9v 1997 for more details on these matters. (Contributed by NM, 21-Jun-1993.) (Revised by BJ, 7-Dec-2020.) Use ax9 2000 instead. (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦))
Theorem	ax9v 1997*	Weakened version of ax-9 1996, with a dv condition on 𝑥, 𝑦. This should be the only proof referencing ax-9 1996, and it should be referenced only by its two weakened versions ax9v1 1998 and ax9v2 1999, from which ax-9 1996 is then rederived as ax9 2000, which shows that either ax9v 1997 or the conjunction of ax9v1 1998 and ax9v2 1999 is sufficient. (Contributed by BJ, 7-Dec-2020.) Use ax9 2000 instead. (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦))
Theorem	ax9v1 1998*	First of two weakened versions of ax9v 1997, with an extra dv condition on 𝑥, 𝑧, see comments there. (Contributed by BJ, 7-Dec-2020.)
⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦))
Theorem	ax9v2 1999*	Second of two weakened versions of ax9v 1997, with an extra dv condition on 𝑦, 𝑧 see comments there. (Contributed by BJ, 7-Dec-2020.)
⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦))
Theorem	ax9 2000	Proof of ax-9 1996 from ax9v1 1998 and ax9v2 1999, proving sufficiency of the conjunction of the latter two weakened versions of ax9v 1997, which is itself a weakened version of ax-9 1996. (Contributed by BJ, 7-Dec-2020.) (Proof shortened by Wolf Lammen, 11-Apr-2021.)
⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦))