![]() |
Metamath
Proof Explorer Theorem List (p. 357 of 479) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30166) |
![]() (30167-31689) |
![]() (31690-47842) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | bj-nnfa 35601 | Nonfreeness implies the equivalent of ax-5 1913. See nf5r 2187. (Contributed by BJ, 28-Jul-2023.) |
⊢ (Ⅎ'𝑥𝜑 → (𝜑 → ∀𝑥𝜑)) | ||
Theorem | bj-nnfad 35602 | Nonfreeness implies the equivalent of ax-5 1913, deduction form. See nf5rd 2189. (Contributed by BJ, 2-Dec-2023.) |
⊢ (𝜑 → Ⅎ'𝑥𝜓) ⇒ ⊢ (𝜑 → (𝜓 → ∀𝑥𝜓)) | ||
Theorem | bj-nnfai 35603 | Nonfreeness implies the equivalent of ax-5 1913, inference form. See nf5ri 2188. (Contributed by BJ, 22-Sep-2024.) |
⊢ Ⅎ'𝑥𝜑 ⇒ ⊢ (𝜑 → ∀𝑥𝜑) | ||
Theorem | bj-nnfe 35604 | Nonfreeness implies the equivalent of ax5e 1915. (Contributed by BJ, 28-Jul-2023.) |
⊢ (Ⅎ'𝑥𝜑 → (∃𝑥𝜑 → 𝜑)) | ||
Theorem | bj-nnfed 35605 | Nonfreeness implies the equivalent of ax5e 1915, deduction form. (Contributed by BJ, 2-Dec-2023.) |
⊢ (𝜑 → Ⅎ'𝑥𝜓) ⇒ ⊢ (𝜑 → (∃𝑥𝜓 → 𝜓)) | ||
Theorem | bj-nnfei 35606 | Nonfreeness implies the equivalent of ax5e 1915, inference form. (Contributed by BJ, 22-Sep-2024.) |
⊢ Ⅎ'𝑥𝜑 ⇒ ⊢ (∃𝑥𝜑 → 𝜑) | ||
Theorem | bj-nnfea 35607 | Nonfreeness implies the equivalent of ax5ea 1916. (Contributed by BJ, 28-Jul-2023.) |
⊢ (Ⅎ'𝑥𝜑 → (∃𝑥𝜑 → ∀𝑥𝜑)) | ||
Theorem | bj-nnfead 35608 | Nonfreeness implies the equivalent of ax5ea 1916, deduction form. (Contributed by BJ, 2-Dec-2023.) |
⊢ (𝜑 → Ⅎ'𝑥𝜓) ⇒ ⊢ (𝜑 → (∃𝑥𝜓 → ∀𝑥𝜓)) | ||
Theorem | bj-nnfeai 35609 | Nonfreeness implies the equivalent of ax5ea 1916, inference form. (Contributed by BJ, 22-Sep-2024.) |
⊢ Ⅎ'𝑥𝜑 ⇒ ⊢ (∃𝑥𝜑 → ∀𝑥𝜑) | ||
Theorem | bj-dfnnf2 35610 | Alternate definition of df-bj-nnf 35597 using only primitive symbols (→, ¬, ∀) in each conjunct. (Contributed by BJ, 20-Aug-2023.) |
⊢ (Ⅎ'𝑥𝜑 ↔ ((𝜑 → ∀𝑥𝜑) ∧ (¬ 𝜑 → ∀𝑥 ¬ 𝜑))) | ||
Theorem | bj-nnfnfTEMP 35611 | 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 1786 except via df-nf 1786 directly. (Proof modification is discouraged.) |
⊢ (Ⅎ'𝑥𝜑 → Ⅎ𝑥𝜑) | ||
Theorem | bj-wnfnf 35612 | When 𝜑 is substituted for 𝜓, this statement expresses nonfreeness in the weak form of nonfreeness (∃ → ∀). Note that this could also be proved from bj-nnfim 35619, bj-nnfe1 35633 and bj-nnfa1 35632. (Contributed by BJ, 9-Dec-2023.) |
⊢ Ⅎ'𝑥(∃𝑥𝜑 → ∀𝑥𝜓) | ||
Theorem | bj-nnfnt 35613 | 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 35619). Intuitionistically, ⊢ (Ⅎ'𝑥¬ 𝜑 ↔ Ⅎ'𝑥¬ ¬ 𝜑). See nfnt 1859. (Contributed by BJ, 28-Jul-2023.) |
⊢ (Ⅎ'𝑥𝜑 ↔ Ⅎ'𝑥 ¬ 𝜑) | ||
Theorem | bj-nnftht 35614 | A variable is nonfree in a theorem. The antecedent is in the "strong necessity" modality of modal logic in order not to require sp 2176 (modal T), as in bj-nnfbi 35598. (Contributed by BJ, 28-Jul-2023.) |
⊢ ((𝜑 ∧ ∀𝑥𝜑) → Ⅎ'𝑥𝜑) | ||
Theorem | bj-nnfth 35615 | A variable is nonfree in a theorem, inference form. (Contributed by BJ, 28-Jul-2023.) |
⊢ 𝜑 ⇒ ⊢ Ⅎ'𝑥𝜑 | ||
Theorem | bj-nnfnth 35616 | A variable is nonfree in the negation of a theorem, inference form. (Contributed by BJ, 27-Aug-2023.) |
⊢ ¬ 𝜑 ⇒ ⊢ Ⅎ'𝑥𝜑 | ||
Theorem | bj-nnfim1 35617 | A consequence of nonfreeness in the antecedent and the consequent of an implication. (Contributed by BJ, 27-Aug-2023.) |
⊢ ((Ⅎ'𝑥𝜑 ∧ Ⅎ'𝑥𝜓) → ((𝜑 → 𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓))) | ||
Theorem | bj-nnfim2 35618 | A consequence of nonfreeness in the antecedent and the consequent of an implication. (Contributed by BJ, 27-Aug-2023.) |
⊢ ((Ⅎ'𝑥𝜑 ∧ Ⅎ'𝑥𝜓) → ((∀𝑥𝜑 → ∃𝑥𝜓) → (𝜑 → 𝜓))) | ||
Theorem | bj-nnfim 35619 | Nonfreeness in the antecedent and the consequent of an implication implies nonfreeness in the implication. (Contributed by BJ, 27-Aug-2023.) |
⊢ ((Ⅎ'𝑥𝜑 ∧ Ⅎ'𝑥𝜓) → Ⅎ'𝑥(𝜑 → 𝜓)) | ||
Theorem | bj-nnfimd 35620 | 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 35621 | 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 35619, bj-nnfnt 35613 and bj-nnfbi 35598, but we want a proof valid in intuitionistic logic. (Proof modification is discouraged.) |
⊢ ((Ⅎ'𝑥𝜑 ∧ Ⅎ'𝑥𝜓) → Ⅎ'𝑥(𝜑 ∧ 𝜓)) | ||
Theorem | bj-nnfand 35622 | Nonfreeness in both conjuncts implies nonfreeness in the conjunction, deduction form. Note: compared with the proof of bj-nnfan 35621, 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 35621 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 35622 will generally be easier to understand). (Contributed by BJ, 19-Nov-2023.) (Proof modification is discouraged.) |
⊢ (𝜑 → Ⅎ'𝑥𝜓) & ⊢ (𝜑 → Ⅎ'𝑥𝜒) ⇒ ⊢ (𝜑 → Ⅎ'𝑥(𝜓 ∧ 𝜒)) | ||
Theorem | bj-nnfor 35623 | Nonfreeness in both disjuncts implies nonfreeness in the disjunction. (Contributed by BJ, 19-Nov-2023.) In classical logic, there is a proof using the definition of disjunction in terms of implication and negation, so using bj-nnfim 35619, bj-nnfnt 35613 and bj-nnfbi 35598, but we want a proof valid in intuitionistic logic. (Proof modification is discouraged.) |
⊢ ((Ⅎ'𝑥𝜑 ∧ Ⅎ'𝑥𝜓) → Ⅎ'𝑥(𝜑 ∨ 𝜓)) | ||
Theorem | bj-nnford 35624 | Nonfreeness in both disjuncts implies nonfreeness in the disjunction, deduction form. See comments for bj-nnfor 35623 and bj-nnfand 35622. (Contributed by BJ, 2-Dec-2023.) (Proof modification is discouraged.) |
⊢ (𝜑 → Ⅎ'𝑥𝜓) & ⊢ (𝜑 → Ⅎ'𝑥𝜒) ⇒ ⊢ (𝜑 → Ⅎ'𝑥(𝜓 ∨ 𝜒)) | ||
Theorem | bj-nnfbit 35625 | Nonfreeness in both sides implies nonfreeness in the biconditional. (Contributed by BJ, 2-Dec-2023.) (Proof modification is discouraged.) |
⊢ ((Ⅎ'𝑥𝜑 ∧ Ⅎ'𝑥𝜓) → Ⅎ'𝑥(𝜑 ↔ 𝜓)) | ||
Theorem | bj-nnfbid 35626 | Nonfreeness in both sides implies nonfreeness in the biconditional, deduction form. (Contributed by BJ, 2-Dec-2023.) (Proof modification is discouraged.) |
⊢ (𝜑 → Ⅎ'𝑥𝜓) & ⊢ (𝜑 → Ⅎ'𝑥𝜒) ⇒ ⊢ (𝜑 → Ⅎ'𝑥(𝜓 ↔ 𝜒)) | ||
Theorem | bj-nnfv 35627* | A non-occurring variable is nonfree in a formula. (Contributed by BJ, 28-Jul-2023.) |
⊢ Ⅎ'𝑥𝜑 | ||
Theorem | bj-nnf-alrim 35628 | Proof of the closed form of alrimi 2206 from modalK (compare alrimiv 1930). See also bj-alrim 35566. Actually, most proofs between 19.3t 2194 and 2sbbid 2239 could be proved without ax-12 2171. (Contributed by BJ, 20-Aug-2023.) |
⊢ (Ⅎ'𝑥𝜑 → (∀𝑥(𝜑 → 𝜓) → (𝜑 → ∀𝑥𝜓))) | ||
Theorem | bj-nnf-exlim 35629 | Proof of the closed form of exlimi 2210 from modalK (compare exlimiv 1933). See also bj-sylget2 35494. (Contributed by BJ, 2-Dec-2023.) |
⊢ (Ⅎ'𝑥𝜓 → (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → 𝜓))) | ||
Theorem | bj-dfnnf3 35630 | Alternate definition of nonfreeness when sp 2176 is available. (Contributed by BJ, 28-Jul-2023.) The proof should not rely on df-nf 1786. (Proof modification is discouraged.) |
⊢ (Ⅎ'𝑥𝜑 ↔ (∃𝑥𝜑 → ∀𝑥𝜑)) | ||
Theorem | bj-nfnnfTEMP 35631 | New nonfreeness is equivalent to old nonfreeness on core FOL axioms plus sp 2176. (Contributed by BJ, 28-Jul-2023.) The proof should not rely on df-nf 1786 except via df-nf 1786 directly. (Proof modification is discouraged.) |
⊢ (Ⅎ'𝑥𝜑 ↔ Ⅎ𝑥𝜑) | ||
Theorem | bj-nnfa1 35632 | See nfa1 2148. (Contributed by BJ, 12-Aug-2023.) (Proof modification is discouraged.) |
⊢ Ⅎ'𝑥∀𝑥𝜑 | ||
Theorem | bj-nnfe1 35633 | See nfe1 2147. (Contributed by BJ, 12-Aug-2023.) (Proof modification is discouraged.) |
⊢ Ⅎ'𝑥∃𝑥𝜑 | ||
Theorem | bj-19.12 35634 | See 19.12 2320. Could be labeled "exalimalex" for "'there exists for all' implies 'for all there exists'". This proof is from excom 2162 and modal (B) on top of modalK logic. (Contributed by BJ, 12-Aug-2023.) The proof should not rely on df-nf 1786 or df-bj-nnf 35597, directly or indirectly. (Proof modification is discouraged.) |
⊢ (∃𝑥∀𝑦𝜑 → ∀𝑦∃𝑥𝜑) | ||
Theorem | bj-nnflemaa 35635 | One of four lemmas for nonfreeness: antecedent and consequent both expressed using universal quantifier. Note: this is bj-hbalt 35554. (Contributed by BJ, 12-Aug-2023.) (Proof modification is discouraged.) |
⊢ (∀𝑥(𝜑 → ∀𝑦𝜑) → (∀𝑥𝜑 → ∀𝑦∀𝑥𝜑)) | ||
Theorem | bj-nnflemee 35636 | One of four lemmas for nonfreeness: antecedent and consequent both expressed using existential quantifier. (Contributed by BJ, 12-Aug-2023.) (Proof modification is discouraged.) |
⊢ (∀𝑥(∃𝑦𝜑 → 𝜑) → (∃𝑦∃𝑥𝜑 → ∃𝑥𝜑)) | ||
Theorem | bj-nnflemae 35637 | One of four lemmas for nonfreeness: antecedent expressed with universal quantifier and consequent expressed with existential quantifier. (Contributed by BJ, 12-Aug-2023.) (Proof modification is discouraged.) |
⊢ (∀𝑥(𝜑 → ∀𝑦𝜑) → (∃𝑥𝜑 → ∀𝑦∃𝑥𝜑)) | ||
Theorem | bj-nnflemea 35638 | One of four lemmas for nonfreeness: antecedent expressed with existential quantifier and consequent expressed with universal quantifier. (Contributed by BJ, 12-Aug-2023.) (Proof modification is discouraged.) |
⊢ (∀𝑥(∃𝑦𝜑 → 𝜑) → (∃𝑦∀𝑥𝜑 → ∀𝑥𝜑)) | ||
Theorem | bj-nnfalt 35639 | See nfal 2316 and bj-nfalt 35584. (Contributed by BJ, 12-Aug-2023.) (Proof modification is discouraged.) |
⊢ (∀𝑥Ⅎ'𝑦𝜑 → Ⅎ'𝑦∀𝑥𝜑) | ||
Theorem | bj-nnfext 35640 | See nfex 2317 and bj-nfext 35585. (Contributed by BJ, 12-Aug-2023.) (Proof modification is discouraged.) |
⊢ (∀𝑥Ⅎ'𝑦𝜑 → Ⅎ'𝑦∃𝑥𝜑) | ||
Theorem | bj-stdpc5t 35641 | Alias of bj-nnf-alrim 35628 for labeling consistency (a standard predicate calculus axiom). Closed form of stdpc5 2201 proved from modalK (obsoleting stdpc5v 1941). (Contributed by BJ, 2-Dec-2023.) Use bj-nnf-alrim 35628 instead. (New usaged is discouraged.) |
⊢ (Ⅎ'𝑥𝜑 → (∀𝑥(𝜑 → 𝜓) → (𝜑 → ∀𝑥𝜓))) | ||
Theorem | bj-19.21t 35642 | Statement 19.21t 2199 proved from modalK (obsoleting 19.21v 1942). (Contributed by BJ, 2-Dec-2023.) |
⊢ (Ⅎ'𝑥𝜑 → (∀𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥𝜓))) | ||
Theorem | bj-19.23t 35643 | Statement 19.23t 2203 proved from modalK (obsoleting 19.23v 1945). (Contributed by BJ, 2-Dec-2023.) |
⊢ (Ⅎ'𝑥𝜓 → (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜓))) | ||
Theorem | bj-19.36im 35644 | One direction of 19.36 2223 from the same axioms as 19.36imv 1948. (Contributed by BJ, 2-Dec-2023.) |
⊢ (Ⅎ'𝑥𝜓 → (∃𝑥(𝜑 → 𝜓) → (∀𝑥𝜑 → 𝜓))) | ||
Theorem | bj-19.37im 35645 | One direction of 19.37 2225 from the same axioms as 19.37imv 1951. (Contributed by BJ, 2-Dec-2023.) |
⊢ (Ⅎ'𝑥𝜑 → (∃𝑥(𝜑 → 𝜓) → (𝜑 → ∃𝑥𝜓))) | ||
Theorem | bj-19.42t 35646 | Closed form of 19.42 2229 from the same axioms as 19.42v 1957. (Contributed by BJ, 2-Dec-2023.) |
⊢ (Ⅎ'𝑥𝜑 → (∃𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥𝜓))) | ||
Theorem | bj-19.41t 35647 | Closed form of 19.41 2228 from the same axioms as 19.41v 1953. The same is doable with 19.27 2220, 19.28 2221, 19.31 2227, 19.32 2226, 19.44 2230, 19.45 2231. (Contributed by BJ, 2-Dec-2023.) |
⊢ (Ⅎ'𝑥𝜓 → (∃𝑥(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ 𝜓))) | ||
Theorem | bj-sbft 35648 | Version of sbft 2261 using Ⅎ', proved from core axioms. (Contributed by BJ, 19-Nov-2023.) |
⊢ (Ⅎ'𝑥𝜑 → ([𝑡 / 𝑥]𝜑 ↔ 𝜑)) | ||
Theorem | bj-pm11.53vw 35649 | Version of pm11.53v 1947 with nonfreeness antecedents. One can also prove the theorem with antecedent (Ⅎ'𝑦∀𝑥𝜑 ∧ ∀𝑦Ⅎ'𝑥𝜓). (Contributed by BJ, 7-Oct-2024.) |
⊢ ((∀𝑥Ⅎ'𝑦𝜑 ∧ Ⅎ'𝑥∀𝑦𝜓) → (∀𝑥∀𝑦(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → ∀𝑦𝜓))) | ||
Theorem | bj-pm11.53v 35650 | Version of pm11.53v 1947 with nonfreeness antecedents. (Contributed by BJ, 7-Oct-2024.) |
⊢ ((∀𝑥Ⅎ'𝑦𝜑 ∧ ∀𝑦Ⅎ'𝑥𝜓) → (∀𝑥∀𝑦(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → ∀𝑦𝜓))) | ||
Theorem | bj-pm11.53a 35651* | A variant of pm11.53v 1947. One can similarly prove a variant with DV (𝑦, 𝜑) and ∀𝑦Ⅎ'𝑥𝜓 instead of DV (𝑥, 𝜓) and ∀𝑥Ⅎ'𝑦𝜑. (Contributed by BJ, 7-Oct-2024.) |
⊢ (∀𝑥Ⅎ'𝑦𝜑 → (∀𝑥∀𝑦(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → ∀𝑦𝜓))) | ||
Theorem | bj-equsvt 35652* | A variant of equsv 2006. (Contributed by BJ, 7-Oct-2024.) |
⊢ (Ⅎ'𝑥𝜑 → (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜑)) | ||
Theorem | bj-equsalvwd 35653* | Variant of equsalvw 2007. (Contributed by BJ, 7-Oct-2024.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜑 → Ⅎ'𝑥𝜒) & ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥(𝑥 = 𝑦 → 𝜓) ↔ 𝜒)) | ||
Theorem | bj-equsexvwd 35654* | Variant of equsexvw 2008. (Contributed by BJ, 7-Oct-2024.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜑 → Ⅎ'𝑥𝜒) & ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥(𝑥 = 𝑦 ∧ 𝜓) ↔ 𝜒)) | ||
Theorem | bj-sbievwd 35655* | Variant of sbievw 2095. (Contributed by BJ, 7-Oct-2024.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜑 → Ⅎ'𝑥𝜒) & ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ([𝑦 / 𝑥]𝜓 ↔ 𝜒)) | ||
Theorem | bj-axc10 35656 | Alternate proof of axc10 2384. Shorter. One can prove a version with DV (𝑥, 𝑦) without ax-13 2371, by using ax6ev 1973 instead of ax6e 2382. (Contributed by BJ, 31-Mar-2021.) (Proof modification is discouraged.) |
⊢ (∀𝑥(𝑥 = 𝑦 → ∀𝑥𝜑) → 𝜑) | ||
Theorem | bj-alequex 35657 | A fol lemma. See alequexv 2004 for a version with a disjoint variable condition requiring fewer axioms. Can be used to reduce the proof of spimt 2385 from 133 to 112 bytes. (Contributed by BJ, 6-Oct-2018.) |
⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → ∃𝑥𝜑) | ||
Theorem | bj-spimt2 35658 | A step in the proof of spimt 2385. (Contributed by BJ, 2-May-2019.) |
⊢ (∀𝑥(𝑥 = 𝑦 → (𝜑 → 𝜓)) → ((∃𝑥𝜓 → 𝜓) → (∀𝑥𝜑 → 𝜓))) | ||
Theorem | bj-cbv3ta 35659 | Closed form of cbv3 2396. (Contributed by BJ, 2-May-2019.) |
⊢ (∀𝑥∀𝑦(𝑥 = 𝑦 → (𝜑 → 𝜓)) → ((∀𝑦(∃𝑥𝜓 → 𝜓) ∧ ∀𝑥(𝜑 → ∀𝑦𝜑)) → (∀𝑥𝜑 → ∀𝑦𝜓))) | ||
Theorem | bj-cbv3tb 35660 | Closed form of cbv3 2396. (Contributed by BJ, 2-May-2019.) |
⊢ (∀𝑥∀𝑦(𝑥 = 𝑦 → (𝜑 → 𝜓)) → ((∀𝑦Ⅎ𝑥𝜓 ∧ ∀𝑥Ⅎ𝑦𝜑) → (∀𝑥𝜑 → ∀𝑦𝜓))) | ||
Theorem | bj-hbsb3t 35661 | A theorem close to a closed form of hbsb3 2486. (Contributed by BJ, 2-May-2019.) |
⊢ (∀𝑥(𝜑 → ∀𝑦𝜑) → ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑)) | ||
Theorem | bj-hbsb3 35662 | Shorter proof of hbsb3 2486. (Contributed by BJ, 2-May-2019.) (Proof modification is discouraged.) |
⊢ (𝜑 → ∀𝑦𝜑) ⇒ ⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑) | ||
Theorem | bj-nfs1t 35663 | A theorem close to a closed form of nfs1 2487. (Contributed by BJ, 2-May-2019.) |
⊢ (∀𝑥(𝜑 → ∀𝑦𝜑) → Ⅎ𝑥[𝑦 / 𝑥]𝜑) | ||
Theorem | bj-nfs1t2 35664 | A theorem close to a closed form of nfs1 2487. (Contributed by BJ, 2-May-2019.) |
⊢ (∀𝑥Ⅎ𝑦𝜑 → Ⅎ𝑥[𝑦 / 𝑥]𝜑) | ||
Theorem | bj-nfs1 35665 | Shorter proof of nfs1 2487 (three essential steps instead of four). (Contributed by BJ, 2-May-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ Ⅎ𝑥[𝑦 / 𝑥]𝜑 | ||
It is known that ax-13 2371 is logically redundant (see ax13w 2132 and the head comment of the section "Logical redundancy of ax-10--13"). More precisely, one can remove dependency on ax-13 2371 from every theorem in set.mm which is totally unbundled (i.e., has disjoint variable conditions on all setvar variables). Indeed, start with the existing proof, and replace any occurrence of ax-13 2371 with ax13w 2132. This section is an experiment to see in practice if (partially) unbundled versions of existing theorems can be proved more efficiently without ax-13 2371 (and using ax6v 1972 / ax6ev 1973 instead of ax-6 1971 / ax6e 2382, as is currently done). One reason to be optimistic is that the first few utility theorems using ax-13 2371 (roughly 200 of them) are then used mainly with dummy variables, which one can assume distinct from any other, so that the unbundled versions of the utility theorems suffice. In this section, we prove versions of theorems in the main part with dv conditions and not requiring ax-13 2371, labeled bj-xxxv (we follow the proof of xxx but use ax6v 1972 and ax6ev 1973 instead of ax-6 1971 and ax6e 2382, and ax-5 1913 instead of ax13v 2372; shorter proofs may be possible). When no additional dv condition is required, we label it bj-xxx. It is important to keep all the bundled theorems already in set.mm, but one may also add the (partially) unbundled versions which dipense with ax-13 2371, so as to remove dependencies on ax-13 2371 from many existing theorems. UPDATE: it turns out that several theorems of the form bj-xxxv, or minor variations, are already in set.mm with label xxxw. It is also possible to remove dependencies on ax-11 2154, typically by replacing a nonfree hypothesis with a disjoint variable condition (see cbv3v2 2234 and following theorems). | ||
Theorem | bj-axc10v 35666* | Version of axc10 2384 with a disjoint variable condition, which does not require ax-13 2371. (Contributed by BJ, 14-Jun-2019.) (Proof modification is discouraged.) |
⊢ (∀𝑥(𝑥 = 𝑦 → ∀𝑥𝜑) → 𝜑) | ||
Theorem | bj-spimtv 35667* | Version of spimt 2385 with a disjoint variable condition, which does not require ax-13 2371. (Contributed by BJ, 14-Jun-2019.) (Proof modification is discouraged.) |
⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝑦 → (𝜑 → 𝜓))) → (∀𝑥𝜑 → 𝜓)) | ||
Theorem | bj-cbv3hv2 35668* | Version of cbv3h 2403 with two disjoint variable conditions, which does not require ax-11 2154 nor ax-13 2371. (Contributed by BJ, 24-Jun-2019.) (Proof modification is discouraged.) |
⊢ (𝜓 → ∀𝑥𝜓) & ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) ⇒ ⊢ (∀𝑥𝜑 → ∀𝑦𝜓) | ||
Theorem | bj-cbv1hv 35669* | Version of cbv1h 2404 with a disjoint variable condition, which does not require ax-13 2371. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.) |
⊢ (𝜑 → (𝜓 → ∀𝑦𝜓)) & ⊢ (𝜑 → (𝜒 → ∀𝑥𝜒)) & ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 → 𝜒))) ⇒ ⊢ (∀𝑥∀𝑦𝜑 → (∀𝑥𝜓 → ∀𝑦𝜒)) | ||
Theorem | bj-cbv2hv 35670* | Version of cbv2h 2405 with a disjoint variable condition, which does not require ax-13 2371. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.) |
⊢ (𝜑 → (𝜓 → ∀𝑦𝜓)) & ⊢ (𝜑 → (𝜒 → ∀𝑥𝜒)) & ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))) ⇒ ⊢ (∀𝑥∀𝑦𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒)) | ||
Theorem | bj-cbv2v 35671* | Version of cbv2 2402 with a disjoint variable condition, which does not require ax-13 2371. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑦𝜓) & ⊢ (𝜑 → Ⅎ𝑥𝜒) & ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))) ⇒ ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒)) | ||
Theorem | bj-cbvaldv 35672* | Version of cbvald 2406 with a disjoint variable condition, which does not require ax-13 2371. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑦𝜓) & ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))) ⇒ ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒)) | ||
Theorem | bj-cbvexdv 35673* | Version of cbvexd 2407 with a disjoint variable condition, which does not require ax-13 2371. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑦𝜓) & ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))) ⇒ ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑦𝜒)) | ||
Theorem | bj-cbval2vv 35674* | Version of cbval2vv 2412 with a disjoint variable condition, which does not require ax-13 2371. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.) |
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑧∀𝑤𝜓) | ||
Theorem | bj-cbvex2vv 35675* | Version of cbvex2vv 2413 with a disjoint variable condition, which does not require ax-13 2371. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.) |
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑧∃𝑤𝜓) | ||
Theorem | bj-cbvaldvav 35676* | Version of cbvaldva 2408 with a disjoint variable condition, which does not require ax-13 2371. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.) |
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒)) | ||
Theorem | bj-cbvexdvav 35677* | Version of cbvexdva 2409 with a disjoint variable condition, which does not require ax-13 2371. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.) |
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑦𝜒)) | ||
Theorem | bj-cbvex4vv 35678* | Version of cbvex4v 2414 with a disjoint variable condition, which does not require ax-13 2371. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.) |
⊢ ((𝑥 = 𝑣 ∧ 𝑦 = 𝑢) → (𝜑 ↔ 𝜓)) & ⊢ ((𝑧 = 𝑓 ∧ 𝑤 = 𝑔) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (∃𝑥∃𝑦∃𝑧∃𝑤𝜑 ↔ ∃𝑣∃𝑢∃𝑓∃𝑔𝜒) | ||
Theorem | bj-equsalhv 35679* |
Version of equsalh 2419 with a disjoint variable condition, which
does not
require ax-13 2371. Remark: this is the same as equsalhw 2287. TODO:
delete after moving the following paragraph somewhere.
Remarks: equsexvw 2008 has been moved to Main; Theorem ax13lem2 2375 has a DV version which is a simple consequence of ax5e 1915; Theorems nfeqf2 2376, dveeq2 2377, nfeqf1 2378, dveeq1 2379, nfeqf 2380, axc9 2381, ax13 2374, have dv versions which are simple consequences of ax-5 1913. (Contributed by BJ, 14-Jun-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜓 → ∀𝑥𝜓) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜓) | ||
Theorem | bj-axc11nv 35680* | Version of axc11n 2425 with a disjoint variable condition; instance of aevlem 2058. TODO: delete after checking surrounding theorems. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥) | ||
Theorem | bj-aecomsv 35681* | Version of aecoms 2427 with a disjoint variable condition, provable from Tarski's FOL. The corresponding version of naecoms 2428 should not be very useful since ¬ ∀𝑥𝑥 = 𝑦, DV (𝑥, 𝑦) is true when the universe has at least two objects (see dtru 5436). (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → 𝜑) ⇒ ⊢ (∀𝑦 𝑦 = 𝑥 → 𝜑) | ||
Theorem | bj-axc11v 35682* | Version of axc11 2429 with a disjoint variable condition, which does not require ax-13 2371 nor ax-10 2137. Remark: the following theorems (hbae 2430, nfae 2432, hbnae 2431, nfnae 2433, hbnaes 2434) would need to be totally unbundled to be proved without ax-13 2371, hence would be simple consequences of ax-5 1913 or nfv 1917. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 → ∀𝑦𝜑)) | ||
Theorem | bj-drnf2v 35683* | Version of drnf2 2443 with a disjoint variable condition, which does not require ax-10 2137, ax-11 2154, ax-12 2171, ax-13 2371. Instance of nfbidv 1925. Note that the version of axc15 2421 with a disjoint variable condition is actually ax12v2 2173 (up to adding a superfluous antecedent). (Contributed by BJ, 17-Jun-2019.) (Proof modification is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 𝑥 = 𝑦 → (Ⅎ𝑧𝜑 ↔ Ⅎ𝑧𝜓)) | ||
Theorem | bj-equs45fv 35684* | Version of equs45f 2458 with a disjoint variable condition, which does not require ax-13 2371. Note that the version of equs5 2459 with a disjoint variable condition is actually sbalex 2235 (up to adding a superfluous antecedent). (Contributed by BJ, 11-Sep-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑)) | ||
Theorem | bj-hbs1 35685* | Version of hbsb2 2481 with a disjoint variable condition, which does not require ax-13 2371, and removal of ax-13 2371 from hbs1 2265. (Contributed by BJ, 23-Jun-2019.) (Proof modification is discouraged.) |
⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑) | ||
Theorem | bj-nfs1v 35686* | Version of nfsb2 2482 with a disjoint variable condition, which does not require ax-13 2371, and removal of ax-13 2371 from nfs1v 2153. (Contributed by BJ, 24-Jun-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥[𝑦 / 𝑥]𝜑 | ||
Theorem | bj-hbsb2av 35687* | Version of hbsb2a 2483 with a disjoint variable condition, which does not require ax-13 2371. (Contributed by BJ, 11-Sep-2019.) (Proof modification is discouraged.) |
⊢ ([𝑦 / 𝑥]∀𝑦𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑) | ||
Theorem | bj-hbsb3v 35688* | Version of hbsb3 2486 with a disjoint variable condition, which does not require ax-13 2371. (Remark: the unbundled version of nfs1 2487 is given by bj-nfs1v 35686.) (Contributed by BJ, 11-Sep-2019.) (Proof modification is discouraged.) |
⊢ (𝜑 → ∀𝑦𝜑) ⇒ ⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑) | ||
Theorem | bj-nfsab1 35689* | Remove dependency on ax-13 2371 from nfsab1 2717. UPDATE / TODO: nfsab1 2717 does not use ax-13 2371 either anymore; bj-nfsab1 35689 is shorter than nfsab1 2717 but uses ax-12 2171. (Contributed by BJ, 23-Jun-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥 𝑦 ∈ {𝑥 ∣ 𝜑} | ||
Theorem | bj-dtrucor2v 35690* | Version of dtrucor2 5370 with a disjoint variable condition, which does not require ax-13 2371 (nor ax-4 1811, ax-5 1913, ax-7 2011, ax-12 2171). (Contributed by BJ, 16-Jul-2019.) (Proof modification is discouraged.) |
⊢ (𝑥 = 𝑦 → 𝑥 ≠ 𝑦) ⇒ ⊢ (𝜑 ∧ ¬ 𝜑) | ||
The closed formula ∀𝑥∀𝑦𝑥 = 𝑦 approximately means that the var metavariables 𝑥 and 𝑦 represent the same variable vi. In a domain with at most one object, however, this formula is always true, hence the "approximately" in the previous sentence. | ||
Theorem | bj-hbaeb2 35691 | Biconditional version of a form of hbae 2430 with commuted quantifiers, not requiring ax-11 2154. (Contributed by BJ, 12-Dec-2019.) (Proof modification is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 ↔ ∀𝑥∀𝑧 𝑥 = 𝑦) | ||
Theorem | bj-hbaeb 35692 | Biconditional version of hbae 2430. (Contributed by BJ, 6-Oct-2018.) (Proof modification is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 ↔ ∀𝑧∀𝑥 𝑥 = 𝑦) | ||
Theorem | bj-hbnaeb 35693 | Biconditional version of hbnae 2431 (to replace it?). (Contributed by BJ, 6-Oct-2018.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 ↔ ∀𝑧 ¬ ∀𝑥 𝑥 = 𝑦) | ||
Theorem | bj-dvv 35694 | A special instance of bj-hbaeb2 35691. A lemma for distinct var metavariables. Note that the right-hand side is a closed formula (a sentence). (Contributed by BJ, 6-Oct-2018.) |
⊢ (∀𝑥 𝑥 = 𝑦 ↔ ∀𝑥∀𝑦 𝑥 = 𝑦) | ||
As a rule of thumb, if a theorem of the form ⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (𝜒 ↔ 𝜃) is in the database, and the "more precise" theorems ⊢ (𝜑 → 𝜓) ⇒ ⊢ (𝜒 → 𝜃) and ⊢ (𝜓 → 𝜑) ⇒ ⊢ (𝜃 → 𝜒) also hold (see bj-bisym 35463), then they should be added to the database. The present case is similar. Similar additions can be done regarding equsex 2417 (and equsalh 2419 and equsexh 2420). Even if only one of these two theorems holds, it should be added to the database. | ||
Theorem | bj-equsal1t 35695 | Duplication of wl-equsal1t 36405, with shorter proof. If one imposes a disjoint variable condition on x,y , then one can use alequexv 2004 and reduce axiom dependencies, and similarly for the following theorems. Note: wl-equsalcom 36406 is also interesting. (Contributed by BJ, 6-Oct-2018.) |
⊢ (Ⅎ𝑥𝜑 → (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜑)) | ||
Theorem | bj-equsal1ti 35696 | Inference associated with bj-equsal1t 35695. (Contributed by BJ, 30-Sep-2018.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜑) | ||
Theorem | bj-equsal1 35697 | One direction of equsal 2416. (Contributed by BJ, 30-Sep-2018.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) ⇒ ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → 𝜓) | ||
Theorem | bj-equsal2 35698 | One direction of equsal 2416. (Contributed by BJ, 30-Sep-2018.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) ⇒ ⊢ (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜓)) | ||
Theorem | bj-equsal 35699 | Shorter proof of equsal 2416. (Contributed by BJ, 30-Sep-2018.) Proof modification is discouraged to avoid using equsal 2416, but "min */exc equsal" is ok. (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜓) | ||
References are made to the second edition (1927, reprinted 1963) of Principia Mathematica, Vol. 1. Theorems are referred to in the form "PM*xx.xx". | ||
Theorem | stdpc5t 35700 | Closed form of stdpc5 2201. (Possible to place it before 19.21t 2199 and use it to prove 19.21t 2199). (Contributed by BJ, 15-Sep-2018.) (Proof modification is discouraged.) |
⊢ (Ⅎ𝑥𝜑 → (∀𝑥(𝜑 → 𝜓) → (𝜑 → ∀𝑥𝜓))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |