Home | Metamath
Proof Explorer Theorem List (p. 25 of 470) | < 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: | Metamath Proof Explorer
(1-29658) |
Hilbert Space Explorer
(29659-31181) |
Users' Mathboxes
(31182-46997) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cbv1 2401 | Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2371. See cbv1v 2333 with disjoint variable conditions, not depending on ax-13 2371. (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 2402 | Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2371. See cbv2w 2334 with disjoint variable conditions, not depending on ax-13 2371. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 3-Oct-2016.) Format hypotheses to common style, avoid ax-10 2137. (Revised by Wolf Lammen, 10-Sep-2023.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑦𝜓) & ⊢ (𝜑 → Ⅎ𝑥𝜒) & ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))) ⇒ ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒)) | ||
Theorem | cbv3h 2403 | Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2371. Use the weaker cbv3hv 2337 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 2404 | Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2371. (Contributed by NM, 11-May-1993.) (Proof shortened by Wolf Lammen, 13-May-2018.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → ∀𝑦𝜓)) & ⊢ (𝜑 → (𝜒 → ∀𝑥𝜒)) & ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 → 𝜒))) ⇒ ⊢ (∀𝑥∀𝑦𝜑 → (∀𝑥𝜓 → ∀𝑦𝜒)) | ||
Theorem | cbv2h 2405 | Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2371. (Contributed by NM, 11-May-1993.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → ∀𝑦𝜓)) & ⊢ (𝜑 → (𝜒 → ∀𝑥𝜒)) & ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))) ⇒ ⊢ (∀𝑥∀𝑦𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒)) | ||
Theorem | cbvald 2406* | Deduction used to change bound variables, using implicit substitution, particularly useful in conjunction with dvelim 2450. Usage of this theorem is discouraged because it depends on ax-13 2371. See cbvaldw 2335 for a version with 𝑥, 𝑦 disjoint, not depending on ax-13 2371. (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 2407* | Deduction used to change bound variables, using implicit substitution, particularly useful in conjunction with dvelim 2450. Usage of this theorem is discouraged because it depends on ax-13 2371. Use the weaker cbvexdw 2336 if possible. (Contributed by NM, 2-Jan-2002.) (Revised by Mario Carneiro, 6-Oct-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑦𝜓) & ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))) ⇒ ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑦𝜒)) | ||
Theorem | cbvaldva 2408* | 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 2371. Use the weaker cbvaldvaw 2041 if possible. (Contributed by David Moews, 1-May-2017.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒)) | ||
Theorem | cbvexdva 2409* | 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 2371. Use the weaker cbvexdvaw 2042 if possible. (Contributed by David Moews, 1-May-2017.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑦𝜒)) | ||
Theorem | cbval2 2410* | Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2371. Use the weaker cbval2v 2340 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 2411* | Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2371. Use the weaker cbvex2v 2341 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 2412* | Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2371. Use the weaker cbval2vw 2043 if possible. (Contributed by NM, 4-Feb-2005.) Remove dependency on ax-10 2137. (Revised by Wolf Lammen, 18-Jul-2021.) (New usage is discouraged.) |
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑧∀𝑤𝜓) | ||
Theorem | cbvex2vv 2413* | Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2371. Use the weaker cbvex2vw 2044 if possible. (Contributed by NM, 26-Jul-1995.) Remove dependency on ax-10 2137. (Revised by Wolf Lammen, 18-Jul-2021.) (New usage is discouraged.) |
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑧∃𝑤𝜓) | ||
Theorem | cbvex4v 2414* | Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2371. Use the weaker cbvex4vw 2045 if possible. (Contributed by NM, 26-Jul-1995.) (New usage is discouraged.) |
⊢ ((𝑥 = 𝑣 ∧ 𝑦 = 𝑢) → (𝜑 ↔ 𝜓)) & ⊢ ((𝑧 = 𝑓 ∧ 𝑤 = 𝑔) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (∃𝑥∃𝑦∃𝑧∃𝑤𝜑 ↔ ∃𝑣∃𝑢∃𝑓∃𝑔𝜒) | ||
Theorem | equs4 2415 | Lemma used in proofs of implicit substitution properties. The converse requires either a disjoint variable condition (sbalex 2235) or a nonfreeness hypothesis (equs45f 2458). Usage of this theorem is discouraged because it depends on ax-13 2371. See equs4v 2003 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 2416 | An equivalence related to implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2371. See equsalvw 2007 and equsalv 2259 for versions with disjoint variable conditions proved from fewer axioms. See also the dual form equsex 2417. (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 2417 | An equivalence related to implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2371. See equsexvw 2008 and equsexv 2260 for versions with disjoint variable conditions proved from fewer axioms. See also the dual form equsal 2416. See equsexALT 2418 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 2418 | Alternate proof of equsex 2417. This proves the result directly, instead of as a corollary of equsal 2416 via equs4 2415. Note in particular that only existential quantifiers appear in the proof and that the only step requiring ax-13 2371 is ax6e 2382. This proof mimics that of equsal 2416 (in particular, note that pm5.32i 575, exbii 1850, 19.41 2228, mpbiran 707 correspond respectively to pm5.74i 270, albii 1821, 19.23 2204, a1bi 362). (Contributed by BJ, 20-Aug-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ 𝜓) | ||
Theorem | equsalh 2419 | An equivalence related to implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2371. See equsalhw 2288 for a version with a disjoint variable condition requiring fewer axioms. (Contributed by NM, 2-Jun-1993.) (New usage is discouraged.) |
⊢ (𝜓 → ∀𝑥𝜓) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜓) | ||
Theorem | equsexh 2420 | An equivalence related to implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2371. See equsexhv 2289 for a version with a disjoint variable condition which does not require ax-13 2371. (Contributed by NM, 5-Aug-1993.) (New usage is discouraged.) |
⊢ (𝜓 → ∀𝑥𝜓) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ 𝜓) | ||
Theorem | axc15 2421 |
Derivation of set.mm's original ax-c15 37246 from ax-c11n 37245 and the shorter
ax-12 2171 that has replaced it.
Theorem ax12 2422 shows the reverse derivation of ax-12 2171 from ax-c15 37246. Normally, axc15 2421 should be used rather than ax-c15 37246, except by theorems specifically studying the latter's properties. Usage of this theorem is discouraged because it depends on ax-13 2371. (Contributed by NM, 2-Feb-2007.) (Proof shortened by Wolf Lammen, 26-Mar-2023.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))) | ||
Theorem | ax12 2422 | Rederivation of Axiom ax-12 2171 from ax12v 2172 (used only via sp 2176) , axc11r 2365, and axc15 2421 (on top of Tarski's FOL). Since this version depends on ax-13 2371, usage of the weaker ax12v 2172, ax12w 2129, ax12i 1970 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 2423 | A bidirectional version of axc15 2421. Usage of this theorem is discouraged because it depends on ax-13 2371. (Contributed by NM, 30-Jun-2006.) (New usage is discouraged.) |
⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦) → (𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑))) | ||
Theorem | ax13ALT 2424 | Alternate proof of ax13 2374 from FOL, sp 2176, and axc9 2381. (Contributed by NM, 21-Dec-2015.) (Proof shortened by Wolf Lammen, 31-Jan-2018.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ 𝑥 = 𝑦 → (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧)) | ||
Theorem | axc11n 2425 | Derive set.mm's original ax-c11n 37245 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 2058. Use aecom 2426 instead when this does not lengthen the proof. Usage of this theorem is discouraged because it depends on ax-13 2371. (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 2426 | 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 2371. (Contributed by NM, 10-May-1993.) Change to a biconditional. (Revised by BJ, 26-Sep-2019.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 ↔ ∀𝑦 𝑦 = 𝑥) | ||
Theorem | aecoms 2427 | A commutation rule for identical variable specifiers. Usage of this theorem is discouraged because it depends on ax-13 2371. (Contributed by NM, 10-May-1993.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → 𝜑) ⇒ ⊢ (∀𝑦 𝑦 = 𝑥 → 𝜑) | ||
Theorem | naecoms 2428 | A commutation rule for distinct variable specifiers. Usage of this theorem is discouraged because it depends on ax-13 2371. (Contributed by NM, 2-Jan-2002.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → 𝜑) ⇒ ⊢ (¬ ∀𝑦 𝑦 = 𝑥 → 𝜑) | ||
Theorem | axc11 2429 | Show that ax-c11 37244 can be derived from ax-c11n 37245 in the form of axc11n 2425. Normally, axc11 2429 should be used rather than ax-c11 37244, except by theorems specifically studying the latter's properties. Usage of this theorem is discouraged because it depends on ax-13 2371. Use the weaker axc11v 2256 when possible. (Contributed by NM, 16-May-2008.) (Proof shortened by Wolf Lammen, 21-Apr-2018.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 → ∀𝑦𝜑)) | ||
Theorem | hbae 2430 | All variables are effectively bound in an identical variable specifier. Usage of this theorem is discouraged because it depends on ax-13 2371. Use the weaker hbaev 2062 when possible. (Contributed by NM, 13-May-1993.) (Proof shortened by Wolf Lammen, 21-Apr-2018.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧∀𝑥 𝑥 = 𝑦) | ||
Theorem | hbnae 2431 | 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 2371. Use the weaker hbnaev 2065 when possible. (Contributed by NM, 13-May-1993.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑧 ¬ ∀𝑥 𝑥 = 𝑦) | ||
Theorem | nfae 2432 | All variables are effectively bound in an identical variable specifier. Usage of this theorem is discouraged because it depends on ax-13 2371. (Contributed by Mario Carneiro, 11-Aug-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑧∀𝑥 𝑥 = 𝑦 | ||
Theorem | nfnae 2433 | All variables are effectively bound in a distinct variable specifier. Usage of this theorem is discouraged because it depends on ax-13 2371. Use the weaker nfnaew 2145 when possible. (Contributed by Mario Carneiro, 11-Aug-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑧 ¬ ∀𝑥 𝑥 = 𝑦 | ||
Theorem | hbnaes 2434 | Rule that applies hbnae 2431 to antecedent. Usage of this theorem is discouraged because it depends on ax-13 2371. (Contributed by NM, 15-May-1993.) (New usage is discouraged.) |
⊢ (∀𝑧 ¬ ∀𝑥 𝑥 = 𝑦 → 𝜑) ⇒ ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → 𝜑) | ||
Theorem | axc16i 2435* | Inference with axc16 2253 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 2371. Use axc16 2253 instead. (New usage is discouraged.) |
⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜓)) & ⊢ (𝜓 → ∀𝑥𝜓) ⇒ ⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑥𝜑)) | ||
Theorem | axc16nfALT 2436* | Alternate proof of axc16nf 2255, shorter but requiring ax-11 2154 and ax-13 2371. (Contributed by Mario Carneiro, 7-Oct-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → Ⅎ𝑧𝜑) | ||
Theorem | dral2 2437 | 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 2371. Usage of albidv 1923 is preferred, which requires fewer axioms. (Contributed by NM, 27-Feb-2005.) Allow a shortening of dral1 2438. (Revised by Wolf Lammen, 4-Mar-2018.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑧𝜑 ↔ ∀𝑧𝜓)) | ||
Theorem | dral1 2438 | 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 2371. Use the weaker dral1v 2366 if possible. (Contributed by NM, 24-Nov-1994.) Remove dependency on ax-11 2154. (Revised by Wolf Lammen, 6-Sep-2018.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 ↔ ∀𝑦𝜓)) | ||
Theorem | dral1ALT 2439 | Alternate proof of dral1 2438, shorter but requiring ax-11 2154. (Contributed by NM, 24-Nov-1994.) (Proof shortened by Wolf Lammen, 22-Apr-2018.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 ↔ ∀𝑦𝜓)) | ||
Theorem | drex1 2440 | 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 2371. Use the weaker drex1v 2368 if possible. (Contributed by NM, 27-Feb-2005.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 𝑥 = 𝑦 → (∃𝑥𝜑 ↔ ∃𝑦𝜓)) | ||
Theorem | drex2 2441 | 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 2371. Usage of exbidv 1924 is preferred, which requires fewer axioms. (Contributed by NM, 27-Feb-2005.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 𝑥 = 𝑦 → (∃𝑧𝜑 ↔ ∃𝑧𝜓)) | ||
Theorem | drnf1 2442 | 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 2371. Use drnf1v 2369 instead. (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 𝑥 = 𝑦 → (Ⅎ𝑥𝜑 ↔ Ⅎ𝑦𝜓)) | ||
Theorem | drnf2 2443 | 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 2371. Use nfbidv 1925 instead. (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 𝑥 = 𝑦 → (Ⅎ𝑧𝜑 ↔ Ⅎ𝑧𝜓)) | ||
Theorem | nfald2 2444 | Variation on nfald 2322 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 2371. Use nfald 2322 instead. (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 & ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥𝜓) ⇒ ⊢ (𝜑 → Ⅎ𝑥∀𝑦𝜓) | ||
Theorem | nfexd2 2445 | Variation on nfexd 2323 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 2371. Use nfexd 2323 instead. (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 & ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥𝜓) ⇒ ⊢ (𝜑 → Ⅎ𝑥∃𝑦𝜓) | ||
Theorem | exdistrf 2446 | 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 2371. Use exdistr 1958 instead. (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦𝜑) ⇒ ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) → ∃𝑥(𝜑 ∧ ∃𝑦𝜓)) | ||
Theorem | dvelimf 2447 | Version of dvelimv 2451 without any variable restrictions. Usage of this theorem is discouraged because it depends on ax-13 2371. (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 2448 | Deduction form of dvelimf 2447. Usage of this theorem is discouraged because it depends on ax-13 2371. (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 2449 | Version of dvelim 2450 without any variable restrictions. Usage of this theorem is discouraged because it depends on ax-13 2371. Check out dvelimhw 2342 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 2450* |
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 2448. Other variants of this theorem are dvelimh 2449 (with no distinct variable restrictions) and dvelimhw 2342 (that avoids ax-13 2371). Usage of this theorem is discouraged because it depends on ax-13 2371. Check out dvelimhw 2342 for a version requiring fewer axioms. (Contributed by NM, 23-Nov-1994.) (New usage is discouraged.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝑧 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝜓 → ∀𝑥𝜓)) | ||
Theorem | dvelimv 2451* | Similar to dvelim 2450 with first hypothesis replaced by a distinct variable condition. Usage of this theorem is discouraged because it depends on ax-13 2371. Check out dvelimhw 2342 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 2452* | Version of dvelim 2450 using "not free" notation. Usage of this theorem is discouraged because it depends on ax-13 2371. (Contributed by Mario Carneiro, 9-Oct-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝑧 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝜓) | ||
Theorem | dveeq2ALT 2453* | Alternate proof of dveeq2 2377, shorter but requiring ax-11 2154. (Contributed by NM, 2-Jan-2002.) (Revised by NM, 20-Jul-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦)) | ||
Theorem | equvini 2454 | 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 2371. See equvinv 2032 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 2455 | A variable elimination law for equality with no distinct variable requirements. Compare equvini 2454. Usage of this theorem is discouraged because it depends on ax-13 2371. Use equvelv 2034 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 2456 | A property related to substitution that unlike equs5 2459 does not require a distinctor antecedent. Usage of this theorem is discouraged because it depends on ax-13 2371. This proof uses ax12 2422, see equs5aALT 2363 for an alternative one using ax-12 2171 but not ax13 2374. Usage of the weaker equs5av 2271 is preferred, which uses ax12v2 2173, but not ax-13 2371. (Contributed by NM, 2-Feb-2007.) (New usage is discouraged.) |
⊢ (∃𝑥(𝑥 = 𝑦 ∧ ∀𝑦𝜑) → ∀𝑥(𝑥 = 𝑦 → 𝜑)) | ||
Theorem | equs5e 2457 | A property related to substitution that unlike equs5 2459 does not require a distinctor antecedent. This proof uses ax12 2422, see equs5eALT 2364 for an alternative one using ax-12 2171 but not ax13 2374. Usage of this theorem is discouraged because it depends on ax-13 2371. (Contributed by NM, 2-Feb-2007.) (Proof shortened by Wolf Lammen, 15-Jan-2018.) (New usage is discouraged.) |
⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑦 → ∃𝑦𝜑)) | ||
Theorem | equs45f 2458 | Two ways of expressing substitution when 𝑦 is not free in 𝜑. The implication "to the left" is equs4 2415 and does not require the nonfreeness hypothesis. Theorem sbalex 2235 replaces the nonfreeness hypothesis with a disjoint variable condition and equs5 2459 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 2371. Use sbalex 2235 instead. (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑)) | ||
Theorem | equs5 2459 | Lemma used in proofs of substitution properties. If there is a disjoint variable condition on 𝑥, 𝑦, then sbalex 2235 can be used instead; if 𝑦 is not free in 𝜑, then equs45f 2458 can be used. Usage of this theorem is discouraged because it depends on ax-13 2371. (Contributed by NM, 14-May-1993.) (Revised by BJ, 1-Oct-2018.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑))) | ||
Theorem | dveel1 2460* | Quantifier introduction when one pair of variables is disjoint. Usage of this theorem is discouraged because it depends on ax-13 2371. (Contributed by NM, 2-Jan-2002.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦 ∈ 𝑧 → ∀𝑥 𝑦 ∈ 𝑧)) | ||
Theorem | dveel2 2461* | Quantifier introduction when one pair of variables is disjoint. Usage of this theorem is discouraged because it depends on ax-13 2371. (Contributed by NM, 2-Jan-2002.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑧 ∈ 𝑦 → ∀𝑥 𝑧 ∈ 𝑦)) | ||
Theorem | axc14 2462 |
Axiom ax-c14 37248 is redundant if we assume ax-5 1913.
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 2461 and ax-5 1913. 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 2371. (Contributed by NM, 29-Jun-1995.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑧 𝑧 = 𝑥 → (¬ ∀𝑧 𝑧 = 𝑦 → (𝑥 ∈ 𝑦 → ∀𝑧 𝑥 ∈ 𝑦))) | ||
Theorem | sb6x 2463 | Equivalence involving substitution for a variable not free. Usage of this theorem is discouraged because it depends on ax-13 2371. Usage of sb6 2088 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 2464 | Substitution does not change an identical variable specifier. Usage of this theorem is discouraged because it depends on ax-13 2371. (Contributed by NM, 15-May-1993.) (New usage is discouraged.) |
⊢ ([𝑤 / 𝑧]∀𝑥 𝑥 = 𝑦 ↔ ∀𝑥 𝑥 = 𝑦) | ||
Theorem | sbequ6 2465 | Substitution does not change a distinctor. Usage of this theorem is discouraged because it depends on ax-13 2371. (Contributed by NM, 5-Aug-1993.) (New usage is discouraged.) |
⊢ ([𝑤 / 𝑧] ¬ ∀𝑥 𝑥 = 𝑦 ↔ ¬ ∀𝑥 𝑥 = 𝑦) | ||
Theorem | sb5rf 2466 | Reversed substitution. Usage of this theorem is discouraged because it depends on ax-13 2371. (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 2467 | Reversed substitution. For a version requiring disjoint variables, but fewer axioms, see sb6rfv 2354. Usage of this theorem is discouraged because it depends on ax-13 2371. Use the weaker sb6rfv 2354 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 2468* | Alternate proof of ax12v2 2173, shorter, but depending on more axioms. (Contributed by NM, 5-Aug-1993.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) | ||
Theorem | 2ax6elem 2469 | We can always find values matching 𝑥 and 𝑦, as long as they are represented by distinct variables. This theorem merges two ax6e 2382 instances ∃𝑧𝑧 = 𝑥 and ∃𝑤𝑤 = 𝑦 into a common expression. Alan Sare contributed a variant of this theorem with distinct variable conditions before, see ax6e2nd 42604. Usage of this theorem is discouraged because it depends on ax-13 2371. (Contributed by Wolf Lammen, 27-Sep-2018.) (New usage is discouraged.) |
⊢ (¬ ∀𝑤 𝑤 = 𝑧 → ∃𝑧∃𝑤(𝑧 = 𝑥 ∧ 𝑤 = 𝑦)) | ||
Theorem | 2ax6e 2470* | We can always find values matching 𝑥 and 𝑦, as long as they are represented by distinct variables. Version of 2ax6elem 2469 with a distinct variable constraint. Usage of this theorem is discouraged because it depends on ax-13 2371. (Contributed by Wolf Lammen, 28-Sep-2018.) (Proof shortened by Wolf Lammen, 3-Oct-2023.) (New usage is discouraged.) |
⊢ ∃𝑧∃𝑤(𝑧 = 𝑥 ∧ 𝑤 = 𝑦) | ||
Theorem | 2sb5rf 2471* | Reversed double substitution. Usage of this theorem is discouraged because it depends on ax-13 2371. (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 2472* | Reversed double substitution. Usage of this theorem is discouraged because it depends on ax-13 2371. (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 2473* | Elimination of double substitution. Usage of this theorem is discouraged because it depends on ax-13 2371. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 29-Sep-2018.) (New usage is discouraged.) |
⊢ (𝜑 ↔ ∃𝑥∃𝑦((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) ∧ [𝑦 / 𝑤][𝑥 / 𝑧]𝜑)) | ||
Theorem | sb4b 2474 | Simplified definition of substitution when variables are distinct. Version of sb6 2088 with a distinctor antecedent. Usage of this theorem is discouraged because it depends on ax-13 2371. (Contributed by NM, 27-May-1997.) Revise df-sb 2068. (Revised by Wolf Lammen, 21-Feb-2024.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑡 → ([𝑡 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑡 → 𝜑))) | ||
Theorem | sb4bOLD 2475 | Obsolete version of sb4b 2474 as of 21-Feb-2024. (Contributed by NM, 27-May-1997.) Revise df-sb 2068. (Revised by Wolf Lammen, 25-Jul-2023.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑡 → ([𝑡 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑡 → 𝜑))) | ||
Theorem | sb3b 2476 | Simplified definition of substitution when variables are distinct. This is the biconditional strengthening of sb3 2477. Usage of this theorem is discouraged because it depends on ax-13 2371. (Contributed by BJ, 6-Oct-2018.) Shorten sb3 2477. (Revised by Wolf Lammen, 21-Feb-2021.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) | ||
Theorem | sb3 2477 | One direction of a simplified definition of substitution when variables are distinct. Usage of this theorem is discouraged because it depends on ax-13 2371. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 21-Feb-2024.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → [𝑦 / 𝑥]𝜑)) | ||
Theorem | sb1 2478 | One direction of a simplified definition of substitution. The converse requires either a disjoint variable condition (sb5 2268) or a nonfreeness hypothesis (sb5f 2501). Usage of this theorem is discouraged because it depends on ax-13 2371. Use the weaker sb1v 2090 when possible. (Contributed by NM, 13-May-1993.) Revise df-sb 2068. (Revised by Wolf Lammen, 21-Feb-2024.) (New usage is discouraged.) |
⊢ ([𝑦 / 𝑥]𝜑 → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) | ||
Theorem | sb2 2479 | One direction of a simplified definition of substitution. The converse requires either a disjoint variable condition (sb6 2088) or a nonfreeness hypothesis (sb6f 2500). Usage of this theorem is discouraged because it depends on ax-13 2371. (Contributed by NM, 13-May-1993.) Revise df-sb 2068. (Revised by Wolf Lammen, 26-Jul-2023.) (New usage is discouraged.) |
⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → [𝑦 / 𝑥]𝜑) | ||
Theorem | sb3OLD 2480 | Obsolete version of sb3 2477 as of 21-Feb-2024. (Contributed by NM, 5-Aug-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → [𝑦 / 𝑥]𝜑)) | ||
Theorem | sb1OLD 2481 | Obsolete version of sb1 2478 as of 21-Feb-2024. (Contributed by NM, 13-May-1993.) Revise df-sb 2068. (Revised by Wolf Lammen, 29-Jul-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ([𝑦 / 𝑥]𝜑 → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) | ||
Theorem | sb3bOLD 2482 | Obsolete version of sb3b 2476 as of 21-Feb-2024. (Contributed by BJ, 6-Oct-2018.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) | ||
Theorem | sb4a 2483 | A version of one implication of sb4b 2474 that does not require a distinctor antecedent. Usage of this theorem is discouraged because it depends on ax-13 2371. Use the weaker sb4av 2236 when possible. (Contributed by NM, 2-Feb-2007.) Revise df-sb 2068. (Revised by Wolf Lammen, 28-Jul-2023.) (New usage is discouraged.) |
⊢ ([𝑡 / 𝑥]∀𝑡𝜑 → ∀𝑥(𝑥 = 𝑡 → 𝜑)) | ||
Theorem | dfsb1 2484 | Alternate definition of substitution. Remark 9.1 in [Megill] p. 447 (p. 15 of the preprint). This was the original definition before df-sb 2068. 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 2371. (Contributed by BJ, 9-Jul-2023.) Revise df-sb 2068. (Revised by Wolf Lammen, 29-Jul-2023.) (New usage is discouraged.) |
⊢ ([𝑦 / 𝑥]𝜑 ↔ ((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) | ||
Theorem | hbsb2 2485 | Bound-variable hypothesis builder for substitution. Usage of this theorem is discouraged because it depends on ax-13 2371. (Contributed by NM, 14-May-1993.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑)) | ||
Theorem | nfsb2 2486 | Bound-variable hypothesis builder for substitution. Usage of this theorem is discouraged because it depends on ax-13 2371. (Contributed by Mario Carneiro, 4-Oct-2016.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥[𝑦 / 𝑥]𝜑) | ||
Theorem | hbsb2a 2487 | Special case of a bound-variable hypothesis builder for substitution. Usage of this theorem is discouraged because it depends on ax-13 2371. (Contributed by NM, 2-Feb-2007.) (New usage is discouraged.) |
⊢ ([𝑦 / 𝑥]∀𝑦𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑) | ||
Theorem | sb4e 2488 | One direction of a simplified definition of substitution that unlike sb4b 2474 does not require a distinctor antecedent. Usage of this theorem is discouraged because it depends on ax-13 2371. (Contributed by NM, 2-Feb-2007.) (New usage is discouraged.) |
⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥(𝑥 = 𝑦 → ∃𝑦𝜑)) | ||
Theorem | hbsb2e 2489 | Special case of a bound-variable hypothesis builder for substitution. Usage of this theorem is discouraged because it depends on ax-13 2371. (Contributed by NM, 2-Feb-2007.) (New usage is discouraged.) |
⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]∃𝑦𝜑) | ||
Theorem | hbsb3 2490 | If 𝑦 is not free in 𝜑, 𝑥 is not free in [𝑦 / 𝑥]𝜑. Usage of this theorem is discouraged because it depends on ax-13 2371. Check out bj-hbsb3v 35175 for a weaker version requiring fewer axioms. (Contributed by NM, 14-May-1993.) (New usage is discouraged.) |
⊢ (𝜑 → ∀𝑦𝜑) ⇒ ⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑) | ||
Theorem | nfs1 2491 | If 𝑦 is not free in 𝜑, 𝑥 is not free in [𝑦 / 𝑥]𝜑. Usage of this theorem is discouraged because it depends on ax-13 2371. Check out nfs1v 2153 for a version requiring fewer axioms. (Contributed by Mario Carneiro, 11-Aug-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ Ⅎ𝑥[𝑦 / 𝑥]𝜑 | ||
Theorem | axc16ALT 2492* | Alternate proof of axc16 2253, shorter but requiring ax-10 2137, ax-11 2154, ax-13 2371 and using df-nf 1786 and df-sb 2068. (Contributed by NM, 17-May-2008.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑥𝜑)) | ||
Theorem | axc16gALT 2493* | Alternate proof of axc16g 2252 that uses df-sb 2068 and requires ax-10 2137, ax-11 2154, ax-13 2371. (Contributed by NM, 15-May-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑧𝜑)) | ||
Theorem | equsb1 2494 | Substitution applied to an atomic wff. Usage of this theorem is discouraged because it depends on ax-13 2371. Use the weaker equsb1v 2103 if possible. (Contributed by NM, 10-May-1993.) (New usage is discouraged.) |
⊢ [𝑦 / 𝑥]𝑥 = 𝑦 | ||
Theorem | equsb2 2495 | Substitution applied to an atomic wff. Usage of this theorem is discouraged because it depends on ax-13 2371. Check out equsb1v 2103 for a version requiring fewer axioms. (Contributed by NM, 10-May-1993.) (New usage is discouraged.) |
⊢ [𝑦 / 𝑥]𝑦 = 𝑥 | ||
Theorem | dfsb2 2496 | An alternate definition of proper substitution that, like dfsb1 2484, mixes free and bound variables to avoid distinct variable requirements. Usage of this theorem is discouraged because it depends on ax-13 2371. (Contributed by NM, 17-Feb-2005.) (New usage is discouraged.) |
⊢ ([𝑦 / 𝑥]𝜑 ↔ ((𝑥 = 𝑦 ∧ 𝜑) ∨ ∀𝑥(𝑥 = 𝑦 → 𝜑))) | ||
Theorem | dfsb3 2497 | An alternate definition of proper substitution df-sb 2068 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 2371. (Contributed by NM, 6-Mar-2007.) (New usage is discouraged.) |
⊢ ([𝑦 / 𝑥]𝜑 ↔ ((𝑥 = 𝑦 → ¬ 𝜑) → ∀𝑥(𝑥 = 𝑦 → 𝜑))) | ||
Theorem | drsb1 2498 | 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 2371. (Contributed by NM, 2-Jun-1993.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → ([𝑧 / 𝑥]𝜑 ↔ [𝑧 / 𝑦]𝜑)) | ||
Theorem | sb2ae 2499* | 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 2371. (Contributed by BJ and WL, 9-Aug-2023.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ↔ [𝑣 / 𝑦]𝜑)) | ||
Theorem | sb6f 2500 | Equivalence for substitution when 𝑦 is not free in 𝜑. The implication "to the left" is sb2 2479 and does not require the nonfreeness hypothesis. Theorem sb6 2088 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 2371. (Contributed by NM, 2-Jun-1993.) (Revised by Mario Carneiro, 4-Oct-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ ([𝑦 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |