Home | Metamath
Proof Explorer Theorem List (p. 351 of 470) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46966) |
Type | Label | Description |
---|---|---|
Statement | ||
Syntax | wmoo 35001 | Syntax for BJ's version of the uniqueness quantifier. |
wff ∃**𝑥𝜑 | ||
Definition | df-bj-mo 35002* | Definition of the uniqueness quantifier which is correct on the empty domain. Instead of the fresh variable 𝑧, one could save a dummy variable by using 𝑥 or 𝑦 at the cost of having nested quantifiers on the same variable. (Contributed by BJ, 12-Mar-2023.) |
⊢ (∃**𝑥𝜑 ↔ ∀𝑧∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦)) | ||
Theorem | bj-ssbeq 35003* | Substitution in an equality, disjoint variables case. Uses only ax-1 6 through ax-6 1972. It might be shorter to prove the result about composition of two substitutions and prove bj-ssbeq 35003 first with a DV condition on 𝑥, 𝑡, and then in the general case. (Contributed by BJ, 22-Dec-2020.) (Proof modification is discouraged.) |
⊢ ([𝑡 / 𝑥]𝑦 = 𝑧 ↔ 𝑦 = 𝑧) | ||
Theorem | bj-ssblem1 35004* | A lemma for the definiens of df-sb 2069. An instance of sp 2177 proved without it. Note: it has a common subproof with sbjust 2067. (Contributed by BJ, 22-Dec-2020.) (Proof modification is discouraged.) |
⊢ (∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑)) → (𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) | ||
Theorem | bj-ssblem2 35005* | An instance of ax-11 2155 proved without it. The converse may not be provable without ax-11 2155 (since using alcomiw 2047 would require a DV on 𝜑, 𝑥, which defeats the purpose). (Contributed by BJ, 22-Dec-2020.) (Proof modification is discouraged.) |
⊢ (∀𝑥∀𝑦(𝑦 = 𝑡 → (𝑥 = 𝑦 → 𝜑)) → ∀𝑦∀𝑥(𝑦 = 𝑡 → (𝑥 = 𝑦 → 𝜑))) | ||
Theorem | bj-ax12v 35006* | A weaker form of ax-12 2172 and ax12v 2173, namely the generalization over 𝑥 of the latter. In this statement, all occurrences of 𝑥 are bound. (Contributed by BJ, 26-Dec-2020.) (Proof modification is discouraged.) |
⊢ ∀𝑥(𝑥 = 𝑡 → (𝜑 → ∀𝑥(𝑥 = 𝑡 → 𝜑))) | ||
Theorem | bj-ax12 35007* | Remove a DV condition from bj-ax12v 35006 (using core axioms only). (Contributed by BJ, 26-Dec-2020.) (Proof modification is discouraged.) |
⊢ ∀𝑥(𝑥 = 𝑡 → (𝜑 → ∀𝑥(𝑥 = 𝑡 → 𝜑))) | ||
Theorem | bj-ax12ssb 35008* | Axiom bj-ax12 35007 expressed using substitution. (Contributed by BJ, 26-Dec-2020.) (Proof modification is discouraged.) |
⊢ [𝑡 / 𝑥](𝜑 → [𝑡 / 𝑥]𝜑) | ||
Theorem | bj-19.41al 35009 | Special case of 19.41 2229 proved from core axioms, ax-10 2138 (modal5), and hba1 2291 (modal4). (Contributed by BJ, 29-Dec-2020.) (Proof modification is discouraged.) |
⊢ (∃𝑥(𝜑 ∧ ∀𝑥𝜓) ↔ (∃𝑥𝜑 ∧ ∀𝑥𝜓)) | ||
Theorem | bj-equsexval 35010* | Special case of equsexv 2261 proved from core axioms, ax-10 2138 (modal5), and hba1 2291 (modal4). (Contributed by BJ, 29-Dec-2020.) (Proof modification is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ ∀𝑥𝜓)) ⇒ ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ ∀𝑥𝜓) | ||
Theorem | bj-subst 35011* | Proof of sbalex 2236 from core axioms, ax-10 2138 (modal5), and bj-ax12 35007. (Contributed by BJ, 29-Dec-2020.) (Proof modification is discouraged.) |
⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑)) | ||
Theorem | bj-ssbid2 35012 | A special case of sbequ2 2242. (Contributed by BJ, 22-Dec-2020.) |
⊢ ([𝑥 / 𝑥]𝜑 → 𝜑) | ||
Theorem | bj-ssbid2ALT 35013 | Alternate proof of bj-ssbid2 35012, not using sbequ2 2242. (Contributed by BJ, 22-Dec-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ([𝑥 / 𝑥]𝜑 → 𝜑) | ||
Theorem | bj-ssbid1 35014 | A special case of sbequ1 2241. (Contributed by BJ, 22-Dec-2020.) |
⊢ (𝜑 → [𝑥 / 𝑥]𝜑) | ||
Theorem | bj-ssbid1ALT 35015 | Alternate proof of bj-ssbid1 35014, not using sbequ1 2241. (Contributed by BJ, 22-Dec-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → [𝑥 / 𝑥]𝜑) | ||
Theorem | bj-ax6elem1 35016* | Lemma for bj-ax6e 35018. (Contributed by BJ, 22-Dec-2020.) (Proof modification is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧)) | ||
Theorem | bj-ax6elem2 35017* | Lemma for bj-ax6e 35018. (Contributed by BJ, 22-Dec-2020.) (Proof modification is discouraged.) |
⊢ (∀𝑥 𝑦 = 𝑧 → ∃𝑥 𝑥 = 𝑦) | ||
Theorem | bj-ax6e 35018 | Proof of ax6e 2383 (hence ax6 2384) from Tarski's system, ax-c9 37238, ax-c16 37240. Remark: ax-6 1972 is used only via its principal (unbundled) instance ax6v 1973. (Contributed by BJ, 22-Dec-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ∃𝑥 𝑥 = 𝑦 | ||
Theorem | bj-spimvwt 35019* | Closed form of spimvw 2000. See also spimt 2386. (Contributed by BJ, 8-Nov-2021.) |
⊢ (∀𝑥(𝑥 = 𝑦 → (𝜑 → 𝜓)) → (∀𝑥𝜑 → 𝜓)) | ||
Theorem | bj-spnfw 35020 | Theorem close to a closed form of spnfw 1984. (Contributed by BJ, 12-May-2019.) |
⊢ ((∃𝑥𝜑 → 𝜓) → (∀𝑥𝜑 → 𝜓)) | ||
Theorem | bj-cbvexiw 35021* | Change bound variable. This is to cbvexvw 2041 what cbvaliw 2010 is to cbvalvw 2040. TODO: move after cbvalivw 2011. (Contributed by BJ, 17-Mar-2020.) |
⊢ (∃𝑥∃𝑦𝜓 → ∃𝑦𝜓) & ⊢ (𝜑 → ∀𝑦𝜑) & ⊢ (𝑦 = 𝑥 → (𝜑 → 𝜓)) ⇒ ⊢ (∃𝑥𝜑 → ∃𝑦𝜓) | ||
Theorem | bj-cbvexivw 35022* | Change bound variable. This is to cbvexvw 2041 what cbvalivw 2011 is to cbvalvw 2040. TODO: move after cbvalivw 2011. (Contributed by BJ, 17-Mar-2020.) |
⊢ (𝑦 = 𝑥 → (𝜑 → 𝜓)) ⇒ ⊢ (∃𝑥𝜑 → ∃𝑦𝜓) | ||
Theorem | bj-modald 35023 | A short form of the axiom D of modal logic. (Contributed by BJ, 4-Apr-2021.) |
⊢ (∀𝑥 ¬ 𝜑 → ¬ ∀𝑥𝜑) | ||
Theorem | bj-denot 35024* | A weakening of ax-6 1972 and ax6v 1973. (Contributed by BJ, 4-Apr-2021.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑥 → ¬ ∀𝑦 ¬ 𝑦 = 𝑥) | ||
Theorem | bj-eqs 35025* | A lemma for substitutions, proved from Tarski's FOL. The version without DV (𝑥, 𝑦) is true but requires ax-13 2372. The disjoint variable condition DV (𝑥, 𝜑) is necessary for both directions: consider substituting 𝑥 = 𝑧 for 𝜑. (Contributed by BJ, 25-May-2021.) |
⊢ (𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑)) | ||
Theorem | bj-cbvexw 35026* | Change bound variable. This is to cbvexvw 2041 what cbvalw 2039 is to cbvalvw 2040. (Contributed by BJ, 17-Mar-2020.) |
⊢ (∃𝑥∃𝑦𝜓 → ∃𝑦𝜓) & ⊢ (𝜑 → ∀𝑦𝜑) & ⊢ (∃𝑦∃𝑥𝜑 → ∃𝑥𝜑) & ⊢ (𝜓 → ∀𝑥𝜓) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓) | ||
Theorem | bj-ax12w 35027* | The general statement that ax12w 2130 proves. (Contributed by BJ, 20-Mar-2020.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝑦 = 𝑧 → (𝜓 ↔ 𝜃)) ⇒ ⊢ (𝜑 → (∀𝑦𝜓 → ∀𝑥(𝜑 → 𝜓))) | ||
Theorem | bj-ax89 35028 | A theorem which could be used as sole axiom for the non-logical predicate instead of ax-8 2109 and ax-9 2117. Indeed, it is implied over propositional calculus by the conjunction of ax-8 2109 and ax-9 2117, as proved here. In the other direction, one can prove ax-8 2109 (respectively ax-9 2117) from bj-ax89 35028 by using mpan2 690 (respectively mpan 689) and equid 2016. TODO: move to main part. (Contributed by BJ, 3-Oct-2019.) |
⊢ ((𝑥 = 𝑦 ∧ 𝑧 = 𝑡) → (𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑡)) | ||
Theorem | bj-elequ12 35029 | An identity law for the non-logical predicate, which combines elequ1 2114 and elequ2 2122. For the analogous theorems for class terms, see eleq1 2826, eleq2 2827 and eleq12 2828. TODO: move to main part. (Contributed by BJ, 29-Sep-2019.) |
⊢ ((𝑥 = 𝑦 ∧ 𝑧 = 𝑡) → (𝑥 ∈ 𝑧 ↔ 𝑦 ∈ 𝑡)) | ||
Theorem | bj-cleljusti 35030* | One direction of cleljust 2116, requiring only ax-1 6-- ax-5 1914 and ax8v1 2111. (Contributed by BJ, 31-Dec-2020.) (Proof modification is discouraged.) |
⊢ (∃𝑧(𝑧 = 𝑥 ∧ 𝑧 ∈ 𝑦) → 𝑥 ∈ 𝑦) | ||
Theorem | bj-alcomexcom 35031 | Commutation of two existential quantifiers on a formula is equivalent to commutation of two universal quantifiers over the same variables on the negation of that formula. Can be placed in the ax-4 1812 section, soon after 2nexaln 1833, and used to prove excom 2163. (Contributed by BJ, 29-Nov-2020.) (Proof modification is discouraged.) |
⊢ ((∀𝑥∀𝑦 ¬ 𝜑 → ∀𝑦∀𝑥 ¬ 𝜑) ↔ (∃𝑦∃𝑥𝜑 → ∃𝑥∃𝑦𝜑)) | ||
Theorem | bj-hbalt 35032 | Closed form of hbal 2168. When in main part, prove hbal 2168 and hbald 2169 from it. (Contributed by BJ, 2-May-2019.) |
⊢ (∀𝑦(𝜑 → ∀𝑥𝜑) → (∀𝑦𝜑 → ∀𝑥∀𝑦𝜑)) | ||
Theorem | axc11n11 35033 | Proof of axc11n 2426 from { ax-1 6-- ax-7 2012, axc11 2430 } . Almost identical to axc11nfromc11 37274. (Contributed by NM, 6-Jul-2021.) (Proof modification is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥) | ||
Theorem | axc11n11r 35034 |
Proof of axc11n 2426 from { ax-1 6--
ax-7 2012, axc9 2382, axc11r 2366 } (note
that axc16 2254 is provable from { ax-1 6--
ax-7 2012, axc11r 2366 }).
Note that axc11n 2426 proves (over minimal calculus) that axc11 2430 and axc11r 2366 are equivalent. Therefore, axc11n11 35033 and axc11n11r 35034 prove that one can use one or the other as an axiom, provided one assumes the axioms listed above (axc11 2430 appears slightly stronger since axc11n11r 35034 requires axc9 2382 while axc11n11 35033 does not). (Contributed by BJ, 6-Jul-2021.) (Proof modification is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥) | ||
Theorem | bj-axc16g16 35035* | Proof of axc16g 2253 from { ax-1 6-- ax-7 2012, axc16 2254 }. (Contributed by BJ, 6-Jul-2021.) (Proof modification is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑧𝜑)) | ||
Theorem | bj-ax12v3 35036* | A weak version of ax-12 2172 which is stronger than ax12v 2173. Note that if one assumes reflexivity of equality ⊢ 𝑥 = 𝑥 (equid 2016), then bj-ax12v3 35036 implies ax-5 1914 over modal logic K (substitute 𝑥 for 𝑦). See also bj-ax12v3ALT 35037. (Contributed by BJ, 6-Jul-2021.) (Proof modification is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) | ||
Theorem | bj-ax12v3ALT 35037* | Alternate proof of bj-ax12v3 35036. Uses axc11r 2366 and axc15 2422 instead of ax-12 2172. (Contributed by BJ, 6-Jul-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) | ||
Theorem | bj-sb 35038* | A weak variant of sbid2 2512 not requiring ax-13 2372 nor ax-10 2138. On top of Tarski's FOL, one implication requires only ax12v 2173, and the other requires only sp 2177. (Contributed by BJ, 25-May-2021.) |
⊢ (𝜑 ↔ ∀𝑦(𝑦 = 𝑥 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) | ||
Theorem | bj-modalbe 35039 | The predicate-calculus version of the axiom (B) of modal logic. See also modal-b 2314. (Contributed by BJ, 20-Oct-2019.) |
⊢ (𝜑 → ∀𝑥∃𝑥𝜑) | ||
Theorem | bj-spst 35040 | Closed form of sps 2179. Once in main part, prove sps 2179 and spsd 2181 from it. (Contributed by BJ, 20-Oct-2019.) |
⊢ ((𝜑 → 𝜓) → (∀𝑥𝜑 → 𝜓)) | ||
Theorem | bj-19.21bit 35041 | Closed form of 19.21bi 2183. (Contributed by BJ, 20-Oct-2019.) |
⊢ ((𝜑 → ∀𝑥𝜓) → (𝜑 → 𝜓)) | ||
Theorem | bj-19.23bit 35042 | Closed form of 19.23bi 2185. (Contributed by BJ, 20-Oct-2019.) |
⊢ ((∃𝑥𝜑 → 𝜓) → (𝜑 → 𝜓)) | ||
Theorem | bj-nexrt 35043 | Closed form of nexr 2186. Contrapositive of 19.8a 2175. (Contributed by BJ, 20-Oct-2019.) |
⊢ (¬ ∃𝑥𝜑 → ¬ 𝜑) | ||
Theorem | bj-alrim 35044 | Closed form of alrimi 2207. (Contributed by BJ, 2-May-2019.) |
⊢ (Ⅎ𝑥𝜑 → (∀𝑥(𝜑 → 𝜓) → (𝜑 → ∀𝑥𝜓))) | ||
Theorem | bj-alrim2 35045 | Uncurried (imported) form of bj-alrim 35044. (Contributed by BJ, 2-May-2019.) |
⊢ ((Ⅎ𝑥𝜑 ∧ ∀𝑥(𝜑 → 𝜓)) → (𝜑 → ∀𝑥𝜓)) | ||
Theorem | bj-nfdt0 35046 | A theorem close to a closed form of nf5d 2282 and nf5dh 2144. (Contributed by BJ, 2-May-2019.) |
⊢ (∀𝑥(𝜑 → (𝜓 → ∀𝑥𝜓)) → (∀𝑥𝜑 → Ⅎ𝑥𝜓)) | ||
Theorem | bj-nfdt 35047 | Closed form of nf5d 2282 and nf5dh 2144. (Contributed by BJ, 2-May-2019.) |
⊢ (∀𝑥(𝜑 → (𝜓 → ∀𝑥𝜓)) → ((𝜑 → ∀𝑥𝜑) → (𝜑 → Ⅎ𝑥𝜓))) | ||
Theorem | bj-nexdt 35048 | Closed form of nexd 2215. (Contributed by BJ, 20-Oct-2019.) |
⊢ (Ⅎ𝑥𝜑 → (∀𝑥(𝜑 → ¬ 𝜓) → (𝜑 → ¬ ∃𝑥𝜓))) | ||
Theorem | bj-nexdvt 35049* | Closed form of nexdv 1940. (Contributed by BJ, 20-Oct-2019.) |
⊢ (∀𝑥(𝜑 → ¬ 𝜓) → (𝜑 → ¬ ∃𝑥𝜓)) | ||
Theorem | bj-alexbiex 35050 | Adding a second quantifier over the same variable is a transparent operation, (∀∃ case). (Contributed by BJ, 20-Oct-2019.) |
⊢ (∀𝑥∃𝑥𝜑 ↔ ∃𝑥𝜑) | ||
Theorem | bj-exexbiex 35051 | Adding a second quantifier over the same variable is a transparent operation, (∃∃ case). (Contributed by BJ, 20-Oct-2019.) |
⊢ (∃𝑥∃𝑥𝜑 ↔ ∃𝑥𝜑) | ||
Theorem | bj-alalbial 35052 | Adding a second quantifier over the same variable is a transparent operation, (∀∀ case). (Contributed by BJ, 20-Oct-2019.) |
⊢ (∀𝑥∀𝑥𝜑 ↔ ∀𝑥𝜑) | ||
Theorem | bj-exalbial 35053 | Adding a second quantifier over the same variable is a transparent operation, (∃∀ case). (Contributed by BJ, 20-Oct-2019.) |
⊢ (∃𝑥∀𝑥𝜑 ↔ ∀𝑥𝜑) | ||
Theorem | bj-19.9htbi 35054 | Strengthening 19.9ht 2315 by replacing its consequent with a biconditional (19.9t 2198 does have a biconditional consequent). This propagates. (Contributed by BJ, 20-Oct-2019.) |
⊢ (∀𝑥(𝜑 → ∀𝑥𝜑) → (∃𝑥𝜑 ↔ 𝜑)) | ||
Theorem | bj-hbntbi 35055 | Strengthening hbnt 2292 by replacing its consequent with a biconditional. See also hbntg 34158 and hbntal 42568. (Contributed by BJ, 20-Oct-2019.) Proved from bj-19.9htbi 35054. (Proof modification is discouraged.) |
⊢ (∀𝑥(𝜑 → ∀𝑥𝜑) → (¬ 𝜑 ↔ ∀𝑥 ¬ 𝜑)) | ||
Theorem | bj-biexal1 35056 | A general FOL biconditional that generalizes 19.9ht 2315 among others. For this and the following theorems, see also 19.35 1881, 19.21 2201, 19.23 2205. When 𝜑 is substituted for 𝜓, both sides express a form of nonfreeness. (Contributed by BJ, 20-Oct-2019.) |
⊢ (∀𝑥(𝜑 → ∀𝑥𝜓) ↔ (∃𝑥𝜑 → ∀𝑥𝜓)) | ||
Theorem | bj-biexal2 35057 | When 𝜑 is substituted for 𝜓, both sides express a form of nonfreeness. (Contributed by BJ, 20-Oct-2019.) |
⊢ (∀𝑥(∃𝑥𝜑 → 𝜓) ↔ (∃𝑥𝜑 → ∀𝑥𝜓)) | ||
Theorem | bj-biexal3 35058 | When 𝜑 is substituted for 𝜓, both sides express a form of nonfreeness. (Contributed by BJ, 20-Oct-2019.) |
⊢ (∀𝑥(𝜑 → ∀𝑥𝜓) ↔ ∀𝑥(∃𝑥𝜑 → 𝜓)) | ||
Theorem | bj-bialal 35059 | When 𝜑 is substituted for 𝜓, both sides express a form of nonfreeness. (Contributed by BJ, 20-Oct-2019.) |
⊢ (∀𝑥(∀𝑥𝜑 → 𝜓) ↔ (∀𝑥𝜑 → ∀𝑥𝜓)) | ||
Theorem | bj-biexex 35060 | When 𝜑 is substituted for 𝜓, both sides express a form of nonfreeness. (Contributed by BJ, 20-Oct-2019.) |
⊢ (∀𝑥(𝜑 → ∃𝑥𝜓) ↔ (∃𝑥𝜑 → ∃𝑥𝜓)) | ||
Theorem | bj-hbext 35061 | Closed form of hbex 2320. (Contributed by BJ, 10-Oct-2019.) |
⊢ (∀𝑦∀𝑥(𝜑 → ∀𝑥𝜑) → (∃𝑦𝜑 → ∀𝑥∃𝑦𝜑)) | ||
Theorem | bj-nfalt 35062 | Closed form of nfal 2318. (Contributed by BJ, 2-May-2019.) |
⊢ (∀𝑥Ⅎ𝑦𝜑 → Ⅎ𝑦∀𝑥𝜑) | ||
Theorem | bj-nfext 35063 | Closed form of nfex 2319. (Contributed by BJ, 10-Oct-2019.) |
⊢ (∀𝑥Ⅎ𝑦𝜑 → Ⅎ𝑦∃𝑥𝜑) | ||
Theorem | bj-eeanvw 35064* | Version of exdistrv 1960 with a disjoint variable condition on 𝑥, 𝑦 not requiring ax-11 2155. (The same can be done with eeeanv 2348 and ee4anv 2349.) (Contributed by BJ, 29-Sep-2019.) (Proof modification is discouraged.) |
⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ ∃𝑦𝜓)) | ||
Theorem | bj-modal4 35065 | First-order logic form of the modal axiom (4). See hba1 2291. This is the standard proof of the implication in modal logic (B5 ⇒ 4). Its dual statement is bj-modal4e 35066. (Contributed by BJ, 12-Aug-2023.) (Proof modification is discouraged.) |
⊢ (∀𝑥𝜑 → ∀𝑥∀𝑥𝜑) | ||
Theorem | bj-modal4e 35066 | First-order logic form of the modal axiom (4) using existential quantifiers. Dual statement of bj-modal4 35065 (hba1 2291). (Contributed by BJ, 21-Dec-2020.) (Proof modification is discouraged.) |
⊢ (∃𝑥∃𝑥𝜑 → ∃𝑥𝜑) | ||
Theorem | bj-modalb 35067 | A short form of the axiom B of modal logic using only primitive symbols (→ , ¬ , ∀). (Contributed by BJ, 4-Apr-2021.) (Proof modification is discouraged.) |
⊢ (¬ 𝜑 → ∀𝑥 ¬ ∀𝑥𝜑) | ||
Theorem | bj-wnf1 35068 | When 𝜑 is substituted for 𝜓, this is the first half of nonfreness (. → ∀) of the weak form of nonfreeness (∃ → ∀). (Contributed by BJ, 9-Dec-2023.) |
⊢ ((∃𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(∃𝑥𝜑 → ∀𝑥𝜓)) | ||
Theorem | bj-wnf2 35069 | When 𝜑 is substituted for 𝜓, this is the first half of nonfreness (. → ∀) of the weak form of nonfreeness (∃ → ∀). (Contributed by BJ, 9-Dec-2023.) |
⊢ (∃𝑥(∃𝑥𝜑 → ∀𝑥𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓)) | ||
Theorem | bj-wnfanf 35070 | When 𝜑 is substituted for 𝜓, this statement expresses that weak nonfreeness implies the universal form of nonfreeness. (Contributed by BJ, 9-Dec-2023.) |
⊢ ((∃𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑 → ∀𝑥𝜓)) | ||
Theorem | bj-wnfenf 35071 | When 𝜑 is substituted for 𝜓, this statement expresses that weak nonfreeness implies the existential form of nonfreeness. (Contributed by BJ, 9-Dec-2023.) |
⊢ ((∃𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(∃𝑥𝜑 → 𝜓)) | ||
Theorem | bj-substax12 35072 |
Equivalent form of the axiom of substitution bj-ax12 35007. Although both
sides need a DV condition on 𝑥, 𝑡 (or as in bj-ax12v3 35036 on
𝑡,
𝜑) to hold, their
equivalence holds without DV conditions. The
forward implication is proved in modal (K4) while the reverse implication
is proved in modal (T5). The LHS has the advantage of not involving
nested quantifiers on the same variable. Its metaweakening is proved from
the core axiom schemes in bj-substw 35073. Note that in the LHS, the reverse
implication holds by equs4 2416 (or equs4v 2004 if a DV condition is added on
𝑥,
𝑡 as in bj-ax12 35007), and the forward implication is sbalex 2236.
The LHS can be read as saying that if there exists a setvar equal to a given term witnessing 𝜑, then all setvars equal to that term also witness 𝜑. An equivalent suggestive form for the LHS is ¬ (∃𝑥(𝑥 = 𝑡 ∧ 𝜑) ∧ ∃𝑥(𝑥 = 𝑡 ∧ ¬ 𝜑)), which expresses that there can be no two variables both equal to a given term, one witnessing 𝜑 and the other witnessing ¬ 𝜑. (Contributed by BJ, 21-May-2024.) (Proof modification is discouraged.) |
⊢ ((∃𝑥(𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑)) ↔ ∀𝑥(𝑥 = 𝑡 → (𝜑 → ∀𝑥(𝑥 = 𝑡 → 𝜑)))) | ||
Theorem | bj-substw 35073* | Weak form of the LHS of bj-substax12 35072 proved from the core axiom schemes. Compare ax12w 2130. (Contributed by BJ, 26-May-2024.) (Proof modification is discouraged.) |
⊢ (𝑥 = 𝑡 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥(𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑)) | ||
Syntax | wnnf 35074 | Syntax for the nonfreeness quantifier. |
wff Ⅎ'𝑥𝜑 | ||
Definition | df-bj-nnf 35075 |
Definition of the nonfreeness quantifier. The formula Ⅎ'𝑥𝜑 has
the intended meaning that the variable 𝑥 is semantically nonfree in
the formula 𝜑. The motivation for this quantifier
is to have a
condition expressible in the logic which is as close as possible to the
non-occurrence condition DV (𝑥, 𝜑) (in Metamath files, "$d x ph
$."), which belongs to the metalogic.
The standard syntactic nonfreeness condition, also expressed in the metalogic, is intermediate between these two notions: semantic nonfreeness implies syntactic nonfreeness, which implies non-occurrence. Both implications are strict; for the first, note that ⊢ Ⅎ'𝑥𝑥 = 𝑥, that is, 𝑥 is semantically (but not syntactically) nonfree in the formula 𝑥 = 𝑥; for the second, note that 𝑥 is syntactically nonfree in the formula ∀𝑥𝑥 = 𝑥 although it occurs in it. We now prove two metatheorems which make precise the above fact that, as far as proving power is concerned, the nonfreeness condition Ⅎ'𝑥𝜑 is very close to the non-occurrence condition DV (𝑥, 𝜑). Let S be a Metamath system with the FOL-syntax of (i)set.mm, containing intuitionistic positive propositional calculus and ax-5 1914 and ax5e 1916. Theorem 1. If the scheme (Ⅎ'𝑥𝜑 & PHI1 & ... & PHIn ⇒ PHI0, DV) is provable in S, then so is the scheme (PHI1 & ... & PHIn ⇒ PHI0, DV ∪ {{𝑥, 𝜑}}). Proof: By bj-nnfv 35105, we can prove (Ⅎ'𝑥𝜑, {{𝑥, 𝜑}}), from which the theorem follows. QED Theorem 2. Suppose that S also contains (the FOL version of) modal logic KB and commutation of quantifiers alcom 2157 and excom 2163 (possibly weakened by a DV condition on the quantifying variables), and that S can be axiomatized such that the only axioms with a DV condition involving a formula variable are among ax-5 1914, ax5e 1916, ax5ea 1917. If the scheme (PHI1 & ... & PHIn ⇒ PHI0, DV) is provable in S, then so is the scheme (Ⅎ'𝑥𝜑 & PHI1 & ... & PHIn ⇒ PHI0, DV ∖ {{𝑥, 𝜑}}). More precisely, if S contains modal 45 and if the variables quantified over in PHI0, ..., PHIn are among 𝑥1, ..., 𝑥m, then the scheme (PHI1 & ... & PHIn ⇒ (antecedent → PHI0), DV ∖ {{𝑥, 𝜑}}) is provable in S, where the antecedent is a finite conjunction of formulas of the form ∀𝑥i1 ...∀𝑥ip Ⅎ'𝑥𝜑 where the 𝑥ij's are among the 𝑥i's. Lemma: If 𝑥 ∉ OC(PHI), then S proves the scheme (Ⅎ'𝑥𝜑 ⇒ Ⅎ'𝑥 PHI, {{𝑥, 𝑎} ∣ 𝑎 ∈ OC(PHI) ∖ {𝜑}}). More precisely, if the variables quantified over in PHI are among 𝑥1, ..., 𝑥m, then ((antecedent → Ⅎ'𝑥 PHI), {{𝑥, 𝑎} ∣ 𝑎 ∈ OC(PHI) ∖ {𝜑}}) is provable in S, with the same form of antecedent as above. Proof: By induction on the height of PHI. We first note that by bj-nnfbi 35076 we can assume that PHI contains only primitive (as opposed to defined) symbols. For the base case, atomic formulas are either 𝜑, in which case the scheme to prove is an instance of id 22, or have variables all in OC(PHI) ∖ {𝜑}, so (Ⅎ'𝑥 PHI, {{𝑥, 𝑎} ∣ 𝑎 ∈ OC(PHI) ∖ {𝜑}}) by bj-nnfv 35105, hence ((Ⅎ'𝑥𝜑 → Ⅎ'𝑥 PHI), {{𝑥, 𝑎} ∣ 𝑎 ∈ OC(PHI) ∖ {𝜑}}) by a1i 11. For the induction step, PHI is either an implication, a negation, a conjunction, a disjunction, a biconditional, a universal or an existential quantification of formulas where 𝑥 does not occur. We use respectively bj-nnfim 35097, bj-nnfnt 35091, bj-nnfan 35099, bj-nnfor 35101, bj-nnfbit 35103, bj-nnfalt 35117, bj-nnfext 35118. For instance, in the implication case, if we have by induction hypothesis ((∀𝑥1 ...∀𝑥m Ⅎ'𝑥𝜑 → Ⅎ'𝑥 PHI), {{𝑥, 𝑎} ∣ 𝑎 ∈ OC(PHI) ∖ {𝜑}}) and ((∀𝑦1 ...∀𝑦n Ⅎ'𝑥𝜑 → Ⅎ'𝑥 PSI), {{𝑥, 𝑎} ∣ 𝑎 ∈ OC(PSI) ∖ {𝜑}}), then bj-nnfim 35097 yields (((∀𝑥1 ...∀𝑥m Ⅎ'𝑥𝜑 ∧ ∀𝑦1 ...∀𝑦n Ⅎ'𝑥𝜑) → Ⅎ'𝑥 (PHI → PSI)), {{𝑥, 𝑎} ∣ 𝑎 ∈ OC(PHI → PSI) ∖ {𝜑}}) and similarly for antecedents which are conjunctions as in the statement of the lemma. In the universal quantification case, say quantification over 𝑦, if we have by induction hypothesis ((∀𝑥1 ...∀𝑥m Ⅎ'𝑥𝜑 → Ⅎ'𝑥 PHI), {{𝑥, 𝑎} ∣ 𝑎 ∈ OC(PHI) ∖ {𝜑}}), then bj-nnfalt 35117 yields ((∀𝑦∀𝑥1 ...∀𝑥m Ⅎ'𝑥𝜑 → Ⅎ'𝑥∀𝑦 PHI), {{𝑥, 𝑎} ∣ 𝑎 ∈ OC(∀𝑦 PHI) ∖ {𝜑}}) and similarly for antecedents which are conjunctions as in the statement of the lemma. Note bj-nnfalt 35117 and bj-nnfext 35118 are proved from positive propositional calculus with alcom 2157 and excom 2163 (possibly weakened by a DV condition on the quantifying variables), and modalB (via bj-19.12 35112). QED Proof of the theorem: Consider a proof of that scheme directly from the axioms. Consider a step where a DV condition involving 𝜑 is used. By hypothesis, that step is an instance of ax-5 1914 or ax5e 1916 or ax5ea 1917. It has the form (PSI → ∀𝑥 PSI) where PSI has the form of the lemma and the DV conditions of the proof contain {{𝑥, 𝑎} ∣ 𝑎 ∈ OC(PSI) }. Therefore, one has ((∀𝑥1 ...∀𝑥m Ⅎ'𝑥𝜑 → Ⅎ'𝑥 PSI), {{𝑥, 𝑎} ∣ 𝑎 ∈ OC(PSI) ∖ {𝜑}}) for appropriate 𝑥i's, and by bj-nnfa 35079 we obtain ((∀𝑥1 ...∀𝑥m Ⅎ'𝑥𝜑 → (PSI → ∀𝑥 PSI)), {{𝑥, 𝑎} ∣ 𝑎 ∈ OC(PSI) ∖ {𝜑}}) and similarly for antecedents which are conjunctions as in the statement of the theorem. Similarly if the step is using ax5e 1916 or ax5ea 1917, we would use bj-nnfe 35082 or bj-nnfea 35085 respectively. Therefore, taking as antecedent of the theorem to prove the conjunction of all the antecedents at each of these steps, we obtain a proof by "carrying the context over", which is possible, as in the deduction theorem when the step uses ax-mp 5, and when the step uses ax-gen 1798, by bj-nnf-alrim 35106 and bj-nnfa1 35110 (which requires modal 45). The condition DV (𝑥, 𝜑) is not required by the resulting proof. Finally, there may be in the global antecedent thus constructed some dummy variables, which can be removed by spvw 1985. QED Compared with df-nf 1787, the present definition is stricter on positive propositional calculus (bj-nnfnfTEMP 35089) and equivalent on core FOL plus sp 2177 (bj-nfnnfTEMP 35109). While being stricter, it still holds for non-occurring variables (bj-nnfv 35105), which is the basic requirement for this quantifier. In particular, it translates more closely the associated variable disjointness condition. Since the nonfreeness quantifier is a means to translate a variable disjointness condition from the metalogic to the logic, it seems preferable. Also, since nonfreeness is mainly used as a hypothesis, this definition would allow more theorems, notably the 19.xx theorems, to be proved from the core axioms, without needing a 19.xxv variant. One can devise infinitely many definitions increasingly close to the non-occurring condition, like ((∃𝑥𝜑 → 𝜑) ∧ (𝜑 → ∀𝑥𝜑)) ∧ ∀𝑥((∃𝑥𝜑 → 𝜑) ∧ (𝜑 → ∀𝑥𝜑)) ∧ ∀𝑥∀𝑥... and each stronger definition would permit more theorems to be proved from the core axioms. A reasonable rule seems to be to stop before nested quantifiers appear (since they typically require ax-10 2138 to work with), and also not to have redundant conjuncts when full metacomplete FOL= is developed. (Contributed by BJ, 28-Jul-2023.) |
⊢ (Ⅎ'𝑥𝜑 ↔ ((∃𝑥𝜑 → 𝜑) ∧ (𝜑 → ∀𝑥𝜑))) | ||
Theorem | bj-nnfbi 35076 | If two formulas are equivalent for all 𝑥, then nonfreeness of 𝑥 in one of them is equivalent to nonfreeness in the other. Compare nfbiit 1854. From this and bj-nnfim 35097 and bj-nnfnt 35091, one can prove analogous nonfreeness conservation results for other propositional operators. The antecedent is in the "strong necessity" modality of modal logic (see also bj-nnftht 35092) in order not to require sp 2177 (modal T). (Contributed by BJ, 27-Aug-2023.) |
⊢ (((𝜑 ↔ 𝜓) ∧ ∀𝑥(𝜑 ↔ 𝜓)) → (Ⅎ'𝑥𝜑 ↔ Ⅎ'𝑥𝜓)) | ||
Theorem | bj-nnfbd 35077* | If two formulas are equivalent for all 𝑥, then nonfreeness of 𝑥 in one of them is equivalent to nonfreeness in the other, deduction form. See bj-nnfbi 35076. (Contributed by BJ, 27-Aug-2023.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (Ⅎ'𝑥𝜓 ↔ Ⅎ'𝑥𝜒)) | ||
Theorem | bj-nnfbii 35078 | If two formulas are equivalent for all 𝑥, then nonfreeness of 𝑥 in one of them is equivalent to nonfreeness in the other, inference form. See bj-nnfbi 35076. (Contributed by BJ, 18-Nov-2023.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (Ⅎ'𝑥𝜑 ↔ Ⅎ'𝑥𝜓) | ||
Theorem | bj-nnfa 35079 | Nonfreeness implies the equivalent of ax-5 1914. See nf5r 2188. (Contributed by BJ, 28-Jul-2023.) |
⊢ (Ⅎ'𝑥𝜑 → (𝜑 → ∀𝑥𝜑)) | ||
Theorem | bj-nnfad 35080 | Nonfreeness implies the equivalent of ax-5 1914, deduction form. See nf5rd 2190. (Contributed by BJ, 2-Dec-2023.) |
⊢ (𝜑 → Ⅎ'𝑥𝜓) ⇒ ⊢ (𝜑 → (𝜓 → ∀𝑥𝜓)) | ||
Theorem | bj-nnfai 35081 | Nonfreeness implies the equivalent of ax-5 1914, inference form. See nf5ri 2189. (Contributed by BJ, 22-Sep-2024.) |
⊢ Ⅎ'𝑥𝜑 ⇒ ⊢ (𝜑 → ∀𝑥𝜑) | ||
Theorem | bj-nnfe 35082 | Nonfreeness implies the equivalent of ax5e 1916. (Contributed by BJ, 28-Jul-2023.) |
⊢ (Ⅎ'𝑥𝜑 → (∃𝑥𝜑 → 𝜑)) | ||
Theorem | bj-nnfed 35083 | Nonfreeness implies the equivalent of ax5e 1916, deduction form. (Contributed by BJ, 2-Dec-2023.) |
⊢ (𝜑 → Ⅎ'𝑥𝜓) ⇒ ⊢ (𝜑 → (∃𝑥𝜓 → 𝜓)) | ||
Theorem | bj-nnfei 35084 | Nonfreeness implies the equivalent of ax5e 1916, inference form. (Contributed by BJ, 22-Sep-2024.) |
⊢ Ⅎ'𝑥𝜑 ⇒ ⊢ (∃𝑥𝜑 → 𝜑) | ||
Theorem | bj-nnfea 35085 | Nonfreeness implies the equivalent of ax5ea 1917. (Contributed by BJ, 28-Jul-2023.) |
⊢ (Ⅎ'𝑥𝜑 → (∃𝑥𝜑 → ∀𝑥𝜑)) | ||
Theorem | bj-nnfead 35086 | Nonfreeness implies the equivalent of ax5ea 1917, deduction form. (Contributed by BJ, 2-Dec-2023.) |
⊢ (𝜑 → Ⅎ'𝑥𝜓) ⇒ ⊢ (𝜑 → (∃𝑥𝜓 → ∀𝑥𝜓)) | ||
Theorem | bj-nnfeai 35087 | Nonfreeness implies the equivalent of ax5ea 1917, inference form. (Contributed by BJ, 22-Sep-2024.) |
⊢ Ⅎ'𝑥𝜑 ⇒ ⊢ (∃𝑥𝜑 → ∀𝑥𝜑) | ||
Theorem | bj-dfnnf2 35088 | Alternate definition of df-bj-nnf 35075 using only primitive symbols (→, ¬, ∀) in each conjunct. (Contributed by BJ, 20-Aug-2023.) |
⊢ (Ⅎ'𝑥𝜑 ↔ ((𝜑 → ∀𝑥𝜑) ∧ (¬ 𝜑 → ∀𝑥 ¬ 𝜑))) | ||
Theorem | bj-nnfnfTEMP 35089 | New nonfreeness implies old nonfreeness on minimal implicational calculus (the proof indicates it uses ax-3 8 because of set.mm's definition of the biconditional, but the proof actually holds in minimal implicational calculus). (Contributed by BJ, 28-Jul-2023.) The proof should not rely on df-nf 1787 except via df-nf 1787 directly. (Proof modification is discouraged.) |
⊢ (Ⅎ'𝑥𝜑 → Ⅎ𝑥𝜑) | ||
Theorem | bj-wnfnf 35090 | When 𝜑 is substituted for 𝜓, this statement expresses nonfreeness in the weak form of nonfreeness (∃ → ∀). Note that this could also be proved from bj-nnfim 35097, bj-nnfe1 35111 and bj-nnfa1 35110. (Contributed by BJ, 9-Dec-2023.) |
⊢ Ⅎ'𝑥(∃𝑥𝜑 → ∀𝑥𝜓) | ||
Theorem | bj-nnfnt 35091 | A variable is nonfree in a formula if and only if it is nonfree in its negation. The foward implication is intuitionistically valid (and that direction is sufficient for the purpose of recursively proving that some formulas have a given variable not free in them, like bj-nnfim 35097). Intuitionistically, ⊢ (Ⅎ'𝑥¬ 𝜑 ↔ Ⅎ'𝑥¬ ¬ 𝜑). See nfnt 1860. (Contributed by BJ, 28-Jul-2023.) |
⊢ (Ⅎ'𝑥𝜑 ↔ Ⅎ'𝑥 ¬ 𝜑) | ||
Theorem | bj-nnftht 35092 | A variable is nonfree in a theorem. The antecedent is in the "strong necessity" modality of modal logic in order not to require sp 2177 (modal T), as in bj-nnfbi 35076. (Contributed by BJ, 28-Jul-2023.) |
⊢ ((𝜑 ∧ ∀𝑥𝜑) → Ⅎ'𝑥𝜑) | ||
Theorem | bj-nnfth 35093 | A variable is nonfree in a theorem, inference form. (Contributed by BJ, 28-Jul-2023.) |
⊢ 𝜑 ⇒ ⊢ Ⅎ'𝑥𝜑 | ||
Theorem | bj-nnfnth 35094 | A variable is nonfree in the negation of a theorem, inference form. (Contributed by BJ, 27-Aug-2023.) |
⊢ ¬ 𝜑 ⇒ ⊢ Ⅎ'𝑥𝜑 | ||
Theorem | bj-nnfim1 35095 | A consequence of nonfreeness in the antecedent and the consequent of an implication. (Contributed by BJ, 27-Aug-2023.) |
⊢ ((Ⅎ'𝑥𝜑 ∧ Ⅎ'𝑥𝜓) → ((𝜑 → 𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓))) | ||
Theorem | bj-nnfim2 35096 | A consequence of nonfreeness in the antecedent and the consequent of an implication. (Contributed by BJ, 27-Aug-2023.) |
⊢ ((Ⅎ'𝑥𝜑 ∧ Ⅎ'𝑥𝜓) → ((∀𝑥𝜑 → ∃𝑥𝜓) → (𝜑 → 𝜓))) | ||
Theorem | bj-nnfim 35097 | Nonfreeness in the antecedent and the consequent of an implication implies nonfreeness in the implication. (Contributed by BJ, 27-Aug-2023.) |
⊢ ((Ⅎ'𝑥𝜑 ∧ Ⅎ'𝑥𝜓) → Ⅎ'𝑥(𝜑 → 𝜓)) | ||
Theorem | bj-nnfimd 35098 | Nonfreeness in the antecedent and the consequent of an implication implies nonfreeness in the implication, deduction form. (Contributed by BJ, 2-Dec-2023.) |
⊢ (𝜑 → Ⅎ'𝑥𝜓) & ⊢ (𝜑 → Ⅎ'𝑥𝜒) ⇒ ⊢ (𝜑 → Ⅎ'𝑥(𝜓 → 𝜒)) | ||
Theorem | bj-nnfan 35099 | Nonfreeness in both conjuncts implies nonfreeness in the conjunction. (Contributed by BJ, 19-Nov-2023.) In classical logic, there is a proof using the definition of conjunction in terms of implication and negation, so using bj-nnfim 35097, bj-nnfnt 35091 and bj-nnfbi 35076, but we want a proof valid in intuitionistic logic. (Proof modification is discouraged.) |
⊢ ((Ⅎ'𝑥𝜑 ∧ Ⅎ'𝑥𝜓) → Ⅎ'𝑥(𝜑 ∧ 𝜓)) | ||
Theorem | bj-nnfand 35100 | Nonfreeness in both conjuncts implies nonfreeness in the conjunction, deduction form. Note: compared with the proof of bj-nnfan 35099, it has two more essential steps but fewer total steps (since there are fewer intermediate formulas to build) and is easier to follow and understand. This statement is of intermediate complexity: for simpler statements, closed-style proofs like that of bj-nnfan 35099 will generally be shorter than deduction-style proofs while still easy to follow, while for more complex statements, the opposite will be true (and deduction-style proofs like that of bj-nnfand 35100 will generally be easier to understand). (Contributed by BJ, 19-Nov-2023.) (Proof modification is discouraged.) |
⊢ (𝜑 → Ⅎ'𝑥𝜓) & ⊢ (𝜑 → Ⅎ'𝑥𝜒) ⇒ ⊢ (𝜑 → Ⅎ'𝑥(𝜓 ∧ 𝜒)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |