![]() |
Metamath
Proof Explorer Theorem List (p. 25 of 486) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30848) |
![]() (30849-32371) |
![]() (32372-48589) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cbvald 2401* | Deduction used to change bound variables, using implicit substitution, particularly useful in conjunction with dvelim 2445. Usage of this theorem is discouraged because it depends on ax-13 2366. See cbvaldw 2329 for a version with 𝑥, 𝑦 disjoint, not depending on ax-13 2366. (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 2402* | Deduction used to change bound variables, using implicit substitution, particularly useful in conjunction with dvelim 2445. Usage of this theorem is discouraged because it depends on ax-13 2366. Use the weaker cbvexdw 2330 if possible. (Contributed by NM, 2-Jan-2002.) (Revised by Mario Carneiro, 6-Oct-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑦𝜓) & ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))) ⇒ ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑦𝜒)) | ||
Theorem | cbvaldva 2403* | 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 2366. Use the weaker cbvaldvaw 2034 if possible. (Contributed by David Moews, 1-May-2017.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒)) | ||
Theorem | cbvexdva 2404* | 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 2366. Use the weaker cbvexdvaw 2035 if possible. (Contributed by David Moews, 1-May-2017.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑦𝜒)) | ||
Theorem | cbval2 2405* | Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2366. Use the weaker cbval2v 2334 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 2406* | Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2366. Use the weaker cbvex2v 2335 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 2407* | Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2366. Use the weaker cbval2vw 2036 if possible. (Contributed by NM, 4-Feb-2005.) Remove dependency on ax-10 2130. (Revised by Wolf Lammen, 18-Jul-2021.) (New usage is discouraged.) |
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑧∀𝑤𝜓) | ||
Theorem | cbvex2vv 2408* | Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2366. Use the weaker cbvex2vw 2037 if possible. (Contributed by NM, 26-Jul-1995.) Remove dependency on ax-10 2130. (Revised by Wolf Lammen, 18-Jul-2021.) (New usage is discouraged.) |
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑧∃𝑤𝜓) | ||
Theorem | cbvex4v 2409* | Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2366. Use the weaker cbvex4vw 2038 if possible. (Contributed by NM, 26-Jul-1995.) (New usage is discouraged.) |
⊢ ((𝑥 = 𝑣 ∧ 𝑦 = 𝑢) → (𝜑 ↔ 𝜓)) & ⊢ ((𝑧 = 𝑓 ∧ 𝑤 = 𝑔) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (∃𝑥∃𝑦∃𝑧∃𝑤𝜑 ↔ ∃𝑣∃𝑢∃𝑓∃𝑔𝜒) | ||
Theorem | equs4 2410 | Lemma used in proofs of implicit substitution properties. The converse requires either a disjoint variable condition (sbalex 2231) or a nonfreeness hypothesis (equs45f 2453). Usage of this theorem is discouraged because it depends on ax-13 2366. See equs4v 1996 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 2411 | An equivalence related to implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2366. See equsalvw 2000 and equsalv 2254 for versions with disjoint variable conditions proved from fewer axioms. See also the dual form equsex 2412. (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 2412 | An equivalence related to implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2366. See equsexvw 2001 and equsexv 2255 for versions with disjoint variable conditions proved from fewer axioms. See also the dual form equsal 2411. See equsexALT 2413 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 2413 | Alternate proof of equsex 2412. This proves the result directly, instead of as a corollary of equsal 2411 via equs4 2410. Note in particular that only existential quantifiers appear in the proof and that the only step requiring ax-13 2366 is ax6e 2377. This proof mimics that of equsal 2411 (in particular, note that pm5.32i 573, exbii 1843, 19.41 2224, mpbiran 707 correspond respectively to pm5.74i 270, albii 1814, 19.23 2200, a1bi 361). (Contributed by BJ, 20-Aug-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ 𝜓) | ||
Theorem | equsalh 2414 | An equivalence related to implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2366. See equsalhw 2281 for a version with a disjoint variable condition requiring fewer axioms. (Contributed by NM, 2-Jun-1993.) (New usage is discouraged.) |
⊢ (𝜓 → ∀𝑥𝜓) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜓) | ||
Theorem | equsexh 2415 | An equivalence related to implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2366. See equsexhv 2282 for a version with a disjoint variable condition which does not require ax-13 2366. (Contributed by NM, 5-Aug-1993.) (New usage is discouraged.) |
⊢ (𝜓 → ∀𝑥𝜓) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ 𝜓) | ||
Theorem | axc15 2416 |
Derivation of set.mm's original ax-c15 38600 from ax-c11n 38599 and the shorter
ax-12 2167 that has replaced it.
Theorem ax12 2417 shows the reverse derivation of ax-12 2167 from ax-c15 38600. Normally, axc15 2416 should be used rather than ax-c15 38600, except by theorems specifically studying the latter's properties. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by NM, 2-Feb-2007.) (Proof shortened by Wolf Lammen, 26-Mar-2023.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))) | ||
Theorem | ax12 2417 | Rederivation of Axiom ax-12 2167 from ax12v 2168 (used only via sp 2172), axc11r 2360, and axc15 2416 (on top of Tarski's FOL). Since this version depends on ax-13 2366, usage of the weaker ax12v 2168, ax12w 2122, ax12i 1963 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 2418 | A bidirectional version of axc15 2416. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by NM, 30-Jun-2006.) (New usage is discouraged.) |
⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦) → (𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑))) | ||
Theorem | ax13ALT 2419 | Alternate proof of ax13 2369 from FOL, sp 2172, and axc9 2376. (Contributed by NM, 21-Dec-2015.) (Proof shortened by Wolf Lammen, 31-Jan-2018.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ 𝑥 = 𝑦 → (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧)) | ||
Theorem | axc11n 2420 | Derive set.mm's original ax-c11n 38599 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 2051. Use aecom 2421 instead when this does not lengthen the proof. Usage of this theorem is discouraged because it depends on ax-13 2366. (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 2421 | 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 2366. (Contributed by NM, 10-May-1993.) Change to a biconditional. (Revised by BJ, 26-Sep-2019.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 ↔ ∀𝑦 𝑦 = 𝑥) | ||
Theorem | aecoms 2422 | A commutation rule for identical variable specifiers. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by NM, 10-May-1993.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → 𝜑) ⇒ ⊢ (∀𝑦 𝑦 = 𝑥 → 𝜑) | ||
Theorem | naecoms 2423 | A commutation rule for distinct variable specifiers. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by NM, 2-Jan-2002.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → 𝜑) ⇒ ⊢ (¬ ∀𝑦 𝑦 = 𝑥 → 𝜑) | ||
Theorem | axc11 2424 | Show that ax-c11 38598 can be derived from ax-c11n 38599 in the form of axc11n 2420. Normally, axc11 2424 should be used rather than ax-c11 38598, except by theorems specifically studying the latter's properties. Usage of this theorem is discouraged because it depends on ax-13 2366. Use the weaker axc11v 2251 when possible. (Contributed by NM, 16-May-2008.) (Proof shortened by Wolf Lammen, 21-Apr-2018.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 → ∀𝑦𝜑)) | ||
Theorem | hbae 2425 | All variables are effectively bound in an identical variable specifier. Usage of this theorem is discouraged because it depends on ax-13 2366. Use the weaker hbaev 2055 when possible. (Contributed by NM, 13-May-1993.) (Proof shortened by Wolf Lammen, 21-Apr-2018.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧∀𝑥 𝑥 = 𝑦) | ||
Theorem | hbnae 2426 | 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 2366. Use the weaker hbnaev 2058 when possible. (Contributed by NM, 13-May-1993.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑧 ¬ ∀𝑥 𝑥 = 𝑦) | ||
Theorem | nfae 2427 | All variables are effectively bound in an identical variable specifier. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by Mario Carneiro, 11-Aug-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑧∀𝑥 𝑥 = 𝑦 | ||
Theorem | nfnae 2428 | All variables are effectively bound in a distinct variable specifier. Usage of this theorem is discouraged because it depends on ax-13 2366. Use the weaker nfnaew 2138 when possible. (Contributed by Mario Carneiro, 11-Aug-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑧 ¬ ∀𝑥 𝑥 = 𝑦 | ||
Theorem | hbnaes 2429 | Rule that applies hbnae 2426 to antecedent. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by NM, 15-May-1993.) (New usage is discouraged.) |
⊢ (∀𝑧 ¬ ∀𝑥 𝑥 = 𝑦 → 𝜑) ⇒ ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → 𝜑) | ||
Theorem | axc16i 2430* | Inference with axc16 2248 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 2366. Use axc16 2248 instead. (New usage is discouraged.) |
⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜓)) & ⊢ (𝜓 → ∀𝑥𝜓) ⇒ ⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑥𝜑)) | ||
Theorem | axc16nfALT 2431* | Alternate proof of axc16nf 2250, shorter but requiring ax-11 2147 and ax-13 2366. (Contributed by Mario Carneiro, 7-Oct-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → Ⅎ𝑧𝜑) | ||
Theorem | dral2 2432 | 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 2366. Usage of albidv 1916 is preferred, which requires fewer axioms. (Contributed by NM, 27-Feb-2005.) Allow a shortening of dral1 2433. (Revised by Wolf Lammen, 4-Mar-2018.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑧𝜑 ↔ ∀𝑧𝜓)) | ||
Theorem | dral1 2433 | 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 2366. Use the weaker dral1v 2361 if possible. (Contributed by NM, 24-Nov-1994.) Remove dependency on ax-11 2147. (Revised by Wolf Lammen, 6-Sep-2018.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 ↔ ∀𝑦𝜓)) | ||
Theorem | dral1ALT 2434 | Alternate proof of dral1 2433, shorter but requiring ax-11 2147. (Contributed by NM, 24-Nov-1994.) (Proof shortened by Wolf Lammen, 22-Apr-2018.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 ↔ ∀𝑦𝜓)) | ||
Theorem | drex1 2435 | 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 2366. Use the weaker drex1v 2363 if possible. (Contributed by NM, 27-Feb-2005.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 𝑥 = 𝑦 → (∃𝑥𝜑 ↔ ∃𝑦𝜓)) | ||
Theorem | drex2 2436 | 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 2366. Usage of exbidv 1917 is preferred, which requires fewer axioms. (Contributed by NM, 27-Feb-2005.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 𝑥 = 𝑦 → (∃𝑧𝜑 ↔ ∃𝑧𝜓)) | ||
Theorem | drnf1 2437 | 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 2366. Use drnf1v 2364 instead. (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 𝑥 = 𝑦 → (Ⅎ𝑥𝜑 ↔ Ⅎ𝑦𝜓)) | ||
Theorem | drnf2 2438 | 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 2366. Use nfbidv 1918 instead. (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 𝑥 = 𝑦 → (Ⅎ𝑧𝜑 ↔ Ⅎ𝑧𝜓)) | ||
Theorem | nfald2 2439 | Variation on nfald 2317 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 2366. Use nfald 2317 instead. (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 & ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥𝜓) ⇒ ⊢ (𝜑 → Ⅎ𝑥∀𝑦𝜓) | ||
Theorem | nfexd2 2440 | Variation on nfexd 2318 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 2366. Use nfexd 2318 instead. (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 & ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥𝜓) ⇒ ⊢ (𝜑 → Ⅎ𝑥∃𝑦𝜓) | ||
Theorem | exdistrf 2441 | 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 2366. Use exdistr 1951 instead. (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦𝜑) ⇒ ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) → ∃𝑥(𝜑 ∧ ∃𝑦𝜓)) | ||
Theorem | dvelimf 2442 | Version of dvelimv 2446 without any variable restrictions. Usage of this theorem is discouraged because it depends on ax-13 2366. (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 2443 | Deduction form of dvelimf 2442. Usage of this theorem is discouraged because it depends on ax-13 2366. (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 2444 | Version of dvelim 2445 without any variable restrictions. Usage of this theorem is discouraged because it depends on ax-13 2366. Check out dvelimhw 2336 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 2445* |
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 2443. Other variants of this theorem are dvelimh 2444 (with no distinct variable restrictions) and dvelimhw 2336 (that avoids ax-13 2366). Usage of this theorem is discouraged because it depends on ax-13 2366. Check out dvelimhw 2336 for a version requiring fewer axioms. (Contributed by NM, 23-Nov-1994.) (New usage is discouraged.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝑧 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝜓 → ∀𝑥𝜓)) | ||
Theorem | dvelimv 2446* | Similar to dvelim 2445 with first hypothesis replaced by a distinct variable condition. Usage of this theorem is discouraged because it depends on ax-13 2366. Check out dvelimhw 2336 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 2447* | Version of dvelim 2445 using "not free" notation. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by Mario Carneiro, 9-Oct-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝑧 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝜓) | ||
Theorem | dveeq2ALT 2448* | Alternate proof of dveeq2 2372, shorter but requiring ax-11 2147. (Contributed by NM, 2-Jan-2002.) (Revised by NM, 20-Jul-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦)) | ||
Theorem | equvini 2449 | 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 2366. See equvinv 2025 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 2450 | A variable elimination law for equality with no distinct variable requirements. Compare equvini 2449. Usage of this theorem is discouraged because it depends on ax-13 2366. Use equvelv 2027 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 2451 | A property related to substitution that unlike equs5 2454 does not require a distinctor antecedent. Usage of this theorem is discouraged because it depends on ax-13 2366. This proof uses ax12 2417, see equs5aALT 2358 for an alternative one using ax-12 2167 but not ax13 2369. Usage of the weaker equs5av 2266 is preferred, which uses ax12v2 2169, but not ax-13 2366. (Contributed by NM, 2-Feb-2007.) (New usage is discouraged.) |
⊢ (∃𝑥(𝑥 = 𝑦 ∧ ∀𝑦𝜑) → ∀𝑥(𝑥 = 𝑦 → 𝜑)) | ||
Theorem | equs5e 2452 | A property related to substitution that unlike equs5 2454 does not require a distinctor antecedent. This proof uses ax12 2417, see equs5eALT 2359 for an alternative one using ax-12 2167 but not ax13 2369. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by NM, 2-Feb-2007.) (Proof shortened by Wolf Lammen, 15-Jan-2018.) (New usage is discouraged.) |
⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑦 → ∃𝑦𝜑)) | ||
Theorem | equs45f 2453 | Two ways of expressing substitution when 𝑦 is not free in 𝜑. The implication "to the left" is equs4 2410 and does not require the nonfreeness hypothesis. Theorem sbalex 2231 replaces the nonfreeness hypothesis with a disjoint variable condition and equs5 2454 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 2366. Use sbalex 2231 instead. (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑)) | ||
Theorem | equs5 2454 | Lemma used in proofs of substitution properties. If there is a disjoint variable condition on 𝑥, 𝑦, then sbalex 2231 can be used instead; if 𝑦 is not free in 𝜑, then equs45f 2453 can be used. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by NM, 14-May-1993.) (Revised by BJ, 1-Oct-2018.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑))) | ||
Theorem | dveel1 2455* | Quantifier introduction when one pair of variables is disjoint. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by NM, 2-Jan-2002.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦 ∈ 𝑧 → ∀𝑥 𝑦 ∈ 𝑧)) | ||
Theorem | dveel2 2456* | Quantifier introduction when one pair of variables is disjoint. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by NM, 2-Jan-2002.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑧 ∈ 𝑦 → ∀𝑥 𝑧 ∈ 𝑦)) | ||
Theorem | axc14 2457 |
Axiom ax-c14 38602 is redundant if we assume ax-5 1906.
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 2456 and ax-5 1906. 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 2366. (Contributed by NM, 29-Jun-1995.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑧 𝑧 = 𝑥 → (¬ ∀𝑧 𝑧 = 𝑦 → (𝑥 ∈ 𝑦 → ∀𝑧 𝑥 ∈ 𝑦))) | ||
Theorem | sb6x 2458 | Equivalence involving substitution for a variable not free. Usage of this theorem is discouraged because it depends on ax-13 2366. Usage of sb6 2081 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 2459 | Substitution does not change an identical variable specifier. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by NM, 15-May-1993.) (New usage is discouraged.) |
⊢ ([𝑤 / 𝑧]∀𝑥 𝑥 = 𝑦 ↔ ∀𝑥 𝑥 = 𝑦) | ||
Theorem | sbequ6 2460 | Substitution does not change a distinctor. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by NM, 5-Aug-1993.) (New usage is discouraged.) |
⊢ ([𝑤 / 𝑧] ¬ ∀𝑥 𝑥 = 𝑦 ↔ ¬ ∀𝑥 𝑥 = 𝑦) | ||
Theorem | sb5rf 2461 | Reversed substitution. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by NM, 3-Feb-2005.) (Revised by Mario Carneiro, 6-Oct-2016.) (Proof shortened by Wolf Lammen, 20-Sep-2018.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (𝜑 ↔ ∃𝑦(𝑦 = 𝑥 ∧ [𝑦 / 𝑥]𝜑)) | ||
Theorem | sb6rf 2462 | Reversed substitution. For a version requiring disjoint variables, but fewer axioms, see sb6rfv 2348. Usage of this theorem is discouraged because it depends on ax-13 2366. Use the weaker sb6rfv 2348 if possible. (Contributed by NM, 1-Aug-1993.) (Revised by Mario Carneiro, 6-Oct-2016.) (Proof shortened by Wolf Lammen, 21-Sep-2018.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (𝜑 ↔ ∀𝑦(𝑦 = 𝑥 → [𝑦 / 𝑥]𝜑)) | ||
Theorem | ax12vALT 2463* | Alternate proof of ax12v2 2169, shorter, but depending on more axioms. (Contributed by NM, 5-Aug-1993.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) | ||
Theorem | 2ax6elem 2464 | We can always find values matching 𝑥 and 𝑦, as long as they are represented by distinct variables. This theorem merges two ax6e 2377 instances ∃𝑧𝑧 = 𝑥 and ∃𝑤𝑤 = 𝑦 into a common expression. Alan Sare contributed a variant of this theorem with distinct variable conditions before, see ax6e2nd 44271. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by Wolf Lammen, 27-Sep-2018.) (New usage is discouraged.) |
⊢ (¬ ∀𝑤 𝑤 = 𝑧 → ∃𝑧∃𝑤(𝑧 = 𝑥 ∧ 𝑤 = 𝑦)) | ||
Theorem | 2ax6e 2465* | We can always find values matching 𝑥 and 𝑦, as long as they are represented by distinct variables. Version of 2ax6elem 2464 with a distinct variable constraint. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by Wolf Lammen, 28-Sep-2018.) (Proof shortened by Wolf Lammen, 3-Oct-2023.) (New usage is discouraged.) |
⊢ ∃𝑧∃𝑤(𝑧 = 𝑥 ∧ 𝑤 = 𝑦) | ||
Theorem | 2sb5rf 2466* | Reversed double substitution. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by NM, 3-Feb-2005.) (Revised by Mario Carneiro, 6-Oct-2016.) Remove distinct variable constraints. (Revised by Wolf Lammen, 28-Sep-2018.) (New usage is discouraged.) |
⊢ Ⅎ𝑧𝜑 & ⊢ Ⅎ𝑤𝜑 ⇒ ⊢ (𝜑 ↔ ∃𝑧∃𝑤((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑)) | ||
Theorem | 2sb6rf 2467* | Reversed double substitution. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by NM, 3-Feb-2005.) (Revised by Mario Carneiro, 6-Oct-2016.) Remove variable constraints. (Revised by Wolf Lammen, 28-Sep-2018.) (Proof shortened by Wolf Lammen, 13-Apr-2023.) (New usage is discouraged.) |
⊢ Ⅎ𝑧𝜑 & ⊢ Ⅎ𝑤𝜑 ⇒ ⊢ (𝜑 ↔ ∀𝑧∀𝑤((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) → [𝑧 / 𝑥][𝑤 / 𝑦]𝜑)) | ||
Theorem | sbel2x 2468* | Elimination of double substitution. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 29-Sep-2018.) (New usage is discouraged.) |
⊢ (𝜑 ↔ ∃𝑥∃𝑦((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) ∧ [𝑦 / 𝑤][𝑥 / 𝑧]𝜑)) | ||
Theorem | sb4b 2469 | Simplified definition of substitution when variables are distinct. Version of sb6 2081 with a distinctor antecedent. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by NM, 27-May-1997.) Revise df-sb 2061. (Revised by Wolf Lammen, 21-Feb-2024.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑡 → ([𝑡 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑡 → 𝜑))) | ||
Theorem | sb3b 2470 | Simplified definition of substitution when variables are distinct. This is the biconditional strengthening of sb3 2471. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by BJ, 6-Oct-2018.) Shorten sb3 2471. (Revised by Wolf Lammen, 21-Feb-2021.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) | ||
Theorem | sb3 2471 | One direction of a simplified definition of substitution when variables are distinct. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 21-Feb-2024.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → [𝑦 / 𝑥]𝜑)) | ||
Theorem | sb1 2472 | One direction of a simplified definition of substitution. The converse requires either a disjoint variable condition (sb5 2263) or a nonfreeness hypothesis (sb5f 2492). Usage of this theorem is discouraged because it depends on ax-13 2366. Use the weaker sb1v 2083 when possible. (Contributed by NM, 13-May-1993.) Revise df-sb 2061. (Revised by Wolf Lammen, 21-Feb-2024.) (New usage is discouraged.) |
⊢ ([𝑦 / 𝑥]𝜑 → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) | ||
Theorem | sb2 2473 | One direction of a simplified definition of substitution. The converse requires either a disjoint variable condition (sb6 2081) or a nonfreeness hypothesis (sb6f 2491). Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by NM, 13-May-1993.) Revise df-sb 2061. (Revised by Wolf Lammen, 26-Jul-2023.) (New usage is discouraged.) |
⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → [𝑦 / 𝑥]𝜑) | ||
Theorem | sb4a 2474 | A version of one implication of sb4b 2469 that does not require a distinctor antecedent. Usage of this theorem is discouraged because it depends on ax-13 2366. Use the weaker sb4av 2232 when possible. (Contributed by NM, 2-Feb-2007.) Revise df-sb 2061. (Revised by Wolf Lammen, 28-Jul-2023.) (New usage is discouraged.) |
⊢ ([𝑡 / 𝑥]∀𝑡𝜑 → ∀𝑥(𝑥 = 𝑡 → 𝜑)) | ||
Theorem | dfsb1 2475 | Alternate definition of substitution. Remark 9.1 in [Megill] p. 447 (p. 15 of the preprint). This was the original definition before df-sb 2061. Note that it does not require dummy variables in its definiens; this is done by having 𝑥 free in the first conjunct and bound in the second. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by BJ, 9-Jul-2023.) Revise df-sb 2061. (Revised by Wolf Lammen, 29-Jul-2023.) (New usage is discouraged.) |
⊢ ([𝑦 / 𝑥]𝜑 ↔ ((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) | ||
Theorem | hbsb2 2476 | Bound-variable hypothesis builder for substitution. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by NM, 14-May-1993.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑)) | ||
Theorem | nfsb2 2477 | Bound-variable hypothesis builder for substitution. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by Mario Carneiro, 4-Oct-2016.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥[𝑦 / 𝑥]𝜑) | ||
Theorem | hbsb2a 2478 | Special case of a bound-variable hypothesis builder for substitution. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by NM, 2-Feb-2007.) (New usage is discouraged.) |
⊢ ([𝑦 / 𝑥]∀𝑦𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑) | ||
Theorem | sb4e 2479 | One direction of a simplified definition of substitution that unlike sb4b 2469 does not require a distinctor antecedent. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by NM, 2-Feb-2007.) (New usage is discouraged.) |
⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥(𝑥 = 𝑦 → ∃𝑦𝜑)) | ||
Theorem | hbsb2e 2480 | Special case of a bound-variable hypothesis builder for substitution. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by NM, 2-Feb-2007.) (New usage is discouraged.) |
⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]∃𝑦𝜑) | ||
Theorem | hbsb3 2481 | If 𝑦 is not free in 𝜑, 𝑥 is not free in [𝑦 / 𝑥]𝜑. Usage of this theorem is discouraged because it depends on ax-13 2366. Check out bj-hbsb3v 36533 for a weaker version requiring fewer axioms. (Contributed by NM, 14-May-1993.) (New usage is discouraged.) |
⊢ (𝜑 → ∀𝑦𝜑) ⇒ ⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑) | ||
Theorem | nfs1 2482 | If 𝑦 is not free in 𝜑, 𝑥 is not free in [𝑦 / 𝑥]𝜑. Usage of this theorem is discouraged because it depends on ax-13 2366. Check out nfs1v 2146 for a version requiring fewer axioms. (Contributed by Mario Carneiro, 11-Aug-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ Ⅎ𝑥[𝑦 / 𝑥]𝜑 | ||
Theorem | axc16ALT 2483* | Alternate proof of axc16 2248, shorter but requiring ax-10 2130, ax-11 2147, ax-13 2366 and using df-nf 1779 and df-sb 2061. (Contributed by NM, 17-May-2008.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑥𝜑)) | ||
Theorem | axc16gALT 2484* | Alternate proof of axc16g 2247 that uses df-sb 2061 and requires ax-10 2130, ax-11 2147, ax-13 2366. (Contributed by NM, 15-May-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑧𝜑)) | ||
Theorem | equsb1 2485 | Substitution applied to an atomic wff. Usage of this theorem is discouraged because it depends on ax-13 2366. Use the weaker equsb1v 2096 if possible. (Contributed by NM, 10-May-1993.) (New usage is discouraged.) |
⊢ [𝑦 / 𝑥]𝑥 = 𝑦 | ||
Theorem | equsb2 2486 | Substitution applied to an atomic wff. Usage of this theorem is discouraged because it depends on ax-13 2366. Check out equsb1v 2096 for a version requiring fewer axioms. (Contributed by NM, 10-May-1993.) (New usage is discouraged.) |
⊢ [𝑦 / 𝑥]𝑦 = 𝑥 | ||
Theorem | dfsb2 2487 | An alternate definition of proper substitution that, like dfsb1 2475, mixes free and bound variables to avoid distinct variable requirements. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by NM, 17-Feb-2005.) (New usage is discouraged.) |
⊢ ([𝑦 / 𝑥]𝜑 ↔ ((𝑥 = 𝑦 ∧ 𝜑) ∨ ∀𝑥(𝑥 = 𝑦 → 𝜑))) | ||
Theorem | dfsb3 2488 | An alternate definition of proper substitution df-sb 2061 that uses only primitive connectives (no defined terms) on the right-hand side. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by NM, 6-Mar-2007.) (New usage is discouraged.) |
⊢ ([𝑦 / 𝑥]𝜑 ↔ ((𝑥 = 𝑦 → ¬ 𝜑) → ∀𝑥(𝑥 = 𝑦 → 𝜑))) | ||
Theorem | drsb1 2489 | 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 2366. (Contributed by NM, 2-Jun-1993.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → ([𝑧 / 𝑥]𝜑 ↔ [𝑧 / 𝑦]𝜑)) | ||
Theorem | sb2ae 2490* | In the case of two successive substitutions for two always equal variables, the second substitution has no effect. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by BJ and WL, 9-Aug-2023.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ↔ [𝑣 / 𝑦]𝜑)) | ||
Theorem | sb6f 2491 | Equivalence for substitution when 𝑦 is not free in 𝜑. The implication "to the left" is sb2 2473 and does not require the nonfreeness hypothesis. Theorem sb6 2081 replaces the nonfreeness hypothesis with a disjoint variable condition on 𝑥, 𝑦 and requires fewer axioms. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by NM, 2-Jun-1993.) (Revised by Mario Carneiro, 4-Oct-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ ([𝑦 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑)) | ||
Theorem | sb5f 2492 | Equivalence for substitution when 𝑦 is not free in 𝜑. The implication "to the right" is sb1 2472 and does not require the nonfreeness hypothesis. Theorem sb5 2263 replaces the nonfreeness hypothesis with a disjoint variable condition on 𝑥, 𝑦 and requires fewer axioms. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 4-Oct-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) | ||
Theorem | nfsb4t 2493 | A variable not free in a proposition remains so after substitution in that proposition with a distinct variable (closed form of nfsb4 2494). Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by NM, 7-Apr-2004.) (Revised by Mario Carneiro, 4-Oct-2016.) (Proof shortened by Wolf Lammen, 11-May-2018.) (New usage is discouraged.) |
⊢ (∀𝑥Ⅎ𝑧𝜑 → (¬ ∀𝑧 𝑧 = 𝑦 → Ⅎ𝑧[𝑦 / 𝑥]𝜑)) | ||
Theorem | nfsb4 2494 | A variable not free in a proposition remains so after substitution in that proposition with a distinct variable (inference associated with nfsb4t 2493). Theorem nfsb 2517 replaces the distinctor antecedent with a disjoint variable condition. See nfsbv 2319 for a weaker version of nfsb 2517 not requiring ax-13 2366. (Contributed by NM, 14-May-1993.) (Revised by Mario Carneiro, 4-Oct-2016.) Usage of this theorem is discouraged because it depends on ax-13 2366. Use nfsbv 2319 instead. (New usage is discouraged.) |
⊢ Ⅎ𝑧𝜑 ⇒ ⊢ (¬ ∀𝑧 𝑧 = 𝑦 → Ⅎ𝑧[𝑦 / 𝑥]𝜑) | ||
Theorem | sbequ8 2495 | Elimination of equality from antecedent after substitution. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by NM, 5-Aug-1993.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 28-Jul-2018.) Revise df-sb 2061. (Revised by Wolf Lammen, 28-Jul-2023.) (New usage is discouraged.) |
⊢ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥](𝑥 = 𝑦 → 𝜑)) | ||
Theorem | sbie 2496 | Conversion of implicit substitution to explicit substitution. For versions requiring disjoint variables, but fewer axioms, see sbiev 2304 and sbievw 2088. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by NM, 30-Jun-1994.) (Revised by Mario Carneiro, 4-Oct-2016.) (Proof shortened by Wolf Lammen, 13-Jul-2019.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓) | ||
Theorem | sbied 2497 | Conversion of implicit substitution to explicit substitution (deduction version of sbie 2496) Usage of this theorem is discouraged because it depends on ax-13 2366. See sbiedw 2305, sbiedvw 2089 for variants using disjoint variables, but requiring fewer axioms. (Contributed by NM, 30-Jun-1994.) (Revised by Mario Carneiro, 4-Oct-2016.) (Proof shortened by Wolf Lammen, 24-Jun-2018.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝜒) & ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))) ⇒ ⊢ (𝜑 → ([𝑦 / 𝑥]𝜓 ↔ 𝜒)) | ||
Theorem | sbiedv 2498* | Conversion of implicit substitution to explicit substitution (deduction version of sbie 2496). Usage of this theorem is discouraged because it depends on ax-13 2366. Use the weaker sbiedvw 2089 when possible. (Contributed by NM, 7-Jan-2017.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ([𝑦 / 𝑥]𝜓 ↔ 𝜒)) | ||
Theorem | 2sbiev 2499* | Conversion of double implicit substitution to explicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2366. See 2sbievw 2090 for a version with extra disjoint variables, but based on fewer axioms. (Contributed by AV, 29-Jul-2023.) (New usage is discouraged.) |
⊢ ((𝑥 = 𝑡 ∧ 𝑦 = 𝑢) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ([𝑡 / 𝑥][𝑢 / 𝑦]𝜑 ↔ 𝜓) | ||
Theorem | sbcom3 2500 | Substituting 𝑦 for 𝑥 and then 𝑧 for 𝑦 is equivalent to substituting 𝑧 for both 𝑥 and 𝑦. Usage of this theorem is discouraged because it depends on ax-13 2366. For a version requiring a disjoint variable, but fewer axioms, see sbcom3vv 2091. (Contributed by Giovanni Mascellani, 8-Apr-2018.) Remove dependency on ax-11 2147. (Revised by Wolf Lammen, 16-Sep-2018.) (Proof shortened by Wolf Lammen, 16-Sep-2018.) (New usage is discouraged.) |
⊢ ([𝑧 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝑧 / 𝑦][𝑧 / 𝑥]𝜑) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |