![]() |
Metamath
Proof Explorer Theorem List (p. 24 of 480) | < 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-30438) |
![]() (30439-31961) |
![]() (31962-47939) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | sbor 2301 | Disjunction inside and outside of a substitution are equivalent. (Contributed by NM, 29-Sep-2002.) |
⊢ ([𝑦 / 𝑥](𝜑 ∨ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 ∨ [𝑦 / 𝑥]𝜓)) | ||
Theorem | sbbi 2302 | Equivalence inside and outside of a substitution are equivalent. (Contributed by NM, 14-May-1993.) |
⊢ ([𝑦 / 𝑥](𝜑 ↔ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜓)) | ||
Theorem | sblbis 2303 | Introduce left biconditional inside of a substitution. (Contributed by NM, 19-Aug-1993.) |
⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓) ⇒ ⊢ ([𝑦 / 𝑥](𝜒 ↔ 𝜑) ↔ ([𝑦 / 𝑥]𝜒 ↔ 𝜓)) | ||
Theorem | sbrbis 2304 | Introduce right biconditional inside of a substitution. (Contributed by NM, 18-Aug-1993.) |
⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓) ⇒ ⊢ ([𝑦 / 𝑥](𝜑 ↔ 𝜒) ↔ (𝜓 ↔ [𝑦 / 𝑥]𝜒)) | ||
Theorem | sbrbif 2305 | Introduce right biconditional inside of a substitution. (Contributed by NM, 18-Aug-1993.) (Revised by Mario Carneiro, 4-Oct-2016.) |
⊢ Ⅎ𝑥𝜒 & ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓) ⇒ ⊢ ([𝑦 / 𝑥](𝜑 ↔ 𝜒) ↔ (𝜓 ↔ 𝜒)) | ||
Theorem | sbiev 2306* | Conversion of implicit substitution to explicit substitution. Version of sbie 2499 with a disjoint variable condition, not requiring ax-13 2369. See sbievw 2093 for a version with a disjoint variable condition requiring fewer axioms. (Contributed by NM, 30-Jun-1994.) (Revised by Wolf Lammen, 18-Jan-2023.) Remove dependence on ax-10 2135 and shorten proof. (Revised by BJ, 18-Jul-2023.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓) | ||
Theorem | sbiedw 2307* | Conversion of implicit substitution to explicit substitution (deduction version of sbiev 2306). Version of sbied 2500 with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 30-Jun-1994.) Avoid ax-13 2369. (Revised by Gino Giotto, 10-Jan-2024.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝜒) & ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))) ⇒ ⊢ (𝜑 → ([𝑦 / 𝑥]𝜓 ↔ 𝜒)) | ||
Theorem | axc7 2308 |
Show that the original axiom ax-c7 38058 can be derived from ax-10 2135
(hbn1 2136), sp 2174 and propositional calculus. See ax10fromc7 38068 for the
rederivation of ax-10 2135 from ax-c7 38058.
Normally, axc7 2308 should be used rather than ax-c7 38058, except by theorems specifically studying the latter's properties. (Contributed by NM, 21-May-2008.) |
⊢ (¬ ∀𝑥 ¬ ∀𝑥𝜑 → 𝜑) | ||
Theorem | axc7e 2309 | Abbreviated version of axc7 2308 using the existential quantifier. Corresponds to the dual of Axiom (B) of modal logic. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 8-Jul-2022.) |
⊢ (∃𝑥∀𝑥𝜑 → 𝜑) | ||
Theorem | modal-b 2310 | The analogue in our predicate calculus of the Brouwer axiom (B) of modal logic S5. (Contributed by NM, 5-Oct-2005.) |
⊢ (𝜑 → ∀𝑥 ¬ ∀𝑥 ¬ 𝜑) | ||
Theorem | 19.9ht 2311 | A closed version of 19.9h 2280. (Contributed by NM, 13-May-1993.) (Proof shortened by Wolf Lammen, 3-Mar-2018.) |
⊢ (∀𝑥(𝜑 → ∀𝑥𝜑) → (∃𝑥𝜑 → 𝜑)) | ||
Theorem | axc4 2312 |
Show that the original axiom ax-c4 38057 can be derived from ax-4 1809
(alim 1810), ax-10 2135 (hbn1 2136), sp 2174 and propositional calculus. See
ax4fromc4 38067 for the rederivation of ax-4 1809
from ax-c4 38057.
Part of the proof is based on the proof of Lemma 22 of [Monk2] p. 114. (Contributed by NM, 21-May-2008.) (Proof modification is discouraged.) |
⊢ (∀𝑥(∀𝑥𝜑 → 𝜓) → (∀𝑥𝜑 → ∀𝑥𝜓)) | ||
Theorem | axc4i 2313 | Inference version of axc4 2312. (Contributed by NM, 3-Jan-1993.) |
⊢ (∀𝑥𝜑 → 𝜓) ⇒ ⊢ (∀𝑥𝜑 → ∀𝑥𝜓) | ||
Theorem | nfal 2314 | If 𝑥 is not free in 𝜑, then it is not free in ∀𝑦𝜑. (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ Ⅎ𝑥∀𝑦𝜑 | ||
Theorem | nfex 2315 | If 𝑥 is not free in 𝜑, then it is not free in ∃𝑦𝜑. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.) Reduce symbol count in nfex 2315, hbex 2316. (Revised by Wolf Lammen, 16-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ Ⅎ𝑥∃𝑦𝜑 | ||
Theorem | hbex 2316 | If 𝑥 is not free in 𝜑, then it is not free in ∃𝑦𝜑. (Contributed by NM, 12-Mar-1993.) Reduce symbol count in nfex 2315, hbex 2316. (Revised by Wolf Lammen, 16-Oct-2021.) |
⊢ (𝜑 → ∀𝑥𝜑) ⇒ ⊢ (∃𝑦𝜑 → ∀𝑥∃𝑦𝜑) | ||
Theorem | nfnf 2317 | If 𝑥 is not free in 𝜑, then it is not free in Ⅎ𝑦𝜑. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ Ⅎ𝑥Ⅎ𝑦𝜑 | ||
Theorem | 19.12 2318 | Theorem 19.12 of [Margaris] p. 89. Assuming the converse is a mistake sometimes made by beginners! But sometimes the converse does hold, as in 19.12vv 2341 and r19.12sn 4723. (Contributed by NM, 12-Mar-1993.) (Proof shortened by Wolf Lammen, 3-Jan-2018.) |
⊢ (∃𝑥∀𝑦𝜑 → ∀𝑦∃𝑥𝜑) | ||
Theorem | nfald 2319 | Deduction form of nfal 2314. (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 16-Oct-2021.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝜓) ⇒ ⊢ (𝜑 → Ⅎ𝑥∀𝑦𝜓) | ||
Theorem | nfexd 2320 | If 𝑥 is not free in 𝜓, then it is not free in ∃𝑦𝜓. (Contributed by Mario Carneiro, 24-Sep-2016.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝜓) ⇒ ⊢ (𝜑 → Ⅎ𝑥∃𝑦𝜓) | ||
Theorem | nfsbv 2321* | If 𝑧 is not free in 𝜑, then it is not free in [𝑦 / 𝑥]𝜑 when 𝑧 is disjoint from both 𝑥 and 𝑦. Version of nfsb 2520 with an additional disjoint variable condition on 𝑥, 𝑧 but not requiring ax-13 2369. (Contributed by Mario Carneiro, 11-Aug-2016.) (Revised by Wolf Lammen, 7-Feb-2023.) Remove disjoint variable condition on 𝑥, 𝑦. (Revised by Steven Nguyen, 13-Aug-2023.) (Proof shortened by Wolf Lammen, 25-Oct-2024.) |
⊢ Ⅎ𝑧𝜑 ⇒ ⊢ Ⅎ𝑧[𝑦 / 𝑥]𝜑 | ||
Theorem | nfsbvOLD 2322* | Obsolete version of nfsbv 2321 as of 25-Oct-2024. (Contributed by Mario Carneiro, 11-Aug-2016.) (Revised by Wolf Lammen, 7-Feb-2023.) Remove disjoint variable condition on 𝑥, 𝑦. (Revised by Steven Nguyen, 13-Aug-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑧𝜑 ⇒ ⊢ Ⅎ𝑧[𝑦 / 𝑥]𝜑 | ||
Theorem | hbsbwOLD 2323* | Obsolete version of hbsbw 2167 as of 23-May-2024. (Contributed by NM, 12-Aug-1993.) (Revised by Gino Giotto, 10-Jan-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → ∀𝑧𝜑) ⇒ ⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑧[𝑦 / 𝑥]𝜑) | ||
Theorem | sbco2v 2324* | A composition law for substitution. Version of sbco2 2508 with disjoint variable conditions but not requiring ax-13 2369. (Contributed by NM, 30-Jun-1994.) (Revised by Wolf Lammen, 29-Apr-2023.) |
⊢ Ⅎ𝑧𝜑 ⇒ ⊢ ([𝑦 / 𝑧][𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑) | ||
Theorem | aaan 2325 | Distribute universal quantifiers. (Contributed by NM, 12-Aug-1993.) Avoid ax-10 2135. (Revised by Gino Giotto, 21-Nov-2024.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (∀𝑥∀𝑦(𝜑 ∧ 𝜓) ↔ (∀𝑥𝜑 ∧ ∀𝑦𝜓)) | ||
Theorem | aaanOLD 2326 | Obsolete version of aaan 2325 as of 21-Nov-2024. (Contributed by NM, 12-Aug-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (∀𝑥∀𝑦(𝜑 ∧ 𝜓) ↔ (∀𝑥𝜑 ∧ ∀𝑦𝜓)) | ||
Theorem | eeor 2327 | Distribute existential quantifiers. (Contributed by NM, 8-Aug-1994.) Avoid ax-10 2135. (Revised by Gino Giotto, 21-Nov-2024.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (∃𝑥∃𝑦(𝜑 ∨ 𝜓) ↔ (∃𝑥𝜑 ∨ ∃𝑦𝜓)) | ||
Theorem | eeorOLD 2328 | Obsolete version of eeor 2327 as of 21-Nov-2024. (Contributed by NM, 8-Aug-1994.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (∃𝑥∃𝑦(𝜑 ∨ 𝜓) ↔ (∃𝑥𝜑 ∨ ∃𝑦𝜓)) | ||
Theorem | cbv3v 2329* | Rule used to change bound variables, using implicit substitution. Version of cbv3 2394 with a disjoint variable condition, which does not require ax-13 2369. (Contributed by NM, 5-Aug-1993.) (Revised by BJ, 31-May-2019.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) ⇒ ⊢ (∀𝑥𝜑 → ∀𝑦𝜓) | ||
Theorem | cbv1v 2330* | Rule used to change bound variables, using implicit substitution. Version of cbv1 2399 with a disjoint variable condition, which does not require ax-13 2369. (Contributed by NM, 5-Aug-1993.) (Revised by BJ, 16-Jun-2019.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑦𝜓) & ⊢ (𝜑 → Ⅎ𝑥𝜒) & ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 → 𝜒))) ⇒ ⊢ (𝜑 → (∀𝑥𝜓 → ∀𝑦𝜒)) | ||
Theorem | cbv2w 2331* | Rule used to change bound variables, using implicit substitution. Version of cbv2 2400 with a disjoint variable condition, which does not require ax-13 2369. (Contributed by NM, 5-Aug-1993.) Avoid ax-13 2369. (Revised by Gino Giotto, 10-Jan-2024.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑦𝜓) & ⊢ (𝜑 → Ⅎ𝑥𝜒) & ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))) ⇒ ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒)) | ||
Theorem | cbvaldw 2332* | Deduction used to change bound variables, using implicit substitution. Version of cbvald 2404 with a disjoint variable condition, which does not require ax-13 2369. (Contributed by NM, 2-Jan-2002.) Avoid ax-13 2369. (Revised by Gino Giotto, 10-Jan-2024.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑦𝜓) & ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))) ⇒ ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒)) | ||
Theorem | cbvexdw 2333* | Deduction used to change bound variables, using implicit substitution. Version of cbvexd 2405 with a disjoint variable condition, which does not require ax-13 2369. (Contributed by NM, 2-Jan-2002.) Avoid ax-13 2369. (Revised by Gino Giotto, 10-Jan-2024.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑦𝜓) & ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))) ⇒ ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑦𝜒)) | ||
Theorem | cbv3hv 2334* | Rule used to change bound variables, using implicit substitution. Version of cbv3h 2401 with a disjoint variable condition on 𝑥, 𝑦, which does not require ax-13 2369. Was used in a proof of axc11n 2423 (but of independent interest). (Contributed by NM, 25-Jul-2015.) (Proof shortened by Wolf Lammen, 29-Nov-2020.) (Proof shortened by BJ, 30-Nov-2020.) |
⊢ (𝜑 → ∀𝑦𝜑) & ⊢ (𝜓 → ∀𝑥𝜓) & ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) ⇒ ⊢ (∀𝑥𝜑 → ∀𝑦𝜓) | ||
Theorem | cbvalv1 2335* | Rule used to change bound variables, using implicit substitution. Version of cbval 2395 with a disjoint variable condition, which does not require ax-13 2369. See cbvalvw 2037 for a version with two more disjoint variable conditions, requiring fewer axioms, and cbvalv 2397 for another variant. (Contributed by NM, 13-May-1993.) (Revised by BJ, 31-May-2019.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓) | ||
Theorem | cbvexv1 2336* | Rule used to change bound variables, using implicit substitution. Version of cbvex 2396 with a disjoint variable condition, which does not require ax-13 2369. See cbvexvw 2038 for a version with two disjoint variable conditions, requiring fewer axioms, and cbvexv 2398 for another variant. (Contributed by NM, 21-Jun-1993.) (Revised by BJ, 31-May-2019.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓) | ||
Theorem | cbval2v 2337* | Rule used to change bound variables, using implicit substitution. Version of cbval2 2408 with a disjoint variable condition, which does not require ax-13 2369. (Contributed by NM, 22-Dec-2003.) (Revised by BJ, 16-Jun-2019.) (Proof shortened by Gino Giotto, 10-Jan-2024.) |
⊢ Ⅎ𝑧𝜑 & ⊢ Ⅎ𝑤𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ Ⅎ𝑦𝜓 & ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑧∀𝑤𝜓) | ||
Theorem | cbvex2v 2338* | Rule used to change bound variables, using implicit substitution. Version of cbvex2 2409 with a disjoint variable condition, which does not require ax-13 2369. (Contributed by NM, 14-Sep-2003.) (Revised by BJ, 16-Jun-2019.) |
⊢ Ⅎ𝑧𝜑 & ⊢ Ⅎ𝑤𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ Ⅎ𝑦𝜓 & ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑧∃𝑤𝜓) | ||
Theorem | dvelimhw 2339* | Proof of dvelimh 2447 without using ax-13 2369 but with additional distinct variable conditions. (Contributed by NM, 1-Oct-2002.) (Revised by Andrew Salmon, 21-Jul-2011.) (Revised by NM, 1-Aug-2017.) (Proof shortened by Wolf Lammen, 23-Dec-2018.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜓 → ∀𝑧𝜓) & ⊢ (𝑧 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧)) ⇒ ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝜓 → ∀𝑥𝜓)) | ||
Theorem | pm11.53 2340* | Theorem *11.53 in [WhiteheadRussell] p. 164. See pm11.53v 1945 for a version requiring fewer axioms. (Contributed by Andrew Salmon, 24-May-2011.) |
⊢ (∀𝑥∀𝑦(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → ∀𝑦𝜓)) | ||
Theorem | 19.12vv 2341* | Special case of 19.12 2318 where its converse holds. See 19.12vvv 1990 for a version with a disjoint variable condition requiring fewer axioms. (Contributed by NM, 18-Jul-2001.) (Revised by Andrew Salmon, 11-Jul-2011.) |
⊢ (∃𝑥∀𝑦(𝜑 → 𝜓) ↔ ∀𝑦∃𝑥(𝜑 → 𝜓)) | ||
Theorem | eean 2342 | Distribute existential quantifiers. (Contributed by NM, 27-Oct-2010.) (Revised by Mario Carneiro, 6-Oct-2016.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ ∃𝑦𝜓)) | ||
Theorem | eeanv 2343* | Distribute a pair of existential quantifiers over a conjunction. Combination of 19.41v 1951 and 19.42v 1955. For a version requiring fewer axioms but with additional disjoint variable conditions, see exdistrv 1957. (Contributed by NM, 26-Jul-1995.) |
⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ ∃𝑦𝜓)) | ||
Theorem | eeeanv 2344* | Distribute three existential quantifiers over a conjunction. (Contributed by NM, 26-Jul-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.) Reduce distinct variable restrictions. (Revised by Wolf Lammen, 20-Jan-2018.) |
⊢ (∃𝑥∃𝑦∃𝑧(𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (∃𝑥𝜑 ∧ ∃𝑦𝜓 ∧ ∃𝑧𝜒)) | ||
Theorem | ee4anv 2345* | Distribute two pairs of existential quantifiers over a conjunction. For a version requiring fewer axioms but with additional disjoint variable conditions, see 4exdistrv 1958. (Contributed by NM, 31-Jul-1995.) |
⊢ (∃𝑥∃𝑦∃𝑧∃𝑤(𝜑 ∧ 𝜓) ↔ (∃𝑥∃𝑦𝜑 ∧ ∃𝑧∃𝑤𝜓)) | ||
Theorem | sb8v 2346* | Substitution of variable in universal quantifier. Version of sb8f 2347 with a disjoint variable condition replacing the nonfree hypothesis Ⅎ𝑦𝜑, not requiring ax-12 2169. (Contributed by SN, 5-Dec-2024.) |
⊢ (∀𝑥𝜑 ↔ ∀𝑦[𝑦 / 𝑥]𝜑) | ||
Theorem | sb8f 2347* | Substitution of variable in universal quantifier. Version of sb8 2514 with a disjoint variable condition, not requiring ax-10 2135 or ax-13 2369. (Contributed by NM, 16-May-1993.) (Revised by Wolf Lammen, 19-Jan-2023.) Avoid ax-10 2135. (Revised by SN, 5-Dec-2024.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (∀𝑥𝜑 ↔ ∀𝑦[𝑦 / 𝑥]𝜑) | ||
Theorem | sb8fOLD 2348* | Obsolete version of sb8f 2347 as of 5-Dec-2024. (Contributed by NM, 16-May-1993.) (Revised by Wolf Lammen, 19-Jan-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (∀𝑥𝜑 ↔ ∀𝑦[𝑦 / 𝑥]𝜑) | ||
Theorem | sb8ef 2349* | Substitution of variable in existential quantifier. Version of sb8e 2515 with a disjoint variable condition, not requiring ax-13 2369. (Contributed by NM, 12-Aug-1993.) (Revised by Wolf Lammen, 19-Jan-2023.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (∃𝑥𝜑 ↔ ∃𝑦[𝑦 / 𝑥]𝜑) | ||
Theorem | 2sb8ef 2350* | An equivalent expression for double existence. Version of 2sb8e 2527 with more disjoint variable conditions, not requiring ax-13 2369. (Contributed by Wolf Lammen, 28-Jan-2023.) |
⊢ Ⅎ𝑤𝜑 & ⊢ Ⅎ𝑧𝜑 ⇒ ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑧∃𝑤[𝑧 / 𝑥][𝑤 / 𝑦]𝜑) | ||
Theorem | sb6rfv 2351* | Reversed substitution. Version of sb6rf 2465 requiring disjoint variables, but fewer axioms. (Contributed by NM, 1-Aug-1993.) (Revised by Wolf Lammen, 7-Feb-2023.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (𝜑 ↔ ∀𝑦(𝑦 = 𝑥 → [𝑦 / 𝑥]𝜑)) | ||
Theorem | sbnf2 2352* | Two ways of expressing "𝑥 is (effectively) not free in 𝜑". (Contributed by Gérard Lang, 14-Nov-2013.) (Revised by Mario Carneiro, 6-Oct-2016.) (Proof shortened by Wolf Lammen, 22-Sep-2018.) Avoid ax-13 2369. (Revised by Wolf Lammen, 30-Jan-2023.) |
⊢ (Ⅎ𝑥𝜑 ↔ ∀𝑦∀𝑧([𝑦 / 𝑥]𝜑 ↔ [𝑧 / 𝑥]𝜑)) | ||
Theorem | exsb 2353* | An equivalent expression for existence. One direction (exsbim 2003) needs fewer axioms. (Contributed by NM, 2-Feb-2005.) Avoid ax-13 2369. (Revised by Wolf Lammen, 16-Oct-2022.) |
⊢ (∃𝑥𝜑 ↔ ∃𝑦∀𝑥(𝑥 = 𝑦 → 𝜑)) | ||
Theorem | 2exsb 2354* | An equivalent expression for double existence. (Contributed by NM, 2-Feb-2005.) (Proof shortened by Wolf Lammen, 30-Sep-2018.) |
⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑧∃𝑤∀𝑥∀𝑦((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝜑)) | ||
Theorem | sbbib 2355* | Reversal of substitution. (Contributed by AV, 6-Aug-2023.) (Proof shortened by Wolf Lammen, 4-Sep-2023.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (∀𝑦([𝑦 / 𝑥]𝜑 ↔ 𝜓) ↔ ∀𝑥(𝜑 ↔ [𝑥 / 𝑦]𝜓)) | ||
Theorem | sbbibvv 2356* | Reversal of substitution. (Contributed by AV, 6-Aug-2023.) |
⊢ (∀𝑦([𝑦 / 𝑥]𝜑 ↔ 𝜓) ↔ ∀𝑥(𝜑 ↔ [𝑥 / 𝑦]𝜓)) | ||
Theorem | cbvsbv 2357* | Change the bound variable (i.e. the substituted one) in wff's linked by implicit substitution. The proof was extracted from a former cbvabv 2803 version. (Contributed by Wolf Lammen, 16-Mar-2025.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ([𝑧 / 𝑥]𝜑 ↔ [𝑧 / 𝑦]𝜓) | ||
Theorem | cbvsbvf 2358* | Change the bound variable (i.e. the substituted one) in wff's linked by implicit substitution. The proof was part of a former cbvabw 2804 version. (Contributed by GG and WL, 26-Oct-2024.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ([𝑧 / 𝑥]𝜑 ↔ [𝑧 / 𝑦]𝜓) | ||
Theorem | cleljustALT 2359* | Alternate proof of cleljust 2113. It is kept here and should not be modified because it is referenced on the Metamath Proof Explorer Home Page (mmset.html) as an example of how disjoint variable conditions are inherited by substitutions. (Contributed by NM, 28-Jan-2004.) (Revised by BJ, 29-Dec-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 ∈ 𝑦 ↔ ∃𝑧(𝑧 = 𝑥 ∧ 𝑧 ∈ 𝑦)) | ||
Theorem | cleljustALT2 2360* | Alternate proof of cleljust 2113. Compared with cleljustALT 2359, it uses nfv 1915 followed by equsexv 2257 instead of ax-5 1911 followed by equsexhv 2286, so it uses the idiom Ⅎ𝑥𝜑 instead of 𝜑 → ∀𝑥𝜑 to express nonfreeness. This style is generally preferred for later theorems. (Contributed by NM, 28-Jan-2004.) (Revised by Mario Carneiro, 21-Dec-2016.) (Revised by BJ, 29-Dec-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 ∈ 𝑦 ↔ ∃𝑧(𝑧 = 𝑥 ∧ 𝑧 ∈ 𝑦)) | ||
Theorem | equs5aALT 2361 | Alternate proof of equs5a 2454. Uses ax-12 2169 but not ax-13 2369. (Contributed by NM, 2-Feb-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∃𝑥(𝑥 = 𝑦 ∧ ∀𝑦𝜑) → ∀𝑥(𝑥 = 𝑦 → 𝜑)) | ||
Theorem | equs5eALT 2362 | Alternate proof of equs5e 2455. Uses ax-12 2169 but not ax-13 2369. (Contributed by NM, 2-Feb-2007.) (Proof shortened by Wolf Lammen, 15-Jan-2018.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑦 → ∃𝑦𝜑)) | ||
Theorem | axc11r 2363 |
Same as axc11 2427 but with reversed antecedent. Note the use
of ax-12 2169
(and not merely ax12v 2170 as in axc11rv 2254).
This theorem is mostly used to eliminate conditions requiring set variables be distinct (cf. cbvaev 2054 and aecom 2424, for example) in proofs. In practice, theorems beyond elementary set theory do not really benefit from such eliminations. As of 2024, it is used in conjunction with ax-13 2369 only, and like that, it should be applied only in niches where indispensable. (Contributed by NM, 25-Jul-2015.) |
⊢ (∀𝑦 𝑦 = 𝑥 → (∀𝑥𝜑 → ∀𝑦𝜑)) | ||
Theorem | dral1v 2364* | Formula-building lemma for use with the Distinctor Reduction Theorem. Version of dral1 2436 with a disjoint variable condition, which does not require ax-13 2369. Remark: the corresponding versions for dral2 2435 and drex2 2439 are instances of albidv 1921 and exbidv 1922 respectively. (Contributed by NM, 24-Nov-1994.) (Revised by BJ, 17-Jun-2019.) Base the proof on ax12v 2170. (Revised by Wolf Lammen, 30-Mar-2024.) Avoid ax-10 2135. (Revised by Gino Giotto, 18-Nov-2024.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 ↔ ∀𝑦𝜓)) | ||
Theorem | dral1vOLD 2365* | Obsolete version of dral1v 2364 as of 18-Nov-2024. (Contributed by NM, 24-Nov-1994.) (Revised by BJ, 17-Jun-2019.) Base the proof on ax12v 2170. (Revised by Wolf Lammen, 30-Mar-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 ↔ ∀𝑦𝜓)) | ||
Theorem | drex1v 2366* | Formula-building lemma for use with the Distinctor Reduction Theorem. Version of drex1 2438 with a disjoint variable condition, which does not require ax-13 2369. (Contributed by NM, 27-Feb-2005.) (Revised by BJ, 17-Jun-2019.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 𝑥 = 𝑦 → (∃𝑥𝜑 ↔ ∃𝑦𝜓)) | ||
Theorem | drnf1v 2367* | Formula-building lemma for use with the Distinctor Reduction Theorem. Version of drnf1 2440 with a disjoint variable condition, which does not require ax-13 2369. (Contributed by Mario Carneiro, 4-Oct-2016.) (Revised by BJ, 17-Jun-2019.) Avoid ax-10 2135. (Revised by Gino Giotto, 18-Nov-2024.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 𝑥 = 𝑦 → (Ⅎ𝑥𝜑 ↔ Ⅎ𝑦𝜓)) | ||
Theorem | drnf1vOLD 2368* | Obsolete version of drnf1v 2367 as of 18-Nov-2024. (Contributed by Mario Carneiro, 4-Oct-2016.) (Revised by BJ, 17-Jun-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 𝑥 = 𝑦 → (Ⅎ𝑥𝜑 ↔ Ⅎ𝑦𝜓)) | ||
Axiom | ax-13 2369 |
Axiom of Quantified Equality. One of the equality and substitution axioms
of predicate calculus with equality.
An equivalent way to express this axiom that may be easier to understand is (¬ 𝑥 = 𝑦 → (¬ 𝑥 = 𝑧 → (𝑦 = 𝑧 → ∀𝑥𝑦 = 𝑧))) (see ax13b 2033). Recall that in the intended interpretation, our variables are metavariables ranging over the variables of predicate calculus (the object language). In order for the first antecedent ¬ 𝑥 = 𝑦 to hold, 𝑥 and 𝑦 must have different values and thus cannot be the same object-language variable (so they are effectively "distinct variables" even though no $d is present). Similarly, 𝑥 and 𝑧 cannot be the same object-language variable. Therefore, 𝑥 will not occur in the wff 𝑦 = 𝑧 when the first two antecedents hold, so analogous to ax-5 1911, the conclusion (𝑦 = 𝑧 → ∀𝑥𝑦 = 𝑧) follows. Note that ax-5 1911 cannot prove this because its distinct variable ($d) requirement is not satisfied directly but only indirectly (outside of Metamath) by the argument above. The original version of this axiom was ax-c9 38063 and was replaced with this shorter ax-13 2369 in December 2015. The old axiom is proved from this one as Theorem axc9 2379. The primary purpose of this axiom is to provide a way to introduce the quantifier ∀𝑥 on 𝑦 = 𝑧 even when 𝑥 and 𝑦 are substituted with the same variable. In this case, the first antecedent becomes ¬ 𝑥 = 𝑥 and the axiom still holds. This axiom is mostly used to eliminate conditions requiring set variables be distinct (cf. ax6ev 1971 and ax6e 2380, for example) in proofs. In practice, theorems beyond elementary set theory do not really benefit from such eliminations, so direct or indirect application of this axiom is discouraged now. You need to explicitly confirm its use in case you see a sensible application in a niche. After some assisting contributions by others over the years, it was in particular the extensive work of Gino Giotto in 2024 that helped reducing dependencies on this axiom on a large scale. Although this version is shorter, the original version axc9 2379 may be more practical to work with because of the "distinctor" form of its antecedents. A typical application of axc9 2379 is in dvelimh 2447 which converts a distinct variable pair to the distinctor antecedent ¬ ∀𝑥𝑥 = 𝑦. In particular, it is conjectured that it is not possible to prove ax6 2381 from ax6v 1970 without this axiom. This axiom can be weakened if desired by adding distinct variable restrictions on pairs 𝑥, 𝑧 and 𝑦, 𝑧. To show that, we add these restrictions to Theorem ax13v 2370 and use only ax13v 2370 for further derivations. Thus, ax13v 2370 should be the only theorem referencing this axiom. Other theorems can reference either ax13v 2370 (preferred) or ax13 2372 (if the stronger form is needed). This axiom scheme is logically redundant (see ax13w 2130) but is used as an auxiliary axiom scheme to achieve scheme completeness (i.e. so that all possible cases of bundling can be proved; see text linked at mmtheorems.html#ax6dgen 2130). It is not known whether this axiom can be derived from the others. (Contributed by NM, 21-Dec-2015.) (New usage is discouraged.) |
⊢ (¬ 𝑥 = 𝑦 → (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧)) | ||
Theorem | ax13v 2370* |
A weaker version of ax-13 2369 with distinct variable restrictions on pairs
𝑥,
𝑧 and 𝑦, 𝑧. In order to show (with
ax13 2372) that this
weakening is still adequate, this should be the only theorem referencing
ax-13 2369 directly.
Had we additionally required 𝑥 and 𝑦 be distinct, too, this theorem would have been a direct consequence of ax-5 1911. So essentially this theorem states, that a distinct variable condition can be replaced with an inequality between set variables. Preferably, use the version ax13w 2130 to avoid the propagation of ax-13 2369. (Contributed by NM, 30-Jun-2016.) (New usage is discouraged.) |
⊢ (¬ 𝑥 = 𝑦 → (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧)) | ||
Theorem | ax13lem1 2371* | A version of ax13v 2370 with one distinct variable restriction dropped. For convenience, 𝑦 is kept on the right side of equations. The proof of ax13 2372 bases on ideas from NM, 24-Dec-2015. (Contributed by Wolf Lammen, 8-Sep-2018.) (New usage is discouraged.) |
⊢ (¬ 𝑥 = 𝑦 → (𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦)) | ||
Theorem | ax13 2372 | Derive ax-13 2369 from ax13v 2370 and Tarski's FOL. This shows that the weakening in ax13v 2370 is still sufficient for a complete system. Preferably, use the weaker ax13w 2130 to avoid the propagation of ax-13 2369. (Contributed by NM, 21-Dec-2015.) (Proof shortened by Wolf Lammen, 31-Jan-2018.) Reduce axiom usage. (Revised by Wolf Lammen, 2-Jun-2021.) (New usage is discouraged.) |
⊢ (¬ 𝑥 = 𝑦 → (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧)) | ||
Theorem | ax13lem2 2373* | Lemma for nfeqf2 2374. This lemma is equivalent to ax13v 2370 with one distinct variable constraint removed. (Contributed by Wolf Lammen, 8-Sep-2018.) Reduce axiom usage. (Revised by Wolf Lammen, 18-Oct-2020.) (New usage is discouraged.) |
⊢ (¬ 𝑥 = 𝑦 → (∃𝑥 𝑧 = 𝑦 → 𝑧 = 𝑦)) | ||
Theorem | nfeqf2 2374* | An equation between setvar is free of any other setvar. Usage of this theorem is discouraged because it depends on ax-13 2369. (Contributed by Wolf Lammen, 9-Jun-2019.) Remove dependency on ax-12 2169. (Revised by Wolf Lammen, 16-Dec-2022.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥 𝑧 = 𝑦) | ||
Theorem | dveeq2 2375* | Quantifier introduction when one pair of variables is distinct. Usage of this theorem is discouraged because it depends on ax-13 2369. (Contributed by NM, 2-Jan-2002.) (Revised by NM, 20-Jul-2015.) Remove dependency on ax-11 2152. (Revised by Wolf Lammen, 8-Sep-2018.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦)) | ||
Theorem | nfeqf1 2376* | An equation between setvar is free of any other setvar. Usage of this theorem is discouraged because it depends on ax-13 2369. (Contributed by Wolf Lammen, 10-Jun-2019.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥 𝑦 = 𝑧) | ||
Theorem | dveeq1 2377* | Quantifier introduction when one pair of variables is distinct. Usage of this theorem is discouraged because it depends on ax-13 2369. (Contributed by NM, 2-Jan-2002.) Remove dependency on ax-11 2152. (Revised by Wolf Lammen, 8-Sep-2018.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧)) | ||
Theorem | nfeqf 2378 | A variable is effectively not free in an equality if it is not either of the involved variables. Ⅎ version of ax-c9 38063. Usage of this theorem is discouraged because it depends on ax-13 2369. (Contributed by Mario Carneiro, 6-Oct-2016.) Remove dependency on ax-11 2152. (Revised by Wolf Lammen, 6-Sep-2018.) (New usage is discouraged.) |
⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦) → Ⅎ𝑧 𝑥 = 𝑦) | ||
Theorem | axc9 2379 | Derive set.mm's original ax-c9 38063 from the shorter ax-13 2369. Usage is discouraged to avoid uninformed ax-13 2369 propagation. (Contributed by NM, 29-Nov-2015.) (Revised by NM, 24-Dec-2015.) (Proof shortened by Wolf Lammen, 29-Apr-2018.) (New usage is discouraged.) |
⊢ (¬ ∀𝑧 𝑧 = 𝑥 → (¬ ∀𝑧 𝑧 = 𝑦 → (𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦))) | ||
Theorem | ax6e 2380 |
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 1809 through ax-9 2114,
all axioms other than
ax-6 1969 are believed to be theorems of free logic,
although the system
without ax-6 1969 is not complete in free logic.
Usage of this theorem is discouraged because it depends on ax-13 2369. It is preferred to use ax6ev 1971 when it is sufficient. (Contributed by NM, 14-May-1993.) Shortened after ax13lem1 2371 became available. (Revised by Wolf Lammen, 8-Sep-2018.) (New usage is discouraged.) |
⊢ ∃𝑥 𝑥 = 𝑦 | ||
Theorem | ax6 2381 |
Theorem showing that ax-6 1969 follows from the weaker version ax6v 1970.
(Even though this theorem depends on ax-6 1969,
all references of ax-6 1969 are
made via ax6v 1970. An earlier version stated ax6v 1970
as a separate axiom,
but having two axioms caused some confusion.)
This theorem should be referenced in place of ax-6 1969 so that all proofs can be traced back to ax6v 1970. When possible, use the weaker ax6v 1970 rather than ax6 2381 since the ax6v 1970 derivation is much shorter and requires fewer axioms. (Contributed by NM, 12-Nov-2013.) (Revised by NM, 25-Jul-2015.) (Proof shortened by Wolf Lammen, 4-Feb-2018.) Usage of this theorem is discouraged because it depends on ax-13 2369. Use ax6v 1970 instead. (New usage is discouraged.) |
⊢ ¬ ∀𝑥 ¬ 𝑥 = 𝑦 | ||
Theorem | axc10 2382 |
Show that the original axiom ax-c10 38059 can be derived from ax6 2381
and axc7 2308
(on top of propositional calculus, ax-gen 1795, and ax-4 1809). See
ax6fromc10 38069 for the rederivation of ax6 2381
from ax-c10 38059.
Normally, axc10 2382 should be used rather than ax-c10 38059, except by theorems specifically studying the latter's properties. See bj-axc10v 35974 for a weaker version requiring fewer axioms. (Contributed by NM, 5-Aug-1993.) (Proof modification is discouraged.) Usage of this theorem is discouraged because it depends on ax-13 2369. (New usage is discouraged.) |
⊢ (∀𝑥(𝑥 = 𝑦 → ∀𝑥𝜑) → 𝜑) | ||
Theorem | spimt 2383 | Closed theorem form of spim 2384. (Contributed by NM, 15-Jan-2008.) (Revised by Mario Carneiro, 17-Oct-2016.) (Proof shortened by Wolf Lammen, 21-Mar-2023.) Usage of this theorem is discouraged because it depends on ax-13 2369. (New usage is discouraged.) |
⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝑦 → (𝜑 → 𝜓))) → (∀𝑥𝜑 → 𝜓)) | ||
Theorem | spim 2384 | Specialization, using implicit substitution. Compare Lemma 14 of [Tarski] p. 70. The spim 2384 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 2369. See spimw 1972 for a version requiring fewer axioms. (Contributed by NM, 10-Jan-1993.) (Revised by Mario Carneiro, 3-Oct-2016.) (Proof shortened by Wolf Lammen, 18-Feb-2018.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) ⇒ ⊢ (∀𝑥𝜑 → 𝜓) | ||
Theorem | spimed 2385 | Deduction version of spime 2386. (Contributed by NM, 14-May-1993.) (Revised by Mario Carneiro, 3-Oct-2016.) (Proof shortened by Wolf Lammen, 19-Feb-2018.) Usage of this theorem is discouraged because it depends on ax-13 2369. Use spimedv 2188 instead. (New usage is discouraged.) |
⊢ (𝜒 → Ⅎ𝑥𝜑) & ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) ⇒ ⊢ (𝜒 → (𝜑 → ∃𝑥𝜓)) | ||
Theorem | spime 2386 | Existential introduction, using implicit substitution. Compare Lemma 14 of [Tarski] p. 70. See spimew 1973 and spimevw 1996 for weaker versions requiring fewer axioms. (Contributed by NM, 7-Aug-1994.) (Revised by Mario Carneiro, 3-Oct-2016.) (Proof shortened by Wolf Lammen, 6-Mar-2018.) Usage of this theorem is discouraged because it depends on ax-13 2369. Use spimefv 2189 instead. (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) ⇒ ⊢ (𝜑 → ∃𝑥𝜓) | ||
Theorem | spimv 2387* | A version of spim 2384 with a distinct variable requirement instead of a bound-variable hypothesis. See spimfv 2230 and spimvw 1997 for versions requiring fewer axioms. (Contributed by NM, 31-Jul-1993.) Usage of this theorem is discouraged because it depends on ax-13 2369. Use spimvw 1997 instead. (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) ⇒ ⊢ (∀𝑥𝜑 → 𝜓) | ||
Theorem | spimvALT 2388* | Alternate proof of spimv 2387. Note that it requires only ax-1 6 through ax-5 1911 together with ax6e 2380. Currently, proofs derive from ax6v 1970, but if ax-6 1969 could be used instead, this proof would reduce axiom usage. (Contributed by NM, 31-Jul-1993.) Remove dependency on ax-10 2135. (Revised by BJ, 29-Nov-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) ⇒ ⊢ (∀𝑥𝜑 → 𝜓) | ||
Theorem | spimev 2389* | Distinct-variable version of spime 2386. (Contributed by NM, 10-Jan-1993.) Usage of this theorem is discouraged because it depends on ax-13 2369. Use spimevw 1996 instead. (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) ⇒ ⊢ (𝜑 → ∃𝑥𝜓) | ||
Theorem | spv 2390* | Specialization, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2369. Use the weaker spvv 1998 if possible. (Contributed by NM, 30-Aug-1993.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥𝜑 → 𝜓) | ||
Theorem | spei 2391 | Inference from existential specialization, using implicit substitution. Remove a distinct variable constraint. Usage of this theorem is discouraged because it depends on ax-13 2369. Use the weaker speiv 1974 if possible. (Contributed by NM, 19-Aug-1993.) (Proof shortened by Wolf Lammen, 12-May-2018.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ 𝜓 ⇒ ⊢ ∃𝑥𝜑 | ||
Theorem | chvar 2392 | Implicit substitution of 𝑦 for 𝑥 into a theorem. Usage of this theorem is discouraged because it depends on ax-13 2369. Use the weaker chvarfv 2231 if possible. (Contributed by Raph Levien, 9-Jul-2003.) (Revised by Mario Carneiro, 3-Oct-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ 𝜑 ⇒ ⊢ 𝜓 | ||
Theorem | chvarv 2393* | Implicit substitution of 𝑦 for 𝑥 into a theorem. Usage of this theorem is discouraged because it depends on ax-13 2369. Use the weaker chvarvv 2000 if possible. (Contributed by NM, 20-Apr-1994.) (Proof shortened by Wolf Lammen, 22-Apr-2018.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ 𝜑 ⇒ ⊢ 𝜓 | ||
Theorem | cbv3 2394 | Rule used to change bound variables, using implicit substitution, that does not use ax-c9 38063. Usage of this theorem is discouraged because it depends on ax-13 2369. Use the weaker cbv3v 2329 if possible. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 12-May-2018.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) ⇒ ⊢ (∀𝑥𝜑 → ∀𝑦𝜓) | ||
Theorem | cbval 2395 | Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2369. Check out cbvalw 2036, cbvalvw 2037, cbvalv1 2335 for versions requiring fewer axioms. (Contributed by NM, 13-May-1993.) (Revised by Mario Carneiro, 3-Oct-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓) | ||
Theorem | cbvex 2396 | Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2369. Check out cbvexvw 2038, cbvexv1 2336 for weaker versions requiring fewer axioms. (Contributed by NM, 21-Jun-1993.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓) | ||
Theorem | cbvalv 2397* | Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2369. See cbvalvw 2037 for a version requiring fewer axioms, to be preferred when sufficient. (Contributed by NM, 5-Aug-1993.) Remove dependency on ax-10 2135 and shorten proof. (Revised by Wolf Lammen, 11-Sep-2023.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓) | ||
Theorem | cbvexv 2398* | Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2369. See cbvexvw 2038 for a version requiring fewer axioms, to be preferred when sufficient. (Contributed by NM, 21-Jun-1993.) Remove dependency on ax-10 2135 and shorten proof. (Revised by Wolf Lammen, 11-Sep-2023.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓) | ||
Theorem | cbv1 2399 | Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2369. See cbv1v 2330 with disjoint variable conditions, not depending on ax-13 2369. (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 2400 | Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2369. See cbv2w 2331 with disjoint variable conditions, not depending on ax-13 2369. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 3-Oct-2016.) Format hypotheses to common style, avoid ax-10 2135. (Revised by Wolf Lammen, 10-Sep-2023.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑦𝜓) & ⊢ (𝜑 → Ⅎ𝑥𝜒) & ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))) ⇒ ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |