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	equs4v 2001*	Version of equs4 2418 with a disjoint variable condition, which requires fewer axioms. (Contributed by NM, 10-May-1993.) (Revised by BJ, 31-May-2019.)
⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))
Theorem	alequexv 2002*	Version of equs4v 2001 with its consequence simplified by exsimpr 1870. (Contributed by BJ, 9-Nov-2021.)
⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → ∃𝑥𝜑)
Theorem	exsbim 2003*	One direction of the equivalence in exsb 2361 is based on fewer axioms. (Contributed by Wolf Lammen, 2-Mar-2023.)
⊢ (∃𝑦∀𝑥(𝑥 = 𝑦 → 𝜑) → ∃𝑥𝜑)
Theorem	equsv 2004*	If a formula does not contain a variable 𝑥, then it is equivalent to the corresponding prototype of substitution with a fresh variable (see sb6 2090). (Contributed by BJ, 23-Jul-2023.)
⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜑)
Theorem	equsalvw 2005*	Version of equsalv 2272 with a disjoint variable condition, and of equsal 2419 with two disjoint variable conditions, which requires fewer axioms. See also the dual form equsexvw 2006. (Contributed by BJ, 31-May-2019.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜓)
Theorem	equsexvw 2006*	Version of equsexv 2273 with a disjoint variable condition, and of equsex 2420 with two disjoint variable conditions, which requires fewer axioms. See also the dual form equsalvw 2005. (Contributed by BJ, 31-May-2019.) (Proof shortened by Wolf Lammen, 23-Oct-2023.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ 𝜓)
Theorem	cbvaliw 2007*	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 2008*	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 2009	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 2022). 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 2017 that this axiom can be recovered from its weakened version ax7v 2010 where 𝑥 and 𝑦 are assumed to be disjoint variables. In particular, the only theorem referencing ax-7 2009 should be ax7v 2010. See the comment of ax7v 2010 for more details on these matters. (Contributed by NM, 10-Jan-1993.) (Revised by BJ, 7-Dec-2020.) Use ax7 2017 instead. (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧))
Theorem	ax7v 2010*	Weakened version of ax-7 2009, with a disjoint variable condition on 𝑥, 𝑦. This should be the only proof referencing ax-7 2009, and it should be referenced only by its two weakened versions ax7v1 2011 and ax7v2 2012, from which ax-7 2009 is then rederived as ax7 2017, which shows that either ax7v 2010 or the conjunction of ax7v1 2011 and ax7v2 2012 is sufficient. In ax7v 2010, it is still allowed to substitute the same variable for 𝑥 and 𝑧, or the same variable for 𝑦 and 𝑧. Therefore, ax7v 2010 "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 2015 and equid 2013 respectively. (Contributed by BJ, 7-Dec-2020.) Use ax7 2017 instead. (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧))
Theorem	ax7v1 2011*	First of two weakened versions of ax7v 2010, with an extra disjoint variable condition on 𝑥, 𝑧, see comments there. (Contributed by BJ, 7-Dec-2020.)
⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧))
Theorem	ax7v2 2012*	Second of two weakened versions of ax7v 2010, with an extra disjoint variable condition on 𝑦, 𝑧, see comments there. (Contributed by BJ, 7-Dec-2020.)
⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧))
Theorem	equid 2013	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 2014	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 2015*	Weaker form of equcomi 2018 with a disjoint variable condition on 𝑥, 𝑦. This is an intermediate step and equcomi 2018 is fully recovered later. (Contributed by BJ, 7-Dec-2020.)
⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥)
Theorem	ax6evr 2016*	A commuted form of ax6ev 1970. (Contributed by BJ, 7-Dec-2020.)
⊢ ∃𝑥 𝑦 = 𝑥
Theorem	ax7 2017	Proof of ax-7 2009 from ax7v1 2011 and ax7v2 2012 (and earlier axioms), proving sufficiency of the conjunction of the latter two weakened versions of ax7v 2010, which is itself a weakened version of ax-7 2009. Note that the weakened version of ax-7 2009 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 2018	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 2019	Commutative law for equality. Equality is a symmetric relation. (Contributed by NM, 20-Aug-1993.)
⊢ (𝑥 = 𝑦 ↔ 𝑦 = 𝑥)
Theorem	equcomd 2020	Deduction form of equcom 2019, symmetry of equality. For the versions for classes, see eqcom 2740 and eqcomd 2739. (Contributed by BJ, 6-Oct-2019.)
⊢ (𝜑 → 𝑥 = 𝑦)    ⇒   ⊢ (𝜑 → 𝑦 = 𝑥)
Theorem	equcoms 2021	An inference commuting equality in antecedent. Used to eliminate the need for a syllogism. (Contributed by NM, 10-Jan-1993.)
⊢ (𝑥 = 𝑦 → 𝜑)    ⇒   ⊢ (𝑦 = 𝑥 → 𝜑)
Theorem	equtr 2022	A transitive law for equality. (Contributed by NM, 23-Aug-1993.)
⊢ (𝑥 = 𝑦 → (𝑦 = 𝑧 → 𝑥 = 𝑧))
Theorem	equtrr 2023	A transitive law for equality. Lemma L17 in [Megill] p. 446 (p. 14 of the preprint). (Contributed by NM, 23-Aug-1993.)
⊢ (𝑥 = 𝑦 → (𝑧 = 𝑥 → 𝑧 = 𝑦))
Theorem	equeuclr 2024	Commuted version of equeucl 2025 (equality is left-Euclidean). (Contributed by BJ, 12-Apr-2021.)
⊢ (𝑥 = 𝑧 → (𝑦 = 𝑧 → 𝑦 = 𝑥))
Theorem	equeucl 2025	Equality is a left-Euclidean binary relation. (Right-Euclideanness is stated in ax-7 2009.) Curried (exported) form of equtr2 2028. (Contributed by BJ, 11-Apr-2021.)
⊢ (𝑥 = 𝑧 → (𝑦 = 𝑧 → 𝑥 = 𝑦))
Theorem	equequ1 2026	An equivalence law for equality. (Contributed by NM, 1-Aug-1993.) (Proof shortened by Wolf Lammen, 10-Dec-2017.)
⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 ↔ 𝑦 = 𝑧))
Theorem	equequ2 2027	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 2028	Equality is a left-Euclidean binary relation. Uncurried (imported) form of equeucl 2025. (Contributed by NM, 12-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by BJ, 11-Apr-2021.)
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑧) → 𝑥 = 𝑦)
Theorem	stdpc6 2029	One of the two equality axioms of standard predicate calculus, called reflexivity of equality. (The other one is stdpc7 2255.) 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 2030*	A variable introduction law for equality. Lemma 15 of [Monk2] p. 109. (Contributed by NM, 9-Jan-1993.) Remove dependencies on ax-10 2146, ax-13 2374. (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 2031*	A modified version of the forward implication of equvinv 2030 adapted to common usage. (Contributed by Wolf Lammen, 8-Sep-2018.)
⊢ (𝑥 = 𝑦 → ∃𝑧(𝑥 = 𝑧 ∧ 𝑦 = 𝑧))
Theorem	equvelv 2032*	A biconditional form of equvel 2458 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 2033	An equivalence between two ways of expressing ax-13 2374. See the comment for ax-13 2374. (Contributed by NM, 2-May-2017.) (Proof shortened by Wolf Lammen, 26-Feb-2018.) (Revised by BJ, 15-Sep-2020.)
⊢ ((¬ 𝑥 = 𝑦 → (𝑦 = 𝑧 → 𝜑)) ↔ (¬ 𝑥 = 𝑦 → (¬ 𝑥 = 𝑧 → (𝑦 = 𝑧 → 𝜑))))
Theorem	spfw 2034*	Weak version of sp 2188. 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 2035*	Weak version of the specialization scheme sp 2188. Lemma 9 of [KalishMontague] p. 87. While it appears that sp 2188 in its general form does not follow from Tarski's FOL axiom schemes, from this theorem we can prove any instance of sp 2188 having mutually distinct setvar variables and no wff metavariables (see ax12wdemo 2140 for an example of the procedure to eliminate the hypothesis). Other approximations of sp 2188 are spfw 2034 (minimal distinct variable requirements), spnfw 1980 (when 𝑥 is not free in ¬ 𝜑), spvw 1982 (when 𝑥 does not appear in 𝜑), sptruw 1807 (when 𝜑 is true), spfalw 1981 (when 𝜑 is false), and spvv 1989 (where 𝜑 is changed into 𝜓). (Contributed by NM, 9-Apr-2017.) (Proof shortened by Wolf Lammen, 27-Feb-2018.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥𝜑 → 𝜑)
Theorem	cbvalw 2036*	Change bound variable. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 9-Apr-2017.)
⊢ (∀𝑥𝜑 → ∀𝑦∀𝑥𝜑)    &   ⊢ (¬ 𝜓 → ∀𝑥 ¬ 𝜓)    &   ⊢ (∀𝑦𝜓 → ∀𝑥∀𝑦𝜓)    &   ⊢ (¬ 𝜑 → ∀𝑦 ¬ 𝜑)    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓)
Theorem	cbvalvw 2037*	Change bound variable. Uses only Tarski's FOL axiom schemes. See cbvalv 2402 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 2038*	Change bound variable. Uses only Tarski's FOL axiom schemes. See cbvexv 2403 for a version with fewer disjoint variable conditions but requiring more axioms. (Contributed by NM, 19-Apr-2017.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓)
Theorem	cbvaldvaw 2039*	Rule used to change the bound variable in a universal quantifier with implicit substitution. Deduction form. Version of cbvaldva 2411 with a disjoint variable condition, requiring fewer axioms. (Contributed by David Moews, 1-May-2017.) Avoid ax-13 2374. (Revised by GG, 10-Jan-2024.) Reduce axiom usage, along an idea of GG. (Revised by Wolf Lammen, 10-Feb-2024.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒))
Theorem	cbvexdvaw 2040*	Rule used to change the bound variable in an existential quantifier with implicit substitution. Deduction form. Version of cbvexdva 2412 with a disjoint variable condition, requiring fewer axioms. (Contributed by David Moews, 1-May-2017.) Avoid ax-13 2374. (Revised by GG, 10-Jan-2024.) Reduce axiom usage. (Revised by Wolf Lammen, 10-Feb-2024.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑦𝜒))
Theorem	cbval2vw 2041*	Rule used to change bound variables, using implicit substitution. Version of cbval2vv 2415 with more disjoint variable conditions, which requires fewer axioms . (Contributed by NM, 4-Feb-2005.) Avoid ax-13 2374. (Revised by GG, 10-Jan-2024.)
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑧∀𝑤𝜓)
Theorem	cbvex2vw 2042*	Rule used to change bound variables, using implicit substitution. Version of cbvex2vv 2416 with more disjoint variable conditions, which requires fewer axioms . (Contributed by NM, 26-Jul-1995.) Avoid ax-13 2374. (Revised by GG, 10-Jan-2024.)
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑧∃𝑤𝜓)
Theorem	cbvex4vw 2043*	Rule used to change bound variables, using implicit substitution. Version of cbvex4v 2417 with more disjoint variable conditions, which requires fewer axioms. (Contributed by NM, 26-Jul-1995.) Avoid ax-13 2374. (Revised by GG, 10-Jan-2024.)
⊢ ((𝑥 = 𝑣 ∧ 𝑦 = 𝑢) → (𝜑 ↔ 𝜓))    &   ⊢ ((𝑧 = 𝑓 ∧ 𝑤 = 𝑔) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (∃𝑥∃𝑦∃𝑧∃𝑤𝜑 ↔ ∃𝑣∃𝑢∃𝑓∃𝑔𝜒)
Theorem	alcomimw 2044*	Weak version of ax-11 2162. See alcomw 2046 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 2045*	Weak version of excomim 2168. Uses only Tarski's FOL axiom schemes. (Contributed by BTernaryTau, 23-Jun-2025.)
⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥∃𝑦𝜑 → ∃𝑦∃𝑥𝜑)
Theorem	alcomw 2046*	Weak version of alcom 2164 and biconditional form of alcomimw 2044. Uses only Tarski's FOL axiom schemes. (Contributed by BTernaryTau, 28-Dec-2024.)
⊢ (𝑥 = 𝑤 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜒))    ⇒   ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑦∀𝑥𝜑)
Theorem	excomw 2047*	Weak version of excom 2167 and biconditional form of excomimw 2045. Uses only Tarski's FOL axiom schemes. (Contributed by TM, 24-Jan-2026.)
⊢ (𝑥 = 𝑤 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜒))    ⇒   ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑦∃𝑥𝜑)
Theorem	hbn1fw 2048*	Weak version of ax-10 2146 from which we can prove any ax-10 2146 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 2049*	Weak version of hbn1 2147. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 9-Apr-2017.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (¬ ∀𝑥𝜑 → ∀𝑥 ¬ ∀𝑥𝜑)
Theorem	hba1w 2050*	Weak version of hba1 2297. See comments for ax10w 2134. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 9-Apr-2017.) (Proof shortened by Wolf Lammen, 10-Oct-2021.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥𝜑 → ∀𝑥∀𝑥𝜑)
Theorem	hbe1w 2051*	Weak version of hbe1 2148. See comments for ax10w 2134. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 19-Apr-2017.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥𝜑 → ∀𝑥∃𝑥𝜑)
Theorem	hbalw 2052*	Weak version of hbal 2172. Uses only Tarski's FOL axiom schemes. Unlike hbal 2172, this theorem requires that 𝑥 and 𝑦 be distinct, i.e., not be bundled. (Contributed by NM, 19-Apr-2017.)
⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜓))    &   ⊢ (𝜑 → ∀𝑥𝜑)    ⇒   ⊢ (∀𝑦𝜑 → ∀𝑥∀𝑦𝜑)
Theorem	19.8aw 2053*	If a formula is true, then it is true for at least one instance. This is to 19.8a 2186 what spw 2035 is to sp 2188. (Contributed by SN, 26-Sep-2024.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝜑 → ∃𝑥𝜑)
Theorem	exexw 2054*	Existential quantification over a given variable is idempotent. Weak version of bj-exexbiex 36755, requiring fewer axioms. (Contributed by GG, 4-Nov-2024.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥𝜑 ↔ ∃𝑥∃𝑥𝜑)
Theorem	spaev 2055*	A special instance of sp 2188 applied to an equality with a disjoint variable condition. Unlike the more general sp 2188, we can prove this without ax-12 2182. Instance of aeveq 2059. 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 2056*	Change bound variable in an equality with a disjoint variable condition. Instance of aev 2060. (Contributed by NM, 22-Jul-2015.) (Revised by BJ, 18-Jun-2019.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧 𝑧 = 𝑦)
Theorem	aevlem0 2057*	Lemma for aevlem 2058. Instance of aev 2060. (Contributed by NM, 8-Jul-2016.) (Proof shortened by Wolf Lammen, 17-Feb-2018.) Remove dependency on ax-12 2182. (Revised by Wolf Lammen, 14-Mar-2021.) Extract from proof of a former lemma for axc11n 2428 and add DV condition to reduce axiom usage. (Revised by BJ, 29-Mar-2021.) (Proof shortened by Wolf Lammen, 30-Mar-2021.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧 𝑧 = 𝑥)
Theorem	aevlem 2058*	Lemma for aev 2060 and axc16g 2265. Change free and bound variables. Instance of aev 2060. (Contributed by NM, 22-Jul-2015.) (Proof shortened by Wolf Lammen, 17-Feb-2018.) Remove dependency on ax-13 2374, along an idea of BJ. (Revised by Wolf Lammen, 30-Nov-2019.) Reduce axiom usage. (Revised by BJ, 29-Mar-2021.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧 𝑧 = 𝑡)
Theorem	aeveq 2059*	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 2060*	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 2162. (Revised by Wolf Lammen, 7-Sep-2018.) Remove dependency on ax-13 2374, inspired by an idea of BJ. (Revised by Wolf Lammen, 30-Nov-2019.) Remove dependency on ax-12 2182. (Revised by Wolf Lammen, 19-Mar-2021.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧 𝑡 = 𝑢)
Theorem	aev2 2061*	A version of aev 2060 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 2059, aev 2060, aev2 2061). Using aev 2060 and alrimiv 1928, 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 30451. This list cannot be extended to ¬ or ⊥ since the scheme ∀𝑥𝑥 = 𝑦 is consistent with ax-mp 5, ax-gen 1796, ax-1 6-- ax-13 2374 (as the one-element universe shows), so for instance (∀𝑥𝑥 = 𝑦 → ⊥), DV (𝑥, 𝑦) is not provable from these axioms alone (indeed, dtru 5383 uses non-logical axioms as well). (Contributed by BJ, 23-Mar-2021.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧∀𝑡 𝑢 = 𝑣)
Theorem	hbaev 2062*	All variables are effectively bound in an identical variable specifier. Version of hbae 2433 with a disjoint variable condition, requiring fewer axioms. Instance of aev2 2061. (Contributed by NM, 13-May-1993.) Reduce axiom usage. (Revised by Wolf Lammen, 22-Mar-2021.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧∀𝑥 𝑥 = 𝑦)
Theorem	naev 2063*	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 2064*	Generalization of hbnaev 2065. (Contributed by Wolf Lammen, 9-Apr-2021.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑧 ¬ ∀𝑡 𝑡 = 𝑢)
Theorem	hbnaev 2065*	Any variable is free in ¬ ∀𝑥𝑥 = 𝑦, if 𝑥 and 𝑦 are distinct. This condition is dropped in hbnae 2434, at the expense of more axiom dependencies. Instance of naev2 2064. (Contributed by NM, 13-May-1993.) (Revised by Wolf Lammen, 9-Apr-2021.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑧 ¬ ∀𝑥 𝑥 = 𝑦)
1.4.8  Define proper substitution
Theorem	sbjust 2066*	Justification theorem for df-sb 2068 proved from Tarski's FOL axiom schemes. (Contributed by BJ, 22-Jan-2023.)
⊢ (∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑)) ↔ ∀𝑧(𝑧 = 𝑡 → ∀𝑥(𝑥 = 𝑧 → 𝜑)))
Syntax	wsb 2067	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 2068*	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 2130. 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 2088, sbcom2 2178 and sbid2v 2511). Note that our definition is valid even when 𝑥 and 𝑡 are replaced with the same variable, as sbid 2260 shows. We achieve this by applying twice Tarski's definition sb6 2090 which is valid for disjoint variables, and introducing a dummy variable 𝑦 which isolates 𝑥 from 𝑡, as in dfsb7 2283 with respect to sb5 2280. We can also achieve this by having 𝑥 free in the first conjunct and bound in the second, as the alternate definition dfsb1 2483 shows. Another version that mixes free and bound variables is dfsb3 2496. When 𝑥 and 𝑡 are distinct, we can express proper substitution with the simpler expressions of sb5 2280 and sb6 2090. 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 2066 would be derivable from propositional axioms alone: one could apply the definiens for [𝑡 / 𝑥]𝜑 twice, using different dummy variables 𝑦 and 𝑧, and then invoke bitr3i 277 to establish their equivalence. This would jeopardize the independence of axioms, as demonstrated in an analoguous situation involving df-ss 3916 to prove ax-8 2115 (see in-ax8 36279). Prefer dfsb 2069 unless you can prove the hypothesis from fewer axioms in special cases, see sbt 2071. (Contributed by NM, 10-May-1993.) Revised from the original definition dfsb1 2483. (Revised by BJ, 22-Dec-2020.) Add the justification hypothesis. (Revised by Wolf Lammen, 4-Feb-2026.)
⊢ (∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑)) ↔ ∀𝑧(𝑧 = 𝑡 → ∀𝑥(𝑥 = 𝑧 → 𝜑)))    ⇒   ⊢ ([𝑡 / 𝑥]𝜑 ↔ ∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
Theorem	dfsb 2069*	Simplify definition df-sb 2068 by removing its provable hypothesis. (Contributed by Wolf Lammen, 5-Feb-2026.)
⊢ ([𝑡 / 𝑥]𝜑 ↔ ∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
Theorem	sbtlem 2070	In the case of sbt 2071, the hypothesis in df-sb 2068 is derivable from propositional axioms and ax-gen 1796 alone. The essential proof step is presented in this lemma. (Contributed by Wolf Lammen, 4-Feb-2026.)
⊢ 𝜑    ⇒   ⊢ ∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑))
Theorem	sbt 2071	A substitution into a theorem yields a theorem. See sbtALT 2074 for a shorter proof requiring more axioms. See chvar 2397 and chvarv 2398 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 2068. (Revised by Steven Nguyen, 6-Jul-2023.) Revise df-sb 2068 again. (Revised by Wolf Lammen, 4-Feb-2026.)
⊢ 𝜑    ⇒   ⊢ [𝑡 / 𝑥]𝜑
Theorem	sbtru 2072	The result of substituting in the truth constant "true" is true. (Contributed by BJ, 2-Sep-2023.)
⊢ [𝑦 / 𝑥]⊤
Theorem	stdpc4 2073	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 3751 and rspsbc 3827. (Contributed by NM, 14-May-1993.) Revise df-sb 2068. (Revised by BJ, 22-Dec-2020.)
⊢ (∀𝑥𝜑 → [𝑡 / 𝑥]𝜑)
Theorem	sbtALT 2074	Alternate proof of sbt 2071, shorter but using additional axioms. (Contributed by NM, 21-Jan-2004.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    ⇒   ⊢ [𝑦 / 𝑥]𝜑
Theorem	2stdpc4 2075	A double specialization using explicit substitution. This is Theorem PM*11.1 in [WhiteheadRussell] p. 159. See stdpc4 2073 for the analogous single specialization. See 2sp 2191 for another double specialization. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ (∀𝑥∀𝑦𝜑 → [𝑧 / 𝑥][𝑤 / 𝑦]𝜑)
Theorem	sbi1 2076	Distribute substitution over implication. (Contributed by NM, 14-May-1993.) Remove dependencies on axioms. (Revised by Steven Nguyen, 24-Jul-2023.)
⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) → ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓))
Theorem	spsbim 2077	Distribute substitution over implication. Closed form of sbimi 2079. Specialization of implication. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) Revise df-sb 2068. (Revised by BJ, 22-Dec-2020.) (Proof shortened by Steven Nguyen, 24-Jul-2023.)
⊢ (∀𝑥(𝜑 → 𝜓) → ([𝑡 / 𝑥]𝜑 → [𝑡 / 𝑥]𝜓))
Theorem	spsbbi 2078	Biconditional property for substitution. Closed form of sbbii 2081. Specialization of biconditional. (Contributed by NM, 2-Jun-1993.) Revise df-sb 2068. (Revised by BJ, 22-Dec-2020.)
⊢ (∀𝑥(𝜑 ↔ 𝜓) → ([𝑡 / 𝑥]𝜑 ↔ [𝑡 / 𝑥]𝜓))
Theorem	sbimi 2079	Distribute substitution over implication. (Contributed by NM, 25-Jun-1998.) Revise df-sb 2068. (Revised by BJ, 22-Dec-2020.) (Proof shortened by Steven Nguyen, 24-Jul-2023.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ ([𝑡 / 𝑥]𝜑 → [𝑡 / 𝑥]𝜓)
Theorem	sb2imi 2080	Distribute substitution over implication. Compare al2imi 1816. (Contributed by Steven Nguyen, 13-Aug-2023.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ ([𝑡 / 𝑥]𝜑 → ([𝑡 / 𝑥]𝜓 → [𝑡 / 𝑥]𝜒))
Theorem	sbbii 2081	Infer substitution into both sides of a logical equivalence. (Contributed by NM, 14-May-1993.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ ([𝑡 / 𝑥]𝜑 ↔ [𝑡 / 𝑥]𝜓)
Theorem	2sbbii 2082	Infer double substitution into both sides of a logical equivalence. (Contributed by AV, 30-Jul-2023.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ ([𝑡 / 𝑥][𝑢 / 𝑦]𝜑 ↔ [𝑡 / 𝑥][𝑢 / 𝑦]𝜓)
Theorem	sbimdv 2083*	Deduction substituting both sides of an implication, with 𝜑 and 𝑥 disjoint. See also sbimd 2250. (Contributed by Wolf Lammen, 6-May-2023.) Revise df-sb 2068. (Revised by Steven Nguyen, 6-Jul-2023.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → ([𝑡 / 𝑥]𝜓 → [𝑡 / 𝑥]𝜒))
Theorem	sbbidv 2084*	Deduction substituting both sides of a biconditional, with 𝜑 and 𝑥 disjoint. See also sbbid 2251. (Contributed by Wolf Lammen, 6-May-2023.) (Proof shortened by Steven Nguyen, 6-Jul-2023.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ([𝑡 / 𝑥]𝜓 ↔ [𝑡 / 𝑥]𝜒))
Theorem	sban 2085	Conjunction inside and outside of a substitution are equivalent. Compare 19.26 1871. (Contributed by NM, 14-May-1993.) (Proof shortened by Steven Nguyen, 13-Aug-2023.)
⊢ ([𝑦 / 𝑥](𝜑 ∧ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓))
Theorem	sb3an 2086	Threefold conjunction inside and outside of a substitution are equivalent. (Contributed by NM, 14-Dec-2006.)
⊢ ([𝑦 / 𝑥](𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓 ∧ [𝑦 / 𝑥]𝜒))
Theorem	spsbe 2087	Existential generalization: if a proposition is true for a specific instance, then there exists an instance where it is true. (Contributed by NM, 29-Jun-1993.) (Proof shortened by Wolf Lammen, 3-May-2018.) Revise df-sb 2068. (Revised by BJ, 22-Dec-2020.) (Proof shortened by Steven Nguyen, 11-Jul-2023.)
⊢ ([𝑡 / 𝑥]𝜑 → ∃𝑥𝜑)
Theorem	sbequ 2088	Equality property for substitution, from Tarski's system. Used in proof of Theorem 9.7 in [Megill] p. 449 (p. 16 of the preprint). (Contributed by NM, 14-May-1993.) Revise df-sb 2068. (Revised by BJ, 30-Dec-2020.)
⊢ (𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 ↔ [𝑦 / 𝑧]𝜑))
Theorem	sbequi 2089	An equality theorem for substitution. (Contributed by NM, 14-May-1993.) (Proof shortened by Wolf Lammen, 15-Sep-2018.) (Proof shortened by Steven Nguyen, 7-Jul-2023.)
⊢ (𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 → [𝑦 / 𝑧]𝜑))
Theorem	sb6 2090*	Alternate definition of substitution when variables are disjoint. Compare Theorem 6.2 of [Quine] p. 40. Also proved as Lemmas 16 and 17 of [Tarski] p. 70. The implication "to the left" also holds without a disjoint variable condition (sb2 2481). Theorem sb6f 2499 replaces the disjoint variable condition with a nonfreeness hypothesis. Theorem sb4b 2477 replaces it with a distinctor antecedent. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Wolf Lammen, 21-Sep-2018.) Revise df-sb 2068. (Revised by BJ, 22-Dec-2020.) Remove use of ax-11 2162. (Revised by Steven Nguyen, 7-Jul-2023.) (Proof shortened by Wolf Lammen, 16-Jul-2023.)
⊢ ([𝑡 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑡 → 𝜑))
Theorem	2sb6 2091*	Equivalence for double substitution. (Contributed by NM, 3-Feb-2005.)
⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 ↔ ∀𝑥∀𝑦((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝜑))
Theorem	sb1v 2092*	One direction of sb5 2280, provable from fewer axioms. Version of sb1 2480 with a disjoint variable condition using fewer axioms. (Contributed by NM, 13-May-1993.) (Revised by Wolf Lammen, 20-Jan-2024.)
⊢ ([𝑦 / 𝑥]𝜑 → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))
Theorem	sbv 2093*	Substitution for a variable not occurring in a proposition. See sbf 2275 for a version without disjoint variable condition on 𝑥, 𝜑. If one adds a disjoint variable condition on 𝑥, 𝑡, then sbv 2093 can be proved directly by chaining equsv 2004 with sb6 2090. (Contributed by BJ, 22-Dec-2020.)
⊢ ([𝑡 / 𝑥]𝜑 ↔ 𝜑)
Theorem	sbcom4 2094*	Commutativity law for substitution. This theorem was incorrectly used as our previous version of pm11.07 2095 but may still be useful. (Contributed by Andrew Salmon, 17-Jun-2011.) (Proof shortened by Jim Kingdon, 22-Jan-2018.)
⊢ ([𝑤 / 𝑥][𝑦 / 𝑧]𝜑 ↔ [𝑦 / 𝑥][𝑤 / 𝑧]𝜑)
Theorem	pm11.07 2095	Axiom *11.07 in [WhiteheadRussell] p. 159. The original reads: *11.07 "Whatever possible argument 𝑥 may be, 𝜑(𝑥, 𝑦) is true whatever possible argument 𝑦 may be" implies the corresponding statement with 𝑥 and 𝑦 interchanged except in "𝜑(𝑥, 𝑦)". Under our formalism this appears to correspond to idi 1 and not to sbcom4 2094 as earlier thought. See https://groups.google.com/g/metamath/c/iS0fOvSemC8/m/M1zTH8wxCAAJ 2094. (Contributed by BJ, 16-Sep-2018.) (New usage is discouraged.)
⊢ 𝜑    ⇒   ⊢ 𝜑
Theorem	sbrimvw 2096*	Substitution in an implication with a variable not free in the antecedent affects only the consequent. Version of sbrim 2308 based on fewer axioms, but with more disjoint variable conditions. Based on an idea of GG. (Contributed by Wolf Lammen, 29-Jan-2024.)
⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ (𝜑 → [𝑦 / 𝑥]𝜓))
Theorem	sbbiiev 2097*	An equivalence of substitutions (as in sbbii 2081) allowing the additional information that 𝑥 = 𝑡. Version of sbiev 2317 and sbievw 2098 without a disjoint variable condition on 𝜓, useful for substituting only part of 𝜑. (Contributed by SN, 24-Aug-2025.)
⊢ (𝑥 = 𝑡 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ([𝑡 / 𝑥]𝜑 ↔ [𝑡 / 𝑥]𝜓)
Theorem	sbievw 2098*	Conversion of implicit substitution to explicit substitution. Version of sbie 2504 and sbiev 2317 with more disjoint variable conditions, requiring fewer axioms. (Contributed by NM, 30-Jun-1994.) (Revised by BJ, 18-Jul-2023.) (Proof shortened by SN, 24-Aug-2025.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓)
Theorem	sbievwOLD 2099*	Obsolete version of sbievw 2098 as of 24-Aug-2025. (Contributed by NM, 30-Jun-1994.) (Revised by BJ, 18-Jul-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓)
Theorem	sbiedvw 2100*	Conversion of implicit substitution to explicit substitution (deduction version of sbievw 2098). Version of sbied 2505 and sbiedv 2506 with more disjoint variable conditions, requiring fewer axioms. (Contributed by NM, 30-Jun-1994.) (Revised by GG, 29-Jan-2024.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ([𝑦 / 𝑥]𝜓 ↔ 𝜒))