Home | Metamath
Proof Explorer Theorem List (p. 24 of 449) | < 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-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | hb3an 2301 | If 𝑥 is not free in 𝜑, 𝜓, and 𝜒, it is not free in (𝜑 ∧ 𝜓 ∧ 𝜒). (Contributed by NM, 14-Sep-2003.) (Proof shortened by Wolf Lammen, 2-Jan-2018.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜓 → ∀𝑥𝜓) & ⊢ (𝜒 → ∀𝑥𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → ∀𝑥(𝜑 ∧ 𝜓 ∧ 𝜒)) | ||
Theorem | sbi2 2302 | Introduction of implication into substitution. (Contributed by NM, 14-May-1993.) |
⊢ (([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓) → [𝑦 / 𝑥](𝜑 → 𝜓)) | ||
Theorem | sbim 2303 | Implication inside and outside of a substitution are equivalent. (Contributed by NM, 14-May-1993.) |
⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓)) | ||
Theorem | sbanOLD 2304 | Obsolete version of sban 2077 as of 13-Aug-2023. Conjunction inside and outside of a substitution are equivalent. (Contributed by NM, 14-May-1993.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ([𝑦 / 𝑥](𝜑 ∧ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓)) | ||
Theorem | sbrim 2305 | Substitution in an implication with a variable not free in the antecedent affects only the consequent. See sbrimv 2306 for a version with disjoint variables not requiring ax-10 2136. (Contributed by NM, 2-Jun-1993.) (Revised by Mario Carneiro, 4-Oct-2016.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ (𝜑 → [𝑦 / 𝑥]𝜓)) | ||
Theorem | sbrimv 2306* | Substitution in an implication with a variable not free in the antecedent affects only the consequent. Version of sbrim 2305 not depending on ax-10 2136, but with disjoint variables. (Contributed by Wolf Lammen, 28-Jan-2024.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ (𝜑 → [𝑦 / 𝑥]𝜓)) | ||
Theorem | sblim 2307 | Substitution in an implication with a variable not free in the consequent affects only the antecedent. (Contributed by NM, 14-Nov-2013.) (Revised by Mario Carneiro, 4-Oct-2016.) |
⊢ Ⅎ𝑥𝜓 ⇒ ⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ ([𝑦 / 𝑥]𝜑 → 𝜓)) | ||
Theorem | sbor 2308 | Disjunction inside and outside of a substitution are equivalent. (Contributed by NM, 29-Sep-2002.) |
⊢ ([𝑦 / 𝑥](𝜑 ∨ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 ∨ [𝑦 / 𝑥]𝜓)) | ||
Theorem | sbbi 2309 | Equivalence inside and outside of a substitution are equivalent. (Contributed by NM, 14-May-1993.) |
⊢ ([𝑦 / 𝑥](𝜑 ↔ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜓)) | ||
Theorem | spsbbiOLD 2310 | Obsolete version of spsbbi 2069 as of 6-Jul-2023. Specialization of biconditional. (Contributed by NM, 2-Jun-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥(𝜑 ↔ 𝜓) → ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜓)) | ||
Theorem | sblbis 2311 | Introduce left biconditional inside of a substitution. (Contributed by NM, 19-Aug-1993.) |
⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓) ⇒ ⊢ ([𝑦 / 𝑥](𝜒 ↔ 𝜑) ↔ ([𝑦 / 𝑥]𝜒 ↔ 𝜓)) | ||
Theorem | sbrbis 2312 | Introduce right biconditional inside of a substitution. (Contributed by NM, 18-Aug-1993.) |
⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓) ⇒ ⊢ ([𝑦 / 𝑥](𝜑 ↔ 𝜒) ↔ (𝜓 ↔ [𝑦 / 𝑥]𝜒)) | ||
Theorem | sbrbif 2313 | Introduce right biconditional inside of a substitution. (Contributed by NM, 18-Aug-1993.) (Revised by Mario Carneiro, 4-Oct-2016.) |
⊢ Ⅎ𝑥𝜒 & ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓) ⇒ ⊢ ([𝑦 / 𝑥](𝜑 ↔ 𝜒) ↔ (𝜓 ↔ 𝜒)) | ||
Theorem | sbnvOLD 2314* | Obsolete version of sbn 2279 as of 8-Jul-2023. Substitution is not affected by negation. Version of sbn 2279 with a disjoint variable condition, not requiring ax-13 2383. (Contributed by Wolf Lammen, 18-Jan-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ([𝑦 / 𝑥] ¬ 𝜑 ↔ ¬ [𝑦 / 𝑥]𝜑) | ||
Theorem | sbi1vOLD 2315* | Obsolete version of sbi1 2067 as of 24-Jul-2023. Move implication out of substitution. Version of sbi1 2067 with a disjoint variable condition, not requiring ax-13 2383. (Contributed by Wolf Lammen, 18-Jan-2023.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) → ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓)) | ||
Theorem | sbi2vOLD 2316* | Obsolete version of sbi2 2302 as of 8-Jul-2023. Move implication into substitution. Version of sbi2 2302 with a disjoint variable condition, not requiring ax-13 2383. (Contributed by Wolf Lammen, 18-Jan-2023.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓) → [𝑦 / 𝑥](𝜑 → 𝜓)) | ||
Theorem | sbimvOLD 2317* | Obsolete version of sbim 2303 as of 24-Jul-2023. Substitution distributes over implication. Version of sbim 2303 with a disjoint variable condition, not requiring ax-13 2383. (Contributed by Wolf Lammen, 18-Jan-2023.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓)) | ||
Theorem | sbanvOLD 2318* | Obsolete version of sban 2077 as of 24-Jul-2023. Substitution distributes over conjunction. Version of sban 2077 with a disjoint variable condition, not requiring ax-13 2383. (Contributed by Wolf Lammen, 18-Jan-2023.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ([𝑦 / 𝑥](𝜑 ∧ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓)) | ||
Theorem | sbbivOLD 2319* | Obsolete version of sbbi 2309 as of 24-Jul-2023. Substitution distributes over a biconditional. Version of sbbi 2309 with a disjoint variable condition, not requiring ax-11 2151 nor ax-13 2383. (Contributed by Wolf Lammen, 18-Jan-2023.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ([𝑦 / 𝑥](𝜑 ↔ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜓)) | ||
Theorem | spsbimvOLD 2320* | Obsolete version of spsbim 2068 as of 6-Jul-2023. Specialization of implication. Version of spsbim 2068 with a disjoint variable condition, not requiring ax-13 2383. (Contributed by Wolf Lammen, 19-Jan-2023.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (∀𝑥(𝜑 → 𝜓) → ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓)) | ||
Theorem | sblbisvOLD 2321* | Obsolete version of sblbis 2311 as of 24-Jul-2023. Introduce left biconditional inside of a substitution. Version of sblbis 2311 with a disjoint variable condition, not requiring ax-13 2383. (Contributed by Wolf Lammen, 18-Jan-2023.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓) ⇒ ⊢ ([𝑦 / 𝑥](𝜒 ↔ 𝜑) ↔ ([𝑦 / 𝑥]𝜒 ↔ 𝜓)) | ||
Theorem | sbiev 2322* | Conversion of implicit substitution to explicit substitution. Version of sbie 2540 with a disjoint variable condition, not requiring ax-13 2383. See sbievw 2094 for a version with a disjoint variable condition requiring fewer axioms. (Contributed by Wolf Lammen, 18-Jan-2023.) Remove dependence on ax-10 2136 and shorten proof. (Revised by BJ, 18-Jul-2023.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓) | ||
Theorem | sbievOLD 2323* | Obsolete proof of sbiev 2322 as of 18-Jul-2023. (Contributed by Wolf Lammen, 18-Jan-2023.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓) | ||
Theorem | sbiedw 2324* | Version of sbied 2541 with a disjoint variable condition, requiring fewer axioms. (Contributed by Gino Giotto, 10-Jan-2024.) Avoid ax-10 2136. (Revised by Wolf Lammen, 28-Jan-2024.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝜒) & ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))) ⇒ ⊢ (𝜑 → ([𝑦 / 𝑥]𝜓 ↔ 𝜒)) | ||
Theorem | sbiedwOLD 2325* | Obsolete version of sbiedw 2324 as of 28-Jan-2024. (Contributed by Gino Giotto, 10-Jan-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝜒) & ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))) ⇒ ⊢ (𝜑 → ([𝑦 / 𝑥]𝜓 ↔ 𝜒)) | ||
Theorem | sbequivvOLD 2326* | Obsolete version of sbequi 2082 as of 7-Jul-2023. Version of sbequi 2082 with disjoint variable conditions, not requiring ax-13 2383. (Contributed by Wolf Lammen, 19-Jan-2023.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 → [𝑦 / 𝑧]𝜑)) | ||
Theorem | sbequvvOLD 2327* | Obsolete version of sbequ 2081 as of 7-Jul-2023. Version of sbequ 2081 with disjoint variable conditions, not requiring ax-13 2383. (Contributed by Wolf Lammen, 19-Jan-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 ↔ [𝑦 / 𝑧]𝜑)) | ||
Theorem | axc7 2328 |
Show that the original axiom ax-c7 35903 can be derived from ax-10 2136
(hbn1 2137) , sp 2172 and propositional calculus. See ax10fromc7 35913 for the
rederivation of ax-10 2136 from ax-c7 35903.
Normally, axc7 2328 should be used rather than ax-c7 35903, except by theorems specifically studying the latter's properties. (Contributed by NM, 21-May-2008.) |
⊢ (¬ ∀𝑥 ¬ ∀𝑥𝜑 → 𝜑) | ||
Theorem | axc7e 2329 | Abbreviated version of axc7 2328 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 2330 | The analogue in our predicate calculus of the Brouwer axiom (B) of modal logic S5. (Contributed by NM, 5-Oct-2005.) |
⊢ (𝜑 → ∀𝑥 ¬ ∀𝑥 ¬ 𝜑) | ||
Theorem | 19.9ht 2331 | A closed version of 19.9h 2286. (Contributed by NM, 13-May-1993.) (Proof shortened by Wolf Lammen, 3-Mar-2018.) |
⊢ (∀𝑥(𝜑 → ∀𝑥𝜑) → (∃𝑥𝜑 → 𝜑)) | ||
Theorem | axc4 2332 |
Show that the original axiom ax-c4 35902 can be derived from ax-4 1801
(alim 1802), ax-10 2136 (hbn1 2137), sp 2172 and propositional calculus. See
ax4fromc4 35912 for the rederivation of ax-4 1801
from ax-c4 35902.
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 2333 | Inference version of axc4 2332. (Contributed by NM, 3-Jan-1993.) |
⊢ (∀𝑥𝜑 → 𝜓) ⇒ ⊢ (∀𝑥𝜑 → ∀𝑥𝜓) | ||
Theorem | nfal 2334 | If 𝑥 is not free in 𝜑, it is not free in ∀𝑦𝜑. (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ Ⅎ𝑥∀𝑦𝜑 | ||
Theorem | nfex 2335 | If 𝑥 is not free in 𝜑, 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 2335, hbex 2336. (Revised by Wolf Lammen, 16-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ Ⅎ𝑥∃𝑦𝜑 | ||
Theorem | hbex 2336 | If 𝑥 is not free in 𝜑, it is not free in ∃𝑦𝜑. (Contributed by NM, 12-Mar-1993.) Reduce symbol count in nfex 2335, hbex 2336. (Revised by Wolf Lammen, 16-Oct-2021.) |
⊢ (𝜑 → ∀𝑥𝜑) ⇒ ⊢ (∃𝑦𝜑 → ∀𝑥∃𝑦𝜑) | ||
Theorem | nfnf 2337 | If 𝑥 is not free in 𝜑, it is not free in Ⅎ𝑦𝜑. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ Ⅎ𝑥Ⅎ𝑦𝜑 | ||
Theorem | 19.12 2338 | 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 2360 and r19.12sn 4650. (Contributed by NM, 12-Mar-1993.) (Proof shortened by Wolf Lammen, 3-Jan-2018.) |
⊢ (∃𝑥∀𝑦𝜑 → ∀𝑦∃𝑥𝜑) | ||
Theorem | nfald 2339 | Deduction form of nfal 2334. (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 16-Oct-2021.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝜓) ⇒ ⊢ (𝜑 → Ⅎ𝑥∀𝑦𝜓) | ||
Theorem | nfexd 2340 | If 𝑥 is not free in 𝜓, it is not free in ∃𝑦𝜓. (Contributed by Mario Carneiro, 24-Sep-2016.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝜓) ⇒ ⊢ (𝜑 → Ⅎ𝑥∃𝑦𝜓) | ||
Theorem | nfsbv 2341* | If 𝑧 is not free in 𝜑, it is not free in [𝑦 / 𝑥]𝜑 when 𝑧 is distinct from 𝑥 and 𝑦. Version of nfsb 2561 requiring more disjoint variables, but fewer axioms. (Contributed by Wolf Lammen, 7-Feb-2023.) Remove disjoint variable condition on 𝑥, 𝑦. (Revised by Steven Nguyen, 13-Aug-2023.) |
⊢ Ⅎ𝑧𝜑 ⇒ ⊢ Ⅎ𝑧[𝑦 / 𝑥]𝜑 | ||
Theorem | nfsbvOLD 2342* | Obsolete version of nfsbv 2341 as of 13-Aug-2023. (Contributed by Wolf Lammen, 7-Feb-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑧𝜑 ⇒ ⊢ Ⅎ𝑧[𝑦 / 𝑥]𝜑 | ||
Theorem | hbsbw 2343* | Version of hbsb 2563 with a disjoint variable condition, which does not require ax-13 2383. (Contributed by Gino Giotto, 10-Jan-2024.) |
⊢ (𝜑 → ∀𝑧𝜑) ⇒ ⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑧[𝑦 / 𝑥]𝜑) | ||
Theorem | sbco2v 2344* | Version of sbco2 2549 with disjoint variable conditions, not requiring ax-13 2383, but ax-11 2151. (Contributed by Wolf Lammen, 29-Apr-2023.) |
⊢ Ⅎ𝑧𝜑 ⇒ ⊢ ([𝑦 / 𝑧][𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑) | ||
Theorem | aaan 2345 | Rearrange universal quantifiers. (Contributed by NM, 12-Aug-1993.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (∀𝑥∀𝑦(𝜑 ∧ 𝜓) ↔ (∀𝑥𝜑 ∧ ∀𝑦𝜓)) | ||
Theorem | eeor 2346 | Rearrange existential quantifiers. (Contributed by NM, 8-Aug-1994.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (∃𝑥∃𝑦(𝜑 ∨ 𝜓) ↔ (∃𝑥𝜑 ∨ ∃𝑦𝜓)) | ||
Theorem | cbv3v 2347* | Version of cbv3 2409 with a disjoint variable condition, which does not require ax-13 2383. (Contributed by BJ, 31-May-2019.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) ⇒ ⊢ (∀𝑥𝜑 → ∀𝑦𝜓) | ||
Theorem | cbv1v 2348* | Version of cbv1 2416 with a disjoint variable condition, which does not require ax-13 2383. (Contributed by BJ, 16-Jun-2019.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑦𝜓) & ⊢ (𝜑 → Ⅎ𝑥𝜒) & ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 → 𝜒))) ⇒ ⊢ (𝜑 → (∀𝑥𝜓 → ∀𝑦𝜒)) | ||
Theorem | cbv2w 2349* | Version of cbv2 2417 with a disjoint variable condition, which does not require ax-13 2383. (Contributed by Gino Giotto, 10-Jan-2024.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑦𝜓) & ⊢ (𝜑 → Ⅎ𝑥𝜒) & ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))) ⇒ ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒)) | ||
Theorem | cbvaldw 2350* | Version of cbvald 2422 with a disjoint variable condition, which does not require ax-13 2383. (Contributed by Gino Giotto, 10-Jan-2024.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑦𝜓) & ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))) ⇒ ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒)) | ||
Theorem | cbvexdw 2351* | Version of cbvexd 2423 with a disjoint variable condition, which does not require ax-13 2383. (Contributed by Gino Giotto, 10-Jan-2024.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑦𝜓) & ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))) ⇒ ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑦𝜒)) | ||
Theorem | cbv3hv 2352* | Version of cbv3h 2418 with a disjoint variable condition on 𝑥, 𝑦, which does not require ax-13 2383. Was used in a proof of axc11n 2443 (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 2353* | Version of cbval 2410 with a disjoint variable condition, which does not require ax-13 2383. See cbvalvw 2034 for a version with two disjoint variable conditions, requiring fewer axioms, and cbvalv 2412 for another variant. (Contributed by BJ, 31-May-2019.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓) | ||
Theorem | cbvexv1 2354* | Version of cbvex 2411 with a disjoint variable condition, which does not require ax-13 2383. See cbvexvw 2035 for a version with two disjoint variable conditions, requiring fewer axioms, and cbvexv 2413 for another variant. (Contributed by BJ, 31-May-2019.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓) | ||
Theorem | cbval2v 2355* | Version of cbval2 2426 with a disjoint variable condition, which does not require ax-13 2383. (Contributed by BJ, 16-Jun-2019.) (Proof shortened by Gino Giotto, 10-Jan-2024.) |
⊢ Ⅎ𝑧𝜑 & ⊢ Ⅎ𝑤𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ Ⅎ𝑦𝜓 & ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑧∀𝑤𝜓) | ||
Theorem | cbval2vOLD 2356* | Obsolete version of cbval2v 2355 as of 14-Jan-2024. (Contributed by BJ, 16-Jan-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑧𝜑 & ⊢ Ⅎ𝑤𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ Ⅎ𝑦𝜓 & ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑧∀𝑤𝜓) | ||
Theorem | cbvex2v 2357* | Version of cbvex2 2428 with a disjoint variable condition, which does not require ax-13 2383. (Contributed by BJ, 16-Jun-2019.) |
⊢ Ⅎ𝑧𝜑 & ⊢ Ⅎ𝑤𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ Ⅎ𝑦𝜓 & ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑧∃𝑤𝜓) | ||
Theorem | dvelimhw 2358* | Proof of dvelimh 2467 without using ax-13 2383 but with additional distinct variable conditions. (Contributed by Andrew Salmon, 21-Jul-2011.) (Revised by NM, 1-Aug-2017.) (Proof shortened by Wolf Lammen, 23-Dec-2018.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜓 → ∀𝑧𝜓) & ⊢ (𝑧 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧)) ⇒ ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝜓 → ∀𝑥𝜓)) | ||
Theorem | pm11.53 2359* | Theorem *11.53 in [WhiteheadRussell] p. 164. See pm11.53v 1936 for a version requiring fewer axioms. (Contributed by Andrew Salmon, 24-May-2011.) |
⊢ (∀𝑥∀𝑦(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → ∀𝑦𝜓)) | ||
Theorem | 19.12vv 2360* | Special case of 19.12 2338 where its converse holds. See 19.12vvv 1986 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 2361 | Rearrange existential quantifiers. (Contributed by NM, 27-Oct-2010.) (Revised by Mario Carneiro, 6-Oct-2016.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ ∃𝑦𝜓)) | ||
Theorem | eeanv 2362* | Distribute a pair of existential quantifiers over a conjunction. Combination of 19.41v 1941 and 19.42v 1945. For a version requiring fewer axioms but with additional disjoint variable conditions, see exdistrv 1947. (Contributed by NM, 26-Jul-1995.) |
⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ ∃𝑦𝜓)) | ||
Theorem | eeeanv 2363* | 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 2364* | Distribute two pairs of existential quantifiers over a conjunction. For a version requiring fewer axioms but with additional disjoint variable conditions, see 4exdistrv 1948. (Contributed by NM, 31-Jul-1995.) |
⊢ (∃𝑥∃𝑦∃𝑧∃𝑤(𝜑 ∧ 𝜓) ↔ (∃𝑥∃𝑦𝜑 ∧ ∃𝑧∃𝑤𝜓)) | ||
Theorem | sb8v 2365* | Substitution of variable in universal quantifier. Version of sb8 2555 with a disjoint variable condition, not requiring ax-13 2383. (Contributed by Wolf Lammen, 19-Jan-2023.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (∀𝑥𝜑 ↔ ∀𝑦[𝑦 / 𝑥]𝜑) | ||
Theorem | sb8ev 2366* | Substitution of variable in existential quantifier. Version of sb8e 2556 with a disjoint variable condition, not requiring ax-13 2383. (Contributed by Wolf Lammen, 19-Jan-2023.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (∃𝑥𝜑 ↔ ∃𝑦[𝑦 / 𝑥]𝜑) | ||
Theorem | 2sb8ev 2367* | Version of 2sb8e 2572 with more disjoint variable conditions, not requiring ax-13 2383. (Contributed by Wolf Lammen, 28-Jan-2023.) |
⊢ Ⅎ𝑤𝜑 & ⊢ Ⅎ𝑧𝜑 ⇒ ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑧∃𝑤[𝑧 / 𝑥][𝑤 / 𝑦]𝜑) | ||
Theorem | 2sb8evOLD 2368* | Obsolete proof of 2sb8ev 2367 as of 19-Mar-2023. (Contributed by Wolf Lammen, 28-Jan-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑤𝜑 & ⊢ Ⅎ𝑧𝜑 ⇒ ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑧∃𝑤[𝑧 / 𝑥][𝑤 / 𝑦]𝜑) | ||
Theorem | sb6rfv 2369* | Reversed substitution. Version of sb6rf 2486 requiring disjoint variables, but fewer axioms. (Contributed by Wolf Lammen, 7-Feb-2023.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (𝜑 ↔ ∀𝑦(𝑦 = 𝑥 → [𝑦 / 𝑥]𝜑)) | ||
Theorem | sbnf2 2370* | 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 2383. (Revised by Wolf Lammen, 30-Jan-2023.) |
⊢ (Ⅎ𝑥𝜑 ↔ ∀𝑦∀𝑧([𝑦 / 𝑥]𝜑 ↔ [𝑧 / 𝑥]𝜑)) | ||
Theorem | exsb 2371* | An equivalent expression for existence. One direction (exsbim 1999) needs fewer axioms. (Contributed by NM, 2-Feb-2005.) Avoid ax-13 2383. (Revised by Wolf Lammen, 16-Oct-2022.) |
⊢ (∃𝑥𝜑 ↔ ∃𝑦∀𝑥(𝑥 = 𝑦 → 𝜑)) | ||
Theorem | 2exsb 2372* | An equivalent expression for double existence. (Contributed by NM, 2-Feb-2005.) (Proof shortened by Wolf Lammen, 30-Sep-2018.) |
⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑧∃𝑤∀𝑥∀𝑦((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝜑)) | ||
Theorem | sbbib 2373* | Reversal of substitution. (Contributed by AV, 6-Aug-2023.) (Proof shortened by Wolf Lammen, 4-Sep-2023.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (∀𝑦([𝑦 / 𝑥]𝜑 ↔ 𝜓) ↔ ∀𝑥(𝜑 ↔ [𝑥 / 𝑦]𝜓)) | ||
Theorem | sbbibvv 2374* | Reversal of substitution. (Contributed by AV, 6-Aug-2023.) |
⊢ (∀𝑦([𝑦 / 𝑥]𝜑 ↔ 𝜓) ↔ ∀𝑥(𝜑 ↔ [𝑥 / 𝑦]𝜓)) | ||
Theorem | cleljustALT 2375* | Alternate proof of cleljust 2114. 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 2376* | Alternate proof of cleljust 2114. Compared with cleljustALT 2375, it uses nfv 1906 followed by equsexv 2260 instead of ax-5 1902 followed by equsexhv 2292, so it uses the idiom Ⅎ𝑥𝜑 instead of 𝜑 → ∀𝑥𝜑 to express non-freeness. 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 2377 | Alternate proof of equs5a 2475. Uses ax-12 2167 but not ax-13 2383. (Contributed by NM, 2-Feb-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∃𝑥(𝑥 = 𝑦 ∧ ∀𝑦𝜑) → ∀𝑥(𝑥 = 𝑦 → 𝜑)) | ||
Theorem | equs5eALT 2378 | Alternate proof of equs5e 2476. Uses ax-12 2167 but not ax-13 2383. (Contributed by NM, 2-Feb-2007.) (Proof shortened by Wolf Lammen, 15-Jan-2018.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑦 → ∃𝑦𝜑)) | ||
Theorem | axc11r 2379 | Same as axc11 2447 but with reversed antecedent. Note the use of ax-12 2167 (and not merely ax12v 2168 as in axc11rv 2257). (Contributed by NM, 25-Jul-2015.) |
⊢ (∀𝑦 𝑦 = 𝑥 → (∀𝑥𝜑 → ∀𝑦𝜑)) | ||
Theorem | dral1v 2380* | Version of dral1 2456 with a disjoint variable condition, which does not require ax-13 2383. Remark: the corresponding versions for dral2 2455 and drex2 2459 are instances of albidv 1912 and exbidv 1913 respectively. (Contributed by BJ, 17-Jun-2019.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 ↔ ∀𝑦𝜓)) | ||
Theorem | drex1v 2381* | Version of drex1 2458 with a disjoint variable condition, which does not require ax-13 2383. (Contributed by BJ, 17-Jun-2019.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 𝑥 = 𝑦 → (∃𝑥𝜑 ↔ ∃𝑦𝜓)) | ||
Theorem | drnf1v 2382* | Version of drnf1 2460 with a disjoint variable condition, which does not require ax-13 2383. (Contributed by BJ, 17-Jun-2019.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 𝑥 = 𝑦 → (Ⅎ𝑥𝜑 ↔ Ⅎ𝑦𝜓)) | ||
Axiom | ax-13 2383 |
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 2030). 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 1902, the conclusion (𝑦 = 𝑧 → ∀𝑥𝑦 = 𝑧) follows. Note that ax-5 1902 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 35908 and was replaced with this shorter ax-13 2383 in December 2015. The old axiom is proved from this one as theorem axc9 2393. 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. Although this version is shorter, the original version axc9 2393 may be more practical to work with because of the "distinctor" form of its antecedents. A typical application of axc9 2393 is in dvelimh 2467 which converts a distinct variable pair to the distinctor antecedent ¬ ∀𝑥𝑥 = 𝑦. In particular, it is conjectured that it is not possible to prove ax6 2395 from ax6v 1962 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 2384 and use only ax13v 2384 for further derivations. Thus, ax13v 2384 should be the only theorem referencing this axiom. Other theorems can reference either ax13v 2384 (preferred) or ax13 2386 (if the stronger form is needed). This axiom scheme is logically redundant (see ax13w 2131) 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 2131). 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 2384* |
A weaker version of ax-13 2383 with distinct variable restrictions on pairs
𝑥,
𝑧 and 𝑦, 𝑧. In order to show (with
ax13 2386) that this
weakening is still adequate, this should be the only theorem referencing
ax-13 2383 directly.
Had we additionally required 𝑥 and 𝑦 be distinct, too, this theorem would have been a direct consequence of ax-5 1902. So essentially this theorem states, that a distinct variable condition can be replaced with an inequality between set variables. (Contributed by NM, 30-Jun-2016.) |
⊢ (¬ 𝑥 = 𝑦 → (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧)) | ||
Theorem | ax13lem1 2385* | A version of ax13v 2384 with one distinct variable restriction dropped. For convenience, 𝑦 is kept on the right side of equations. The proof of ax13 2386 bases on ideas from NM, 24-Dec-2015. (Contributed by Wolf Lammen, 8-Sep-2018.) (New usage is discouraged.) |
⊢ (¬ 𝑥 = 𝑦 → (𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦)) | ||
Theorem | ax13 2386 | Derive ax-13 2383 from ax13v 2384 and Tarski's FOL. This shows that the weakening in ax13v 2384 is still sufficient for a complete system. (Contributed by NM, 21-Dec-2015.) (Proof shortened by Wolf Lammen, 31-Jan-2018.) Reduce axiom usage (Revised by Wolf Lammen, 2-Jun-2021.) |
⊢ (¬ 𝑥 = 𝑦 → (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧)) | ||
Theorem | ax13lem2 2387* | Lemma for nfeqf2 2388. This lemma is equivalent to ax13v 2384 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 2388* | An equation between setvar is free of any other setvar. (Contributed by Wolf Lammen, 9-Jun-2019.) Remove dependency on ax-12 2167. (Revised by Wolf Lammen, 16-Dec-2022.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥 𝑧 = 𝑦) | ||
Theorem | dveeq2 2389* | Quantifier introduction when one pair of variables is distinct. (Contributed by NM, 2-Jan-2002.) (Revised by NM, 20-Jul-2015.) Remove dependency on ax-11 2151. (Revised by Wolf Lammen, 8-Sep-2018.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦)) | ||
Theorem | nfeqf1 2390* | An equation between setvar is free of any other setvar. (Contributed by Wolf Lammen, 10-Jun-2019.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥 𝑦 = 𝑧) | ||
Theorem | dveeq1 2391* | Quantifier introduction when one pair of variables is distinct. (Contributed by NM, 2-Jan-2002.) Remove dependency on ax-11 2151. (Revised by Wolf Lammen, 8-Sep-2018.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧)) | ||
Theorem | nfeqf 2392 | A variable is effectively not free in an equality if it is not either of the involved variables. Ⅎ version of ax-c9 35908. (Contributed by Mario Carneiro, 6-Oct-2016.) Remove dependency on ax-11 2151. (Revised by Wolf Lammen, 6-Sep-2018.) |
⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦) → Ⅎ𝑧 𝑥 = 𝑦) | ||
Theorem | axc9 2393 | Derive set.mm's original ax-c9 35908 from the shorter ax-13 2383. (Contributed by NM, 29-Nov-2015.) (Revised by NM, 24-Dec-2015.) (Proof shortened by Wolf Lammen, 29-Apr-2018.) |
⊢ (¬ ∀𝑧 𝑧 = 𝑥 → (¬ ∀𝑧 𝑧 = 𝑦 → (𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦))) | ||
Theorem | ax6e 2394 |
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 1801 through ax-9 2115,
all axioms other than
ax-6 1961 are believed to be theorems of free logic,
although the system
without ax-6 1961 is not complete in free logic.
It is preferred to use ax6ev 1963 when it is sufficient. (Contributed by NM, 14-May-1993.) Shortened after ax13lem1 2385 became available. (Revised by Wolf Lammen, 8-Sep-2018.) |
⊢ ∃𝑥 𝑥 = 𝑦 | ||
Theorem | ax6 2395 |
Theorem showing that ax-6 1961 follows from the weaker version ax6v 1962.
(Even though this theorem depends on ax-6 1961,
all references of ax-6 1961 are
made via ax6v 1962. An earlier version stated ax6v 1962
as a separate axiom,
but having two axioms caused some confusion.)
This theorem should be referenced in place of ax-6 1961 so that all proofs can be traced back to ax6v 1962. When possible, use the weaker ax6v 1962 rather than ax6 2395 since the ax6v 1962 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.) |
⊢ ¬ ∀𝑥 ¬ 𝑥 = 𝑦 | ||
Theorem | axc10 2396 |
Show that the original axiom ax-c10 35904 can be derived from ax6 2395
and axc7 2328
(on top of propositional calculus, ax-gen 1787, and ax-4 1801). See
ax6fromc10 35914 for the rederivation of ax6 2395
from ax-c10 35904.
Normally, axc10 2396 should be used rather than ax-c10 35904, except by theorems specifically studying the latter's properties. (Contributed by NM, 5-Aug-1993.) (Proof modification is discouraged.) |
⊢ (∀𝑥(𝑥 = 𝑦 → ∀𝑥𝜑) → 𝜑) | ||
Theorem | spimt 2397 | Closed theorem form of spim 2399. (Contributed by NM, 15-Jan-2008.) (Revised by Mario Carneiro, 17-Oct-2016.) (Proof shortened by Wolf Lammen, 21-Mar-2023.) |
⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝑦 → (𝜑 → 𝜓))) → (∀𝑥𝜑 → 𝜓)) | ||
Theorem | spimtOLD 2398 | Obsolete version of spimt 2397 as of 21-Mar-2023. (Contributed by NM, 15-Jan-2008.) (Revised by Mario Carneiro, 17-Oct-2016.) (Proof shortened by Wolf Lammen, 24-Feb-2018.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝑦 → (𝜑 → 𝜓))) → (∀𝑥𝜑 → 𝜓)) | ||
Theorem | spim 2399 | Specialization, using implicit substitution. Compare Lemma 14 of [Tarski] p. 70. The spim 2399 series of theorems requires that only one direction of the substitution hypothesis hold. (Contributed by NM, 10-Jan-1993.) (Revised by Mario Carneiro, 3-Oct-2016.) (Proof shortened by Wolf Lammen, 18-Feb-2018.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) ⇒ ⊢ (∀𝑥𝜑 → 𝜓) | ||
Theorem | spimed 2400 | Deduction version of spime 2401. See also spimedv 2188. (Contributed by NM, 14-May-1993.) (Revised by Mario Carneiro, 3-Oct-2016.) (Proof shortened by Wolf Lammen, 19-Feb-2018.) |
⊢ (𝜒 → Ⅎ𝑥𝜑) & ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) ⇒ ⊢ (𝜒 → (𝜑 → ∃𝑥𝜓)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |