Home | Metamath
Proof Explorer Theorem List (p. 25 of 450) | < 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-28695) |
Hilbert Space Explorer
(28696-30218) |
Users' Mathboxes
(30219-44955) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ax6e 2401 |
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 1810 through ax-9 2124,
all axioms other than
ax-6 1970 are believed to be theorems of free logic,
although the system
without ax-6 1970 is not complete in free logic.
Usage of this theorem is discouraged because it depends on ax-13 2390. It is preferred to use ax6ev 1972 when it is sufficient. (Contributed by NM, 14-May-1993.) Shortened after ax13lem1 2392 became available. (Revised by Wolf Lammen, 8-Sep-2018.) (New usage is discouraged.) |
⊢ ∃𝑥 𝑥 = 𝑦 | ||
Theorem | ax6 2402 |
Theorem showing that ax-6 1970 follows from the weaker version ax6v 1971.
(Even though this theorem depends on ax-6 1970,
all references of ax-6 1970 are
made via ax6v 1971. An earlier version stated ax6v 1971
as a separate axiom,
but having two axioms caused some confusion.)
This theorem should be referenced in place of ax-6 1970 so that all proofs can be traced back to ax6v 1971. Usage of this theorem is discouraged because it depends on ax-13 2390. When possible, use the weaker ax6v 1971 rather than ax6 2402 since the ax6v 1971 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.) (New usage is discouraged.) |
⊢ ¬ ∀𝑥 ¬ 𝑥 = 𝑦 | ||
Theorem | axc10 2403 |
Show that the original axiom ax-c10 36037 can be derived from ax6 2402
and axc7 2336
(on top of propositional calculus, ax-gen 1796, and ax-4 1810). See
ax6fromc10 36047 for the rederivation of ax6 2402
from ax-c10 36037.
Normally, axc10 2403 should be used rather than ax-c10 36037, except by theorems specifically studying the latter's properties. Usage of this theorem has been discouraged later on to avoid ax-13 2390 propagation. Check out bj-axc10v 34115 for a weaker version requiring less axioms. (Contributed by NM, 5-Aug-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥(𝑥 = 𝑦 → ∀𝑥𝜑) → 𝜑) | ||
Theorem | spimt 2404 | Closed theorem form of spim 2405. Usage of this theorem is discouraged because it depends on ax-13 2390. (Contributed by NM, 15-Jan-2008.) (Revised by Mario Carneiro, 17-Oct-2016.) (Proof shortened by Wolf Lammen, 21-Mar-2023.) (New usage is discouraged.) |
⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝑦 → (𝜑 → 𝜓))) → (∀𝑥𝜑 → 𝜓)) | ||
Theorem | spim 2405 | Specialization, using implicit substitution. Compare Lemma 14 of [Tarski] p. 70. The spim 2405 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 2390. Check out spimw 1973 for a version requiring less 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 2406 | Deduction version of spime 2407. Usage of this theorem is discouraged because it depends on ax-13 2390. Use the weaker spimedv 2197 if possible. (Contributed by NM, 14-May-1993.) (Revised by Mario Carneiro, 3-Oct-2016.) (Proof shortened by Wolf Lammen, 19-Feb-2018.) (New usage is discouraged.) |
⊢ (𝜒 → Ⅎ𝑥𝜑) & ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) ⇒ ⊢ (𝜒 → (𝜑 → ∃𝑥𝜓)) | ||
Theorem | spime 2407 | Existential introduction, using implicit substitution. Compare Lemma 14 of [Tarski] p. 70. Usage of this theorem is discouraged because it depends on ax-13 2390. Check out spimew 1974 for a weaker version requiring less axioms. (Contributed by NM, 7-Aug-1994.) (Revised by Mario Carneiro, 3-Oct-2016.) (Proof shortened by Wolf Lammen, 6-Mar-2018.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) ⇒ ⊢ (𝜑 → ∃𝑥𝜓) | ||
Theorem | spimv 2408* | A version of spim 2405 with a distinct variable requirement instead of a bound-variable hypothesis. Usage of this theorem is discouraged because it depends on ax-13 2390. See spimfv 2241 and spimvw 2002 for versions requiring fewer axioms. (Contributed by NM, 31-Jul-1993.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) ⇒ ⊢ (∀𝑥𝜑 → 𝜓) | ||
Theorem | spimvALT 2409* | Alternate proof of spimv 2408. Note that it requires only ax-1 6 through ax-5 1911 together with ax6e 2401. Currently, proofs derive from ax6v 1971, but if ax-6 1970 could be used instead, this proof would reduce axiom usage. (Contributed by NM, 31-Jul-1993.) Remove dependency on ax-10 2145. (Revised by BJ, 29-Nov-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) ⇒ ⊢ (∀𝑥𝜑 → 𝜓) | ||
Theorem | spimev 2410* | Distinct-variable version of spime 2407. Usage of this theorem is discouraged because it depends on ax-13 2390. Use the weaker spimevw 2001 if possible. (Contributed by NM, 10-Jan-1993.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) ⇒ ⊢ (𝜑 → ∃𝑥𝜓) | ||
Theorem | spv 2411* | Specialization, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2390. Use the weaker spvv 2003 if possible. (Contributed by NM, 30-Aug-1993.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥𝜑 → 𝜓) | ||
Theorem | spei 2412 | Inference from existential specialization, using implicit substitution. Remove a distinct variable constraint. Usage of this theorem is discouraged because it depends on ax-13 2390. Use the weaker speiv 1976 if possible. (Contributed by NM, 19-Aug-1993.) (Proof shortened by Wolf Lammen, 12-May-2018.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ 𝜓 ⇒ ⊢ ∃𝑥𝜑 | ||
Theorem | chvar 2413 | Implicit substitution of 𝑦 for 𝑥 into a theorem. Usage of this theorem is discouraged because it depends on ax-13 2390. Use the weaker chvarfv 2242 if possible. (Contributed by Raph Levien, 9-Jul-2003.) (Revised by Mario Carneiro, 3-Oct-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ 𝜑 ⇒ ⊢ 𝜓 | ||
Theorem | chvarv 2414* | Implicit substitution of 𝑦 for 𝑥 into a theorem. Usage of this theorem is discouraged because it depends on ax-13 2390. Use the weaker chvarvv 2005 if possible. (Contributed by NM, 20-Apr-1994.) (Proof shortened by Wolf Lammen, 22-Apr-2018.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ 𝜑 ⇒ ⊢ 𝜓 | ||
Theorem | cbv3 2415 | Rule used to change bound variables, using implicit substitution, that does not use ax-c9 36041. Usage of this theorem is discouraged because it depends on ax-13 2390. Use the weaker cbv3v 2355 if possible. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 12-May-2018.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) ⇒ ⊢ (∀𝑥𝜑 → ∀𝑦𝜓) | ||
Theorem | cbval 2416 | Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2390. Check out cbvalw 2042, cbvalvw 2043, cbvalv1 2361 for versions requiring fewer axioms. (Contributed by NM, 13-May-1993.) (Revised by Mario Carneiro, 3-Oct-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓) | ||
Theorem | cbvex 2417 | Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2390. Check out cbvexvw 2044, cbvexv1 2362 for weaker versions requiring fewer axioms. (Contributed by NM, 21-Jun-1993.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓) | ||
Theorem | cbvalv 2418* | Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2390. See cbvalvw 2043 for a version requiring fewer axioms, to be preferred when sufficient. (Contributed by NM, 5-Aug-1993.) Remove dependency on ax-10 2145, shorten. (Revised by Wolf Lammen, 11-Sep-2023.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓) | ||
Theorem | cbvexv 2419* | Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2390. See cbvexvw 2044 for a version requiring fewer axioms, to be preferred when sufficient. (Contributed by NM, 21-Jun-1993.) Remove dependency on ax-10 2145, shorten. (Revised by Wolf Lammen, 11-Sep-2023.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓) | ||
Theorem | cbvalvOLD 2420* | Obsolete version of cbvalv 2418 as of 11-Sep-2023. (Contributed by NM, 5-Aug-1993.) Remove dependency on ax-10 2145. (Revised by Wolf Lammen, 17-Jul-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓) | ||
Theorem | cbvexvOLD 2421* | Obsolete version of cbvexv 2419 as of 11-Sep-2023. (Contributed by NM, 21-Jun-1993.) Remove dependency on ax-10 2145. (Revised by Wolf Lammen, 17-Jul-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓) | ||
Theorem | cbv1 2422 | Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2390. See cbv1v 2356 with disjoint variable conditions, not depending on ax-13 2390. (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 2423 | Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2390. See cbv2w 2357 with disjoint variable conditions, not depending on ax-13 2390. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 3-Oct-2016.) Format hypotheses to common style, avoid ax-10 2145. (Revised by Wolf Lammen, 10-Sep-2023.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑦𝜓) & ⊢ (𝜑 → Ⅎ𝑥𝜒) & ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))) ⇒ ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒)) | ||
Theorem | cbv3h 2424 | Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2390. Use the weaker cbv3hv 2360 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 2425 | Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2390. (Contributed by NM, 11-May-1993.) (Proof shortened by Wolf Lammen, 13-May-2018.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → ∀𝑦𝜓)) & ⊢ (𝜑 → (𝜒 → ∀𝑥𝜒)) & ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 → 𝜒))) ⇒ ⊢ (∀𝑥∀𝑦𝜑 → (∀𝑥𝜓 → ∀𝑦𝜒)) | ||
Theorem | cbv2h 2426 | Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2390. (Contributed by NM, 11-May-1993.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → ∀𝑦𝜓)) & ⊢ (𝜑 → (𝜒 → ∀𝑥𝜒)) & ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))) ⇒ ⊢ (∀𝑥∀𝑦𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒)) | ||
Theorem | cbv2OLD 2427 | Obsolete version of cbv2 2423 as of 10-Sep-2023. (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.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑦𝜓) & ⊢ (𝜑 → Ⅎ𝑥𝜒) & ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))) ⇒ ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒)) | ||
Theorem | cbvald 2428* | Deduction used to change bound variables, using implicit substitution, particularly useful in conjunction with dvelim 2473. Usage of this theorem is discouraged because it depends on ax-13 2390. See cbvaldw 2358 for a version with 𝑥, 𝑦 disjoint, not depending on ax-13 2390. (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 2429* | Deduction used to change bound variables, using implicit substitution, particularly useful in conjunction with dvelim 2473. Usage of this theorem is discouraged because it depends on ax-13 2390. Use the weaker cbvexdw 2359 if possible. (Contributed by NM, 2-Jan-2002.) (Revised by Mario Carneiro, 6-Oct-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑦𝜓) & ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))) ⇒ ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑦𝜒)) | ||
Theorem | cbvaldva 2430* | 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 2390. Use the weaker cbvaldvaw 2045 if possible. (Contributed by David Moews, 1-May-2017.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒)) | ||
Theorem | cbvexdva 2431* | 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 2390. Use the weaker cbvexdvaw 2046 if possible. (Contributed by David Moews, 1-May-2017.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑦𝜒)) | ||
Theorem | cbval2 2432* | Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2390. Use the weaker cbval2v 2363 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 | cbval2OLD 2433* | Obsolete version of cbval2 2432 as of 11-Sep-2023. (Contributed by NM, 22-Dec-2003.) (Revised by Mario Carneiro, 6-Oct-2016.) (Proof shortened by Wolf Lammen, 22-Apr-2018.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑧𝜑 & ⊢ Ⅎ𝑤𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ Ⅎ𝑦𝜓 & ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑧∀𝑤𝜓) | ||
Theorem | cbvex2 2434* | Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2390. Use the weaker cbvex2v 2365 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 2435* | Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2390. Use the weaker cbval2vw 2047 if possible. (Contributed by NM, 4-Feb-2005.) Remove dependency on ax-10 2145. (Revised by Wolf Lammen, 18-Jul-2021.) (New usage is discouraged.) |
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑧∀𝑤𝜓) | ||
Theorem | cbvex2vv 2436* | Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2390. Use the weaker cbvex2vw 2048 if possible. (Contributed by NM, 26-Jul-1995.) Remove dependency on ax-10 2145. (Revised by Wolf Lammen, 18-Jul-2021.) (New usage is discouraged.) |
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑧∃𝑤𝜓) | ||
Theorem | cbvex4v 2437* | Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2390. Use the weaker cbvex4vw 2049 if possible. (Contributed by NM, 26-Jul-1995.) (New usage is discouraged.) |
⊢ ((𝑥 = 𝑣 ∧ 𝑦 = 𝑢) → (𝜑 ↔ 𝜓)) & ⊢ ((𝑧 = 𝑓 ∧ 𝑤 = 𝑔) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (∃𝑥∃𝑦∃𝑧∃𝑤𝜑 ↔ ∃𝑣∃𝑢∃𝑓∃𝑔𝜒) | ||
Theorem | equs4 2438 | Lemma used in proofs of implicit substitution properties. The converse requires either a disjoint variable condition (sb56 2277) or a non-freeness hypothesis (equs45f 2482). Usage of this theorem is discouraged because it depends on ax-13 2390. See equs4v 2006 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 2439 | An equivalence related to implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2390. See equsalvw 2010 and equsalv 2268 for versions with disjoint variable conditions proved from fewer axioms. See also the dual form equsex 2440. (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 2440 | An equivalence related to implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2390. See equsexvw 2011 and equsexv 2269 for versions with disjoint variable conditions proved from fewer axioms. See also the dual form equsal 2439. See equsexALT 2441 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 2441 | Alternate proof of equsex 2440. This proves the result directly, instead of as a corollary of equsal 2439 via equs4 2438. Note in particular that only existential quantifiers appear in the proof and that the only step requiring ax-13 2390 is ax6e 2401. This proof mimics that of equsal 2439 (in particular, note that pm5.32i 577, exbii 1848, 19.41 2237, mpbiran 707 correspond respectively to pm5.74i 273, albii 1820, 19.23 2211, a1bi 365). (Contributed by BJ, 20-Aug-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ 𝜓) | ||
Theorem | equsalh 2442 | An equivalence related to implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2390. See equsalhw 2299 for a version with a disjoint variable condition requiring fewer axioms. (Contributed by NM, 2-Jun-1993.) (New usage is discouraged.) |
⊢ (𝜓 → ∀𝑥𝜓) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜓) | ||
Theorem | equsexh 2443 | An equivalence related to implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2390. See equsexhv 2300 for a version with a disjoint variable condition which does not require ax-13 2390. (Contributed by NM, 5-Aug-1993.) (New usage is discouraged.) |
⊢ (𝜓 → ∀𝑥𝜓) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ 𝜓) | ||
Theorem | axc15 2444 |
Derivation of set.mm's original ax-c15 36040 from ax-c11n 36039 and the shorter
ax-12 2177 that has replaced it.
Theorem ax12 2445 shows the reverse derivation of ax-12 2177 from ax-c15 36040. Normally, axc15 2444 should be used rather than ax-c15 36040, except by theorems specifically studying the latter's properties. Usage of this theorem is discouraged because it depends on ax-13 2390. (Contributed by NM, 2-Feb-2007.) (Proof shortened by Wolf Lammen, 26-Mar-2023.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))) | ||
Theorem | ax12 2445 | Rederivation of axiom ax-12 2177 from ax12v 2178 (used only via sp 2182) , axc11r 2386, and axc15 2444 (on top of Tarski's FOL). Since this version depends on ax-13 2390, usage of the weaker ax12v 2178, ax12w 2137, ax12i 1969 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 2446 | A bidirectional version of axc15 2444. Usage of this theorem is discouraged because it depends on ax-13 2390. (Contributed by NM, 30-Jun-2006.) (New usage is discouraged.) |
⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦) → (𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑))) | ||
Theorem | ax13ALT 2447 | Alternate proof of ax13 2393 from FOL, sp 2182, and axc9 2400. (Contributed by NM, 21-Dec-2015.) (Proof shortened by Wolf Lammen, 31-Jan-2018.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ 𝑥 = 𝑦 → (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧)) | ||
Theorem | axc11n 2448 | Derive set.mm's original ax-c11n 36039 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 2060. Use aecom 2449 instead when this does not lengthen the proof. Usage of this theorem is discouraged because it depends on ax-13 2390. (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 2449 | 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 2390. (Contributed by NM, 10-May-1993.) Change to a biconditional. (Revised by BJ, 26-Sep-2019.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 ↔ ∀𝑦 𝑦 = 𝑥) | ||
Theorem | aecoms 2450 | A commutation rule for identical variable specifiers. Usage of this theorem is discouraged because it depends on ax-13 2390. (Contributed by NM, 10-May-1993.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → 𝜑) ⇒ ⊢ (∀𝑦 𝑦 = 𝑥 → 𝜑) | ||
Theorem | naecoms 2451 | A commutation rule for distinct variable specifiers. Usage of this theorem is discouraged because it depends on ax-13 2390. (Contributed by NM, 2-Jan-2002.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → 𝜑) ⇒ ⊢ (¬ ∀𝑦 𝑦 = 𝑥 → 𝜑) | ||
Theorem | axc11 2452 | Show that ax-c11 36038 can be derived from ax-c11n 36039 in the form of axc11n 2448. Normally, axc11 2452 should be used rather than ax-c11 36038, except by theorems specifically studying the latter's properties. Usage of this theorem is discouraged because it depends on ax-13 2390. Use the weaker axc11v 2265 when possible. (Contributed by NM, 16-May-2008.) (Proof shortened by Wolf Lammen, 21-Apr-2018.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 → ∀𝑦𝜑)) | ||
Theorem | hbae 2453 | All variables are effectively bound in an identical variable specifier. Usage of this theorem is discouraged because it depends on ax-13 2390. Use the weaker hbaev 2064 when possible. (Contributed by NM, 13-May-1993.) (Proof shortened by Wolf Lammen, 21-Apr-2018.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧∀𝑥 𝑥 = 𝑦) | ||
Theorem | hbnae 2454 | 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 2390. Use the weaker hbnaev 2067 when possible. (Contributed by NM, 13-May-1993.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑧 ¬ ∀𝑥 𝑥 = 𝑦) | ||
Theorem | nfae 2455 | All variables are effectively bound in an identical variable specifier. Usage of this theorem is discouraged because it depends on ax-13 2390. (Contributed by Mario Carneiro, 11-Aug-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑧∀𝑥 𝑥 = 𝑦 | ||
Theorem | nfnae 2456 | All variables are effectively bound in a distinct variable specifier. Usage of this theorem is discouraged because it depends on ax-13 2390. Use the weaker nfnaew 2153 when possible. (Contributed by Mario Carneiro, 11-Aug-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑧 ¬ ∀𝑥 𝑥 = 𝑦 | ||
Theorem | hbnaes 2457 | Rule that applies hbnae 2454 to antecedent. Usage of this theorem is discouraged because it depends on ax-13 2390. (Contributed by NM, 15-May-1993.) (New usage is discouraged.) |
⊢ (∀𝑧 ¬ ∀𝑥 𝑥 = 𝑦 → 𝜑) ⇒ ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → 𝜑) | ||
Theorem | axc16i 2458* | Inference with axc16 2262 as its conclusion. Usage of axc16 2262 is preferred since it requires fewer axioms. (Contributed by NM, 20-May-2008.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜓)) & ⊢ (𝜓 → ∀𝑥𝜓) ⇒ ⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑥𝜑)) | ||
Theorem | axc16nfALT 2459* | Alternate proof of axc16nf 2264, shorter but requiring ax-11 2161 and ax-13 2390. (Contributed by Mario Carneiro, 7-Oct-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → Ⅎ𝑧𝜑) | ||
Theorem | dral2 2460 | 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 2390. Usage of albidv 1921 is preferred, which requires fewer axioms. (Contributed by NM, 27-Feb-2005.) Allow a shortening of dral1 2461. (Revised by Wolf Lammen, 4-Mar-2018.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑧𝜑 ↔ ∀𝑧𝜓)) | ||
Theorem | dral1 2461 | 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 2390. Use the weaker dral1v 2387 if possible. (Contributed by NM, 24-Nov-1994.) Remove dependency on ax-11 2161. (Revised by Wolf Lammen, 6-Sep-2018.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 ↔ ∀𝑦𝜓)) | ||
Theorem | dral1ALT 2462 | Alternate proof of dral1 2461, shorter but requiring ax-11 2161. (Contributed by NM, 24-Nov-1994.) (Proof shortened by Wolf Lammen, 22-Apr-2018.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 ↔ ∀𝑦𝜓)) | ||
Theorem | drex1 2463 | 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 2390. Use the weaker drex1v 2388 if possible. (Contributed by NM, 27-Feb-2005.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 𝑥 = 𝑦 → (∃𝑥𝜑 ↔ ∃𝑦𝜓)) | ||
Theorem | drex2 2464 | 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 2390. Usage of exbidv 1922 is preferred, which requires fewer axioms. (Contributed by NM, 27-Feb-2005.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 𝑥 = 𝑦 → (∃𝑧𝜑 ↔ ∃𝑧𝜓)) | ||
Theorem | drnf1 2465 | Formula-building lemma for use with the Distinctor Reduction Theorem. Usage of this theorem is discouraged because it depends on ax-13 2390. Use the weaker drnf1v 2389 if possible. (Contributed by Mario Carneiro, 4-Oct-2016.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 𝑥 = 𝑦 → (Ⅎ𝑥𝜑 ↔ Ⅎ𝑦𝜓)) | ||
Theorem | drnf2 2466 | Formula-building lemma for use with the Distinctor Reduction Theorem. Usage of this theorem is discouraged because it depends on ax-13 2390. Usage of nfbidv 1923 is preferred, which requires fewer axioms. (Contributed by Mario Carneiro, 4-Oct-2016.) (Proof shortened by Wolf Lammen, 5-May-2018.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 𝑥 = 𝑦 → (Ⅎ𝑧𝜑 ↔ Ⅎ𝑧𝜓)) | ||
Theorem | nfald2 2467 | Variation on nfald 2347 which adds the hypothesis that 𝑥 and 𝑦 are distinct in the inner subproof. Usage of this theorem is discouraged because it depends on ax-13 2390. Check out nfald 2347 for a version requiring fewer axioms. (Contributed by Mario Carneiro, 8-Oct-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 & ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥𝜓) ⇒ ⊢ (𝜑 → Ⅎ𝑥∀𝑦𝜓) | ||
Theorem | nfexd2 2468 | Variation on nfexd 2348 which adds the hypothesis that 𝑥 and 𝑦 are distinct in the inner subproof. Usage of this theorem is discouraged because it depends on ax-13 2390. Check out nfexd 2348 for a version requiring fewer axioms. (Contributed by Mario Carneiro, 8-Oct-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 & ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥𝜓) ⇒ ⊢ (𝜑 → Ⅎ𝑥∃𝑦𝜓) | ||
Theorem | exdistrf 2469 | 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 𝑦). Usage of this theorem is discouraged because it depends on ax-13 2390. Check out exdistr 1955 for a version requiring fewer axioms. (Contributed by Mario Carneiro, 20-Mar-2013.) (Proof shortened by Wolf Lammen, 14-May-2018.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦𝜑) ⇒ ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) → ∃𝑥(𝜑 ∧ ∃𝑦𝜓)) | ||
Theorem | dvelimf 2470 | Version of dvelimv 2474 without any variable restrictions. Usage of this theorem is discouraged because it depends on ax-13 2390. (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 2471 | Deduction form of dvelimf 2470. Usage of this theorem is discouraged because it depends on ax-13 2390. (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 2472 | Version of dvelim 2473 without any variable restrictions. Usage of this theorem is discouraged because it depends on ax-13 2390. Check out dvelimhw 2366 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 2473* |
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 2471. Other variants of this theorem are dvelimh 2472 (with no distinct variable restrictions) and dvelimhw 2366 (that avoids ax-13 2390). Usage of this theorem is discouraged because it depends on ax-13 2390. Check out dvelimhw 2366 for a version requiring fewer axioms. (Contributed by NM, 23-Nov-1994.) (New usage is discouraged.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝑧 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝜓 → ∀𝑥𝜓)) | ||
Theorem | dvelimv 2474* | Similar to dvelim 2473 with first hypothesis replaced by a distinct variable condition. Usage of this theorem is discouraged because it depends on ax-13 2390. Check out dvelimhw 2366 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 2475* | Version of dvelim 2473 using "not free" notation. Usage of this theorem is discouraged because it depends on ax-13 2390. (Contributed by Mario Carneiro, 9-Oct-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝑧 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝜓) | ||
Theorem | dveeq2ALT 2476* | Alternate proof of dveeq2 2396, shorter but requiring ax-11 2161. (Contributed by NM, 2-Jan-2002.) (Revised by NM, 20-Jul-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦)) | ||
Theorem | equvini 2477 | 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 2390. See equvinv 2036 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 | equviniOLD 2478 | Obsolete version of equvini 2477 as of 16-Sep-2023. (Contributed by NM, 10-Jan-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 15-Sep-2018.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝑥 = 𝑦 → ∃𝑧(𝑥 = 𝑧 ∧ 𝑧 = 𝑦)) | ||
Theorem | equvel 2479 | A variable elimination law for equality with no distinct variable requirements. Compare equvini 2477. Usage of this theorem is discouraged because it depends on ax-13 2390. Use equvelv 2038 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 2480 | A property related to substitution that unlike equs5 2483 does not require a distinctor antecedent. Usage of this theorem is discouraged because it depends on ax-13 2390. This proof uses ax12 2445, see equs5aALT 2384 for an alternative one using ax-12 2177 but not ax13 2393. Usage of the weaker equs5av 2279 is preferred, which uses ax12v2 2179, but not ax-13 2390. (Contributed by NM, 2-Feb-2007.) (New usage is discouraged.) |
⊢ (∃𝑥(𝑥 = 𝑦 ∧ ∀𝑦𝜑) → ∀𝑥(𝑥 = 𝑦 → 𝜑)) | ||
Theorem | equs5e 2481 | A property related to substitution that unlike equs5 2483 does not require a distinctor antecedent. This proof uses ax12 2445, see equs5eALT 2385 for an alternative one using ax-12 2177 but not ax13 2393. Usage of this theorem is discouraged because it depends on ax-13 2390. (Contributed by NM, 2-Feb-2007.) (Proof shortened by Wolf Lammen, 15-Jan-2018.) (New usage is discouraged.) |
⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑦 → ∃𝑦𝜑)) | ||
Theorem | equs45f 2482 | Two ways of expressing substitution when 𝑦 is not free in 𝜑. The implication "to the left" is equs4 2438 and does not require the non-freeness hypothesis. Theorem sb56 2277 replaces the non-freeness hypothesis with a disjoint variable condition and equs5 2483 replaces it with a distinctor as antecedent. Usage of this theorem is discouraged because it depends on ax-13 2390. (Contributed by NM, 25-Apr-2008.) (Revised by Mario Carneiro, 4-Oct-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑)) | ||
Theorem | equs5 2483 | Lemma used in proofs of substitution properties. If there is a disjoint variable condition on 𝑥, 𝑦, then sb56 2277 can be used instead; if 𝑦 is not free in 𝜑, then equs45f 2482 can be used. Usage of this theorem is discouraged because it depends on ax-13 2390. (Contributed by NM, 14-May-1993.) (Revised by BJ, 1-Oct-2018.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑))) | ||
Theorem | dveel1 2484* | Quantifier introduction when one pair of variables is distinct. Usage of this theorem is discouraged because it depends on ax-13 2390. (Contributed by NM, 2-Jan-2002.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦 ∈ 𝑧 → ∀𝑥 𝑦 ∈ 𝑧)) | ||
Theorem | dveel2 2485* | Quantifier introduction when one pair of variables is distinct. Usage of this theorem is discouraged because it depends on ax-13 2390. (Contributed by NM, 2-Jan-2002.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑧 ∈ 𝑦 → ∀𝑥 𝑧 ∈ 𝑦)) | ||
Theorem | axc14 2486 |
Axiom ax-c14 36042 is redundant if we assume ax-5 1911.
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 2485 and ax-5 1911. 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 2390. (Contributed by NM, 29-Jun-1995.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑧 𝑧 = 𝑥 → (¬ ∀𝑧 𝑧 = 𝑦 → (𝑥 ∈ 𝑦 → ∀𝑧 𝑥 ∈ 𝑦))) | ||
Theorem | sb6x 2487 | Equivalence involving substitution for a variable not free. Usage of this theorem is discouraged because it depends on ax-13 2390. Usage of sb6 2093 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 2488 | Substitution does not change an identical variable specifier. Usage of this theorem is discouraged because it depends on ax-13 2390. (Contributed by NM, 15-May-1993.) (New usage is discouraged.) |
⊢ ([𝑤 / 𝑧]∀𝑥 𝑥 = 𝑦 ↔ ∀𝑥 𝑥 = 𝑦) | ||
Theorem | sbequ6 2489 | Substitution does not change a distinctor. Usage of this theorem is discouraged because it depends on ax-13 2390. (Contributed by NM, 5-Aug-1993.) (New usage is discouraged.) |
⊢ ([𝑤 / 𝑧] ¬ ∀𝑥 𝑥 = 𝑦 ↔ ¬ ∀𝑥 𝑥 = 𝑦) | ||
Theorem | sb5rf 2490 | Reversed substitution. Usage of this theorem is discouraged because it depends on ax-13 2390. (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 2491 | Reversed substitution. For a version requiring disjoint variables, but fewer axioms, see sb6rfv 2376. Usage of this theorem is discouraged because it depends on ax-13 2390. Use the weaker sb6rfv 2376 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 2492* | Alternate proof of ax12v2 2179, shorter, but depending on more axioms. (Contributed by NM, 5-Aug-1993.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) | ||
Theorem | 2ax6elem 2493 | We can always find values matching 𝑥 and 𝑦, as long as they are represented by distinct variables. This theorem merges two ax6e 2401 instances ∃𝑧𝑧 = 𝑥 and ∃𝑤𝑤 = 𝑦 into a common expression. Alan Sare contributed a variant of this theorem with distinct variable conditions before, see ax6e2nd 40941. Usage of this theorem is discouraged because it depends on ax-13 2390. (Contributed by Wolf Lammen, 27-Sep-2018.) (New usage is discouraged.) |
⊢ (¬ ∀𝑤 𝑤 = 𝑧 → ∃𝑧∃𝑤(𝑧 = 𝑥 ∧ 𝑤 = 𝑦)) | ||
Theorem | 2ax6e 2494* | We can always find values matching 𝑥 and 𝑦, as long as they are represented by distinct variables. Version of 2ax6elem 2493 with a distinct variable constraint. Usage of this theorem is discouraged because it depends on ax-13 2390. (Contributed by Wolf Lammen, 28-Sep-2018.) (Proof shortened by Wolf Lammen, 3-Oct-2023.) (New usage is discouraged.) |
⊢ ∃𝑧∃𝑤(𝑧 = 𝑥 ∧ 𝑤 = 𝑦) | ||
Theorem | 2ax6eOLD 2495* | Obsolete version of 2ax6e 2494 as of 3-Oct-2023. (Contributed by Wolf Lammen, 28-Sep-2018.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ∃𝑧∃𝑤(𝑧 = 𝑥 ∧ 𝑤 = 𝑦) | ||
Theorem | 2sb5rf 2496* | Reversed double substitution. Usage of this theorem is discouraged because it depends on ax-13 2390. (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 2497* | Reversed double substitution. Usage of this theorem is discouraged because it depends on ax-13 2390. (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 2498* | Elimination of double substitution. Usage of this theorem is discouraged because it depends on ax-13 2390. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 29-Sep-2018.) (New usage is discouraged.) |
⊢ (𝜑 ↔ ∃𝑥∃𝑦((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) ∧ [𝑦 / 𝑤][𝑥 / 𝑧]𝜑)) | ||
Theorem | sb4b 2499 | Simplified definition of substitution when variables are distinct. Version of sb6 2093 with a distinctor. Usage of this theorem is discouraged because it depends on ax-13 2390. (Contributed by NM, 27-May-1997.) Revise df-sb 2070. (Revised by Wolf Lammen, 21-Feb-2024.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑡 → ([𝑡 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑡 → 𝜑))) | ||
Theorem | sb4bOLD 2500 | Obsolete version of sb4b 2499 as of 21-Feb-2024. (Contributed by NM, 27-May-1997.) Revise df-sb 2070. (Revised by Wolf Lammen, 25-Jul-2023.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑡 → ([𝑡 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑡 → 𝜑))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |