P. 21 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 2001-2100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ax6v 2001*	Axiom B7 of [Tarski] p. 75, which requires that 𝑥 and 𝑦 be distinct. This trivial proof is intended merely to weaken Axiom ax-6 2000 by adding a distinct variable restriction ($d). From here on, ax-6 2000 should not be referenced directly by any other proof, so that Theorem ax6 2415 will show that we can recover ax-6 2000 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 prerequisite, similar to adding an unnecessary logical hypothesis, that results in a weakening of the theorem. This means that any future theorem that references ax6v 2001 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 2000. When possible, use of this theorem rather than ax6 2415 is preferred since its derivation is much shorter and requires fewer axioms. (Contributed by NM, 7-Aug-2015.)
⊢ ¬ ∀𝑥 ¬ 𝑥 = 𝑦
Theorem	ax6ev 2002*	At least one individual exists. Weaker version of ax6e 2414. When possible, use of this theorem rather than ax6e 2414 is preferred since its derivation is much shorter and requires fewer axioms. (Contributed by NM, 3-Aug-2017.)
⊢ ∃𝑥 𝑥 = 𝑦
Theorem	spimw 2003*	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	spimew 2004*	Existential introduction, using implicit substitution. Compare Lemma 14 of [Tarski] p. 70. (Contributed by NM, 7-Aug-1994.) (Proof shortened by Wolf Lammen, 22-Oct-2023.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))    ⇒   ⊢ (𝜑 → ∃𝑥𝜓)
Theorem	speiv 2005*	Inference from existential specialization. (Contributed by NM, 19-Aug-1993.) Use spimew 2004. (Revised by Wolf Lammen, 22-Oct-2023.)
⊢ (𝑥 = 𝑦 → (𝜓 → 𝜑))    &   ⊢ 𝜓    ⇒   ⊢ ∃𝑥𝜑
Theorem	speivw 2006*	Version of spei 2425 with a disjoint variable condition, which does not require ax-13 2403 (neither ax-7 2041 nor ax-12 2215). (Contributed by BJ, 31-May-2019.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ 𝜓    ⇒   ⊢ ∃𝑥𝜑
Theorem	exgen 2007	Rule of existential generalization, similar to universal generalization ax-gen 1828, but valid only if an individual exists. Its proof requires ax-6 2000 in our axiomatization but the equality predicate does not occur in its statement. Some fundamental theorems of predicate calculus can be proven from ax-gen 1828, ax-4 1842 and this theorem alone, not requiring ax-7 2041 or excessive distinct variable conditions. (Contributed by Wolf Lammen, 12-Nov-2017.) (Proof shortened by Wolf Lammen, 20-Oct-2023.)
⊢ 𝜑    ⇒   ⊢ ∃𝑥𝜑
Theorem	extru 2008	There exists a variable such that ⊤ holds; that is, there exists a variable. This corresponds under the standard translation to one of the formulations of the modal axiom (D), the other being 19.2 2009. (Contributed by Anthony Hart, 13-Sep-2011.) (Proof shortened by BJ, 12-May-2019.)
⊢ ∃𝑥⊤
Theorem	19.2 2009	Theorem 19.2 of [Margaris] p. 89. This corresponds to the axiom (D) of modal logic (the other standard formulation being extru 2008). 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 2226 for a more conventional proof of a more general result, which uses additional axioms. The reverse implication is the defining property of effective nonfreeness (see df-nf 1817). (Contributed by NM, 2-Aug-2017.) Remove dependency on ax-7 2041. (Revised by Wolf Lammen, 4-Dec-2017.)
⊢ (∀𝑥𝜑 → ∃𝑥𝜑)
Theorem	19.2d 2010	Deduction associated with 19.2 2009. (Contributed by BJ, 12-May-2019.)
⊢ (𝜑 → ∀𝑥𝜓)    ⇒   ⊢ (𝜑 → ∃𝑥𝜓)
Theorem	19.8w 2011	Weak version of 19.8a 2219 and instance of 19.2d 2010. (Contributed by NM, 1-Aug-2017.) (Proof shortened by Wolf Lammen, 4-Dec-2017.)
⊢ (𝜑 → ∀𝑥𝜑)    ⇒   ⊢ (𝜑 → ∃𝑥𝜑)
Theorem	spnfw 2012	Weak version of sp 2221. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 1-Aug-2017.) (Proof shortened by Wolf Lammen, 13-Aug-2017.)
⊢ (¬ 𝜑 → ∀𝑥 ¬ 𝜑)    ⇒   ⊢ (∀𝑥𝜑 → 𝜑)
Theorem	spfalw 2013	Version of sp 2221 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	spvw 2014*	Version of sp 2221 when 𝑥 does not occur in 𝜑. Converse of ax-5 1943. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 10-Apr-2017.) (Proof shortened by Wolf Lammen, 4-Dec-2017.) Shorten 19.3v 2015. (Revised by Wolf Lammen, 20-Oct-2023.)
⊢ (∀𝑥𝜑 → 𝜑)
Theorem	19.3v 2015*	Version of 19.3 2240 with a disjoint variable condition, requiring fewer axioms. Any formula can be universally quantified using a variable which it does not contain. See also 19.9v 2017. (Contributed by Anthony Hart, 13-Sep-2011.) Remove dependency on ax-7 2041. (Revised by Wolf Lammen, 4-Dec-2017.) (Proof shortened by Wolf Lammen, 20-Oct-2023.)
⊢ (∀𝑥𝜑 ↔ 𝜑)
Theorem	19.8v 2016*	Version of 19.8a 2219 with a disjoint variable condition, requiring fewer axioms. Converse of ax5e 1945. (Contributed by BJ, 12-Mar-2020.)
⊢ (𝜑 → ∃𝑥𝜑)
Theorem	19.9v 2017*	Version of 19.9 2243 with a disjoint variable condition, requiring fewer axioms. Any formula can be existentially quantified using a variable which it does not contain. See also 19.3v 2015. (Contributed by NM, 28-May-1995.) Remove dependency on ax-7 2041. (Revised by Wolf Lammen, 4-Dec-2017.)
⊢ (∃𝑥𝜑 ↔ 𝜑)
Theorem	spimevw 2018*	Existential introduction, using implicit substitution. This is to spimew 2004 what spimvw 2019 is to spimw 2003. Version of spimev 2423 and spimefv 2236 with an additional disjoint variable condition, using only Tarski's FOL axiom schemes. (Contributed by NM, 10-Jan-1993.) (Revised by BJ, 17-Mar-2020.)
⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))    ⇒   ⊢ (𝜑 → ∃𝑥𝜓)
Theorem	spimvw 2019*	A weak form of specialization. Lemma 8 of [KalishMontague] p. 87. Uses only Tarski's FOL axiom schemes. For stronger forms using more axioms, see spimv 2421 and spimfv 2277. (Contributed by NM, 9-Apr-2017.)
⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))    ⇒   ⊢ (∀𝑥𝜑 → 𝜓)
Theorem	spsv 2020*	Generalization of antecedent. A trivial weak version of sps 2223 avoiding ax-12 2215. (Contributed by SN, 13-Nov-2025.) (Proof shortened by WL, 19-Nov-2025.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (∀𝑥𝜑 → 𝜓)
Theorem	spvv 2021*	Specialization, using implicit substitution. Version of spv 2424 with a disjoint variable condition, which does not require ax-7 2041, ax-12 2215, ax-13 2403. (Contributed by NM, 30-Aug-1993.) (Revised by BJ, 31-May-2019.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥𝜑 → 𝜓)
Theorem	chvarvv 2022*	Implicit substitution of 𝑦 for 𝑥 into a theorem. Version of chvarv 2427 with a disjoint variable condition, which does not require ax-13 2403. (Contributed by NM, 20-Apr-1994.) (Revised by BJ, 31-May-2019.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ 𝜓
Theorem	19.39 2023	Theorem 19.39 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.)
⊢ ((∃𝑥𝜑 → ∃𝑥𝜓) → ∃𝑥(𝜑 → 𝜓))
Theorem	19.24 2024	Theorem 19.24 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.)
⊢ ((∀𝑥𝜑 → ∀𝑥𝜓) → ∃𝑥(𝜑 → 𝜓))
Theorem	19.34 2025	Theorem 19.34 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.)
⊢ ((∀𝑥𝜑 ∨ ∃𝑥𝜓) → ∃𝑥(𝜑 ∨ 𝜓))
Theorem	19.36v 2026*	Version of 19.36 2268 with a disjoint variable condition instead of a nonfreeness hypothesis. (Contributed by NM, 18-Aug-1993.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 17-Jan-2020.)
⊢ (∃𝑥(𝜑 → 𝜓) ↔ (∀𝑥𝜑 → 𝜓))
Theorem	19.12vvv 2027*	Version of 19.12vv 2378 with a disjoint variable condition, requiring fewer axioms. See also 19.12 2359. (Contributed by BJ, 18-Mar-2020.)
⊢ (∃𝑥∀𝑦(𝜑 → 𝜓) ↔ ∀𝑦∃𝑥(𝜑 → 𝜓))
Theorem	19.27v 2028*	Version of 19.27 2265 with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 3-Jun-2004.)
⊢ (∀𝑥(𝜑 ∧ 𝜓) ↔ (∀𝑥𝜑 ∧ 𝜓))
Theorem	19.28v 2029*	Version of 19.28 2266 with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 25-Mar-2004.)
⊢ (∀𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∀𝑥𝜓))
Theorem	19.37v 2030*	Version of 19.37 2270 with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 21-Jun-1993.)
⊢ (∃𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∃𝑥𝜓))
Theorem	19.44v 2031*	Version of 19.44 2275 with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 12-Mar-1993.)
⊢ (∃𝑥(𝜑 ∨ 𝜓) ↔ (∃𝑥𝜑 ∨ 𝜓))
Theorem	19.45v 2032*	Version of 19.45 2276 with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 12-Mar-1993.)
⊢ (∃𝑥(𝜑 ∨ 𝜓) ↔ (𝜑 ∨ ∃𝑥𝜓))
Theorem	equs4v 2033*	Version of equs4 2447 with a disjoint variable condition, which requires fewer axioms. (Contributed by NM, 10-May-1993.) (Revised by BJ, 31-May-2019.)
⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))
Theorem	alequexv 2034*	Version of equs4v 2033 with its consequence simplified by exsimpr 1902. (Contributed by BJ, 9-Nov-2021.)
⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → ∃𝑥𝜑)
Theorem	exsbim 2035*	One direction of the equivalence in exsb 2390 is based on fewer axioms. (Contributed by Wolf Lammen, 2-Mar-2023.)
⊢ (∃𝑦∀𝑥(𝑥 = 𝑦 → 𝜑) → ∃𝑥𝜑)
Theorem	equsv 2036*	If a formula does not contain a variable 𝑥, then it is equivalent to the corresponding prototype of substitution with a fresh variable (see sb6 2122). (Contributed by BJ, 23-Jul-2023.)
⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜑)
Theorem	equsalvw 2037*	Version of equsalv 2303 with a disjoint variable condition, and of equsal 2448 with two disjoint variable conditions, which requires fewer axioms. See also the dual form equsexvw 2038. (Contributed by BJ, 31-May-2019.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜓)
Theorem	equsexvw 2038*	Version of equsexv 2304 with a disjoint variable condition, and of equsex 2449 with two disjoint variable conditions, which requires fewer axioms. See also the dual form equsalvw 2037. (Contributed by BJ, 31-May-2019.) (Proof shortened by Wolf Lammen, 23-Oct-2023.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ 𝜓)
Theorem	cbvaliw 2039*	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 2040*	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.7  Axiom scheme ax-7 (Equality)
Axiom	ax-7 2041	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 2054). 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 2049 that this axiom can be recovered from its weakened version ax7v 2042 where 𝑥 and 𝑦 are assumed to be disjoint variables. In particular, the only theorem referencing ax-7 2041 should be ax7v 2042. See the comment of ax7v 2042 for more details on these matters. (Contributed by NM, 10-Jan-1993.) (Revised by BJ, 7-Dec-2020.) Use ax7 2049 instead. (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧))
Theorem	ax7v 2042*	Weakened version of ax-7 2041, with a disjoint variable condition on 𝑥, 𝑦. This should be the only proof referencing ax-7 2041, and it should be referenced only by its two weakened versions ax7v1 2043 and ax7v2 2044, from which ax-7 2041 is then rederived as ax7 2049, which shows that either ax7v 2042 or the conjunction of ax7v1 2043 and ax7v2 2044 is sufficient. In ax7v 2042, it is still allowed to substitute the same variable for 𝑥 and 𝑧, or the same variable for 𝑦 and 𝑧. Therefore, ax7v 2042 "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 2047 and equid 2045 respectively. (Contributed by BJ, 7-Dec-2020.) Use ax7 2049 instead. (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧))
Theorem	ax7v1 2043*	First of two weakened versions of ax7v 2042, with an extra disjoint variable condition on 𝑥, 𝑧, see comments there. (Contributed by BJ, 7-Dec-2020.)
⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧))
Theorem	ax7v2 2044*	Second of two weakened versions of ax7v 2042, with an extra disjoint variable condition on 𝑦, 𝑧, see comments there. (Contributed by BJ, 7-Dec-2020.)
⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧))
Theorem	equid 2045	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, 22-Aug-2020.)
⊢ 𝑥 = 𝑥
Theorem	nfequid 2046	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 2047*	Weaker form of equcomi 2050 with a disjoint variable condition on 𝑥, 𝑦. This is an intermediate step and equcomi 2050 is fully recovered later. (Contributed by BJ, 7-Dec-2020.)
⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥)
Theorem	ax6evr 2048*	A commuted form of ax6ev 2002. (Contributed by BJ, 7-Dec-2020.)
⊢ ∃𝑥 𝑦 = 𝑥
Theorem	ax7 2049	Proof of ax-7 2041 from ax7v1 2043 and ax7v2 2044 (and earlier axioms), proving sufficiency of the conjunction of the latter two weakened versions of ax7v 2042, which is itself a weakened version of ax-7 2041. Note that the weakened version of ax-7 2041 obtained by adding a disjoint variable 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 2050	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 2051	Commutative law for equality. Equality is a symmetric relation. (Contributed by NM, 20-Aug-1993.)
⊢ (𝑥 = 𝑦 ↔ 𝑦 = 𝑥)
Theorem	equcomd 2052	Deduction form of equcom 2051, symmetry of equality. For the versions for classes, see eqcom 2769 and eqcomd 2768. (Contributed by BJ, 6-Oct-2019.)
⊢ (𝜑 → 𝑥 = 𝑦)    ⇒   ⊢ (𝜑 → 𝑦 = 𝑥)
Theorem	equcoms 2053	An inference commuting equality in antecedent. Used to eliminate the need for a syllogism. (Contributed by NM, 10-Jan-1993.)
⊢ (𝑥 = 𝑦 → 𝜑)    ⇒   ⊢ (𝑦 = 𝑥 → 𝜑)
Theorem	equtr 2054	A transitive law for equality. (Contributed by NM, 23-Aug-1993.)
⊢ (𝑥 = 𝑦 → (𝑦 = 𝑧 → 𝑥 = 𝑧))
Theorem	equtrr 2055	A transitive law for equality. Lemma L17 in [Megill] p. 446 (p. 14 of the preprint). (Contributed by NM, 23-Aug-1993.)
⊢ (𝑥 = 𝑦 → (𝑧 = 𝑥 → 𝑧 = 𝑦))
Theorem	equeuclr 2056	Commuted version of equeucl 2057 (equality is left-Euclidean). (Contributed by BJ, 12-Apr-2021.)
⊢ (𝑥 = 𝑧 → (𝑦 = 𝑧 → 𝑦 = 𝑥))
Theorem	equeucl 2057	Equality is a left-Euclidean binary relation. (Right-Euclideanness is stated in ax-7 2041.) Curried (exported) form of equtr2 2060. (Contributed by BJ, 11-Apr-2021.)
⊢ (𝑥 = 𝑧 → (𝑦 = 𝑧 → 𝑥 = 𝑦))
Theorem	equequ1 2058	An equivalence law for equality. (Contributed by NM, 1-Aug-1993.) (Proof shortened by Wolf Lammen, 10-Dec-2017.)
⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 ↔ 𝑦 = 𝑧))
Theorem	equequ2 2059	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 2060	Equality is a left-Euclidean binary relation. Uncurried (imported) form of equeucl 2057. (Contributed by NM, 12-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by BJ, 11-Apr-2021.)
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑧) → 𝑥 = 𝑦)
Theorem	stdpc6 2061	One of the two equality axioms of standard predicate calculus, called reflexivity of equality. (The other one is stdpc7 2287.) 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	equvinv 2062*	A variable introduction law for equality. Lemma 15 of [Monk2] p. 109. (Contributed by NM, 9-Jan-1993.) Remove dependencies on ax-10 2178, ax-13 2403. (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.) (Proof shortened by Wolf Lammen, 12-Jul-2022.)
⊢ (𝑥 = 𝑦 ↔ ∃𝑧(𝑧 = 𝑥 ∧ 𝑧 = 𝑦))
Theorem	equvinva 2063*	A modified version of the forward implication of equvinv 2062 adapted to common usage. (Contributed by Wolf Lammen, 8-Sep-2018.)
⊢ (𝑥 = 𝑦 → ∃𝑧(𝑥 = 𝑧 ∧ 𝑦 = 𝑧))
Theorem	equvelv 2064*	A biconditional form of equvel 2487 with disjoint variable conditions and proved from Tarski's FOL axiom schemes. (Contributed by Andrew Salmon, 2-Jun-2011.) Reduce axiom usage. (Revised by Wolf Lammen, 10-Apr-2021.) (Proof shortened by Wolf Lammen, 12-Jul-2022.)
⊢ (∀𝑧(𝑧 = 𝑥 → 𝑧 = 𝑦) ↔ 𝑥 = 𝑦)
Theorem	ax13b 2065	An equivalence between two ways of expressing ax-13 2403. See the comment for ax-13 2403. (Contributed by NM, 2-May-2017.) (Proof shortened by Wolf Lammen, 26-Feb-2018.) (Revised by BJ, 15-Sep-2020.)
⊢ ((¬ 𝑥 = 𝑦 → (𝑦 = 𝑧 → 𝜑)) ↔ (¬ 𝑥 = 𝑦 → (¬ 𝑥 = 𝑧 → (𝑦 = 𝑧 → 𝜑))))
Theorem	spfw 2066*	Weak version of sp 2221. 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	spw 2067*	Weak version of the specialization scheme sp 2221. Lemma 9 of [KalishMontague] p. 87. While it appears that sp 2221 in its general form does not follow from Tarski's FOL axiom schemes, from this theorem we can prove any instance of sp 2221 having mutually distinct setvar variables and no wff metavariables (see ax12wdemo 2172 for an example of the procedure to eliminate the hypothesis). Other approximations of sp 2221 are spfw 2066 (minimal distinct variable requirements), spnfw 2012 (when 𝑥 is not free in ¬ 𝜑), spvw 2014 (when 𝑥 does not appear in 𝜑), sptruw 1839 (when 𝜑 is true), spfalw 2013 (when 𝜑 is false), and spvv 2021 (where 𝜑 is changed into 𝜓). (Contributed by NM, 9-Apr-2017.) (Proof shortened by Wolf Lammen, 27-Feb-2018.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥𝜑 → 𝜑)
Theorem	cbvalw 2068*	Change bound variable. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 9-Apr-2017.)
⊢ (∀𝑥𝜑 → ∀𝑦∀𝑥𝜑)    &   ⊢ (¬ 𝜓 → ∀𝑥 ¬ 𝜓)    &   ⊢ (∀𝑦𝜓 → ∀𝑥∀𝑦𝜓)    &   ⊢ (¬ 𝜑 → ∀𝑦 ¬ 𝜑)    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓)
Theorem	cbvalvw 2069*	Change bound variable. Uses only Tarski's FOL axiom schemes. See cbvalv 2431 for a version with fewer disjoint variable conditions but requiring more axioms. (Contributed by NM, 9-Apr-2017.) (Proof shortened by Wolf Lammen, 28-Feb-2018.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓)
Theorem	cbvexvw 2070*	Change bound variable. Uses only Tarski's FOL axiom schemes. See cbvexv 2432 for a version with fewer disjoint variable conditions but requiring more axioms. (Contributed by NM, 19-Apr-2017.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓)
Theorem	cbvaldvaw 2071*	Rule used to change the bound variable in a universal quantifier with implicit substitution. Deduction form. Version of cbvaldva 2440 with a disjoint variable condition, requiring fewer axioms. (Contributed by David Moews, 1-May-2017.) Avoid ax-13 2403. (Revised by GG, 10-Jan-2024.) Reduce axiom usage, along an idea of GG. (Revised by Wolf Lammen, 10-Feb-2024.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒))
Theorem	cbvexdvaw 2072*	Rule used to change the bound variable in an existential quantifier with implicit substitution. Deduction form. Version of cbvexdva 2441 with a disjoint variable condition, requiring fewer axioms. (Contributed by David Moews, 1-May-2017.) Avoid ax-13 2403. (Revised by GG, 10-Jan-2024.) Reduce axiom usage. (Revised by Wolf Lammen, 10-Feb-2024.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑦𝜒))
Theorem	cbval2vw 2073*	Rule used to change bound variables, using implicit substitution. Version of cbval2vv 2444 with more disjoint variable conditions, which requires fewer axioms . (Contributed by NM, 4-Feb-2005.) Avoid ax-13 2403. (Revised by GG, 10-Jan-2024.)
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑧∀𝑤𝜓)
Theorem	cbvex2vw 2074*	Rule used to change bound variables, using implicit substitution. Version of cbvex2vv 2445 with more disjoint variable conditions, which requires fewer axioms . (Contributed by NM, 26-Jul-1995.) Avoid ax-13 2403. (Revised by GG, 10-Jan-2024.)
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑧∃𝑤𝜓)
Theorem	cbvex4vw 2075*	Rule used to change bound variables, using implicit substitution. Version of cbvex4v 2446 with more disjoint variable conditions, which requires fewer axioms. (Contributed by NM, 26-Jul-1995.) Avoid ax-13 2403. (Revised by GG, 10-Jan-2024.)
⊢ ((𝑥 = 𝑣 ∧ 𝑦 = 𝑢) → (𝜑 ↔ 𝜓))    &   ⊢ ((𝑧 = 𝑓 ∧ 𝑤 = 𝑔) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (∃𝑥∃𝑦∃𝑧∃𝑤𝜑 ↔ ∃𝑣∃𝑢∃𝑓∃𝑔𝜒)
Theorem	alcomimw 2076*	Weak version of ax-11 2194. See alcomw 2078 for the biconditional form. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 10-Apr-2017.) (Proof shortened by Wolf Lammen, 28-Dec-2023.)
⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑)
Theorem	excomimw 2077*	Weak version of excomim 2200. Uses only Tarski's FOL axiom schemes. (Contributed by BTernaryTau, 23-Jun-2025.)
⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥∃𝑦𝜑 → ∃𝑦∃𝑥𝜑)
Theorem	alcomw 2078*	Weak version of alcom 2196 and biconditional form of alcomimw 2076. Uses only Tarski's FOL axiom schemes. (Contributed by BTernaryTau, 28-Dec-2024.)
⊢ (𝑥 = 𝑤 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜒))    ⇒   ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑦∀𝑥𝜑)
Theorem	excomw 2079*	Weak version of excom 2199 and biconditional form of excomimw 2077. Uses only Tarski's FOL axiom schemes. (Contributed by TM, 24-Jan-2026.)
⊢ (𝑥 = 𝑤 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜒))    ⇒   ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑦∃𝑥𝜑)
Theorem	hbn1fw 2080*	Weak version of ax-10 2178 from which we can prove any ax-10 2178 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 2081*	Weak version of hbn1 2179. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 9-Apr-2017.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (¬ ∀𝑥𝜑 → ∀𝑥 ¬ ∀𝑥𝜑)
Theorem	hba1w 2082*	Weak version of hba1 2328. See comments for ax10w 2166. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 9-Apr-2017.) (Proof shortened by Wolf Lammen, 10-Oct-2021.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥𝜑 → ∀𝑥∀𝑥𝜑)
Theorem	hbe1w 2083*	Weak version of hbe1 2180. See comments for ax10w 2166. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 19-Apr-2017.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥𝜑 → ∀𝑥∃𝑥𝜑)
Theorem	hbalw 2084*	Weak version of hbal 2204. Uses only Tarski's FOL axiom schemes. Unlike hbal 2204, this theorem requires that 𝑥 and 𝑦 be distinct, i.e., not be bundled. (Contributed by NM, 19-Apr-2017.)
⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜓))    &   ⊢ (𝜑 → ∀𝑥𝜑)    ⇒   ⊢ (∀𝑦𝜑 → ∀𝑥∀𝑦𝜑)
Theorem	19.8aw 2085*	If a formula is true, then it is true for at least one instance. This is to 19.8a 2219 what spw 2067 is to sp 2221. (Contributed by SN, 26-Sep-2024.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝜑 → ∃𝑥𝜑)
Theorem	exexw 2086*	Existential quantification over a given variable is idempotent. Weak version of bj-exexbiex 37435, requiring fewer axioms. (Contributed by GG, 4-Nov-2024.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥𝜑 ↔ ∃𝑥∃𝑥𝜑)
Theorem	spaev 2087*	A special instance of sp 2221 applied to an equality with a disjoint variable condition. Unlike the more general sp 2221, we can prove this without ax-12 2215. Instance of aeveq 2091. 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 2088*	Change bound variable in an equality with a disjoint variable condition. Instance of aev 2092. (Contributed by NM, 22-Jul-2015.) (Revised by BJ, 18-Jun-2019.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧 𝑧 = 𝑦)
Theorem	aevlem0 2089*	Lemma for aevlem 2090. Instance of aev 2092. (Contributed by NM, 8-Jul-2016.) (Proof shortened by Wolf Lammen, 17-Feb-2018.) Remove dependency on ax-12 2215. (Revised by Wolf Lammen, 14-Mar-2021.) Extract from proof of a former lemma for axc11n 2457 and add DV condition to reduce axiom usage. (Revised by BJ, 29-Mar-2021.) (Proof shortened by Wolf Lammen, 30-Mar-2021.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧 𝑧 = 𝑥)
Theorem	aevlem 2090*	Lemma for aev 2092 and axc16g 2296. Change free and bound variables. Instance of aev 2092. (Contributed by NM, 22-Jul-2015.) (Proof shortened by Wolf Lammen, 17-Feb-2018.) Remove dependency on ax-13 2403, along an idea of BJ. (Revised by Wolf Lammen, 30-Nov-2019.) Reduce axiom usage. (Revised by BJ, 29-Mar-2021.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧 𝑧 = 𝑡)
Theorem	aeveq 2091*	The antecedent ∀𝑥𝑥 = 𝑦 with a disjoint variable condition (typical of a one-object universe) forces equality of everything. (Contributed by Wolf Lammen, 19-Mar-2021.)
⊢ (∀𝑥 𝑥 = 𝑦 → 𝑧 = 𝑡)
Theorem	aev 2092*	A "distinctor elimination" lemma with no disjoint variable conditions on variables in the consequent. (Contributed by NM, 8-Nov-2006.) Remove dependency on ax-11 2194. (Revised by Wolf Lammen, 7-Sep-2018.) Remove dependency on ax-13 2403, inspired by an idea of BJ. (Revised by Wolf Lammen, 30-Nov-2019.) Remove dependency on ax-12 2215. (Revised by Wolf Lammen, 19-Mar-2021.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧 𝑡 = 𝑢)
Theorem	aev2 2093*	A version of aev 2092 with two universal quantifiers in the consequent. One can prove similar statements with arbitrary numbers of universal quantifiers in the consequent (the series begins with aeveq 2091, aev 2092, aev2 2093). Using aev 2092 and alrimiv 1960, 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 30941. This list cannot be extended to ¬ or ⊥ since the scheme ∀𝑥𝑥 = 𝑦 is consistent with ax-mp 5, ax-gen 1828, ax-1 6-- ax-13 2403 (as the one-element universe shows), so for instance (∀𝑥𝑥 = 𝑦 → ⊥), DV (𝑥, 𝑦) is not provable from these axioms alone (indeed, dtru 5416 uses non-logical axioms as well). (Contributed by BJ, 23-Mar-2021.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧∀𝑡 𝑢 = 𝑣)
Theorem	hbaev 2094*	All variables are effectively bound in an identical variable specifier. Version of hbae 2462 with a disjoint variable condition, requiring fewer axioms. Instance of aev2 2093. (Contributed by NM, 13-May-1993.) Reduce axiom usage. (Revised by Wolf Lammen, 22-Mar-2021.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧∀𝑥 𝑥 = 𝑦)
Theorem	naev 2095*	If some set variables can assume different values, then any two distinct set variables cannot always be the same. (Contributed by Wolf Lammen, 10-Aug-2019.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ¬ ∀𝑢 𝑢 = 𝑣)
Theorem	naev2 2096*	Generalization of hbnaev 2097. (Contributed by Wolf Lammen, 9-Apr-2021.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑧 ¬ ∀𝑡 𝑡 = 𝑢)
Theorem	hbnaev 2097*	Any variable is free in ¬ ∀𝑥𝑥 = 𝑦, if 𝑥 and 𝑦 are distinct. This condition is dropped in hbnae 2463, at the expense of more axiom dependencies. Instance of naev2 2096. (Contributed by NM, 13-May-1993.) (Revised by Wolf Lammen, 9-Apr-2021.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑧 ¬ ∀𝑥 𝑥 = 𝑦)
1.4.8  Define proper substitution
Theorem	sbjust 2098*	Justification theorem for df-sb 2100 proved from Tarski's FOL axiom schemes. (Contributed by BJ, 22-Jan-2023.)
⊢ (∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑)) ↔ ∀𝑧(𝑧 = 𝑡 → ∀𝑥(𝑥 = 𝑧 → 𝜑)))
Syntax	wsb 2099	Extend wff definition to include proper substitution. Read: "the wff that results when 𝑦 is properly substituted for 𝑥 in wff 𝜑". (Contributed by NM, 24-Jan-2006.)
wff [𝑦 / 𝑥]𝜑
Definition	df-sb 2100*	Define proper substitution. For our notation, we use [𝑡 / 𝑥]𝜑 to mean "the wff that results from the proper substitution of 𝑡 for 𝑥 in the wff 𝜑". That is, 𝑡 properly replaces 𝑥. For example, [𝑡 / 𝑥]𝑧 ∈ 𝑥 is the same as 𝑧 ∈ 𝑡 (when 𝑥 and 𝑧 are distinct), as shown in elsb2 2162. Our notation was introduced in Haskell B. Curry's Foundations of Mathematical Logic (1977), p. 316 and is frequently used in textbooks of lambda calculus and combinatory logic. This notation improves the common but ambiguous notation, "𝜑(𝑡) is the wff that results when 𝑡 is properly substituted for 𝑥 in 𝜑(𝑥)". For example, if the original 𝜑(𝑥) is 𝑥 = 𝑡, then 𝜑(𝑡) is 𝑡 = 𝑡, from which we obtain that 𝜑(𝑥) is 𝑥 = 𝑥. So what exactly does 𝜑(𝑥) mean? Curry's notation solves this problem. A very similar notation, namely (𝑦 ∣ 𝑥)𝜑, was introduced in Bourbaki's Set Theory (Chapter 1, Description of Formal Mathematic, 1953). In most books, proper substitution has a somewhat complicated recursive definition with multiple cases based on the occurrences of free and bound variables in the wff. Instead, we use a single formula that is exactly equivalent and gives us a direct definition. We later prove that our definition has the properties we expect of proper substitution (see Theorems sbequ 2120, sbcom2 2209 and sbid2v 2540). Note that our definition is valid even when 𝑥 and 𝑡 are replaced with the same variable, as sbid 2292 shows. We achieve this by applying twice Tarski's definition sb6 2122 which is valid for disjoint variables, and introducing a dummy variable 𝑦 which isolates 𝑥 from 𝑡, as in dfsb7 2314 with respect to sb5 2311. We can also achieve this by having 𝑥 free in the first conjunct and bound in the second, as the alternate definition dfsb1 2512 shows. Another version that mixes free and bound variables is dfsb3 2525. When 𝑥 and 𝑡 are distinct, we can express proper substitution with the simpler expressions of sb5 2311 and sb6 2122. Note that the occurrences of a given variable in the definiens are either all bound (𝑥, 𝑦) or all free (𝑡). Also note that the definiens uses only primitive symbols. This double level definition will make several proofs using it appear as doubled. Alternately, one could often first prove as a lemma the same theorem with a disjoint variable condition on the substitute and the substituted variables, and then prove the original theorem by applying this lemma twice in a row. The hypothesis asserts that the definition is independent of the particular choice of the dummy variable 𝑦. Without this hypothesis, sbjust 2098 would be derivable from propositional axioms alone: one could apply the definiens for [𝑡 / 𝑥]𝜑 twice, using different dummy variables 𝑦 and 𝑧, and then invoke bitr3i 280 to establish their equivalence. This would jeopardize the independence of axioms, as demonstrated in an analoguous situation involving df-ss 3919 to prove ax-8 2147 (see in-ax8 36846). Prefer dfsb 2101 unless you can prove the hypothesis from fewer axioms in special cases, see sbt 2103. (Contributed by NM, 10-May-1993.) Revised from the original definition dfsb1 2512. (Revised by BJ, 22-Dec-2020.) Add the justification hypothesis. (Revised by Wolf Lammen, 4-Feb-2026.)
⊢ (∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑)) ↔ ∀𝑧(𝑧 = 𝑡 → ∀𝑥(𝑥 = 𝑧 → 𝜑)))    ⇒   ⊢ ([𝑡 / 𝑥]𝜑 ↔ ∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))