Home | Metamath
Proof Explorer Theorem List (p. 24 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-28697) |
Hilbert Space Explorer
(28698-30220) |
Users' Mathboxes
(30221-44913) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | hba1 2301 | The setvar 𝑥 is not free in ∀𝑥𝜑. This corresponds to the axiom (4) of modal logic. Example in Appendix in [Megill] p. 450 (p. 19 of the preprint). Also Lemma 22 of [Monk2] p. 114. (Contributed by NM, 24-Jan-1993.) (Proof shortened by Wolf Lammen, 12-Oct-2021.) |
⊢ (∀𝑥𝜑 → ∀𝑥∀𝑥𝜑) | ||
Theorem | hbnt 2302 | Closed theorem version of bound-variable hypothesis builder hbn 2303. (Contributed by NM, 10-May-1993.) (Proof shortened by Wolf Lammen, 14-Oct-2021.) |
⊢ (∀𝑥(𝜑 → ∀𝑥𝜑) → (¬ 𝜑 → ∀𝑥 ¬ 𝜑)) | ||
Theorem | hbn 2303 | If 𝑥 is not free in 𝜑, it is not free in ¬ 𝜑. (Contributed by NM, 10-Jan-1993.) (Proof shortened by Wolf Lammen, 17-Dec-2017.) |
⊢ (𝜑 → ∀𝑥𝜑) ⇒ ⊢ (¬ 𝜑 → ∀𝑥 ¬ 𝜑) | ||
Theorem | hbnd 2304 | Deduction form of bound-variable hypothesis builder hbn 2303. (Contributed by NM, 3-Jan-2002.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜑 → (𝜓 → ∀𝑥𝜓)) ⇒ ⊢ (𝜑 → (¬ 𝜓 → ∀𝑥 ¬ 𝜓)) | ||
Theorem | hbim1 2305 | A closed form of hbim 2307. (Contributed by NM, 2-Jun-1993.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜑 → (𝜓 → ∀𝑥𝜓)) ⇒ ⊢ ((𝜑 → 𝜓) → ∀𝑥(𝜑 → 𝜓)) | ||
Theorem | hbimd 2306 | Deduction form of bound-variable hypothesis builder hbim 2307. (Contributed by NM, 14-May-1993.) (Proof shortened by Wolf Lammen, 3-Jan-2018.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜑 → (𝜓 → ∀𝑥𝜓)) & ⊢ (𝜑 → (𝜒 → ∀𝑥𝜒)) ⇒ ⊢ (𝜑 → ((𝜓 → 𝜒) → ∀𝑥(𝜓 → 𝜒))) | ||
Theorem | hbim 2307 | If 𝑥 is not free in 𝜑 and 𝜓, it is not free in (𝜑 → 𝜓). (Contributed by NM, 24-Jan-1993.) (Proof shortened by Mel L. O'Cat, 3-Mar-2008.) (Proof shortened by Wolf Lammen, 1-Jan-2018.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜓 → ∀𝑥𝜓) ⇒ ⊢ ((𝜑 → 𝜓) → ∀𝑥(𝜑 → 𝜓)) | ||
Theorem | hban 2308 | If 𝑥 is not free in 𝜑 and 𝜓, it is not free in (𝜑 ∧ 𝜓). (Contributed by NM, 14-May-1993.) (Proof shortened by Wolf Lammen, 2-Jan-2018.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜓 → ∀𝑥𝜓) ⇒ ⊢ ((𝜑 ∧ 𝜓) → ∀𝑥(𝜑 ∧ 𝜓)) | ||
Theorem | hb3an 2309 | 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 2310 | Introduction of implication into substitution. (Contributed by NM, 14-May-1993.) |
⊢ (([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓) → [𝑦 / 𝑥](𝜑 → 𝜓)) | ||
Theorem | sbim 2311 | Implication inside and outside of a substitution are equivalent. (Contributed by NM, 14-May-1993.) |
⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓)) | ||
Theorem | sbanOLD 2312 | Obsolete version of sban 2086 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 2313 | Substitution in an implication with a variable not free in the antecedent affects only the consequent. See sbrimv 2314 for a version with disjoint variables not requiring ax-10 2145. (Contributed by NM, 2-Jun-1993.) (Revised by Mario Carneiro, 4-Oct-2016.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ (𝜑 → [𝑦 / 𝑥]𝜓)) | ||
Theorem | sbrimv 2314* | Substitution in an implication with a variable not free in the antecedent affects only the consequent. Version of sbrim 2313 not depending on ax-10 2145, but with disjoint variables. (Contributed by Wolf Lammen, 28-Jan-2024.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ (𝜑 → [𝑦 / 𝑥]𝜓)) | ||
Theorem | sblim 2315 | 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 2316 | Disjunction inside and outside of a substitution are equivalent. (Contributed by NM, 29-Sep-2002.) |
⊢ ([𝑦 / 𝑥](𝜑 ∨ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 ∨ [𝑦 / 𝑥]𝜓)) | ||
Theorem | sbbi 2317 | Equivalence inside and outside of a substitution are equivalent. (Contributed by NM, 14-May-1993.) |
⊢ ([𝑦 / 𝑥](𝜑 ↔ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜓)) | ||
Theorem | spsbbiOLD 2318 | Obsolete version of spsbbi 2078 as of 6-Jul-2023. Specialization of biconditional. (Contributed by NM, 2-Jun-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥(𝜑 ↔ 𝜓) → ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜓)) | ||
Theorem | sblbis 2319 | Introduce left biconditional inside of a substitution. (Contributed by NM, 19-Aug-1993.) |
⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓) ⇒ ⊢ ([𝑦 / 𝑥](𝜒 ↔ 𝜑) ↔ ([𝑦 / 𝑥]𝜒 ↔ 𝜓)) | ||
Theorem | sbrbis 2320 | Introduce right biconditional inside of a substitution. (Contributed by NM, 18-Aug-1993.) |
⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓) ⇒ ⊢ ([𝑦 / 𝑥](𝜑 ↔ 𝜒) ↔ (𝜓 ↔ [𝑦 / 𝑥]𝜒)) | ||
Theorem | sbrbif 2321 | Introduce right biconditional inside of a substitution. (Contributed by NM, 18-Aug-1993.) (Revised by Mario Carneiro, 4-Oct-2016.) |
⊢ Ⅎ𝑥𝜒 & ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓) ⇒ ⊢ ([𝑦 / 𝑥](𝜑 ↔ 𝜒) ↔ (𝜓 ↔ 𝜒)) | ||
Theorem | sbnvOLD 2322* | Obsolete version of sbn 2287 as of 8-Jul-2023. Substitution is not affected by negation. Version of sbn 2287 with a disjoint variable condition, not requiring ax-13 2390. (Contributed by Wolf Lammen, 18-Jan-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ([𝑦 / 𝑥] ¬ 𝜑 ↔ ¬ [𝑦 / 𝑥]𝜑) | ||
Theorem | sbi1vOLD 2323* | Obsolete version of sbi1 2076 as of 24-Jul-2023. Move implication out of substitution. Version of sbi1 2076 with a disjoint variable condition, not requiring ax-13 2390. (Contributed by Wolf Lammen, 18-Jan-2023.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) → ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓)) | ||
Theorem | sbi2vOLD 2324* | Obsolete version of sbi2 2310 as of 8-Jul-2023. Move implication into substitution. Version of sbi2 2310 with a disjoint variable condition, not requiring ax-13 2390. (Contributed by Wolf Lammen, 18-Jan-2023.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓) → [𝑦 / 𝑥](𝜑 → 𝜓)) | ||
Theorem | sbimvOLD 2325* | Obsolete version of sbim 2311 as of 24-Jul-2023. Substitution distributes over implication. Version of sbim 2311 with a disjoint variable condition, not requiring ax-13 2390. (Contributed by Wolf Lammen, 18-Jan-2023.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓)) | ||
Theorem | sbanvOLD 2326* | Obsolete version of sban 2086 as of 24-Jul-2023. Substitution distributes over conjunction. Version of sban 2086 with a disjoint variable condition, not requiring ax-13 2390. (Contributed by Wolf Lammen, 18-Jan-2023.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ([𝑦 / 𝑥](𝜑 ∧ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓)) | ||
Theorem | sbbivOLD 2327* | Obsolete version of sbbi 2317 as of 24-Jul-2023. Substitution distributes over a biconditional. Version of sbbi 2317 with a disjoint variable condition, not requiring ax-11 2161 nor ax-13 2390. (Contributed by Wolf Lammen, 18-Jan-2023.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ([𝑦 / 𝑥](𝜑 ↔ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜓)) | ||
Theorem | spsbimvOLD 2328* | Obsolete version of spsbim 2077 as of 6-Jul-2023. Specialization of implication. Version of spsbim 2077 with a disjoint variable condition, not requiring ax-13 2390. (Contributed by Wolf Lammen, 19-Jan-2023.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (∀𝑥(𝜑 → 𝜓) → ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓)) | ||
Theorem | sblbisvOLD 2329* | Obsolete version of sblbis 2319 as of 24-Jul-2023. Introduce left biconditional inside of a substitution. Version of sblbis 2319 with a disjoint variable condition, not requiring ax-13 2390. (Contributed by Wolf Lammen, 18-Jan-2023.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓) ⇒ ⊢ ([𝑦 / 𝑥](𝜒 ↔ 𝜑) ↔ ([𝑦 / 𝑥]𝜒 ↔ 𝜓)) | ||
Theorem | sbiev 2330* | Conversion of implicit substitution to explicit substitution. Version of sbie 2544 with a disjoint variable condition, not requiring ax-13 2390. See sbievw 2103 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 2145 and shorten proof. (Revised by BJ, 18-Jul-2023.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓) | ||
Theorem | sbievOLD 2331* | Obsolete proof of sbiev 2330 as of 18-Jul-2023. (Contributed by Wolf Lammen, 18-Jan-2023.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓) | ||
Theorem | sbiedw 2332* | Conversion of implicit substitution to explicit substitution (deduction version of sbiev 2330). Version of sbied 2545 with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 30-Jun-1994.) (Revised by Gino Giotto, 10-Jan-2024.) Avoid ax-10 2145. (Revised by Wolf Lammen, 28-Jan-2024.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝜒) & ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))) ⇒ ⊢ (𝜑 → ([𝑦 / 𝑥]𝜓 ↔ 𝜒)) | ||
Theorem | sbiedwOLD 2333* | Obsolete version of sbiedw 2332 as of 28-Jan-2024. (Contributed by Gino Giotto, 10-Jan-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝜒) & ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))) ⇒ ⊢ (𝜑 → ([𝑦 / 𝑥]𝜓 ↔ 𝜒)) | ||
Theorem | sbequivvOLD 2334* | Obsolete version of sbequi 2091 as of 7-Jul-2023. Version of sbequi 2091 with disjoint variable conditions, not requiring ax-13 2390. (Contributed by Wolf Lammen, 19-Jan-2023.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 → [𝑦 / 𝑧]𝜑)) | ||
Theorem | sbequvvOLD 2335* | Obsolete version of sbequ 2090 as of 7-Jul-2023. Version of sbequ 2090 with disjoint variable conditions, not requiring ax-13 2390. (Contributed by Wolf Lammen, 19-Jan-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 ↔ [𝑦 / 𝑧]𝜑)) | ||
Theorem | axc7 2336 |
Show that the original axiom ax-c7 36023 can be derived from ax-10 2145
(hbn1 2146) , sp 2182 and propositional calculus. See ax10fromc7 36033 for the
rederivation of ax-10 2145 from ax-c7 36023.
Normally, axc7 2336 should be used rather than ax-c7 36023, except by theorems specifically studying the latter's properties. (Contributed by NM, 21-May-2008.) |
⊢ (¬ ∀𝑥 ¬ ∀𝑥𝜑 → 𝜑) | ||
Theorem | axc7e 2337 | Abbreviated version of axc7 2336 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 2338 | The analogue in our predicate calculus of the Brouwer axiom (B) of modal logic S5. (Contributed by NM, 5-Oct-2005.) |
⊢ (𝜑 → ∀𝑥 ¬ ∀𝑥 ¬ 𝜑) | ||
Theorem | 19.9ht 2339 | A closed version of 19.9h 2294. (Contributed by NM, 13-May-1993.) (Proof shortened by Wolf Lammen, 3-Mar-2018.) |
⊢ (∀𝑥(𝜑 → ∀𝑥𝜑) → (∃𝑥𝜑 → 𝜑)) | ||
Theorem | axc4 2340 |
Show that the original axiom ax-c4 36022 can be derived from ax-4 1810
(alim 1811), ax-10 2145 (hbn1 2146), sp 2182 and propositional calculus. See
ax4fromc4 36032 for the rederivation of ax-4 1810
from ax-c4 36022.
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 2341 | Inference version of axc4 2340. (Contributed by NM, 3-Jan-1993.) |
⊢ (∀𝑥𝜑 → 𝜓) ⇒ ⊢ (∀𝑥𝜑 → ∀𝑥𝜓) | ||
Theorem | nfal 2342 | If 𝑥 is not free in 𝜑, it is not free in ∀𝑦𝜑. (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ Ⅎ𝑥∀𝑦𝜑 | ||
Theorem | nfex 2343 | 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 2343, hbex 2344. (Revised by Wolf Lammen, 16-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ Ⅎ𝑥∃𝑦𝜑 | ||
Theorem | hbex 2344 | If 𝑥 is not free in 𝜑, it is not free in ∃𝑦𝜑. (Contributed by NM, 12-Mar-1993.) Reduce symbol count in nfex 2343, hbex 2344. (Revised by Wolf Lammen, 16-Oct-2021.) |
⊢ (𝜑 → ∀𝑥𝜑) ⇒ ⊢ (∃𝑦𝜑 → ∀𝑥∃𝑦𝜑) | ||
Theorem | nfnf 2345 | 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 2346 | 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 2368 and r19.12sn 4658. (Contributed by NM, 12-Mar-1993.) (Proof shortened by Wolf Lammen, 3-Jan-2018.) |
⊢ (∃𝑥∀𝑦𝜑 → ∀𝑦∃𝑥𝜑) | ||
Theorem | nfald 2347 | Deduction form of nfal 2342. (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 16-Oct-2021.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝜓) ⇒ ⊢ (𝜑 → Ⅎ𝑥∀𝑦𝜓) | ||
Theorem | nfexd 2348 | If 𝑥 is not free in 𝜓, it is not free in ∃𝑦𝜓. (Contributed by Mario Carneiro, 24-Sep-2016.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝜓) ⇒ ⊢ (𝜑 → Ⅎ𝑥∃𝑦𝜓) | ||
Theorem | nfsbv 2349* | If 𝑧 is not free in 𝜑, it is not free in [𝑦 / 𝑥]𝜑 when 𝑧 is distinct from 𝑥 and 𝑦. Version of nfsb 2565 requiring more disjoint variables, but fewer axioms. (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.) |
⊢ Ⅎ𝑧𝜑 ⇒ ⊢ Ⅎ𝑧[𝑦 / 𝑥]𝜑 | ||
Theorem | nfsbvOLD 2350* | Obsolete version of nfsbv 2349 as of 13-Aug-2023. (Contributed by Wolf Lammen, 7-Feb-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑧𝜑 ⇒ ⊢ Ⅎ𝑧[𝑦 / 𝑥]𝜑 | ||
Theorem | hbsbw 2351* | If 𝑧 is not free in 𝜑, it is not free in [𝑦 / 𝑥]𝜑 when 𝑦 and 𝑧 are distinct. Version of hbsb 2567 with a disjoint variable condition, which does not require ax-13 2390. (Contributed by NM, 12-Aug-1993.) (Revised by Gino Giotto, 10-Jan-2024.) |
⊢ (𝜑 → ∀𝑧𝜑) ⇒ ⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑧[𝑦 / 𝑥]𝜑) | ||
Theorem | sbco2v 2352* | A composition law for substitution. Version of sbco2 2553 with disjoint variable conditions, not requiring ax-13 2390, but ax-11 2161. (Contributed by NM, 30-Jun-1994.) (Revised by Wolf Lammen, 29-Apr-2023.) |
⊢ Ⅎ𝑧𝜑 ⇒ ⊢ ([𝑦 / 𝑧][𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑) | ||
Theorem | aaan 2353 | Rearrange universal quantifiers. (Contributed by NM, 12-Aug-1993.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (∀𝑥∀𝑦(𝜑 ∧ 𝜓) ↔ (∀𝑥𝜑 ∧ ∀𝑦𝜓)) | ||
Theorem | eeor 2354 | Rearrange existential quantifiers. (Contributed by NM, 8-Aug-1994.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (∃𝑥∃𝑦(𝜑 ∨ 𝜓) ↔ (∃𝑥𝜑 ∨ ∃𝑦𝜓)) | ||
Theorem | cbv3v 2355* | Rule used to change bound variables, using implicit substitution. Version of cbv3 2415 with a disjoint variable condition, which does not require ax-13 2390. (Contributed by NM, 5-Aug-1993.) (Revised by BJ, 31-May-2019.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) ⇒ ⊢ (∀𝑥𝜑 → ∀𝑦𝜓) | ||
Theorem | cbv1v 2356* | Rule used to change bound variables, using implicit substitution. Version of cbv1 2422 with a disjoint variable condition, which does not require ax-13 2390. (Contributed by NM, 5-Aug-1993.) (Revised by BJ, 16-Jun-2019.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑦𝜓) & ⊢ (𝜑 → Ⅎ𝑥𝜒) & ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 → 𝜒))) ⇒ ⊢ (𝜑 → (∀𝑥𝜓 → ∀𝑦𝜒)) | ||
Theorem | cbv2w 2357* | Rule used to change bound variables, using implicit substitution. Version of cbv2 2423 with a disjoint variable condition, which does not require ax-13 2390. (Contributed by NM, 5-Aug-1993.) (Revised by Gino Giotto, 10-Jan-2024.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑦𝜓) & ⊢ (𝜑 → Ⅎ𝑥𝜒) & ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))) ⇒ ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒)) | ||
Theorem | cbvaldw 2358* | Deduction used to change bound variables, using implicit substitution. Version of cbvald 2428 with a disjoint variable condition, which does not require ax-13 2390. (Contributed by NM, 2-Jan-2002.) (Revised by Gino Giotto, 10-Jan-2024.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑦𝜓) & ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))) ⇒ ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒)) | ||
Theorem | cbvexdw 2359* | Deduction used to change bound variables, using implicit substitution. Version of cbvexd 2429 with a disjoint variable condition, which does not require ax-13 2390. (Contributed by NM, 2-Jan-2002.) (Revised by Gino Giotto, 10-Jan-2024.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑦𝜓) & ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))) ⇒ ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑦𝜒)) | ||
Theorem | cbv3hv 2360* | Rule used to change bound variables, using implicit substitution. Version of cbv3h 2424 with a disjoint variable condition on 𝑥, 𝑦, which does not require ax-13 2390. Was used in a proof of axc11n 2448 (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 2361* | Rule used to change bound variables, using implicit substitution. Version of cbval 2416 with a disjoint variable condition, which does not require ax-13 2390. See cbvalvw 2043 for a version with two disjoint variable conditions, requiring fewer axioms, and cbvalv 2418 for another variant. (Contributed by NM, 13-May-1993.) (Revised by BJ, 31-May-2019.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓) | ||
Theorem | cbvexv1 2362* | Rule used to change bound variables, using implicit substitution. Version of cbvex 2417 with a disjoint variable condition, which does not require ax-13 2390. See cbvexvw 2044 for a version with two disjoint variable conditions, requiring fewer axioms, and cbvexv 2419 for another variant. (Contributed by NM, 21-Jun-1993.) (Revised by BJ, 31-May-2019.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓) | ||
Theorem | cbval2v 2363* | Rule used to change bound variables, using implicit substitution. Version of cbval2 2432 with a disjoint variable condition, which does not require ax-13 2390. (Contributed by NM, 22-Dec-2003.) (Revised by BJ, 16-Jun-2019.) (Proof shortened by Gino Giotto, 10-Jan-2024.) |
⊢ Ⅎ𝑧𝜑 & ⊢ Ⅎ𝑤𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ Ⅎ𝑦𝜓 & ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑧∀𝑤𝜓) | ||
Theorem | cbval2vOLD 2364* | Obsolete version of cbval2v 2363 as of 14-Jan-2024. (Contributed by BJ, 16-Jan-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑧𝜑 & ⊢ Ⅎ𝑤𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ Ⅎ𝑦𝜓 & ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑧∀𝑤𝜓) | ||
Theorem | cbvex2v 2365* | Rule used to change bound variables, using implicit substitution. Version of cbvex2 2434 with a disjoint variable condition, which does not require ax-13 2390. (Contributed by NM, 14-Sep-2003.) (Revised by BJ, 16-Jun-2019.) |
⊢ Ⅎ𝑧𝜑 & ⊢ Ⅎ𝑤𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ Ⅎ𝑦𝜓 & ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑧∃𝑤𝜓) | ||
Theorem | dvelimhw 2366* | Proof of dvelimh 2472 without using ax-13 2390 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 2367* | 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 2368* | Special case of 19.12 2346 where its converse holds. See 19.12vvv 1995 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 2369 | Rearrange existential quantifiers. (Contributed by NM, 27-Oct-2010.) (Revised by Mario Carneiro, 6-Oct-2016.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ ∃𝑦𝜓)) | ||
Theorem | eeanv 2370* | Distribute a pair of existential quantifiers over a conjunction. Combination of 19.41v 1950 and 19.42v 1954. For a version requiring fewer axioms but with additional disjoint variable conditions, see exdistrv 1956. (Contributed by NM, 26-Jul-1995.) |
⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ ∃𝑦𝜓)) | ||
Theorem | eeeanv 2371* | 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 2372* | Distribute two pairs of existential quantifiers over a conjunction. For a version requiring fewer axioms but with additional disjoint variable conditions, see 4exdistrv 1957. (Contributed by NM, 31-Jul-1995.) |
⊢ (∃𝑥∃𝑦∃𝑧∃𝑤(𝜑 ∧ 𝜓) ↔ (∃𝑥∃𝑦𝜑 ∧ ∃𝑧∃𝑤𝜓)) | ||
Theorem | sb8v 2373* | Substitution of variable in universal quantifier. Version of sb8 2559 with a disjoint variable condition, not requiring ax-13 2390. (Contributed by NM, 16-May-1993.) (Revised by Wolf Lammen, 19-Jan-2023.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (∀𝑥𝜑 ↔ ∀𝑦[𝑦 / 𝑥]𝜑) | ||
Theorem | sb8ev 2374* | Substitution of variable in existential quantifier. Version of sb8e 2560 with a disjoint variable condition, not requiring ax-13 2390. (Contributed by NM, 12-Aug-1993.) (Revised by Wolf Lammen, 19-Jan-2023.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (∃𝑥𝜑 ↔ ∃𝑦[𝑦 / 𝑥]𝜑) | ||
Theorem | 2sb8ev 2375* | An equivalent expression for double existence. Version of 2sb8e 2576 with more disjoint variable conditions, not requiring ax-13 2390. (Contributed by Wolf Lammen, 28-Jan-2023.) |
⊢ Ⅎ𝑤𝜑 & ⊢ Ⅎ𝑧𝜑 ⇒ ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑧∃𝑤[𝑧 / 𝑥][𝑤 / 𝑦]𝜑) | ||
Theorem | sb6rfv 2376* | Reversed substitution. Version of sb6rf 2491 requiring disjoint variables, but fewer axioms. (Contributed by NM, 1-Aug-1993.) (Revised by Wolf Lammen, 7-Feb-2023.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (𝜑 ↔ ∀𝑦(𝑦 = 𝑥 → [𝑦 / 𝑥]𝜑)) | ||
Theorem | sbnf2 2377* | 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 2390. (Revised by Wolf Lammen, 30-Jan-2023.) |
⊢ (Ⅎ𝑥𝜑 ↔ ∀𝑦∀𝑧([𝑦 / 𝑥]𝜑 ↔ [𝑧 / 𝑥]𝜑)) | ||
Theorem | exsb 2378* | An equivalent expression for existence. One direction (exsbim 2008) needs fewer axioms. (Contributed by NM, 2-Feb-2005.) Avoid ax-13 2390. (Revised by Wolf Lammen, 16-Oct-2022.) |
⊢ (∃𝑥𝜑 ↔ ∃𝑦∀𝑥(𝑥 = 𝑦 → 𝜑)) | ||
Theorem | 2exsb 2379* | An equivalent expression for double existence. (Contributed by NM, 2-Feb-2005.) (Proof shortened by Wolf Lammen, 30-Sep-2018.) |
⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑧∃𝑤∀𝑥∀𝑦((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝜑)) | ||
Theorem | sbbib 2380* | Reversal of substitution. (Contributed by AV, 6-Aug-2023.) (Proof shortened by Wolf Lammen, 4-Sep-2023.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (∀𝑦([𝑦 / 𝑥]𝜑 ↔ 𝜓) ↔ ∀𝑥(𝜑 ↔ [𝑥 / 𝑦]𝜓)) | ||
Theorem | sbbibvv 2381* | Reversal of substitution. (Contributed by AV, 6-Aug-2023.) |
⊢ (∀𝑦([𝑦 / 𝑥]𝜑 ↔ 𝜓) ↔ ∀𝑥(𝜑 ↔ [𝑥 / 𝑦]𝜓)) | ||
Theorem | cleljustALT 2382* | Alternate proof of cleljust 2123. 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 2383* | Alternate proof of cleljust 2123. Compared with cleljustALT 2382, it uses nfv 1915 followed by equsexv 2269 instead of ax-5 1911 followed by equsexhv 2300, 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 2384 | Alternate proof of equs5a 2480. Uses ax-12 2177 but not ax-13 2390. (Contributed by NM, 2-Feb-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∃𝑥(𝑥 = 𝑦 ∧ ∀𝑦𝜑) → ∀𝑥(𝑥 = 𝑦 → 𝜑)) | ||
Theorem | equs5eALT 2385 | Alternate proof of equs5e 2481. Uses ax-12 2177 but not ax-13 2390. (Contributed by NM, 2-Feb-2007.) (Proof shortened by Wolf Lammen, 15-Jan-2018.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑦 → ∃𝑦𝜑)) | ||
Theorem | axc11r 2386 |
Same as axc11 2452 but with reversed antecedent. Note the use
of ax-12 2177
(and not merely ax12v 2178 as in axc11rv 2266).
This theorem is mostly used to eliminate conditions requiring set variables be distinct (cf. cbvaev 2058 and aecom 2449, 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 2390 only, and like that, it should be applied only in niches where indispensable. (Contributed by NM, 25-Jul-2015.) |
⊢ (∀𝑦 𝑦 = 𝑥 → (∀𝑥𝜑 → ∀𝑦𝜑)) | ||
Theorem | dral1v 2387* | Formula-building lemma for use with the Distinctor Reduction Theorem. Version of dral1 2461 with a disjoint variable condition, which does not require ax-13 2390. Remark: the corresponding versions for dral2 2460 and drex2 2464 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 2178. (Revised by Wolf Lammen, 30-Mar-2024.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 ↔ ∀𝑦𝜓)) | ||
Theorem | drex1v 2388* | Formula-building lemma for use with the Distinctor Reduction Theorem. Version of drex1 2463 with a disjoint variable condition, which does not require ax-13 2390. (Contributed by NM, 27-Feb-2005.) (Revised by BJ, 17-Jun-2019.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 𝑥 = 𝑦 → (∃𝑥𝜑 ↔ ∃𝑦𝜓)) | ||
Theorem | drnf1v 2389* | Formula-building lemma for use with the Distinctor Reduction Theorem. Version of drnf1 2465 with a disjoint variable condition, which does not require ax-13 2390. (Contributed by Mario Carneiro, 4-Oct-2016.) (Revised by BJ, 17-Jun-2019.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 𝑥 = 𝑦 → (Ⅎ𝑥𝜑 ↔ Ⅎ𝑦𝜓)) | ||
Axiom | ax-13 2390 |
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 2039). 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 36028 and was replaced with this shorter ax-13 2390 in December 2015. The old axiom is proved from this one as theorem axc9 2400. 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 1972 and ax6e 2401, 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 2400 may be more practical to work with because of the "distinctor" form of its antecedents. A typical application of axc9 2400 is in dvelimh 2472 which converts a distinct variable pair to the distinctor antecedent ¬ ∀𝑥𝑥 = 𝑦. In particular, it is conjectured that it is not possible to prove ax6 2402 from ax6v 1971 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 2391 and use only ax13v 2391 for further derivations. Thus, ax13v 2391 should be the only theorem referencing this axiom. Other theorems can reference either ax13v 2391 (preferred) or ax13 2393 (if the stronger form is needed). This axiom scheme is logically redundant (see ax13w 2140) 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 2140). 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 2391* |
A weaker version of ax-13 2390 with distinct variable restrictions on pairs
𝑥,
𝑧 and 𝑦, 𝑧. In order to show (with
ax13 2393) that this
weakening is still adequate, this should be the only theorem referencing
ax-13 2390 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 2140 to avoid the propagation of ax-13 2390. (Contributed by NM, 30-Jun-2016.) (New usage is discouraged.) |
⊢ (¬ 𝑥 = 𝑦 → (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧)) | ||
Theorem | ax13lem1 2392* | A version of ax13v 2391 with one distinct variable restriction dropped. For convenience, 𝑦 is kept on the right side of equations. The proof of ax13 2393 bases on ideas from NM, 24-Dec-2015. (Contributed by Wolf Lammen, 8-Sep-2018.) (New usage is discouraged.) |
⊢ (¬ 𝑥 = 𝑦 → (𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦)) | ||
Theorem | ax13 2393 | Derive ax-13 2390 from ax13v 2391 and Tarski's FOL. This shows that the weakening in ax13v 2391 is still sufficient for a complete system. Preferably, use the weaker ax13w 2140 to avoid the propagation of ax-13 2390. (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 2394* | Lemma for nfeqf2 2395. This lemma is equivalent to ax13v 2391 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 2395* | An equation between setvar is free of any other setvar. Usage of this theorem is discouraged because it depends on ax-13 2390. (Contributed by Wolf Lammen, 9-Jun-2019.) Remove dependency on ax-12 2177. (Revised by Wolf Lammen, 16-Dec-2022.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥 𝑧 = 𝑦) | ||
Theorem | dveeq2 2396* | 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.) (Revised by NM, 20-Jul-2015.) Remove dependency on ax-11 2161. (Revised by Wolf Lammen, 8-Sep-2018.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦)) | ||
Theorem | nfeqf1 2397* | An equation between setvar is free of any other setvar. Usage of this theorem is discouraged because it depends on ax-13 2390. (Contributed by Wolf Lammen, 10-Jun-2019.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥 𝑦 = 𝑧) | ||
Theorem | dveeq1 2398* | 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.) Remove dependency on ax-11 2161. (Revised by Wolf Lammen, 8-Sep-2018.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧)) | ||
Theorem | nfeqf 2399 | A variable is effectively not free in an equality if it is not either of the involved variables. Ⅎ version of ax-c9 36028. Usage of this theorem is discouraged because it depends on ax-13 2390. (Contributed by Mario Carneiro, 6-Oct-2016.) Remove dependency on ax-11 2161. (Revised by Wolf Lammen, 6-Sep-2018.) (New usage is discouraged.) |
⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦) → Ⅎ𝑧 𝑥 = 𝑦) | ||
Theorem | axc9 2400 | Derive set.mm's original ax-c9 36028 from the shorter ax-13 2390. Usage is discouraged to avoid uninformed ax-13 2390 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.) |
⊢ (¬ ∀𝑧 𝑧 = 𝑥 → (¬ ∀𝑧 𝑧 = 𝑦 → (𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |