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	19.8w 2001	Weak version of 19.8a 2219 and instance of 19.2d 2000. (Contributed by NM, 1-Aug-2017.) (Proof shortened by Wolf Lammen, 4-Dec-2017.)
⊢ (𝜑 → ∀𝑥𝜑)    ⇒   ⊢ (𝜑 → ∃𝑥𝜑)
Theorem	spnfw 2002	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 2003	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 2004*	Version of sp 2221 when 𝑥 does not occur in 𝜑. Converse of ax-5 1933. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 10-Apr-2017.) (Proof shortened by Wolf Lammen, 4-Dec-2017.) Shorten 19.3v 2005. (Revised by Wolf Lammen, 20-Oct-2023.)
⊢ (∀𝑥𝜑 → 𝜑)
Theorem	19.3v 2005*	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 2007. (Contributed by Anthony Hart, 13-Sep-2011.) Remove dependency on ax-7 2031. (Revised by Wolf Lammen, 4-Dec-2017.) (Proof shortened by Wolf Lammen, 20-Oct-2023.)
⊢ (∀𝑥𝜑 ↔ 𝜑)
Theorem	19.8v 2006*	Version of 19.8a 2219 with a disjoint variable condition, requiring fewer axioms. Converse of ax5e 1935. (Contributed by BJ, 12-Mar-2020.)
⊢ (𝜑 → ∃𝑥𝜑)
Theorem	19.9v 2007*	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 2005. (Contributed by NM, 28-May-1995.) Remove dependency on ax-7 2031. (Revised by Wolf Lammen, 4-Dec-2017.)
⊢ (∃𝑥𝜑 ↔ 𝜑)
Theorem	spimevw 2008*	Existential introduction, using implicit substitution. This is to spimew 1994 what spimvw 2009 is to spimw 1993. Version of spimev 2426 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 2009*	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 2424 and spimfv 2277. (Contributed by NM, 9-Apr-2017.)
⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))    ⇒   ⊢ (∀𝑥𝜑 → 𝜓)
Theorem	spsv 2010*	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 2011*	Specialization, using implicit substitution. Version of spv 2427 with a disjoint variable condition, which does not require ax-7 2031, ax-12 2215, ax-13 2406. (Contributed by NM, 30-Aug-1993.) (Revised by BJ, 31-May-2019.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥𝜑 → 𝜓)
Theorem	chvarvv 2012*	Implicit substitution of 𝑦 for 𝑥 into a theorem. Version of chvarv 2430 with a disjoint variable condition, which does not require ax-13 2406. (Contributed by NM, 20-Apr-1994.) (Revised by BJ, 31-May-2019.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ 𝜓
Theorem	19.39 2013	Theorem 19.39 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.)
⊢ ((∃𝑥𝜑 → ∃𝑥𝜓) → ∃𝑥(𝜑 → 𝜓))
Theorem	19.24 2014	Theorem 19.24 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.)
⊢ ((∀𝑥𝜑 → ∀𝑥𝜓) → ∃𝑥(𝜑 → 𝜓))
Theorem	19.34 2015	Theorem 19.34 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.)
⊢ ((∀𝑥𝜑 ∨ ∃𝑥𝜓) → ∃𝑥(𝜑 ∨ 𝜓))
Theorem	19.36v 2016*	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 2017*	Version of 19.12vv 2381 with a disjoint variable condition, requiring fewer axioms. See also 19.12 2362. (Contributed by BJ, 18-Mar-2020.)
⊢ (∃𝑥∀𝑦(𝜑 → 𝜓) ↔ ∀𝑦∃𝑥(𝜑 → 𝜓))
Theorem	19.27v 2018*	Version of 19.27 2265 with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 3-Jun-2004.)
⊢ (∀𝑥(𝜑 ∧ 𝜓) ↔ (∀𝑥𝜑 ∧ 𝜓))
Theorem	19.28v 2019*	Version of 19.28 2266 with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 25-Mar-2004.)
⊢ (∀𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∀𝑥𝜓))
Theorem	19.37v 2020*	Version of 19.37 2270 with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 21-Jun-1993.)
⊢ (∃𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∃𝑥𝜓))
Theorem	19.44v 2021*	Version of 19.44 2275 with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 12-Mar-1993.)
⊢ (∃𝑥(𝜑 ∨ 𝜓) ↔ (∃𝑥𝜑 ∨ 𝜓))
Theorem	19.45v 2022*	Version of 19.45 2276 with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 12-Mar-1993.)
⊢ (∃𝑥(𝜑 ∨ 𝜓) ↔ (𝜑 ∨ ∃𝑥𝜓))
Theorem	equs4v 2023*	Version of equs4 2450 with a disjoint variable condition, which requires fewer axioms. (Contributed by NM, 10-May-1993.) (Revised by BJ, 31-May-2019.)
⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))
Theorem	alequexv 2024*	Version of equs4v 2023 with its consequence simplified by exsimpr 1892. (Contributed by BJ, 9-Nov-2021.)
⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → ∃𝑥𝜑)
Theorem	exsbim 2025*	One direction of the equivalence in exsb 2393 is based on fewer axioms. (Contributed by Wolf Lammen, 2-Mar-2023.)
⊢ (∃𝑦∀𝑥(𝑥 = 𝑦 → 𝜑) → ∃𝑥𝜑)
Theorem	equsv 2026*	If a formula does not contain a variable 𝑥, then it is equivalent to the corresponding prototype of substitution with a fresh variable (see sb6 2121). (Contributed by BJ, 23-Jul-2023.)
⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜑)
Theorem	equsalvw 2027*	Version of equsalv 2305 with a disjoint variable condition, and of equsal 2451 with two disjoint variable conditions, which requires fewer axioms. See also the dual form equsexvw 2028. (Contributed by BJ, 31-May-2019.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜓)
Theorem	equsexvw 2028*	Version of equsexv 2306 with a disjoint variable condition, and of equsex 2452 with two disjoint variable conditions, which requires fewer axioms. See also the dual form equsalvw 2027. (Contributed by BJ, 31-May-2019.) (Proof shortened by Wolf Lammen, 23-Oct-2023.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ 𝜓)
Theorem	cbvaliw 2029*	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 2030*	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 2031	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 2044). 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 2039 that this axiom can be recovered from its weakened version ax7v 2032 where 𝑥 and 𝑦 are assumed to be disjoint variables. In particular, the only theorem referencing ax-7 2031 should be ax7v 2032. See the comment of ax7v 2032 for more details on these matters. (Contributed by NM, 10-Jan-1993.) (Revised by BJ, 7-Dec-2020.) Use ax7 2039 instead. (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧))
Theorem	ax7v 2032*	Weakened version of ax-7 2031, with a disjoint variable condition on 𝑥, 𝑦. This should be the only proof referencing ax-7 2031, and it should be referenced only by its two weakened versions ax7v1 2033 and ax7v2 2034, from which ax-7 2031 is then rederived as ax7 2039, which shows that either ax7v 2032 or the conjunction of ax7v1 2033 and ax7v2 2034 is sufficient. In ax7v 2032, it is still allowed to substitute the same variable for 𝑥 and 𝑧, or the same variable for 𝑦 and 𝑧. Therefore, ax7v 2032 "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 2037 and equid 2035 respectively. (Contributed by BJ, 7-Dec-2020.) Use ax7 2039 instead. (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧))
Theorem	ax7v1 2033*	First of two weakened versions of ax7v 2032, with an extra disjoint variable condition on 𝑥, 𝑧, see comments there. (Contributed by BJ, 7-Dec-2020.)
⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧))
Theorem	ax7v2 2034*	Second of two weakened versions of ax7v 2032, with an extra disjoint variable condition on 𝑦, 𝑧, see comments there. (Contributed by BJ, 7-Dec-2020.)
⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧))
Theorem	equid 2035	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 2036	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 2037*	Weaker form of equcomi 2040 with a disjoint variable condition on 𝑥, 𝑦. This is an intermediate step and equcomi 2040 is fully recovered later. (Contributed by BJ, 7-Dec-2020.)
⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥)
Theorem	ax6evr 2038*	A commuted form of ax6ev 1992. (Contributed by BJ, 7-Dec-2020.)
⊢ ∃𝑥 𝑦 = 𝑥
Theorem	ax7 2039	Proof of ax-7 2031 from ax7v1 2033 and ax7v2 2034 (and earlier axioms), proving sufficiency of the conjunction of the latter two weakened versions of ax7v 2032, which is itself a weakened version of ax-7 2031. Note that the weakened version of ax-7 2031 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 2040	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 2041	Commutative law for equality. Equality is a symmetric relation. (Contributed by NM, 20-Aug-1993.)
⊢ (𝑥 = 𝑦 ↔ 𝑦 = 𝑥)
Theorem	equcomd 2042	Deduction form of equcom 2041, symmetry of equality. For the versions for classes, see eqcom 2772 and eqcomd 2771. (Contributed by BJ, 6-Oct-2019.)
⊢ (𝜑 → 𝑥 = 𝑦)    ⇒   ⊢ (𝜑 → 𝑦 = 𝑥)
Theorem	equcoms 2043	An inference commuting equality in antecedent. Used to eliminate the need for a syllogism. (Contributed by NM, 10-Jan-1993.)
⊢ (𝑥 = 𝑦 → 𝜑)    ⇒   ⊢ (𝑦 = 𝑥 → 𝜑)
Theorem	equtr 2044	A transitive law for equality. (Contributed by NM, 23-Aug-1993.)
⊢ (𝑥 = 𝑦 → (𝑦 = 𝑧 → 𝑥 = 𝑧))
Theorem	equtrr 2045	A transitive law for equality. Lemma L17 in [Megill] p. 446 (p. 14 of the preprint). (Contributed by NM, 23-Aug-1993.)
⊢ (𝑥 = 𝑦 → (𝑧 = 𝑥 → 𝑧 = 𝑦))
Theorem	equeuclr 2046	Commuted version of equeucl 2047 (equality is left-Euclidean). (Contributed by BJ, 12-Apr-2021.)
⊢ (𝑥 = 𝑧 → (𝑦 = 𝑧 → 𝑦 = 𝑥))
Theorem	equeucl 2047	Equality is a left-Euclidean binary relation. (Right-Euclideanness is stated in ax-7 2031.) Curried (exported) form of equtr2 2050. (Contributed by BJ, 11-Apr-2021.)
⊢ (𝑥 = 𝑧 → (𝑦 = 𝑧 → 𝑥 = 𝑦))
Theorem	equequ1 2048	An equivalence law for equality. (Contributed by NM, 1-Aug-1993.) (Proof shortened by Wolf Lammen, 10-Dec-2017.)
⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 ↔ 𝑦 = 𝑧))
Theorem	equequ2 2049	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 2050	Equality is a left-Euclidean binary relation. Uncurried (imported) form of equeucl 2047. (Contributed by NM, 12-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by BJ, 11-Apr-2021.)
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑧) → 𝑥 = 𝑦)
Theorem	stdpc6 2051	One of the two equality axioms of standard predicate calculus, called reflexivity of equality. (The other one is stdpc7 2288.) 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 2052*	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 2406. (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 2053*	A modified version of the forward implication of equvinv 2052 adapted to common usage. (Contributed by Wolf Lammen, 8-Sep-2018.)
⊢ (𝑥 = 𝑦 → ∃𝑧(𝑥 = 𝑧 ∧ 𝑦 = 𝑧))
Theorem	equvelv 2054*	A biconditional form of equvel 2490 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 2055	An equivalence between two ways of expressing ax-13 2406. See the comment for ax-13 2406. (Contributed by NM, 2-May-2017.) (Proof shortened by Wolf Lammen, 26-Feb-2018.) (Revised by BJ, 15-Sep-2020.)
⊢ ((¬ 𝑥 = 𝑦 → (𝑦 = 𝑧 → 𝜑)) ↔ (¬ 𝑥 = 𝑦 → (¬ 𝑥 = 𝑧 → (𝑦 = 𝑧 → 𝜑))))
Theorem	spfw 2056*	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 2057*	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 2056 (minimal distinct variable requirements), spnfw 2002 (when 𝑥 is not free in ¬ 𝜑), spvw 2004 (when 𝑥 does not appear in 𝜑), sptruw 1829 (when 𝜑 is true), spfalw 2003 (when 𝜑 is false), and spvv 2011 (where 𝜑 is changed into 𝜓). (Contributed by NM, 9-Apr-2017.) (Proof shortened by Wolf Lammen, 27-Feb-2018.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥𝜑 → 𝜑)
Theorem	cbvalw 2058*	Change bound variable. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 9-Apr-2017.)
⊢ (∀𝑥𝜑 → ∀𝑦∀𝑥𝜑)    &   ⊢ (¬ 𝜓 → ∀𝑥 ¬ 𝜓)    &   ⊢ (∀𝑦𝜓 → ∀𝑥∀𝑦𝜓)    &   ⊢ (¬ 𝜑 → ∀𝑦 ¬ 𝜑)    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓)
Theorem	cbvalvw 2059*	Change bound variable. Uses only Tarski's FOL axiom schemes. See cbvalv 2434 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 2060*	Change bound variable. Uses only Tarski's FOL axiom schemes. See cbvexv 2435 for a version with fewer disjoint variable conditions but requiring more axioms. (Contributed by NM, 19-Apr-2017.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓)
Theorem	cbvaldvaw 2061*	Rule used to change the bound variable in a universal quantifier with implicit substitution. Deduction form. Version of cbvaldva 2443 with a disjoint variable condition, requiring fewer axioms. (Contributed by David Moews, 1-May-2017.) Avoid ax-13 2406. (Revised by GG, 10-Jan-2024.) Reduce axiom usage, along an idea of GG. (Revised by Wolf Lammen, 10-Feb-2024.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒))
Theorem	cbvexdvaw 2062*	Rule used to change the bound variable in an existential quantifier with implicit substitution. Deduction form. Version of cbvexdva 2444 with a disjoint variable condition, requiring fewer axioms. (Contributed by David Moews, 1-May-2017.) Avoid ax-13 2406. (Revised by GG, 10-Jan-2024.) Reduce axiom usage. (Revised by Wolf Lammen, 10-Feb-2024.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑦𝜒))
Theorem	cbval2vw 2063*	Rule used to change bound variables, using implicit substitution. Version of cbval2vv 2447 with more disjoint variable conditions, which requires fewer axioms . (Contributed by NM, 4-Feb-2005.) Avoid ax-13 2406. (Revised by GG, 10-Jan-2024.)
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑧∀𝑤𝜓)
Theorem	cbvex2vw 2064*	Rule used to change bound variables, using implicit substitution. Version of cbvex2vv 2448 with more disjoint variable conditions, which requires fewer axioms . (Contributed by NM, 26-Jul-1995.) Avoid ax-13 2406. (Revised by GG, 10-Jan-2024.)
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑧∃𝑤𝜓)
Theorem	cbvex4vw 2065*	Rule used to change bound variables, using implicit substitution. Version of cbvex4v 2449 with more disjoint variable conditions, which requires fewer axioms. (Contributed by NM, 26-Jul-1995.) Avoid ax-13 2406. (Revised by GG, 10-Jan-2024.)
⊢ ((𝑥 = 𝑣 ∧ 𝑦 = 𝑢) → (𝜑 ↔ 𝜓))    &   ⊢ ((𝑧 = 𝑓 ∧ 𝑤 = 𝑔) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (∃𝑥∃𝑦∃𝑧∃𝑤𝜑 ↔ ∃𝑣∃𝑢∃𝑓∃𝑔𝜒)
Theorem	alcomimw 2066*	Weak version of ax-11 2194. See alcomw 2068 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 2067*	Weak version of excomim 2200. Uses only Tarski's FOL axiom schemes. (Contributed by BTernaryTau, 23-Jun-2025.)
⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥∃𝑦𝜑 → ∃𝑦∃𝑥𝜑)
Theorem	alcomw 2068*	Weak version of alcom 2196 and biconditional form of alcomimw 2066. Uses only Tarski's FOL axiom schemes. (Contributed by BTernaryTau, 28-Dec-2024.)
⊢ (𝑥 = 𝑤 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜒))    ⇒   ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑦∀𝑥𝜑)
Theorem	excomw 2069*	Weak version of excom 2199 and biconditional form of excomimw 2067. Uses only Tarski's FOL axiom schemes. (Contributed by TM, 24-Jan-2026.)
⊢ (𝑥 = 𝑤 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜒))    ⇒   ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑦∃𝑥𝜑)
Theorem	hbn1fw 2070*	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 2071*	Weak version of hbn1 2179. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 9-Apr-2017.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (¬ ∀𝑥𝜑 → ∀𝑥 ¬ ∀𝑥𝜑)
Theorem	hba1w 2072*	Weak version of hba1 2330. 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 2073*	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 2074*	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 2075*	If a formula is true, then it is true for at least one instance. This is to 19.8a 2219 what spw 2057 is to sp 2221. (Contributed by SN, 26-Sep-2024.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝜑 → ∃𝑥𝜑)
Theorem	exexw 2076*	Existential quantification over a given variable is idempotent. Weak version of bj-exexbiex 37187, requiring fewer axioms. (Contributed by GG, 4-Nov-2024.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥𝜑 ↔ ∃𝑥∃𝑥𝜑)
Theorem	spaev 2077*	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 2081. 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 2078*	Change bound variable in an equality with a disjoint variable condition. Instance of aev 2082. (Contributed by NM, 22-Jul-2015.) (Revised by BJ, 18-Jun-2019.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧 𝑧 = 𝑦)
Theorem	aevlem0 2079*	Lemma for aevlem 2080. Instance of aev 2082. (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 2460 and add DV condition to reduce axiom usage. (Revised by BJ, 29-Mar-2021.) (Proof shortened by Wolf Lammen, 30-Mar-2021.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧 𝑧 = 𝑥)
Theorem	aevlem 2080*	Lemma for aev 2082 and axc16g 2298. Change free and bound variables. Instance of aev 2082. (Contributed by NM, 22-Jul-2015.) (Proof shortened by Wolf Lammen, 17-Feb-2018.) Remove dependency on ax-13 2406, along an idea of BJ. (Revised by Wolf Lammen, 30-Nov-2019.) Reduce axiom usage. (Revised by BJ, 29-Mar-2021.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧 𝑧 = 𝑡)
Theorem	aeveq 2081*	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 2082*	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 2406, 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 2083*	A version of aev 2082 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 2081, aev 2082, aev2 2083). Using aev 2082 and alrimiv 1950, 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 30720. This list cannot be extended to ¬ or ⊥ since the scheme ∀𝑥𝑥 = 𝑦 is consistent with ax-mp 5, ax-gen 1818, ax-1 6-- ax-13 2406 (as the one-element universe shows), so for instance (∀𝑥𝑥 = 𝑦 → ⊥), DV (𝑥, 𝑦) is not provable from these axioms alone (indeed, dtru 5409 uses non-logical axioms as well). (Contributed by BJ, 23-Mar-2021.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧∀𝑡 𝑢 = 𝑣)
Theorem	hbaev 2084*	All variables are effectively bound in an identical variable specifier. Version of hbae 2465 with a disjoint variable condition, requiring fewer axioms. Instance of aev2 2083. (Contributed by NM, 13-May-1993.) Reduce axiom usage. (Revised by Wolf Lammen, 22-Mar-2021.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧∀𝑥 𝑥 = 𝑦)
Theorem	naev 2085*	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 2086*	Generalization of hbnaev 2087. (Contributed by Wolf Lammen, 9-Apr-2021.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑧 ¬ ∀𝑡 𝑡 = 𝑢)
Theorem	hbnaev 2087*	Any variable is free in ¬ ∀𝑥𝑥 = 𝑦, if 𝑥 and 𝑦 are distinct. This condition is dropped in hbnae 2466, at the expense of more axiom dependencies. Instance of naev2 2086. (Contributed by NM, 13-May-1993.) (Revised by Wolf Lammen, 9-Apr-2021.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑧 ¬ ∀𝑥 𝑥 = 𝑦)
1.4.8  Define proper substitution
Theorem	justify-df 2088	Metamath handles substitution uniformly. Any expression may replace a variable provided that their types are compatible and that no substituting expression contains a set variable prohibited by a distinct variable condition. The axioms are formulated so that every such substitution is valid when the side conditions are satisfied. Consequently, every theorem derived from the axioms inherits the same substitution property. This agrees with standard mathematical practice, where substitution is unrestricted apart from type and freshness requirements. Definitions introduce abbreviations for expressions represented by their definiens, usually the right-hand side of a defining biconditional. When a definition contains dummy variables, however, the definiens is not uniquely determined by the definiendum, since the names of fresh bound variables do not appear in the definiendum. Definitions of this kind are meaningful only if the particular names chosen for dummy variables are irrelevant. In ordinary logic and mathematics, renaming fresh bound variables (alpha-renaming) is regarded as insignificant. Metamath's substitution mechanism reflects this principle, and therefore definitions must also respect it. Early versions of this database relied on this convention implicitly. Beginning in 2023, definitions involving dummy variables were accompanied by justification theorems (for example, rename-sb 2092) showing that alpha-renaming the definiens yields an equivalent expression. Consequently, different choices of dummy variable names cannot produce equivalences that are not already derivable within the formal system. Metamath records not only proofs but also the list of axioms on which they depend. Since definitions are intended merely as abbreviations, their use should not affect these dependency lists. Unfortunately, the simple form of definition used before 2026 did not preserve this invariance. Two instances of a definition differing only in the names of dummy variables could be used to reprove the corresponding justification theorem with unusually low axiom usage, unattainable by proofs using axioms alone. Thus the recorded dependencies could depend on whether the definition was used or expanded away. Beginning in February 2026, definitions involving dummy variables were therefore modified to incorporate alpha-renaming explicitly. In the intermediate scheme, the corresponding justification theorem was added as a hypothesis of the definition, ensuring that every use of the definition inherited the axioms needed to establish the renaming property. This eliminated artificial reductions in dependency lists. Using the alpha-renaming property as an external hypothesis is, however, not ideal. A better approach is to encode the property directly in the definiens itself. This preserves the invariance of axiom dependencies while allowing reductions that are impossible with the hypothesis-based form. Formal justifications for this improved definition scheme are given in just1-df 2089, just2-df 2090, and just3-df 2091. An implementation is provided by definition df-sb 2094 and the theorems that follow, where the underlying techniques may be studied in greater detail. (Contributed by Wolf Lammen, 12-Jun-2026.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    ⇒   ⊢ 𝜑
Theorem	just1-df 2089	First justification theorem for definitions whose definiens is a conjunction, as in df-sb 2094. Here 𝜑 denotes the definiendum, while 𝜓 and 𝜒 represent the two components of the definiens. The theorem shows that the definiendum implies either component separately. (Contributed by Wolf Lammen, 6-Jun-2026.) (New usage is discouraged.)
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	just2-df 2090	Second justification theorem for definitions whose definiens is a conjunction, as in df-sb 2094. If 𝜑 is equivalent to (𝜓 ∧ 𝜒), then it implies (𝜓 ↔ 𝜒). In the case of df-sb 2094, this expresses the invariance of the definition under alpha-renaming of the bound variable. (Contributed by Wolf Lammen, 6-Jun-2026.)
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))    ⇒   ⊢ (𝜑 → (𝜓 ↔ 𝜒))
Theorem	just3-df 2091	Third justification theorem for definitions whose definiens is a conjunction, as in df-sb 2094. In addition to the defining equivalence, the second hypothesis requires the conjuncts of the definiens to be equivalent. When the conjuncts are quantified and differ only by a bound-variable renaming, this equivalence is usually obtained from an implicit substitution between the underlying expressions. In some cases, however, it can be proved more directly and with fewer axioms. Under these assumptions, either conjunct implies the definiendum. Together with just1-df 2089, the definiendum is therefore equivalent to either conjunct. (Contributed by Wolf Lammen, 6-Jun-2026.)
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))    &   ⊢ (𝜓 ↔ 𝜒)    ⇒   ⊢ (𝜓 → 𝜑)
Theorem	rename-sb 2092*	The equivalence needed for df-sb 2094 in just3-df 2091. It is proved from Tarski's FOL axiom schemes. (Contributed by BJ, 22-Jan-2023.)
⊢ (∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑)) ↔ ∀𝑧(𝑧 = 𝑡 → ∀𝑥(𝑥 = 𝑧 → 𝜑)))
Syntax	wsb 2093	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 2094*	Define proper substitution. We write [𝑡 / 𝑥]𝜑 for "the wff obtained by properly substituting 𝑡 for 𝑥 in the wff 𝜑". Thus, 𝑡 properly replaces 𝑥. For example, [𝑡 / 𝑥]𝑧 ∈ 𝑥 is 𝑧 ∈ 𝑡 (when 𝑥 and 𝑧 are distinct), as shown in elsb2 2162. In practice, the definiens reduces to "∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑)) " (see just3-df 2091). Here it is followed by the same expression with a fresh dummy variable 𝑧, making explicit the independence of the dummy variable's name (see just2-df 2090). This is a necessity of Metamath supporting axiom dependency lists. See justify-df 2088 for more information about this technique. The added conjunct will make some proofs appear duplicated. Alternately, one may first prove as a lemma the same theorem under a disjoint variable condition on the substituted and the substituting variables, then obtain the original theorem by applying that lemma twice. Our notation, without the alpha-renamed repetition, 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 obtained by properly substituting 𝑡 for 𝑥 in 𝜑(𝑥)". For example, if the original 𝜑(𝑥) is 𝑥 = 𝑡, then 𝜑(𝑡) is 𝑡 = 𝑡, from which we obtain that 𝜑(𝑥) is 𝑥 = 𝑥. So what exactly does 𝜑(𝑥) mean? Curry's notation avoids this problem. A closely related notation, (𝑦 ∣ 𝑥)𝜑, was introduced in Bourbaki's Set Theory (Chapter 1, Description of Formal Mathematic, 1953). Most textbooks define proper substitution recursively by considering various cases involving free and bound variables. Instead, we use a single formula that is exactly equivalent and serves as a direct definition. We later prove that this definition has the expected properties of proper substitution; see sbequ 2119, sbcom2 2209, and sbid2v 2543. This definition remains valid when 𝑥 and 𝑡 are replaced with the same variable, as shown by sbid 2293. This is achieved by applying Tarski's definition sb6 2121 twice, which is valid for disjoint variables, and introducing a dummy variable 𝑦 that isolates 𝑥 from 𝑡, as in dfsb7 2316 relative to sb5 2313. We can also achieve this by having 𝑥 free in the first conjunct and bound in the second, as the alternate definition dfsb1 2515 shows. Another version that mixes free and bound variables is dfsb3 2528. When 𝑥 and 𝑡 are distinct, proper substitution can be expressed more simply using sb5 2313 and sb6 2121. Note that each variable in the definiens is either entirely bound (𝑥, 𝑦) or entirely free (𝑡). The definiens also uses only primitive symbols. Prefer the more general form dfsb 2096 when axiom usage is unimportant. It provides a simpler right hand side together with a proof of its alpha-renaming. (Contributed by NM, 10-May-1993.) Revised from the original definition dfsb1 2515. (Revised by BJ, 22-Dec-2020.) Support alpha-renaming. (Revised by Wolf Lammen, 4-Jun-2026.)
⊢ ([𝑡 / 𝑥]𝜑 ↔ (∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑)) ∧ ∀𝑧(𝑧 = 𝑡 → ∀𝑥(𝑥 = 𝑧 → 𝜑))))
Theorem	dfsbimp 2095*	A simple consequence of df-sb 2094. (Contributed by Wolf Lammen, 4-Jun-2026.)
⊢ ([𝑡 / 𝑥]𝜑 → ∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
Theorem	dfsb 2096*	Simplify definition df-sb 2094 by proving the renaming independency. (Contributed by Wolf Lammen, 5-Feb-2026.) df-sb 2094 changed. (Revised by Wolf Lammen, 4-Jun-2026.)
⊢ ([𝑡 / 𝑥]𝜑 ↔ ∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
Theorem	sbtlem 2097	In the case of sbt 2098, rename-sb 2092 is derivable from propositional axioms and ax-gen 1818 alone. The essential proof step is presented in this lemma. (Contributed by Wolf Lammen, 4-Feb-2026.)
⊢ 𝜑    ⇒   ⊢ ∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑))
Theorem	sbt 2098	A substitution into a theorem yields a theorem. See sbtALT 2103 for a shorter proof requiring more axioms. See chvar 2429 and chvarv 2430 for versions using implicit substitution. (Contributed by NM, 21-Jan-2004.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 20-Jul-2018.) Revise df-sb 2094. (Revised by Steven Nguyen, 6-Jul-2023.) Revise df-sb 2094 again. (Revised by Wolf Lammen, 4-Jun-2026.)
⊢ 𝜑    ⇒   ⊢ [𝑡 / 𝑥]𝜑
Theorem	sbtru 2099	The result of substituting in the truth constant "true" is true. (Contributed by BJ, 2-Sep-2023.)
⊢ [𝑦 / 𝑥]⊤
Theorem	stdpc4lem 2100*	In the case of stdpc4 2101, rename-sb 2092 is derivable from fewer axioms than dfsb 2096. The essential proof step is presented in this lemma. Based on a proof of BJ, 22-Dec-2020. (Contributed by Wolf Lammen, 4-Jun-2026.)
⊢ (∀𝑥𝜑 → ∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))