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	spsv 2001*	Generalization of antecedent. A trivial weak version of sps 2214 avoiding ax-12 2206. (Contributed by SN, 13-Nov-2025.) (Proof shortened by WL, 19-Nov-2025.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (∀𝑥𝜑 → 𝜓)
Theorem	spvv 2002*	Specialization, using implicit substitution. Version of spv 2418 with a disjoint variable condition, which does not require ax-7 2022, ax-12 2206, ax-13 2397. (Contributed by NM, 30-Aug-1993.) (Revised by BJ, 31-May-2019.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥𝜑 → 𝜓)
Theorem	chvarvv 2003*	Implicit substitution of 𝑦 for 𝑥 into a theorem. Version of chvarv 2421 with a disjoint variable condition, which does not require ax-13 2397. (Contributed by NM, 20-Apr-1994.) (Revised by BJ, 31-May-2019.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ 𝜓
Theorem	19.39 2004	Theorem 19.39 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.)
⊢ ((∃𝑥𝜑 → ∃𝑥𝜓) → ∃𝑥(𝜑 → 𝜓))
Theorem	19.24 2005	Theorem 19.24 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.)
⊢ ((∀𝑥𝜑 → ∀𝑥𝜓) → ∃𝑥(𝜑 → 𝜓))
Theorem	19.34 2006	Theorem 19.34 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.)
⊢ ((∀𝑥𝜑 ∨ ∃𝑥𝜓) → ∃𝑥(𝜑 ∨ 𝜓))
Theorem	19.36v 2007*	Version of 19.36 2259 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 2008*	Version of 19.12vv 2372 with a disjoint variable condition, requiring fewer axioms. See also 19.12 2353. (Contributed by BJ, 18-Mar-2020.)
⊢ (∃𝑥∀𝑦(𝜑 → 𝜓) ↔ ∀𝑦∃𝑥(𝜑 → 𝜓))
Theorem	19.27v 2009*	Version of 19.27 2256 with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 3-Jun-2004.)
⊢ (∀𝑥(𝜑 ∧ 𝜓) ↔ (∀𝑥𝜑 ∧ 𝜓))
Theorem	19.28v 2010*	Version of 19.28 2257 with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 25-Mar-2004.)
⊢ (∀𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∀𝑥𝜓))
Theorem	19.37v 2011*	Version of 19.37 2261 with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 21-Jun-1993.)
⊢ (∃𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∃𝑥𝜓))
Theorem	19.44v 2012*	Version of 19.44 2266 with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 12-Mar-1993.)
⊢ (∃𝑥(𝜑 ∨ 𝜓) ↔ (∃𝑥𝜑 ∨ 𝜓))
Theorem	19.45v 2013*	Version of 19.45 2267 with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 12-Mar-1993.)
⊢ (∃𝑥(𝜑 ∨ 𝜓) ↔ (𝜑 ∨ ∃𝑥𝜓))
Theorem	equs4v 2014*	Version of equs4 2441 with a disjoint variable condition, which requires fewer axioms. (Contributed by NM, 10-May-1993.) (Revised by BJ, 31-May-2019.)
⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))
Theorem	alequexv 2015*	Version of equs4v 2014 with its consequence simplified by exsimpr 1883. (Contributed by BJ, 9-Nov-2021.)
⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → ∃𝑥𝜑)
Theorem	exsbim 2016*	One direction of the equivalence in exsb 2384 is based on fewer axioms. (Contributed by Wolf Lammen, 2-Mar-2023.)
⊢ (∃𝑦∀𝑥(𝑥 = 𝑦 → 𝜑) → ∃𝑥𝜑)
Theorem	equsv 2017*	If a formula does not contain a variable 𝑥, then it is equivalent to the corresponding prototype of substitution with a fresh variable (see sb6 2112). (Contributed by BJ, 23-Jul-2023.)
⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜑)
Theorem	equsalvw 2018*	Version of equsalv 2296 with a disjoint variable condition, and of equsal 2442 with two disjoint variable conditions, which requires fewer axioms. See also the dual form equsexvw 2019. (Contributed by BJ, 31-May-2019.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜓)
Theorem	equsexvw 2019*	Version of equsexv 2297 with a disjoint variable condition, and of equsex 2443 with two disjoint variable conditions, which requires fewer axioms. See also the dual form equsalvw 2018. (Contributed by BJ, 31-May-2019.) (Proof shortened by Wolf Lammen, 23-Oct-2023.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ 𝜓)
Theorem	cbvaliw 2020*	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 2021*	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 2022	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 2035). 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 2030 that this axiom can be recovered from its weakened version ax7v 2023 where 𝑥 and 𝑦 are assumed to be disjoint variables. In particular, the only theorem referencing ax-7 2022 should be ax7v 2023. See the comment of ax7v 2023 for more details on these matters. (Contributed by NM, 10-Jan-1993.) (Revised by BJ, 7-Dec-2020.) Use ax7 2030 instead. (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧))
Theorem	ax7v 2023*	Weakened version of ax-7 2022, with a disjoint variable condition on 𝑥, 𝑦. This should be the only proof referencing ax-7 2022, and it should be referenced only by its two weakened versions ax7v1 2024 and ax7v2 2025, from which ax-7 2022 is then rederived as ax7 2030, which shows that either ax7v 2023 or the conjunction of ax7v1 2024 and ax7v2 2025 is sufficient. In ax7v 2023, it is still allowed to substitute the same variable for 𝑥 and 𝑧, or the same variable for 𝑦 and 𝑧. Therefore, ax7v 2023 "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 2028 and equid 2026 respectively. (Contributed by BJ, 7-Dec-2020.) Use ax7 2030 instead. (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧))
Theorem	ax7v1 2024*	First of two weakened versions of ax7v 2023, with an extra disjoint variable condition on 𝑥, 𝑧, see comments there. (Contributed by BJ, 7-Dec-2020.)
⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧))
Theorem	ax7v2 2025*	Second of two weakened versions of ax7v 2023, with an extra disjoint variable condition on 𝑦, 𝑧, see comments there. (Contributed by BJ, 7-Dec-2020.)
⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧))
Theorem	equid 2026	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 2027	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 2028*	Weaker form of equcomi 2031 with a disjoint variable condition on 𝑥, 𝑦. This is an intermediate step and equcomi 2031 is fully recovered later. (Contributed by BJ, 7-Dec-2020.)
⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥)
Theorem	ax6evr 2029*	A commuted form of ax6ev 1983. (Contributed by BJ, 7-Dec-2020.)
⊢ ∃𝑥 𝑦 = 𝑥
Theorem	ax7 2030	Proof of ax-7 2022 from ax7v1 2024 and ax7v2 2025 (and earlier axioms), proving sufficiency of the conjunction of the latter two weakened versions of ax7v 2023, which is itself a weakened version of ax-7 2022. Note that the weakened version of ax-7 2022 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 2031	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 2032	Commutative law for equality. Equality is a symmetric relation. (Contributed by NM, 20-Aug-1993.)
⊢ (𝑥 = 𝑦 ↔ 𝑦 = 𝑥)
Theorem	equcomd 2033	Deduction form of equcom 2032, symmetry of equality. For the versions for classes, see eqcom 2763 and eqcomd 2762. (Contributed by BJ, 6-Oct-2019.)
⊢ (𝜑 → 𝑥 = 𝑦)    ⇒   ⊢ (𝜑 → 𝑦 = 𝑥)
Theorem	equcoms 2034	An inference commuting equality in antecedent. Used to eliminate the need for a syllogism. (Contributed by NM, 10-Jan-1993.)
⊢ (𝑥 = 𝑦 → 𝜑)    ⇒   ⊢ (𝑦 = 𝑥 → 𝜑)
Theorem	equtr 2035	A transitive law for equality. (Contributed by NM, 23-Aug-1993.)
⊢ (𝑥 = 𝑦 → (𝑦 = 𝑧 → 𝑥 = 𝑧))
Theorem	equtrr 2036	A transitive law for equality. Lemma L17 in [Megill] p. 446 (p. 14 of the preprint). (Contributed by NM, 23-Aug-1993.)
⊢ (𝑥 = 𝑦 → (𝑧 = 𝑥 → 𝑧 = 𝑦))
Theorem	equeuclr 2037	Commuted version of equeucl 2038 (equality is left-Euclidean). (Contributed by BJ, 12-Apr-2021.)
⊢ (𝑥 = 𝑧 → (𝑦 = 𝑧 → 𝑦 = 𝑥))
Theorem	equeucl 2038	Equality is a left-Euclidean binary relation. (Right-Euclideanness is stated in ax-7 2022.) Curried (exported) form of equtr2 2041. (Contributed by BJ, 11-Apr-2021.)
⊢ (𝑥 = 𝑧 → (𝑦 = 𝑧 → 𝑥 = 𝑦))
Theorem	equequ1 2039	An equivalence law for equality. (Contributed by NM, 1-Aug-1993.) (Proof shortened by Wolf Lammen, 10-Dec-2017.)
⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 ↔ 𝑦 = 𝑧))
Theorem	equequ2 2040	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 2041	Equality is a left-Euclidean binary relation. Uncurried (imported) form of equeucl 2038. (Contributed by NM, 12-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by BJ, 11-Apr-2021.)
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑧) → 𝑥 = 𝑦)
Theorem	stdpc6 2042	One of the two equality axioms of standard predicate calculus, called reflexivity of equality. (The other one is stdpc7 2279.) 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 2043*	A variable introduction law for equality. Lemma 15 of [Monk2] p. 109. (Contributed by NM, 9-Jan-1993.) Remove dependencies on ax-10 2169, ax-13 2397. (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 2044*	A modified version of the forward implication of equvinv 2043 adapted to common usage. (Contributed by Wolf Lammen, 8-Sep-2018.)
⊢ (𝑥 = 𝑦 → ∃𝑧(𝑥 = 𝑧 ∧ 𝑦 = 𝑧))
Theorem	equvelv 2045*	A biconditional form of equvel 2481 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 2046	An equivalence between two ways of expressing ax-13 2397. See the comment for ax-13 2397. (Contributed by NM, 2-May-2017.) (Proof shortened by Wolf Lammen, 26-Feb-2018.) (Revised by BJ, 15-Sep-2020.)
⊢ ((¬ 𝑥 = 𝑦 → (𝑦 = 𝑧 → 𝜑)) ↔ (¬ 𝑥 = 𝑦 → (¬ 𝑥 = 𝑧 → (𝑦 = 𝑧 → 𝜑))))
Theorem	spfw 2047*	Weak version of sp 2212. 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 2048*	Weak version of the specialization scheme sp 2212. Lemma 9 of [KalishMontague] p. 87. While it appears that sp 2212 in its general form does not follow from Tarski's FOL axiom schemes, from this theorem we can prove any instance of sp 2212 having mutually distinct setvar variables and no wff metavariables (see ax12wdemo 2163 for an example of the procedure to eliminate the hypothesis). Other approximations of sp 2212 are spfw 2047 (minimal distinct variable requirements), spnfw 1993 (when 𝑥 is not free in ¬ 𝜑), spvw 1995 (when 𝑥 does not appear in 𝜑), sptruw 1820 (when 𝜑 is true), spfalw 1994 (when 𝜑 is false), and spvv 2002 (where 𝜑 is changed into 𝜓). (Contributed by NM, 9-Apr-2017.) (Proof shortened by Wolf Lammen, 27-Feb-2018.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥𝜑 → 𝜑)
Theorem	cbvalw 2049*	Change bound variable. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 9-Apr-2017.)
⊢ (∀𝑥𝜑 → ∀𝑦∀𝑥𝜑)    &   ⊢ (¬ 𝜓 → ∀𝑥 ¬ 𝜓)    &   ⊢ (∀𝑦𝜓 → ∀𝑥∀𝑦𝜓)    &   ⊢ (¬ 𝜑 → ∀𝑦 ¬ 𝜑)    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓)
Theorem	cbvalvw 2050*	Change bound variable. Uses only Tarski's FOL axiom schemes. See cbvalv 2425 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 2051*	Change bound variable. Uses only Tarski's FOL axiom schemes. See cbvexv 2426 for a version with fewer disjoint variable conditions but requiring more axioms. (Contributed by NM, 19-Apr-2017.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓)
Theorem	cbvaldvaw 2052*	Rule used to change the bound variable in a universal quantifier with implicit substitution. Deduction form. Version of cbvaldva 2434 with a disjoint variable condition, requiring fewer axioms. (Contributed by David Moews, 1-May-2017.) Avoid ax-13 2397. (Revised by GG, 10-Jan-2024.) Reduce axiom usage, along an idea of GG. (Revised by Wolf Lammen, 10-Feb-2024.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒))
Theorem	cbvexdvaw 2053*	Rule used to change the bound variable in an existential quantifier with implicit substitution. Deduction form. Version of cbvexdva 2435 with a disjoint variable condition, requiring fewer axioms. (Contributed by David Moews, 1-May-2017.) Avoid ax-13 2397. (Revised by GG, 10-Jan-2024.) Reduce axiom usage. (Revised by Wolf Lammen, 10-Feb-2024.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑦𝜒))
Theorem	cbval2vw 2054*	Rule used to change bound variables, using implicit substitution. Version of cbval2vv 2438 with more disjoint variable conditions, which requires fewer axioms . (Contributed by NM, 4-Feb-2005.) Avoid ax-13 2397. (Revised by GG, 10-Jan-2024.)
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑧∀𝑤𝜓)
Theorem	cbvex2vw 2055*	Rule used to change bound variables, using implicit substitution. Version of cbvex2vv 2439 with more disjoint variable conditions, which requires fewer axioms . (Contributed by NM, 26-Jul-1995.) Avoid ax-13 2397. (Revised by GG, 10-Jan-2024.)
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑧∃𝑤𝜓)
Theorem	cbvex4vw 2056*	Rule used to change bound variables, using implicit substitution. Version of cbvex4v 2440 with more disjoint variable conditions, which requires fewer axioms. (Contributed by NM, 26-Jul-1995.) Avoid ax-13 2397. (Revised by GG, 10-Jan-2024.)
⊢ ((𝑥 = 𝑣 ∧ 𝑦 = 𝑢) → (𝜑 ↔ 𝜓))    &   ⊢ ((𝑧 = 𝑓 ∧ 𝑤 = 𝑔) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (∃𝑥∃𝑦∃𝑧∃𝑤𝜑 ↔ ∃𝑣∃𝑢∃𝑓∃𝑔𝜒)
Theorem	alcomimw 2057*	Weak version of ax-11 2185. See alcomw 2059 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 2058*	Weak version of excomim 2191. Uses only Tarski's FOL axiom schemes. (Contributed by BTernaryTau, 23-Jun-2025.)
⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥∃𝑦𝜑 → ∃𝑦∃𝑥𝜑)
Theorem	alcomw 2059*	Weak version of alcom 2187 and biconditional form of alcomimw 2057. Uses only Tarski's FOL axiom schemes. (Contributed by BTernaryTau, 28-Dec-2024.)
⊢ (𝑥 = 𝑤 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜒))    ⇒   ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑦∀𝑥𝜑)
Theorem	excomw 2060*	Weak version of excom 2190 and biconditional form of excomimw 2058. Uses only Tarski's FOL axiom schemes. (Contributed by TM, 24-Jan-2026.)
⊢ (𝑥 = 𝑤 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜒))    ⇒   ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑦∃𝑥𝜑)
Theorem	hbn1fw 2061*	Weak version of ax-10 2169 from which we can prove any ax-10 2169 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 2062*	Weak version of hbn1 2170. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 9-Apr-2017.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (¬ ∀𝑥𝜑 → ∀𝑥 ¬ ∀𝑥𝜑)
Theorem	hba1w 2063*	Weak version of hba1 2321. See comments for ax10w 2157. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 9-Apr-2017.) (Proof shortened by Wolf Lammen, 10-Oct-2021.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥𝜑 → ∀𝑥∀𝑥𝜑)
Theorem	hbe1w 2064*	Weak version of hbe1 2171. See comments for ax10w 2157. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 19-Apr-2017.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥𝜑 → ∀𝑥∃𝑥𝜑)
Theorem	hbalw 2065*	Weak version of hbal 2195. Uses only Tarski's FOL axiom schemes. Unlike hbal 2195, this theorem requires that 𝑥 and 𝑦 be distinct, i.e., not be bundled. (Contributed by NM, 19-Apr-2017.)
⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜓))    &   ⊢ (𝜑 → ∀𝑥𝜑)    ⇒   ⊢ (∀𝑦𝜑 → ∀𝑥∀𝑦𝜑)
Theorem	19.8aw 2066*	If a formula is true, then it is true for at least one instance. This is to 19.8a 2210 what spw 2048 is to sp 2212. (Contributed by SN, 26-Sep-2024.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝜑 → ∃𝑥𝜑)
Theorem	exexw 2067*	Existential quantification over a given variable is idempotent. Weak version of bj-exexbiex 37123, requiring fewer axioms. (Contributed by GG, 4-Nov-2024.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥𝜑 ↔ ∃𝑥∃𝑥𝜑)
Theorem	spaev 2068*	A special instance of sp 2212 applied to an equality with a disjoint variable condition. Unlike the more general sp 2212, we can prove this without ax-12 2206. Instance of aeveq 2072. 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 2069*	Change bound variable in an equality with a disjoint variable condition. Instance of aev 2073. (Contributed by NM, 22-Jul-2015.) (Revised by BJ, 18-Jun-2019.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧 𝑧 = 𝑦)
Theorem	aevlem0 2070*	Lemma for aevlem 2071. Instance of aev 2073. (Contributed by NM, 8-Jul-2016.) (Proof shortened by Wolf Lammen, 17-Feb-2018.) Remove dependency on ax-12 2206. (Revised by Wolf Lammen, 14-Mar-2021.) Extract from proof of a former lemma for axc11n 2451 and add DV condition to reduce axiom usage. (Revised by BJ, 29-Mar-2021.) (Proof shortened by Wolf Lammen, 30-Mar-2021.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧 𝑧 = 𝑥)
Theorem	aevlem 2071*	Lemma for aev 2073 and axc16g 2289. Change free and bound variables. Instance of aev 2073. (Contributed by NM, 22-Jul-2015.) (Proof shortened by Wolf Lammen, 17-Feb-2018.) Remove dependency on ax-13 2397, along an idea of BJ. (Revised by Wolf Lammen, 30-Nov-2019.) Reduce axiom usage. (Revised by BJ, 29-Mar-2021.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧 𝑧 = 𝑡)
Theorem	aeveq 2072*	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 2073*	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 2185. (Revised by Wolf Lammen, 7-Sep-2018.) Remove dependency on ax-13 2397, inspired by an idea of BJ. (Revised by Wolf Lammen, 30-Nov-2019.) Remove dependency on ax-12 2206. (Revised by Wolf Lammen, 19-Mar-2021.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧 𝑡 = 𝑢)
Theorem	aev2 2074*	A version of aev 2073 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 2072, aev 2073, aev2 2074). Using aev 2073 and alrimiv 1941, 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 30601. This list cannot be extended to ¬ or ⊥ since the scheme ∀𝑥𝑥 = 𝑦 is consistent with ax-mp 5, ax-gen 1809, ax-1 6-- ax-13 2397 (as the one-element universe shows), so for instance (∀𝑥𝑥 = 𝑦 → ⊥), DV (𝑥, 𝑦) is not provable from these axioms alone (indeed, dtru 5398 uses non-logical axioms as well). (Contributed by BJ, 23-Mar-2021.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧∀𝑡 𝑢 = 𝑣)
Theorem	hbaev 2075*	All variables are effectively bound in an identical variable specifier. Version of hbae 2456 with a disjoint variable condition, requiring fewer axioms. Instance of aev2 2074. (Contributed by NM, 13-May-1993.) Reduce axiom usage. (Revised by Wolf Lammen, 22-Mar-2021.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧∀𝑥 𝑥 = 𝑦)
Theorem	naev 2076*	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 2077*	Generalization of hbnaev 2078. (Contributed by Wolf Lammen, 9-Apr-2021.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑧 ¬ ∀𝑡 𝑡 = 𝑢)
Theorem	hbnaev 2078*	Any variable is free in ¬ ∀𝑥𝑥 = 𝑦, if 𝑥 and 𝑦 are distinct. This condition is dropped in hbnae 2457, at the expense of more axiom dependencies. Instance of naev2 2077. (Contributed by NM, 13-May-1993.) (Revised by Wolf Lammen, 9-Apr-2021.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑧 ¬ ∀𝑥 𝑥 = 𝑦)
1.4.8  Define proper substitution
Theorem	justify-df 2079	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 2083) 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 2080, just2-df 2081, and just3-df 2082. An implementation is provided by definition df-sb 2085 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 2080	First justification theorem for definitions whose definiens is a conjunction, as in df-sb 2085. 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 2081	Second justification theorem for definitions whose definiens is a conjunction, as in df-sb 2085. If 𝜑 is equivalent to (𝜓 ∧ 𝜒), then it implies (𝜓 ↔ 𝜒). In the case of df-sb 2085, this expresses the invariance of the definition under alpha-renaming of the bound variable. (Contributed by Wolf Lammen, 6-Jun-2026.)
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))    ⇒   ⊢ (𝜑 → (𝜓 ↔ 𝜒))
Theorem	just3-df 2082	Third justification theorem for definitions whose definiens is a conjunction, as in df-sb 2085. 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 2080, the definiendum is therefore equivalent to either conjunct. (Contributed by Wolf Lammen, 6-Jun-2026.)
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))    &   ⊢ (𝜓 ↔ 𝜒)    ⇒   ⊢ (𝜓 → 𝜑)
Theorem	rename-sb 2083*	The equivalence needed for df-sb 2085 in just3-df 2082. It is proved from Tarski's FOL axiom schemes. (Contributed by BJ, 22-Jan-2023.)
⊢ (∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑)) ↔ ∀𝑧(𝑧 = 𝑡 → ∀𝑥(𝑥 = 𝑧 → 𝜑)))
Syntax	wsb 2084	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 2085*	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 2153. In practice, the definiens reduces to "∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑)) " (see just3-df 2082). 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 2081). This is a necessity of Metamath supporting axiom dependency lists. See justify-df 2079 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 2110, sbcom2 2200, and sbid2v 2534. This definition remains valid when 𝑥 and 𝑡 are replaced with the same variable, as shown by sbid 2284. This is achieved by applying Tarski's definition sb6 2112 twice, which is valid for disjoint variables, and introducing a dummy variable 𝑦 that isolates 𝑥 from 𝑡, as in dfsb7 2307 relative to sb5 2304. We can also achieve this by having 𝑥 free in the first conjunct and bound in the second, as the alternate definition dfsb1 2506 shows. Another version that mixes free and bound variables is dfsb3 2519. When 𝑥 and 𝑡 are distinct, proper substitution can be expressed more simply using sb5 2304 and sb6 2112. 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 2087 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 2506. (Revised by BJ, 22-Dec-2020.) Support alpha-renaming. (Revised by Wolf Lammen, 4-Jun-2026.)
⊢ ([𝑡 / 𝑥]𝜑 ↔ (∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑)) ∧ ∀𝑧(𝑧 = 𝑡 → ∀𝑥(𝑥 = 𝑧 → 𝜑))))
Theorem	dfsbimp 2086*	A simple consequence of df-sb 2085. (Contributed by Wolf Lammen, 4-Jun-2026.)
⊢ ([𝑡 / 𝑥]𝜑 → ∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
Theorem	dfsb 2087*	Simplify definition df-sb 2085 by proving the renaming independency. (Contributed by Wolf Lammen, 5-Feb-2026.) df-sb 2085 changed. (Revised by Wolf Lammen, 4-Jun-2026.)
⊢ ([𝑡 / 𝑥]𝜑 ↔ ∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
Theorem	sbtlem 2088	In the case of sbt 2089, rename-sb 2083 is derivable from propositional axioms and ax-gen 1809 alone. The essential proof step is presented in this lemma. (Contributed by Wolf Lammen, 4-Feb-2026.)
⊢ 𝜑    ⇒   ⊢ ∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑))
Theorem	sbt 2089	A substitution into a theorem yields a theorem. See sbtALT 2094 for a shorter proof requiring more axioms. See chvar 2420 and chvarv 2421 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 2085. (Revised by Steven Nguyen, 6-Jul-2023.) Revise df-sb 2085 again. (Revised by Wolf Lammen, 4-Jun-2026.)
⊢ 𝜑    ⇒   ⊢ [𝑡 / 𝑥]𝜑
Theorem	sbtru 2090	The result of substituting in the truth constant "true" is true. (Contributed by BJ, 2-Sep-2023.)
⊢ [𝑦 / 𝑥]⊤
Theorem	stdpc4lem 2091*	In the case of stdpc4 2092, rename-sb 2083 is derivable from fewer axioms than dfsb 2087. 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.)
⊢ (∀𝑥𝜑 → ∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
Theorem	stdpc4 2092	The specialization axiom of standard predicate calculus. It states that if a statement 𝜑 holds for all 𝑥, then it also holds for the specific case of 𝑡 (properly) substituted for 𝑥. Translated to traditional notation, it can be read: "∀𝑥𝜑(𝑥) → 𝜑(𝑡), provided that 𝑡 is free for 𝑥 in 𝜑(𝑥)". Axiom 4 of [Mendelson] p. 69. See also spsbc 3752 and rspsbc 3827. (Contributed by NM, 14-May-1993.) Revise df-sb 2085. (Revised by BJ, 22-Dec-2020.) Revise df-sb again. (Revised by Wolf Lammen, 4-Jun-2026.)
⊢ (∀𝑥𝜑 → [𝑡 / 𝑥]𝜑)
Theorem	stdpc4ALT 2093	Alternate proof of stdpc4 2092, shorter but using additional axioms. (Contributed by WL, 5-Jun-2026.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥𝜑 → [𝑡 / 𝑥]𝜑)
Theorem	sbtALT 2094	Alternate proof of sbt 2089, shorter but using additional axioms. (Contributed by NM, 21-Jan-2004.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    ⇒   ⊢ [𝑦 / 𝑥]𝜑
Theorem	2stdpc4 2095	A double specialization using explicit substitution. This is Theorem PM*11.1 in [WhiteheadRussell] p. 159. See stdpc4 2092 for the analogous single specialization. See 2sp 2215 for another double specialization. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ (∀𝑥∀𝑦𝜑 → [𝑧 / 𝑥][𝑤 / 𝑦]𝜑)
Theorem	sbi1lem 2096*	Lemma for sbi1 2097. The core of the proof was extracted from a proof of SN. (Contributed by Wolf Lammen, 5-Jun-2026.)
⊢ (([𝑡 / 𝑥](𝜑 → 𝜓) ∧ [𝑡 / 𝑥]𝜑) → ∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜓)))
Theorem	sbi1 2097	Distribute substitution over implication. (Contributed by NM, 14-May-1993.) Remove dependencies on axioms. (Revised by Steven Nguyen, 24-Jul-2023.) Definition df-sb 2085 changed. (Revised by Wolf Lammen, 5-Jun-2026.)
⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) → ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓))
Theorem	sbi1ALT 2098	Alternate proof of sbt 2089, shorter but using additional axioms. (Contributed by NM, 14-May-1993.) Remove dependencies on axioms. (Revised by Steven Nguyen, 24-Jul-2023.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) → ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓))
Theorem	spsbim 2099	Distribute substitution over implication. Closed form of sbimi 2101. Specialization of implication. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) Revise df-sb 2085. (Revised by BJ, 22-Dec-2020.) (Proof shortened by Steven Nguyen, 24-Jul-2023.)
⊢ (∀𝑥(𝜑 → 𝜓) → ([𝑡 / 𝑥]𝜑 → [𝑡 / 𝑥]𝜓))
Theorem	spsbbi 2100	Biconditional property for substitution. Closed form of sbbii 2103. Specialization of biconditional. (Contributed by NM, 2-Jun-1993.) Revise df-sb 2085. (Revised by BJ, 22-Dec-2020.)
⊢ (∀𝑥(𝜑 ↔ 𝜓) → ([𝑡 / 𝑥]𝜑 ↔ [𝑡 / 𝑥]𝜓))