P. 25 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 2401-2500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	equs5eALT 2401	Alternate proof of equs5e 2492. Uses ax-12 2215 but not ax-13 2406. (Contributed by NM, 2-Feb-2007.) (Proof shortened by Wolf Lammen, 15-Jan-2018.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑦 → ∃𝑦𝜑))
Theorem	axc11r 2402	Same as axc11 2464 but with reversed antecedent. Note the use of ax-12 2215 (and not merely ax12v 2216 as in axc11rv 2303). This theorem is mostly used to eliminate conditions requiring set variables be distinct (cf. cbvaev 2078 and aecom 2461, for example) in proofs. In practice, theorems beyond elementary set theory do not really benefit from such eliminations. As of 2024, it is used in conjunction with ax-13 2406 only, and like that, it should be applied only in niches where indispensable. (Contributed by NM, 25-Jul-2015.)
⊢ (∀𝑦 𝑦 = 𝑥 → (∀𝑥𝜑 → ∀𝑦𝜑))
Theorem	dral1v 2403*	Formula-building lemma for use with the Distinctor Reduction Theorem. Version of dral1 2473 with a disjoint variable condition, which does not require ax-13 2406. Remark: the corresponding versions for dral2 2472 and drex2 2476 are instances of albidv 1943 and exbidv 1944 respectively. (Contributed by NM, 24-Nov-1994.) (Revised by BJ, 17-Jun-2019.) Base the proof on ax12v 2216. (Revised by Wolf Lammen, 30-Mar-2024.) Avoid ax-10 2178. (Revised by GG, 18-Nov-2024.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 ↔ ∀𝑦𝜓))
Theorem	drex1v 2404*	Formula-building lemma for use with the Distinctor Reduction Theorem. Version of drex1 2475 with a disjoint variable condition, which does not require ax-13 2406. (Contributed by NM, 27-Feb-2005.) (Revised by BJ, 17-Jun-2019.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 𝑥 = 𝑦 → (∃𝑥𝜑 ↔ ∃𝑦𝜓))
Theorem	drnf1v 2405*	Formula-building lemma for use with the Distinctor Reduction Theorem. Version of drnf1 2477 with a disjoint variable condition, which does not require ax-13 2406. (Contributed by Mario Carneiro, 4-Oct-2016.) (Revised by BJ, 17-Jun-2019.) Avoid ax-10 2178. (Revised by GG, 18-Nov-2024.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 𝑥 = 𝑦 → (Ⅎ𝑥𝜑 ↔ Ⅎ𝑦𝜓))
1.5.4  Axiom scheme ax-13 (Quantified Equality)
Axiom	ax-13 2406	Axiom of Quantified Equality. One of the equality and substitution axioms of predicate calculus with equality. An equivalent way to express this axiom that may be easier to understand is (¬ 𝑥 = 𝑦 → (¬ 𝑥 = 𝑧 → (𝑦 = 𝑧 → ∀𝑥𝑦 = 𝑧))) (see ax13b 2055). Recall that in the intended interpretation, our variables are metavariables ranging over the variables of predicate calculus (the object language). In order for the first antecedent ¬ 𝑥 = 𝑦 to hold, 𝑥 and 𝑦 must have different values and thus cannot be the same object-language variable (so they are effectively "distinct variables" even though no $d is present). Similarly, 𝑥 and 𝑧 cannot be the same object-language variable. Therefore, 𝑥 will not occur in the wff 𝑦 = 𝑧 when the first two antecedents hold, so analogous to ax-5 1933, the conclusion (𝑦 = 𝑧 → ∀𝑥𝑦 = 𝑧) follows. Note that ax-5 1933 cannot prove this because its distinct variable ($d) requirement is not satisfied directly but only indirectly (outside of Metamath) by the argument above. The original version of this axiom was ax-c9 39526 and was replaced with this shorter ax-13 2406 in December 2015. The old axiom is proved from this one as Theorem axc9 2416. The primary purpose of this axiom is to provide a way to introduce the quantifier ∀𝑥 on 𝑦 = 𝑧 even when 𝑥 and 𝑦 are substituted with the same variable. In this case, the first antecedent becomes ¬ 𝑥 = 𝑥 and the axiom still holds. This axiom is mostly used to eliminate conditions requiring set variables be distinct (cf. ax6ev 1992 and ax6e 2417, for example) in proofs. In practice, theorems beyond elementary set theory do not really benefit from such eliminations, so direct or indirect application of this axiom is discouraged now. You need to explicitly confirm its use in case you see a sensible application in a niche. After some assisting contributions by others over the years, it was in particular the extensive work of Gino Giotto in 2024 that helped reducing dependencies on this axiom on a large scale. Although this version is shorter, the original version axc9 2416 may be more practical to work with because of the "distinctor" form of its antecedents. A typical application of axc9 2416 is in dvelimh 2484 which converts a distinct variable pair to the distinctor antecedent ¬ ∀𝑥𝑥 = 𝑦. In particular, it is conjectured that it is not possible to prove ax6 2418 from ax6v 1991 without this axiom. This axiom can be weakened if desired by adding distinct variable restrictions on pairs 𝑥, 𝑧 and 𝑦, 𝑧. To show that, we add these restrictions to Theorem ax13v 2407 and use only ax13v 2407 for further derivations. Thus, ax13v 2407 should be the only theorem referencing this axiom. Other theorems can reference either ax13v 2407 (preferred) or ax13 2409 (if the stronger form is needed). This axiom scheme is logically redundant (see ax13w 2173) but is used as an auxiliary axiom scheme to achieve scheme completeness (i.e. so that all possible cases of bundling can be proved; see text linked at mmtheorems.html#ax6dgen 2173). It is not known whether this axiom can be derived from the others. (Contributed by NM, 21-Dec-2015.) (New usage is discouraged.)
⊢ (¬ 𝑥 = 𝑦 → (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧))
Theorem	ax13v 2407*	A weaker version of ax-13 2406 with distinct variable restrictions on pairs 𝑥, 𝑧 and 𝑦, 𝑧. In order to show (with ax13 2409) that this weakening is still adequate, this should be the only theorem referencing ax-13 2406 directly. Had we additionally required 𝑥 and 𝑦 be distinct, too, this theorem would have been a direct consequence of ax-5 1933. So essentially this theorem states, that a distinct variable condition can be replaced with an inequality between set variables. Preferably, use the version ax13w 2173 to avoid the propagation of ax-13 2406. (Contributed by NM, 30-Jun-2016.) (New usage is discouraged.)
⊢ (¬ 𝑥 = 𝑦 → (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧))
Theorem	ax13lem1 2408*	A version of ax13v 2407 with one distinct variable restriction dropped. For convenience, 𝑦 is kept on the right side of equations. The proof of ax13 2409 bases on ideas from NM, 24-Dec-2015. (Contributed by Wolf Lammen, 8-Sep-2018.) (New usage is discouraged.)
⊢ (¬ 𝑥 = 𝑦 → (𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦))
Theorem	ax13 2409	Derive ax-13 2406 from ax13v 2407 and Tarski's FOL. This shows that the weakening in ax13v 2407 is still sufficient for a complete system. Preferably, use the weaker ax13w 2173 to avoid the propagation of ax-13 2406. (Contributed by NM, 21-Dec-2015.) (Proof shortened by Wolf Lammen, 31-Jan-2018.) Reduce axiom usage. (Revised by Wolf Lammen, 2-Jun-2021.) (New usage is discouraged.)
⊢ (¬ 𝑥 = 𝑦 → (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧))
Theorem	ax13lem2 2410*	Lemma for nfeqf2 2411. This lemma is equivalent to ax13v 2407 with one distinct variable constraint removed. (Contributed by Wolf Lammen, 8-Sep-2018.) Reduce axiom usage. (Revised by Wolf Lammen, 18-Oct-2020.) (New usage is discouraged.)
⊢ (¬ 𝑥 = 𝑦 → (∃𝑥 𝑧 = 𝑦 → 𝑧 = 𝑦))
Theorem	nfeqf2 2411*	An equation between setvar is free of any other setvar. Usage of this theorem is discouraged because it depends on ax-13 2406. (Contributed by Wolf Lammen, 9-Jun-2019.) Remove dependency on ax-12 2215. (Revised by Wolf Lammen, 16-Dec-2022.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥 𝑧 = 𝑦)
Theorem	dveeq2 2412*	Quantifier introduction when one pair of variables is distinct. Usage of this theorem is discouraged because it depends on ax-13 2406. (Contributed by NM, 2-Jan-2002.) (Revised by NM, 20-Jul-2015.) Remove dependency on ax-11 2194. (Revised by Wolf Lammen, 8-Sep-2018.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦))
Theorem	nfeqf1 2413*	An equation between setvar is free of any other setvar. Usage of this theorem is discouraged because it depends on ax-13 2406. (Contributed by Wolf Lammen, 10-Jun-2019.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥 𝑦 = 𝑧)
Theorem	dveeq1 2414*	Quantifier introduction when one pair of variables is distinct. Usage of this theorem is discouraged because it depends on ax-13 2406. (Contributed by NM, 2-Jan-2002.) Remove dependency on ax-11 2194. (Revised by Wolf Lammen, 8-Sep-2018.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧))
Theorem	nfeqf 2415	A variable is effectively not free in an equality if it is not either of the involved variables. Ⅎ version of ax-c9 39526. Usage of this theorem is discouraged because it depends on ax-13 2406. (Contributed by Mario Carneiro, 6-Oct-2016.) Remove dependency on ax-11 2194. (Revised by Wolf Lammen, 6-Sep-2018.) (New usage is discouraged.)
⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦) → Ⅎ𝑧 𝑥 = 𝑦)
Theorem	axc9 2416	Derive set.mm's original ax-c9 39526 from the shorter ax-13 2406. Usage is discouraged to avoid uninformed ax-13 2406 propagation. (Contributed by NM, 29-Nov-2015.) (Revised by NM, 24-Dec-2015.) (Proof shortened by Wolf Lammen, 29-Apr-2018.) (New usage is discouraged.)
⊢ (¬ ∀𝑧 𝑧 = 𝑥 → (¬ ∀𝑧 𝑧 = 𝑦 → (𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)))
Theorem	ax6e 2417	At least one individual exists. This is not a theorem of free logic, which is sound in empty domains. For such a logic, we would add this theorem as an axiom of set theory (Axiom 0 of [Kunen] p. 10). In the system consisting of ax-4 1832 through ax-9 2155, all axioms other than ax-6 1990 are believed to be theorems of free logic, although the system without ax-6 1990 is not complete in free logic. Usage of this theorem is discouraged because it depends on ax-13 2406. It is preferred to use ax6ev 1992 when it is sufficient. (Contributed by NM, 14-May-1993.) Shortened after ax13lem1 2408 became available. (Revised by Wolf Lammen, 8-Sep-2018.) (New usage is discouraged.)
⊢ ∃𝑥 𝑥 = 𝑦
Theorem	ax6 2418	Theorem showing that ax-6 1990 follows from the weaker version ax6v 1991. (Even though this theorem depends on ax-6 1990, all references of ax-6 1990 are made via ax6v 1991. An earlier version stated ax6v 1991 as a separate axiom, but having two axioms caused some confusion.) This theorem should be referenced in place of ax-6 1990 so that all proofs can be traced back to ax6v 1991. When possible, use the weaker ax6v 1991 rather than ax6 2418 since the ax6v 1991 derivation is much shorter and requires fewer axioms. (Contributed by NM, 12-Nov-2013.) (Revised by NM, 25-Jul-2015.) (Proof shortened by Wolf Lammen, 4-Feb-2018.) Usage of this theorem is discouraged because it depends on ax-13 2406. Use ax6v 1991 instead. (New usage is discouraged.)
⊢ ¬ ∀𝑥 ¬ 𝑥 = 𝑦
Theorem	axc10 2419	Show that the original axiom ax-c10 39522 can be derived from ax6 2418 and axc7 2352 (on top of propositional calculus, ax-gen 1818, and ax-4 1832). See ax6fromc10 39532 for the rederivation of ax6 2418 from ax-c10 39522. Normally, axc10 2419 should be used rather than ax-c10 39522, except by theorems specifically studying the latter's properties. See bj-axc10v 37290 for a weaker version requiring fewer axioms. (Contributed by NM, 5-Aug-1993.) (Proof modification is discouraged.) Usage of this theorem is discouraged because it depends on ax-13 2406. (New usage is discouraged.)
⊢ (∀𝑥(𝑥 = 𝑦 → ∀𝑥𝜑) → 𝜑)
Theorem	spimt 2420	Closed theorem form of spim 2421. (Contributed by NM, 15-Jan-2008.) (Revised by Mario Carneiro, 17-Oct-2016.) (Proof shortened by Wolf Lammen, 21-Mar-2023.) Usage of this theorem is discouraged because it depends on ax-13 2406. (New usage is discouraged.)
⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝑦 → (𝜑 → 𝜓))) → (∀𝑥𝜑 → 𝜓))
Theorem	spim 2421	Specialization, using implicit substitution. Compare Lemma 14 of [Tarski] p. 70. The spim 2421 series of theorems requires that only one direction of the substitution hypothesis hold. Usage of this theorem is discouraged because it depends on ax-13 2406. See spimw 1993 for a version requiring fewer axioms. (Contributed by NM, 10-Jan-1993.) (Revised by Mario Carneiro, 3-Oct-2016.) (Proof shortened by Wolf Lammen, 18-Feb-2018.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))    ⇒   ⊢ (∀𝑥𝜑 → 𝜓)
Theorem	spimed 2422	Deduction version of spime 2423. (Contributed by NM, 14-May-1993.) (Revised by Mario Carneiro, 3-Oct-2016.) (Proof shortened by Wolf Lammen, 19-Feb-2018.) Usage of this theorem is discouraged because it depends on ax-13 2406. Use spimedv 2235 instead. (New usage is discouraged.)
⊢ (𝜒 → Ⅎ𝑥𝜑)    &   ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))    ⇒   ⊢ (𝜒 → (𝜑 → ∃𝑥𝜓))
Theorem	spime 2423	Existential introduction, using implicit substitution. Compare Lemma 14 of [Tarski] p. 70. See spimew 1994 and spimevw 2008 for weaker versions requiring fewer axioms. (Contributed by NM, 7-Aug-1994.) (Revised by Mario Carneiro, 3-Oct-2016.) (Proof shortened by Wolf Lammen, 6-Mar-2018.) Usage of this theorem is discouraged because it depends on ax-13 2406. Use spimefv 2236 instead. (New usage is discouraged.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))    ⇒   ⊢ (𝜑 → ∃𝑥𝜓)
Theorem	spimv 2424*	A version of spim 2421 with a distinct variable requirement instead of a bound-variable hypothesis. See spimfv 2277 and spimvw 2009 for versions requiring fewer axioms. (Contributed by NM, 31-Jul-1993.) Usage of this theorem is discouraged because it depends on ax-13 2406. Use spimvw 2009 instead. (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))    ⇒   ⊢ (∀𝑥𝜑 → 𝜓)
Theorem	spimvALT 2425*	Alternate proof of spimv 2424. Note that it requires only ax-1 6 through ax-5 1933 together with ax6e 2417. Currently, proofs derive from ax6v 1991, but if ax-6 1990 could be used instead, this proof would reduce axiom usage. (Contributed by NM, 31-Jul-1993.) Remove dependency on ax-10 2178. (Revised by BJ, 29-Nov-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))    ⇒   ⊢ (∀𝑥𝜑 → 𝜓)
Theorem	spimev 2426*	Distinct-variable version of spime 2423. (Contributed by NM, 10-Jan-1993.) Usage of this theorem is discouraged because it depends on ax-13 2406. Use spimevw 2008 instead. (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))    ⇒   ⊢ (𝜑 → ∃𝑥𝜓)
Theorem	spv 2427*	Specialization, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2406. Use the weaker spvv 2011 if possible. (Contributed by NM, 30-Aug-1993.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥𝜑 → 𝜓)
Theorem	spei 2428	Inference from existential specialization, using implicit substitution. Remove a distinct variable constraint. Usage of this theorem is discouraged because it depends on ax-13 2406. Use the weaker speiv 1995 if possible. (Contributed by NM, 19-Aug-1993.) (Proof shortened by Wolf Lammen, 12-May-2018.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ 𝜓    ⇒   ⊢ ∃𝑥𝜑
Theorem	chvar 2429	Implicit substitution of 𝑦 for 𝑥 into a theorem. Usage of this theorem is discouraged because it depends on ax-13 2406. Use the weaker chvarfv 2278 if possible. (Contributed by Raph Levien, 9-Jul-2003.) (Revised by Mario Carneiro, 3-Oct-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ 𝜓
Theorem	chvarv 2430*	Implicit substitution of 𝑦 for 𝑥 into a theorem. Usage of this theorem is discouraged because it depends on ax-13 2406. Use the weaker chvarvv 2012 if possible. (Contributed by NM, 20-Apr-1994.) (Proof shortened by Wolf Lammen, 22-Apr-2018.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ 𝜓
Theorem	cbv3 2431	Rule used to change bound variables, using implicit substitution, that does not use ax-c9 39526. Usage of this theorem is discouraged because it depends on ax-13 2406. Use the weaker cbv3v 2369 if possible. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 12-May-2018.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))    ⇒   ⊢ (∀𝑥𝜑 → ∀𝑦𝜓)
Theorem	cbval 2432	Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2406. Check out cbvalw 2058, cbvalvw 2059, cbvalv1 2375 for versions requiring fewer axioms. (Contributed by NM, 13-May-1993.) (Revised by Mario Carneiro, 3-Oct-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓)
Theorem	cbvex 2433	Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2406. Check out cbvexvw 2060, cbvexv1 2376 for weaker versions requiring fewer axioms. (Contributed by NM, 21-Jun-1993.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓)
Theorem	cbvalv 2434*	Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2406. See cbvalvw 2059 for a version requiring fewer axioms, to be preferred when sufficient. (Contributed by NM, 5-Aug-1993.) Remove dependency on ax-10 2178 and shorten proof. (Revised by Wolf Lammen, 11-Sep-2023.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓)
Theorem	cbvexv 2435*	Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2406. See cbvexvw 2060 for a version requiring fewer axioms, to be preferred when sufficient. (Contributed by NM, 21-Jun-1993.) Remove dependency on ax-10 2178 and shorten proof. (Revised by Wolf Lammen, 11-Sep-2023.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓)
Theorem	cbv1 2436	Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2406. See cbv1v 2370 with disjoint variable conditions, not depending on ax-13 2406. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 3-Oct-2016.) Format hypotheses to common style. (Revised by Wolf Lammen, 13-May-2018.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑦𝜓)    &   ⊢ (𝜑 → Ⅎ𝑥𝜒)    &   ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 → 𝜒)))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 → ∀𝑦𝜒))
Theorem	cbv2 2437	Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2406. See cbv2w 2371 with disjoint variable conditions, not depending on ax-13 2406. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 3-Oct-2016.) Format hypotheses to common style, avoid ax-10 2178. (Revised by Wolf Lammen, 10-Sep-2023.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑦𝜓)    &   ⊢ (𝜑 → Ⅎ𝑥𝜒)    &   ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒))
Theorem	cbv3h 2438	Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2406. Use the weaker cbv3hv 2374 if possible. (Contributed by NM, 8-Jun-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 12-May-2018.) (New usage is discouraged.)
⊢ (𝜑 → ∀𝑦𝜑)    &   ⊢ (𝜓 → ∀𝑥𝜓)    &   ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))    ⇒   ⊢ (∀𝑥𝜑 → ∀𝑦𝜓)
Theorem	cbv1h 2439	Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2406. (Contributed by NM, 11-May-1993.) (Proof shortened by Wolf Lammen, 13-May-2018.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → ∀𝑦𝜓))    &   ⊢ (𝜑 → (𝜒 → ∀𝑥𝜒))    &   ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 → 𝜒)))    ⇒   ⊢ (∀𝑥∀𝑦𝜑 → (∀𝑥𝜓 → ∀𝑦𝜒))
Theorem	cbv2h 2440	Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2406. (Contributed by NM, 11-May-1993.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → ∀𝑦𝜓))    &   ⊢ (𝜑 → (𝜒 → ∀𝑥𝜒))    &   ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (∀𝑥∀𝑦𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒))
Theorem	cbvald 2441*	Deduction used to change bound variables, using implicit substitution, particularly useful in conjunction with dvelim 2485. Usage of this theorem is discouraged because it depends on ax-13 2406. See cbvaldw 2372 for a version with 𝑥, 𝑦 disjoint, not depending on ax-13 2406. (Contributed by NM, 2-Jan-2002.) (Revised by Mario Carneiro, 6-Oct-2016.) (Revised by Wolf Lammen, 13-May-2018.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑦𝜓)    &   ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒))
Theorem	cbvexd 2442*	Deduction used to change bound variables, using implicit substitution, particularly useful in conjunction with dvelim 2485. Usage of this theorem is discouraged because it depends on ax-13 2406. Use the weaker cbvexdw 2373 if possible. (Contributed by NM, 2-Jan-2002.) (Revised by Mario Carneiro, 6-Oct-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑦𝜓)    &   ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑦𝜒))
Theorem	cbvaldva 2443*	Rule used to change the bound variable in a universal quantifier with implicit substitution. Deduction form. Usage of this theorem is discouraged because it depends on ax-13 2406. Use the weaker cbvaldvaw 2061 if possible. (Contributed by David Moews, 1-May-2017.) (New usage is discouraged.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒))
Theorem	cbvexdva 2444*	Rule used to change the bound variable in an existential quantifier with implicit substitution. Deduction form. Usage of this theorem is discouraged because it depends on ax-13 2406. Use the weaker cbvexdvaw 2062 if possible. (Contributed by David Moews, 1-May-2017.) (New usage is discouraged.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑦𝜒))
Theorem	cbval2 2445*	Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2406. Use the weaker cbval2v 2377 if possible. (Contributed by NM, 22-Dec-2003.) (Revised by Mario Carneiro, 6-Oct-2016.) (Proof shortened by Wolf Lammen, 11-Sep-2023.) (New usage is discouraged.)
⊢ Ⅎ𝑧𝜑    &   ⊢ Ⅎ𝑤𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ Ⅎ𝑦𝜓    &   ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑧∀𝑤𝜓)
Theorem	cbvex2 2446*	Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2406. Use the weaker cbvex2v 2378 if possible. (Contributed by NM, 14-Sep-2003.) (Revised by Mario Carneiro, 6-Oct-2016.) (Proof shortened by Wolf Lammen, 16-Jun-2019.) (New usage is discouraged.)
⊢ Ⅎ𝑧𝜑    &   ⊢ Ⅎ𝑤𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ Ⅎ𝑦𝜓    &   ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑧∃𝑤𝜓)
Theorem	cbval2vv 2447*	Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2406. Use the weaker cbval2vw 2063 if possible. (Contributed by NM, 4-Feb-2005.) Remove dependency on ax-10 2178. (Revised by Wolf Lammen, 18-Jul-2021.) (New usage is discouraged.)
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑧∀𝑤𝜓)
Theorem	cbvex2vv 2448*	Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2406. Use the weaker cbvex2vw 2064 if possible. (Contributed by NM, 26-Jul-1995.) Remove dependency on ax-10 2178. (Revised by Wolf Lammen, 18-Jul-2021.) (New usage is discouraged.)
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑧∃𝑤𝜓)
Theorem	cbvex4v 2449*	Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2406. Use the weaker cbvex4vw 2065 if possible. (Contributed by NM, 26-Jul-1995.) (New usage is discouraged.)
⊢ ((𝑥 = 𝑣 ∧ 𝑦 = 𝑢) → (𝜑 ↔ 𝜓))    &   ⊢ ((𝑧 = 𝑓 ∧ 𝑤 = 𝑔) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (∃𝑥∃𝑦∃𝑧∃𝑤𝜑 ↔ ∃𝑣∃𝑢∃𝑓∃𝑔𝜒)
Theorem	equs4 2450	Lemma used in proofs of implicit substitution properties. The converse requires either a disjoint variable condition (sbalex 2280) or a nonfreeness hypothesis (equs45f 2493). Usage of this theorem is discouraged because it depends on ax-13 2406. See equs4v 2023 for a weaker version requiring fewer axioms. (Contributed by NM, 10-May-1993.) (Proof shortened by Mario Carneiro, 20-May-2014.) (Proof shortened by Wolf Lammen, 5-Feb-2018.) (New usage is discouraged.)
⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))
Theorem	equsal 2451	An equivalence related to implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2406. See equsalvw 2027 and equsalv 2305 for versions with disjoint variable conditions proved from fewer axioms. See also the dual form equsex 2452. (Contributed by NM, 2-Jun-1993.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) (Revised by Mario Carneiro, 3-Oct-2016.) (Proof shortened by Wolf Lammen, 5-Feb-2018.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜓)
Theorem	equsex 2452	An equivalence related to implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2406. See equsexvw 2028 and equsexv 2306 for versions with disjoint variable conditions proved from fewer axioms. See also the dual form equsal 2451. See equsexALT 2453 for an alternate proof. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 3-Oct-2016.) (Proof shortened by Wolf Lammen, 6-Feb-2018.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ 𝜓)
Theorem	equsexALT 2453	Alternate proof of equsex 2452. This proves the result directly, instead of as a corollary of equsal 2451 via equs4 2450. Note in particular that only existential quantifiers appear in the proof and that the only step requiring ax-13 2406 is ax6e 2417. This proof mimics that of equsal 2451 (in particular, note that pm5.32i 584, exbii 1871, 19.41 2273, mpbiran 721 correspond respectively to pm5.74i 274, albii 1842, 19.23 2249, a1bi 365). (Contributed by BJ, 20-Aug-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ 𝜓)
Theorem	equsalh 2454	An equivalence related to implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2406. See equsalhw 2328 for a version with a disjoint variable condition requiring fewer axioms. (Contributed by NM, 2-Jun-1993.) (New usage is discouraged.)
⊢ (𝜓 → ∀𝑥𝜓)    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜓)
Theorem	equsexh 2455	An equivalence related to implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2406. See equsexhv 2329 for a version with a disjoint variable condition which does not require ax-13 2406. (Contributed by NM, 5-Aug-1993.) (New usage is discouraged.)
⊢ (𝜓 → ∀𝑥𝜓)    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ 𝜓)
Theorem	axc15 2456	Derivation of set.mm's original ax-c15 39525 from ax-c11n 39524 and the shorter ax-12 2215 that has replaced it. Theorem ax12 2457 shows the reverse derivation of ax-12 2215 from ax-c15 39525. Normally, axc15 2456 should be used rather than ax-c15 39525, except by theorems specifically studying the latter's properties. Usage of this theorem is discouraged because it depends on ax-13 2406. (Contributed by NM, 2-Feb-2007.) (Proof shortened by Wolf Lammen, 26-Mar-2023.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))))
Theorem	ax12 2457	Rederivation of Axiom ax-12 2215 from ax12v 2216 (used only via sp 2221), axc11r 2402, and axc15 2456 (on top of Tarski's FOL). Since this version depends on ax-13 2406, usage of the weaker ax12v 2216, ax12w 2170, ax12i 1989 are preferred. (Contributed by NM, 22-Jan-2007.) Proof uses contemporary axioms. (Revised by Wolf Lammen, 8-Aug-2020.) (Proof shortened by BJ, 4-Jul-2021.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → (∀𝑦𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
Theorem	ax12b 2458	A bidirectional version of axc15 2456. Usage of this theorem is discouraged because it depends on ax-13 2406. (Contributed by NM, 30-Jun-2006.) (New usage is discouraged.)
⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦) → (𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑)))
Theorem	ax13ALT 2459	Alternate proof of ax13 2409 from FOL, sp 2221, and axc9 2416. (Contributed by NM, 21-Dec-2015.) (Proof shortened by Wolf Lammen, 31-Jan-2018.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ 𝑥 = 𝑦 → (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧))
Theorem	axc11n 2460	Derive set.mm's original ax-c11n 39524 from others. Commutation law for identical variable specifiers. The antecedent and consequent are true when 𝑥 and 𝑦 are substituted with the same variable. Lemma L12 in [Megill] p. 445 (p. 12 of the preprint). If a disjoint variable condition is added on 𝑥 and 𝑦, then this becomes an instance of aevlem 2080. Use aecom 2461 instead when this does not lengthen the proof. Usage of this theorem is discouraged because it depends on ax-13 2406. (Contributed by NM, 10-May-1993.) (Revised by NM, 7-Nov-2015.) (Proof shortened by Wolf Lammen, 6-Mar-2018.) (Revised by Wolf Lammen, 30-Nov-2019.) (Proof shortened by BJ, 29-Mar-2021.) (Proof shortened by Wolf Lammen, 2-Jul-2021.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥)
Theorem	aecom 2461	Commutation law for identical variable specifiers. Both sides of the biconditional are true when 𝑥 and 𝑦 are substituted with the same variable. Usage of this theorem is discouraged because it depends on ax-13 2406. (Contributed by NM, 10-May-1993.) Change to a biconditional. (Revised by BJ, 26-Sep-2019.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 ↔ ∀𝑦 𝑦 = 𝑥)
Theorem	aecoms 2462	A commutation rule for identical variable specifiers. Usage of this theorem is discouraged because it depends on ax-13 2406. (Contributed by NM, 10-May-1993.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → 𝜑)    ⇒   ⊢ (∀𝑦 𝑦 = 𝑥 → 𝜑)
Theorem	naecoms 2463	A commutation rule for distinct variable specifiers. Usage of this theorem is discouraged because it depends on ax-13 2406. (Contributed by NM, 2-Jan-2002.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → 𝜑)    ⇒   ⊢ (¬ ∀𝑦 𝑦 = 𝑥 → 𝜑)
Theorem	axc11 2464	Show that ax-c11 39523 can be derived from ax-c11n 39524 in the form of axc11n 2460. Normally, axc11 2464 should be used rather than ax-c11 39523, except by theorems specifically studying the latter's properties. Usage of this theorem is discouraged because it depends on ax-13 2406. Use the weaker axc11v 2302 when possible. (Contributed by NM, 16-May-2008.) (Proof shortened by Wolf Lammen, 21-Apr-2018.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 → ∀𝑦𝜑))
Theorem	hbae 2465	All variables are effectively bound in an identical variable specifier. Usage of this theorem is discouraged because it depends on ax-13 2406. Use the weaker hbaev 2084 when possible. (Contributed by NM, 13-May-1993.) (Proof shortened by Wolf Lammen, 21-Apr-2018.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧∀𝑥 𝑥 = 𝑦)
Theorem	hbnae 2466	All variables are effectively bound in a distinct variable specifier. Lemma L19 in [Megill] p. 446 (p. 14 of the preprint). Usage of this theorem is discouraged because it depends on ax-13 2406. Use the weaker hbnaev 2087 when possible. (Contributed by NM, 13-May-1993.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑧 ¬ ∀𝑥 𝑥 = 𝑦)
Theorem	nfae 2467	All variables are effectively bound in an identical variable specifier. Usage of this theorem is discouraged because it depends on ax-13 2406. (Contributed by Mario Carneiro, 11-Aug-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑧∀𝑥 𝑥 = 𝑦
Theorem	nfnae 2468	All variables are effectively bound in a distinct variable specifier. Usage of this theorem is discouraged because it depends on ax-13 2406. Use the weaker nfnaew 2186 when possible. (Contributed by Mario Carneiro, 11-Aug-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑧 ¬ ∀𝑥 𝑥 = 𝑦
Theorem	hbnaes 2469	Rule that applies hbnae 2466 to antecedent. Usage of this theorem is discouraged because it depends on ax-13 2406. (Contributed by NM, 15-May-1993.) (New usage is discouraged.)
⊢ (∀𝑧 ¬ ∀𝑥 𝑥 = 𝑦 → 𝜑)    ⇒   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → 𝜑)
Theorem	axc16i 2470*	Inference with axc16 2299 as its conclusion. (Contributed by NM, 20-May-2008.) (Proof modification is discouraged.) Usage of this theorem is discouraged because it depends on ax-13 2406. Use axc16 2299 instead. (New usage is discouraged.)
⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜓))    &   ⊢ (𝜓 → ∀𝑥𝜓)    ⇒   ⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑥𝜑))
Theorem	axc16nfALT 2471*	Alternate proof of axc16nf 2301, shorter but requiring ax-11 2194 and ax-13 2406. (Contributed by Mario Carneiro, 7-Oct-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → Ⅎ𝑧𝜑)
Theorem	dral2 2472	Formula-building lemma for use with the Distinctor Reduction Theorem. Part of Theorem 9.4 of [Megill] p. 448 (p. 16 of preprint). Usage of this theorem is discouraged because it depends on ax-13 2406. Usage of albidv 1943 is preferred, which requires fewer axioms. (Contributed by NM, 27-Feb-2005.) Allow a shortening of dral1 2473. (Revised by Wolf Lammen, 4-Mar-2018.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑧𝜑 ↔ ∀𝑧𝜓))
Theorem	dral1 2473	Formula-building lemma for use with the Distinctor Reduction Theorem. Part of Theorem 9.4 of [Megill] p. 448 (p. 16 of preprint). Usage of this theorem is discouraged because it depends on ax-13 2406. Use the weaker dral1v 2403 if possible. (Contributed by NM, 24-Nov-1994.) Remove dependency on ax-11 2194. (Revised by Wolf Lammen, 6-Sep-2018.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 ↔ ∀𝑦𝜓))
Theorem	dral1ALT 2474	Alternate proof of dral1 2473, shorter but requiring ax-11 2194. (Contributed by NM, 24-Nov-1994.) (Proof shortened by Wolf Lammen, 22-Apr-2018.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 ↔ ∀𝑦𝜓))
Theorem	drex1 2475	Formula-building lemma for use with the Distinctor Reduction Theorem. Part of Theorem 9.4 of [Megill] p. 448 (p. 16 of preprint). Usage of this theorem is discouraged because it depends on ax-13 2406. Use the weaker drex1v 2404 if possible. (Contributed by NM, 27-Feb-2005.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 𝑥 = 𝑦 → (∃𝑥𝜑 ↔ ∃𝑦𝜓))
Theorem	drex2 2476	Formula-building lemma for use with the Distinctor Reduction Theorem. Part of Theorem 9.4 of [Megill] p. 448 (p. 16 of preprint). Usage of this theorem is discouraged because it depends on ax-13 2406. Usage of exbidv 1944 is preferred, which requires fewer axioms. (Contributed by NM, 27-Feb-2005.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 𝑥 = 𝑦 → (∃𝑧𝜑 ↔ ∃𝑧𝜓))
Theorem	drnf1 2477	Formula-building lemma for use with the Distinctor Reduction Theorem. (Contributed by Mario Carneiro, 4-Oct-2016.) Usage of this theorem is discouraged because it depends on ax-13 2406. Use drnf1v 2405 instead. (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 𝑥 = 𝑦 → (Ⅎ𝑥𝜑 ↔ Ⅎ𝑦𝜓))
Theorem	drnf2 2478	Formula-building lemma for use with the Distinctor Reduction Theorem. (Contributed by Mario Carneiro, 4-Oct-2016.) (Proof shortened by Wolf Lammen, 5-May-2018.) Usage of this theorem is discouraged because it depends on ax-13 2406. Use nfbidv 1945 instead. (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 𝑥 = 𝑦 → (Ⅎ𝑧𝜑 ↔ Ⅎ𝑧𝜓))
Theorem	nfald2 2479	Variation on nfald 2363 which adds the hypothesis that 𝑥 and 𝑦 are distinct in the inner subproof. (Contributed by Mario Carneiro, 8-Oct-2016.) Usage of this theorem is discouraged because it depends on ax-13 2406. Use nfald 2363 instead. (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    &   ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝜑 → Ⅎ𝑥∀𝑦𝜓)
Theorem	nfexd2 2480	Variation on nfexd 2364 which adds the hypothesis that 𝑥 and 𝑦 are distinct in the inner subproof. (Contributed by Mario Carneiro, 8-Oct-2016.) Usage of this theorem is discouraged because it depends on ax-13 2406. Use nfexd 2364 instead. (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    &   ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝜑 → Ⅎ𝑥∃𝑦𝜓)
Theorem	exdistrf 2481	Distribution of existential quantifiers, with a bound-variable hypothesis saying that 𝑦 is not free in 𝜑, but 𝑥 can be free in 𝜑 (and there is no distinct variable condition on 𝑥 and 𝑦). (Contributed by Mario Carneiro, 20-Mar-2013.) (Proof shortened by Wolf Lammen, 14-May-2018.) Usage of this theorem is discouraged because it depends on ax-13 2406. Use exdistr 1977 instead. (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦𝜑)    ⇒   ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) → ∃𝑥(𝜑 ∧ ∃𝑦𝜓))
Theorem	dvelimf 2482	Version of dvelimv 2486 without any variable restrictions. Usage of this theorem is discouraged because it depends on ax-13 2406. (Contributed by NM, 1-Oct-2002.) (Revised by Mario Carneiro, 6-Oct-2016.) (Proof shortened by Wolf Lammen, 11-May-2018.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑧𝜓    &   ⊢ (𝑧 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝜓)
Theorem	dvelimdf 2483	Deduction form of dvelimf 2482. Usage of this theorem is discouraged because it depends on ax-13 2406. (Contributed by NM, 7-Apr-2004.) (Revised by Mario Carneiro, 6-Oct-2016.) (Proof shortened by Wolf Lammen, 11-May-2018.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑧𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    &   ⊢ (𝜑 → Ⅎ𝑧𝜒)    &   ⊢ (𝜑 → (𝑧 = 𝑦 → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (𝜑 → (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝜒))
Theorem	dvelimh 2484	Version of dvelim 2485 without any variable restrictions. Usage of this theorem is discouraged because it depends on ax-13 2406. Check out dvelimhw 2379 for a version requiring fewer axioms. (Contributed by NM, 1-Oct-2002.) (Proof shortened by Wolf Lammen, 11-May-2018.) (New usage is discouraged.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜓 → ∀𝑧𝜓)    &   ⊢ (𝑧 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝜓 → ∀𝑥𝜓))
Theorem	dvelim 2485*	This theorem can be used to eliminate a distinct variable restriction on 𝑥 and 𝑧 and replace it with the "distinctor" ¬ ∀𝑥𝑥 = 𝑦 as an antecedent. 𝜑 normally has 𝑧 free and can be read 𝜑(𝑧), and 𝜓 substitutes 𝑦 for 𝑧 and can be read 𝜑(𝑦). We do not require that 𝑥 and 𝑦 be distinct: if they are not, the distinctor will become false (in multiple-element domains of discourse) and "protect" the consequent. To obtain a closed-theorem form of this inference, prefix the hypotheses with ∀𝑥∀𝑧, conjoin them, and apply dvelimdf 2483. Other variants of this theorem are dvelimh 2484 (with no distinct variable restrictions) and dvelimhw 2379 (that avoids ax-13 2406). Usage of this theorem is discouraged because it depends on ax-13 2406. Check out dvelimhw 2379 for a version requiring fewer axioms. (Contributed by NM, 23-Nov-1994.) (New usage is discouraged.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝑧 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝜓 → ∀𝑥𝜓))
Theorem	dvelimv 2486*	Similar to dvelim 2485 with first hypothesis replaced by a distinct variable condition. Usage of this theorem is discouraged because it depends on ax-13 2406. Check out dvelimhw 2379 for a version requiring fewer axioms. (Contributed by NM, 25-Jul-2015.) (Proof shortened by Wolf Lammen, 30-Apr-2018.) (New usage is discouraged.)
⊢ (𝑧 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝜓 → ∀𝑥𝜓))
Theorem	dvelimnf 2487*	Version of dvelim 2485 using "not free" notation. Usage of this theorem is discouraged because it depends on ax-13 2406. (Contributed by Mario Carneiro, 9-Oct-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝑧 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝜓)
Theorem	dveeq2ALT 2488*	Alternate proof of dveeq2 2412, shorter but requiring ax-11 2194. (Contributed by NM, 2-Jan-2002.) (Revised by NM, 20-Jul-2015.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦))
Theorem	equvini 2489	A variable introduction law for equality. Lemma 15 of [Monk2] p. 109, however we do not require 𝑧 to be distinct from 𝑥 and 𝑦. Usage of this theorem is discouraged because it depends on ax-13 2406. See equvinv 2052 for a shorter proof requiring fewer axioms when 𝑧 is required to be distinct from 𝑥 and 𝑦. (Contributed by NM, 10-Jan-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 16-Sep-2023.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → ∃𝑧(𝑥 = 𝑧 ∧ 𝑧 = 𝑦))
Theorem	equvel 2490	A variable elimination law for equality with no distinct variable requirements. Compare equvini 2489. Usage of this theorem is discouraged because it depends on ax-13 2406. Use equvelv 2054 when possible. (Contributed by NM, 1-Mar-2013.) (Proof shortened by Mario Carneiro, 17-Oct-2016.) (Proof shortened by Wolf Lammen, 15-Jun-2019.) (New usage is discouraged.)
⊢ (∀𝑧(𝑧 = 𝑥 ↔ 𝑧 = 𝑦) → 𝑥 = 𝑦)
Theorem	equs5a 2491	A property related to substitution that unlike equs5 2494 does not require a distinctor antecedent. Usage of this theorem is discouraged because it depends on ax-13 2406. This proof uses ax12 2457, see equs5aALT 2400 for an alternative one using ax-12 2215 but not ax13 2409. Usage of the weaker equs5av 2314 is preferred, which uses ax12v2 2217, but not ax-13 2406. (Contributed by NM, 2-Feb-2007.) (New usage is discouraged.)
⊢ (∃𝑥(𝑥 = 𝑦 ∧ ∀𝑦𝜑) → ∀𝑥(𝑥 = 𝑦 → 𝜑))
Theorem	equs5e 2492	A property related to substitution that unlike equs5 2494 does not require a distinctor antecedent. This proof uses ax12 2457, see equs5eALT 2401 for an alternative one using ax-12 2215 but not ax13 2409. Usage of this theorem is discouraged because it depends on ax-13 2406. (Contributed by NM, 2-Feb-2007.) (Proof shortened by Wolf Lammen, 15-Jan-2018.) (New usage is discouraged.)
⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑦 → ∃𝑦𝜑))
Theorem	equs45f 2493	Two ways of expressing substitution when 𝑦 is not free in 𝜑. The implication "to the left" is equs4 2450 and does not require the nonfreeness hypothesis. Theorem sbalex 2280 replaces the nonfreeness hypothesis with a disjoint variable condition and equs5 2494 replaces it with a distinctor antecedent. (Contributed by NM, 25-Apr-2008.) (Revised by Mario Carneiro, 4-Oct-2016.) Usage of this theorem is discouraged because it depends on ax-13 2406. Use sbalex 2280 instead. (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑))
Theorem	equs5 2494	Lemma used in proofs of substitution properties. If there is a disjoint variable condition on 𝑥, 𝑦, then sbalex 2280 can be used instead; if 𝑦 is not free in 𝜑, then equs45f 2493 can be used. Usage of this theorem is discouraged because it depends on ax-13 2406. (Contributed by NM, 14-May-1993.) (Revised by BJ, 1-Oct-2018.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑)))
Theorem	dveel1 2495*	Quantifier introduction when one pair of variables is disjoint. Usage of this theorem is discouraged because it depends on ax-13 2406. (Contributed by NM, 2-Jan-2002.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦 ∈ 𝑧 → ∀𝑥 𝑦 ∈ 𝑧))
Theorem	dveel2 2496*	Quantifier introduction when one pair of variables is disjoint. Usage of this theorem is discouraged because it depends on ax-13 2406. (Contributed by NM, 2-Jan-2002.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑧 ∈ 𝑦 → ∀𝑥 𝑧 ∈ 𝑦))
Theorem	axc14 2497	Axiom ax-c14 39527 is redundant if we assume ax-5 1933. Remark 9.6 in [Megill] p. 448 (p. 16 of the preprint), regarding axiom scheme C14'. Note that 𝑤 is a dummy variable introduced in the proof. Its purpose is to satisfy the distinct variable requirements of dveel2 2496 and ax-5 1933. By the end of the proof it has vanished, and the final theorem has no distinct variable requirements. Usage of this theorem is discouraged because it depends on ax-13 2406. (Contributed by NM, 29-Jun-1995.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑧 𝑧 = 𝑥 → (¬ ∀𝑧 𝑧 = 𝑦 → (𝑥 ∈ 𝑦 → ∀𝑧 𝑥 ∈ 𝑦)))
Theorem	sb6x 2498	Equivalence involving substitution for a variable not free. Usage of this theorem is discouraged because it depends on ax-13 2406. Usage of sb6 2121 is preferred, which requires fewer axioms. (Contributed by NM, 2-Jun-1993.) (Revised by Mario Carneiro, 4-Oct-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ ([𝑦 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑))
Theorem	sbequ5 2499	Substitution does not change an identical variable specifier. Usage of this theorem is discouraged because it depends on ax-13 2406. (Contributed by NM, 15-May-1993.) (New usage is discouraged.)
⊢ ([𝑤 / 𝑧]∀𝑥 𝑥 = 𝑦 ↔ ∀𝑥 𝑥 = 𝑦)
Theorem	sbequ6 2500	Substitution does not change a distinctor. Usage of this theorem is discouraged because it depends on ax-13 2406. (Contributed by NM, 5-Aug-1993.) (New usage is discouraged.)
⊢ ([𝑤 / 𝑧] ¬ ∀𝑥 𝑥 = 𝑦 ↔ ¬ ∀𝑥 𝑥 = 𝑦)