Home | Metamath
Proof Explorer Theorem List (p. 347 of 462) | < 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-28971) |
Hilbert Space Explorer
(28972-30494) |
Users' Mathboxes
(30495-46134) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | bj-nnfbi 34601 | If two formulas are equivalent for all 𝑥, then nonfreeness of 𝑥 in one of them is equivalent to nonfreeness in the other. Compare nfbiit 1858. From this and bj-nnfim 34622 and bj-nnfnt 34616, 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 34617) in order not to require sp 2180 (modal T). (Contributed by BJ, 27-Aug-2023.) |
⊢ (((𝜑 ↔ 𝜓) ∧ ∀𝑥(𝜑 ↔ 𝜓)) → (Ⅎ'𝑥𝜑 ↔ Ⅎ'𝑥𝜓)) | ||
Theorem | bj-nnfbd 34602* | 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 34601. (Contributed by BJ, 27-Aug-2023.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (Ⅎ'𝑥𝜓 ↔ Ⅎ'𝑥𝜒)) | ||
Theorem | bj-nnfbii 34603 | 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 34601. (Contributed by BJ, 18-Nov-2023.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (Ⅎ'𝑥𝜑 ↔ Ⅎ'𝑥𝜓) | ||
Theorem | bj-nnfa 34604 | Nonfreeness implies the equivalent of ax-5 1918. See nf5r 2191. (Contributed by BJ, 28-Jul-2023.) |
⊢ (Ⅎ'𝑥𝜑 → (𝜑 → ∀𝑥𝜑)) | ||
Theorem | bj-nnfad 34605 | Nonfreeness implies the equivalent of ax-5 1918, deduction form. See nf5rd 2194. (Contributed by BJ, 2-Dec-2023.) |
⊢ (𝜑 → Ⅎ'𝑥𝜓) ⇒ ⊢ (𝜑 → (𝜓 → ∀𝑥𝜓)) | ||
Theorem | bj-nnfai 34606 | Nonfreeness implies the equivalent of ax-5 1918, inference form. See nf5ri 2193. (Contributed by BJ, 22-Sep-2024.) |
⊢ Ⅎ'𝑥𝜑 ⇒ ⊢ (𝜑 → ∀𝑥𝜑) | ||
Theorem | bj-nnfe 34607 | Nonfreeness implies the equivalent of ax5e 1920. (Contributed by BJ, 28-Jul-2023.) |
⊢ (Ⅎ'𝑥𝜑 → (∃𝑥𝜑 → 𝜑)) | ||
Theorem | bj-nnfed 34608 | Nonfreeness implies the equivalent of ax5e 1920, deduction form. (Contributed by BJ, 2-Dec-2023.) |
⊢ (𝜑 → Ⅎ'𝑥𝜓) ⇒ ⊢ (𝜑 → (∃𝑥𝜓 → 𝜓)) | ||
Theorem | bj-nnfei 34609 | Nonfreeness implies the equivalent of ax5e 1920, inference form. (Contributed by BJ, 22-Sep-2024.) |
⊢ Ⅎ'𝑥𝜑 ⇒ ⊢ (∃𝑥𝜑 → 𝜑) | ||
Theorem | bj-nnfea 34610 | Nonfreeness implies the equivalent of ax5ea 1921. (Contributed by BJ, 28-Jul-2023.) |
⊢ (Ⅎ'𝑥𝜑 → (∃𝑥𝜑 → ∀𝑥𝜑)) | ||
Theorem | bj-nnfead 34611 | Nonfreeness implies the equivalent of ax5ea 1921, deduction form. (Contributed by BJ, 2-Dec-2023.) |
⊢ (𝜑 → Ⅎ'𝑥𝜓) ⇒ ⊢ (𝜑 → (∃𝑥𝜓 → ∀𝑥𝜓)) | ||
Theorem | bj-nnfeai 34612 | Nonfreeness implies the equivalent of ax5ea 1921, inference form. (Contributed by BJ, 22-Sep-2024.) |
⊢ Ⅎ'𝑥𝜑 ⇒ ⊢ (∃𝑥𝜑 → ∀𝑥𝜑) | ||
Theorem | bj-dfnnf2 34613 | Alternate definition of df-bj-nnf 34600 using only primitive symbols (→, ¬, ∀) in each conjunct. (Contributed by BJ, 20-Aug-2023.) |
⊢ (Ⅎ'𝑥𝜑 ↔ ((𝜑 → ∀𝑥𝜑) ∧ (¬ 𝜑 → ∀𝑥 ¬ 𝜑))) | ||
Theorem | bj-nnfnfTEMP 34614 | 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 1792 except via df-nf 1792 directly. (Proof modification is discouraged.) |
⊢ (Ⅎ'𝑥𝜑 → Ⅎ𝑥𝜑) | ||
Theorem | bj-wnfnf 34615 | When 𝜑 is substituted for 𝜓, this statement expresses nonfreeness in the weak form of nonfreeness (∃ → ∀). Note that this could also be proved from bj-nnfim 34622, bj-nnfe1 34636 and bj-nnfa1 34635. (Contributed by BJ, 9-Dec-2023.) |
⊢ Ⅎ'𝑥(∃𝑥𝜑 → ∀𝑥𝜓) | ||
Theorem | bj-nnfnt 34616 | 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 34622). Intuitionistically, ⊢ (Ⅎ'𝑥¬ 𝜑 ↔ Ⅎ'𝑥¬ ¬ 𝜑). See nfnt 1864. (Contributed by BJ, 28-Jul-2023.) |
⊢ (Ⅎ'𝑥𝜑 ↔ Ⅎ'𝑥 ¬ 𝜑) | ||
Theorem | bj-nnftht 34617 | A variable is nonfree in a theorem. The antecedent is in the "strong necessity" modality of modal logic in order not to require sp 2180 (modal T), as in bj-nnfbi 34601. (Contributed by BJ, 28-Jul-2023.) |
⊢ ((𝜑 ∧ ∀𝑥𝜑) → Ⅎ'𝑥𝜑) | ||
Theorem | bj-nnfth 34618 | A variable is nonfree in a theorem, inference form. (Contributed by BJ, 28-Jul-2023.) |
⊢ 𝜑 ⇒ ⊢ Ⅎ'𝑥𝜑 | ||
Theorem | bj-nnfnth 34619 | A variable is nonfree in the negation of a theorem, inference form. (Contributed by BJ, 27-Aug-2023.) |
⊢ ¬ 𝜑 ⇒ ⊢ Ⅎ'𝑥𝜑 | ||
Theorem | bj-nnfim1 34620 | A consequence of nonfreeness in the antecedent and the consequent of an implication. (Contributed by BJ, 27-Aug-2023.) |
⊢ ((Ⅎ'𝑥𝜑 ∧ Ⅎ'𝑥𝜓) → ((𝜑 → 𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓))) | ||
Theorem | bj-nnfim2 34621 | A consequence of nonfreeness in the antecedent and the consequent of an implication. (Contributed by BJ, 27-Aug-2023.) |
⊢ ((Ⅎ'𝑥𝜑 ∧ Ⅎ'𝑥𝜓) → ((∀𝑥𝜑 → ∃𝑥𝜓) → (𝜑 → 𝜓))) | ||
Theorem | bj-nnfim 34622 | Nonfreeness in the antecedent and the consequent of an implication implies nonfreeness in the implication. (Contributed by BJ, 27-Aug-2023.) |
⊢ ((Ⅎ'𝑥𝜑 ∧ Ⅎ'𝑥𝜓) → Ⅎ'𝑥(𝜑 → 𝜓)) | ||
Theorem | bj-nnfimd 34623 | 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 34624 | 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 34622, bj-nnfnt 34616 and bj-nnfbi 34601, but we want a proof valid in intuitionistic logic. (Proof modification is discouraged.) |
⊢ ((Ⅎ'𝑥𝜑 ∧ Ⅎ'𝑥𝜓) → Ⅎ'𝑥(𝜑 ∧ 𝜓)) | ||
Theorem | bj-nnfand 34625 | Nonfreeness in both conjuncts implies nonfreeness in the conjunction, deduction form. Note: compared with the proof of bj-nnfan 34624, 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 34624 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 34625 will generally be easier to understand). (Contributed by BJ, 19-Nov-2023.) (Proof modification is discouraged.) |
⊢ (𝜑 → Ⅎ'𝑥𝜓) & ⊢ (𝜑 → Ⅎ'𝑥𝜒) ⇒ ⊢ (𝜑 → Ⅎ'𝑥(𝜓 ∧ 𝜒)) | ||
Theorem | bj-nnfor 34626 | 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 34622, bj-nnfnt 34616 and bj-nnfbi 34601, but we want a proof valid in intuitionistic logic. (Proof modification is discouraged.) |
⊢ ((Ⅎ'𝑥𝜑 ∧ Ⅎ'𝑥𝜓) → Ⅎ'𝑥(𝜑 ∨ 𝜓)) | ||
Theorem | bj-nnford 34627 | Nonfreeness in both disjuncts implies nonfreeness in the disjunction, deduction form. See comments for bj-nnfor 34626 and bj-nnfand 34625. (Contributed by BJ, 2-Dec-2023.) (Proof modification is discouraged.) |
⊢ (𝜑 → Ⅎ'𝑥𝜓) & ⊢ (𝜑 → Ⅎ'𝑥𝜒) ⇒ ⊢ (𝜑 → Ⅎ'𝑥(𝜓 ∨ 𝜒)) | ||
Theorem | bj-nnfbit 34628 | Nonfreeness in both sides implies nonfreeness in the biconditional. (Contributed by BJ, 2-Dec-2023.) (Proof modification is discouraged.) |
⊢ ((Ⅎ'𝑥𝜑 ∧ Ⅎ'𝑥𝜓) → Ⅎ'𝑥(𝜑 ↔ 𝜓)) | ||
Theorem | bj-nnfbid 34629 | Nonfreeness in both sides implies nonfreeness in the biconditional, deduction form. (Contributed by BJ, 2-Dec-2023.) (Proof modification is discouraged.) |
⊢ (𝜑 → Ⅎ'𝑥𝜓) & ⊢ (𝜑 → Ⅎ'𝑥𝜒) ⇒ ⊢ (𝜑 → Ⅎ'𝑥(𝜓 ↔ 𝜒)) | ||
Theorem | bj-nnfv 34630* | A non-occurring variable is nonfree in a formula. (Contributed by BJ, 28-Jul-2023.) |
⊢ Ⅎ'𝑥𝜑 | ||
Theorem | bj-nnf-alrim 34631 | Proof of the closed form of alrimi 2211 from modalK (compare alrimiv 1935). See also bj-alrim 34569. Actually, most proofs between 19.3t 2199 and 2sbbid 2244 could be proved without ax-12 2175. (Contributed by BJ, 20-Aug-2023.) |
⊢ (Ⅎ'𝑥𝜑 → (∀𝑥(𝜑 → 𝜓) → (𝜑 → ∀𝑥𝜓))) | ||
Theorem | bj-nnf-exlim 34632 | Proof of the closed form of exlimi 2215 from modalK (compare exlimiv 1938). See also bj-sylget2 34497. (Contributed by BJ, 2-Dec-2023.) |
⊢ (Ⅎ'𝑥𝜓 → (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → 𝜓))) | ||
Theorem | bj-dfnnf3 34633 | Alternate definition of nonfreeness when sp 2180 is available. (Contributed by BJ, 28-Jul-2023.) The proof should not rely on df-nf 1792. (Proof modification is discouraged.) |
⊢ (Ⅎ'𝑥𝜑 ↔ (∃𝑥𝜑 → ∀𝑥𝜑)) | ||
Theorem | bj-nfnnfTEMP 34634 | New nonfreeness is equivalent to old nonfreeness on core FOL axioms plus sp 2180. (Contributed by BJ, 28-Jul-2023.) The proof should not rely on df-nf 1792 except via df-nf 1792 directly. (Proof modification is discouraged.) |
⊢ (Ⅎ'𝑥𝜑 ↔ Ⅎ𝑥𝜑) | ||
Theorem | bj-nnfa1 34635 | See nfa1 2152. (Contributed by BJ, 12-Aug-2023.) (Proof modification is discouraged.) |
⊢ Ⅎ'𝑥∀𝑥𝜑 | ||
Theorem | bj-nnfe1 34636 | See nfe1 2151. (Contributed by BJ, 12-Aug-2023.) (Proof modification is discouraged.) |
⊢ Ⅎ'𝑥∃𝑥𝜑 | ||
Theorem | bj-19.12 34637 | See 19.12 2326. Could be labeled "exalimalex" for "'there exists for all' implies 'for all there exists'". This proof is from excom 2166 and modal (B) on top of modalK logic. (Contributed by BJ, 12-Aug-2023.) The proof should not rely on df-nf 1792 or df-bj-nnf 34600, directly or indirectly. (Proof modification is discouraged.) |
⊢ (∃𝑥∀𝑦𝜑 → ∀𝑦∃𝑥𝜑) | ||
Theorem | bj-nnflemaa 34638 | One of four lemmas for nonfreeness: antecedent and consequent both expressed using universal quantifier. Note: this is bj-hbalt 34557. (Contributed by BJ, 12-Aug-2023.) (Proof modification is discouraged.) |
⊢ (∀𝑥(𝜑 → ∀𝑦𝜑) → (∀𝑥𝜑 → ∀𝑦∀𝑥𝜑)) | ||
Theorem | bj-nnflemee 34639 | 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 34640 | 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 34641 | 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 34642 | See nfal 2322 and bj-nfalt 34587. (Contributed by BJ, 12-Aug-2023.) (Proof modification is discouraged.) |
⊢ (∀𝑥Ⅎ'𝑦𝜑 → Ⅎ'𝑦∀𝑥𝜑) | ||
Theorem | bj-nnfext 34643 | See nfex 2323 and bj-nfext 34588. (Contributed by BJ, 12-Aug-2023.) (Proof modification is discouraged.) |
⊢ (∀𝑥Ⅎ'𝑦𝜑 → Ⅎ'𝑦∃𝑥𝜑) | ||
Theorem | bj-stdpc5t 34644 | Alias of bj-nnf-alrim 34631 for labeling consistency (a standard predicate calculus axiom). Closed form of stdpc5 2206 proved from modalK (obsoleting stdpc5v 1946). (Contributed by BJ, 2-Dec-2023.) Use bj-nnf-alrim 34631 instead. (New usaged is discouraged.) |
⊢ (Ⅎ'𝑥𝜑 → (∀𝑥(𝜑 → 𝜓) → (𝜑 → ∀𝑥𝜓))) | ||
Theorem | bj-19.21t 34645 | Statement 19.21t 2204 proved from modalK (obsoleting 19.21v 1947). (Contributed by BJ, 2-Dec-2023.) |
⊢ (Ⅎ'𝑥𝜑 → (∀𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥𝜓))) | ||
Theorem | bj-19.23t 34646 | Statement 19.23t 2208 proved from modalK (obsoleting 19.23v 1950). (Contributed by BJ, 2-Dec-2023.) |
⊢ (Ⅎ'𝑥𝜓 → (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜓))) | ||
Theorem | bj-19.36im 34647 | One direction of 19.36 2228 from the same axioms as 19.36imv 1953. (Contributed by BJ, 2-Dec-2023.) |
⊢ (Ⅎ'𝑥𝜓 → (∃𝑥(𝜑 → 𝜓) → (∀𝑥𝜑 → 𝜓))) | ||
Theorem | bj-19.37im 34648 | One direction of 19.37 2230 from the same axioms as 19.37imv 1956. (Contributed by BJ, 2-Dec-2023.) |
⊢ (Ⅎ'𝑥𝜑 → (∃𝑥(𝜑 → 𝜓) → (𝜑 → ∃𝑥𝜓))) | ||
Theorem | bj-19.42t 34649 | Closed form of 19.42 2234 from the same axioms as 19.42v 1962. (Contributed by BJ, 2-Dec-2023.) |
⊢ (Ⅎ'𝑥𝜑 → (∃𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥𝜓))) | ||
Theorem | bj-19.41t 34650 | Closed form of 19.41 2233 from the same axioms as 19.41v 1958. The same is doable with 19.27 2225, 19.28 2226, 19.31 2232, 19.32 2231, 19.44 2235, 19.45 2236. (Contributed by BJ, 2-Dec-2023.) |
⊢ (Ⅎ'𝑥𝜓 → (∃𝑥(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ 𝜓))) | ||
Theorem | bj-sbft 34651 | Version of sbft 2266 using Ⅎ', proved from core axioms. (Contributed by BJ, 19-Nov-2023.) |
⊢ (Ⅎ'𝑥𝜑 → ([𝑡 / 𝑥]𝜑 ↔ 𝜑)) | ||
Theorem | bj-pm11.53vw 34652 | Version of pm11.53v 1952 with nonfreeness antecedents. One can also prove the theorem with antecedent (Ⅎ'𝑦∀𝑥𝜑 ∧ ∀𝑦Ⅎ'𝑥𝜓). (Contributed by BJ, 7-Oct-2024.) |
⊢ ((∀𝑥Ⅎ'𝑦𝜑 ∧ Ⅎ'𝑥∀𝑦𝜓) → (∀𝑥∀𝑦(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → ∀𝑦𝜓))) | ||
Theorem | bj-pm11.53v 34653 | Version of pm11.53v 1952 with nonfreeness antecedents. (Contributed by BJ, 7-Oct-2024.) |
⊢ ((∀𝑥Ⅎ'𝑦𝜑 ∧ ∀𝑦Ⅎ'𝑥𝜓) → (∀𝑥∀𝑦(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → ∀𝑦𝜓))) | ||
Theorem | bj-pm11.53a 34654* | A variant of pm11.53v 1952. One can similarly prove a variant with DV (𝑦, 𝜑) and ∀𝑦Ⅎ'𝑥𝜓 instead of DV (𝑥, 𝜓) and ∀𝑥Ⅎ'𝑦𝜑. (Contributed by BJ, 7-Oct-2024.) |
⊢ (∀𝑥Ⅎ'𝑦𝜑 → (∀𝑥∀𝑦(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → ∀𝑦𝜓))) | ||
Theorem | bj-equsvt 34655* | A variant of equsv 2011. (Contributed by BJ, 7-Oct-2024.) |
⊢ (Ⅎ'𝑥𝜑 → (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜑)) | ||
Theorem | bj-equsalvwd 34656* | Variant of equsalvw 2012. (Contributed by BJ, 7-Oct-2024.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜑 → Ⅎ'𝑥𝜒) & ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥(𝑥 = 𝑦 → 𝜓) ↔ 𝜒)) | ||
Theorem | bj-equsexvwd 34657* | Variant of equsexvw 2013. (Contributed by BJ, 7-Oct-2024.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜑 → Ⅎ'𝑥𝜒) & ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥(𝑥 = 𝑦 ∧ 𝜓) ↔ 𝜒)) | ||
Theorem | bj-sbievwd 34658* | Variant of sbievw 2099. (Contributed by BJ, 7-Oct-2024.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜑 → Ⅎ'𝑥𝜒) & ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ([𝑦 / 𝑥]𝜓 ↔ 𝜒)) | ||
Theorem | bj-axc10 34659 | Alternate proof of axc10 2382. Shorter. One can prove a version with DV (𝑥, 𝑦) without ax-13 2369, by using ax6ev 1978 instead of ax6e 2380. (Contributed by BJ, 31-Mar-2021.) (Proof modification is discouraged.) |
⊢ (∀𝑥(𝑥 = 𝑦 → ∀𝑥𝜑) → 𝜑) | ||
Theorem | bj-alequex 34660 | A fol lemma. See alequexv 2009 for a version with a disjoint variable condition requiring fewer axioms. Can be used to reduce the proof of spimt 2383 from 133 to 112 bytes. (Contributed by BJ, 6-Oct-2018.) |
⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → ∃𝑥𝜑) | ||
Theorem | bj-spimt2 34661 | A step in the proof of spimt 2383. (Contributed by BJ, 2-May-2019.) |
⊢ (∀𝑥(𝑥 = 𝑦 → (𝜑 → 𝜓)) → ((∃𝑥𝜓 → 𝜓) → (∀𝑥𝜑 → 𝜓))) | ||
Theorem | bj-cbv3ta 34662 | Closed form of cbv3 2394. (Contributed by BJ, 2-May-2019.) |
⊢ (∀𝑥∀𝑦(𝑥 = 𝑦 → (𝜑 → 𝜓)) → ((∀𝑦(∃𝑥𝜓 → 𝜓) ∧ ∀𝑥(𝜑 → ∀𝑦𝜑)) → (∀𝑥𝜑 → ∀𝑦𝜓))) | ||
Theorem | bj-cbv3tb 34663 | Closed form of cbv3 2394. (Contributed by BJ, 2-May-2019.) |
⊢ (∀𝑥∀𝑦(𝑥 = 𝑦 → (𝜑 → 𝜓)) → ((∀𝑦Ⅎ𝑥𝜓 ∧ ∀𝑥Ⅎ𝑦𝜑) → (∀𝑥𝜑 → ∀𝑦𝜓))) | ||
Theorem | bj-hbsb3t 34664 | A theorem close to a closed form of hbsb3 2488. (Contributed by BJ, 2-May-2019.) |
⊢ (∀𝑥(𝜑 → ∀𝑦𝜑) → ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑)) | ||
Theorem | bj-hbsb3 34665 | Shorter proof of hbsb3 2488. (Contributed by BJ, 2-May-2019.) (Proof modification is discouraged.) |
⊢ (𝜑 → ∀𝑦𝜑) ⇒ ⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑) | ||
Theorem | bj-nfs1t 34666 | A theorem close to a closed form of nfs1 2489. (Contributed by BJ, 2-May-2019.) |
⊢ (∀𝑥(𝜑 → ∀𝑦𝜑) → Ⅎ𝑥[𝑦 / 𝑥]𝜑) | ||
Theorem | bj-nfs1t2 34667 | A theorem close to a closed form of nfs1 2489. (Contributed by BJ, 2-May-2019.) |
⊢ (∀𝑥Ⅎ𝑦𝜑 → Ⅎ𝑥[𝑦 / 𝑥]𝜑) | ||
Theorem | bj-nfs1 34668 | Shorter proof of nfs1 2489 (three essential steps instead of four). (Contributed by BJ, 2-May-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ Ⅎ𝑥[𝑦 / 𝑥]𝜑 | ||
It is known that ax-13 2369 is logically redundant (see ax13w 2136 and the head comment of the section "Logical redundancy of ax-10--13"). More precisely, one can remove dependency on ax-13 2369 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 2369 with ax13w 2136. This section is an experiment to see in practice if (partially) unbundled versions of existing theorems can be proved more efficiently without ax-13 2369 (and using ax6v 1977 / ax6ev 1978 instead of ax-6 1976 / ax6e 2380, as is currently done). One reason to be optimistic is that the first few utility theorems using ax-13 2369 (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 2369, labeled bj-xxxv (we follow the proof of xxx but use ax6v 1977 and ax6ev 1978 instead of ax-6 1976 and ax6e 2380, and ax-5 1918 instead of ax13v 2370; 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 2369, so as to remove dependencies on ax-13 2369 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 2158, typically by replacing a nonfree hypothesis with a disjoint variable condition (see cbv3v2 2239 and following theorems). | ||
Theorem | bj-axc10v 34669* | Version of axc10 2382 with a disjoint variable condition, which does not require ax-13 2369. (Contributed by BJ, 14-Jun-2019.) (Proof modification is discouraged.) |
⊢ (∀𝑥(𝑥 = 𝑦 → ∀𝑥𝜑) → 𝜑) | ||
Theorem | bj-spimtv 34670* | Version of spimt 2383 with a disjoint variable condition, which does not require ax-13 2369. (Contributed by BJ, 14-Jun-2019.) (Proof modification is discouraged.) |
⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝑦 → (𝜑 → 𝜓))) → (∀𝑥𝜑 → 𝜓)) | ||
Theorem | bj-cbv3hv2 34671* | Version of cbv3h 2401 with two disjoint variable conditions, which does not require ax-11 2158 nor ax-13 2369. (Contributed by BJ, 24-Jun-2019.) (Proof modification is discouraged.) |
⊢ (𝜓 → ∀𝑥𝜓) & ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) ⇒ ⊢ (∀𝑥𝜑 → ∀𝑦𝜓) | ||
Theorem | bj-cbv1hv 34672* | Version of cbv1h 2402 with a disjoint variable condition, which does not require ax-13 2369. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.) |
⊢ (𝜑 → (𝜓 → ∀𝑦𝜓)) & ⊢ (𝜑 → (𝜒 → ∀𝑥𝜒)) & ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 → 𝜒))) ⇒ ⊢ (∀𝑥∀𝑦𝜑 → (∀𝑥𝜓 → ∀𝑦𝜒)) | ||
Theorem | bj-cbv2hv 34673* | Version of cbv2h 2403 with a disjoint variable condition, which does not require ax-13 2369. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.) |
⊢ (𝜑 → (𝜓 → ∀𝑦𝜓)) & ⊢ (𝜑 → (𝜒 → ∀𝑥𝜒)) & ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))) ⇒ ⊢ (∀𝑥∀𝑦𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒)) | ||
Theorem | bj-cbv2v 34674* | Version of cbv2 2400 with a disjoint variable condition, which does not require ax-13 2369. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑦𝜓) & ⊢ (𝜑 → Ⅎ𝑥𝜒) & ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))) ⇒ ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒)) | ||
Theorem | bj-cbvaldv 34675* | Version of cbvald 2404 with a disjoint variable condition, which does not require ax-13 2369. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑦𝜓) & ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))) ⇒ ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒)) | ||
Theorem | bj-cbvexdv 34676* | Version of cbvexd 2405 with a disjoint variable condition, which does not require ax-13 2369. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑦𝜓) & ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))) ⇒ ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑦𝜒)) | ||
Theorem | bj-cbval2vv 34677* | Version of cbval2vv 2410 with a disjoint variable condition, which does not require ax-13 2369. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.) |
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑧∀𝑤𝜓) | ||
Theorem | bj-cbvex2vv 34678* | Version of cbvex2vv 2411 with a disjoint variable condition, which does not require ax-13 2369. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.) |
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑧∃𝑤𝜓) | ||
Theorem | bj-cbvaldvav 34679* | Version of cbvaldva 2406 with a disjoint variable condition, which does not require ax-13 2369. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.) |
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒)) | ||
Theorem | bj-cbvexdvav 34680* | Version of cbvexdva 2407 with a disjoint variable condition, which does not require ax-13 2369. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.) |
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑦𝜒)) | ||
Theorem | bj-cbvex4vv 34681* | Version of cbvex4v 2412 with a disjoint variable condition, which does not require ax-13 2369. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.) |
⊢ ((𝑥 = 𝑣 ∧ 𝑦 = 𝑢) → (𝜑 ↔ 𝜓)) & ⊢ ((𝑧 = 𝑓 ∧ 𝑤 = 𝑔) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (∃𝑥∃𝑦∃𝑧∃𝑤𝜑 ↔ ∃𝑣∃𝑢∃𝑓∃𝑔𝜒) | ||
Theorem | bj-equsalhv 34682* |
Version of equsalh 2417 with a disjoint variable condition, which
does not
require ax-13 2369. Remark: this is the same as equsalhw 2292. TODO:
delete after moving the following paragraph somewhere.
Remarks: equsexvw 2013 has been moved to Main; Theorem ax13lem2 2373 has a DV version which is a simple consequence of ax5e 1920; Theorems nfeqf2 2374, dveeq2 2375, nfeqf1 2376, dveeq1 2377, nfeqf 2378, axc9 2379, ax13 2372, have dv versions which are simple consequences of ax-5 1918. (Contributed by BJ, 14-Jun-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜓 → ∀𝑥𝜓) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜓) | ||
Theorem | bj-axc11nv 34683* | Version of axc11n 2423 with a disjoint variable condition; instance of aevlem 2061. TODO: delete after checking surrounding theorems. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥) | ||
Theorem | bj-aecomsv 34684* | Version of aecoms 2425 with a disjoint variable condition, provable from Tarski's FOL. The corresponding version of naecoms 2426 should not be very useful since ¬ ∀𝑥𝑥 = 𝑦, DV (𝑥, 𝑦) is true when the universe has at least two objects (see dtru 5252). (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → 𝜑) ⇒ ⊢ (∀𝑦 𝑦 = 𝑥 → 𝜑) | ||
Theorem | bj-axc11v 34685* | Version of axc11 2427 with a disjoint variable condition, which does not require ax-13 2369 nor ax-10 2141. Remark: the following theorems (hbae 2428, nfae 2430, hbnae 2429, nfnae 2431, hbnaes 2432) would need to be totally unbundled to be proved without ax-13 2369, hence would be simple consequences of ax-5 1918 or nfv 1922. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 → ∀𝑦𝜑)) | ||
Theorem | bj-drnf2v 34686* | Version of drnf2 2441 with a disjoint variable condition, which does not require ax-10 2141, ax-11 2158, ax-12 2175, ax-13 2369. Instance of nfbidv 1930. Note that the version of axc15 2419 with a disjoint variable condition is actually ax12v2 2177 (up to adding a superfluous antecedent). (Contributed by BJ, 17-Jun-2019.) (Proof modification is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 𝑥 = 𝑦 → (Ⅎ𝑧𝜑 ↔ Ⅎ𝑧𝜓)) | ||
Theorem | bj-equs45fv 34687* | Version of equs45f 2456 with a disjoint variable condition, which does not require ax-13 2369. Note that the version of equs5 2457 with a disjoint variable condition is actually sbalex 2240 (up to adding a superfluous antecedent). (Contributed by BJ, 11-Sep-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑)) | ||
Theorem | bj-hbs1 34688* | Version of hbsb2 2483 with a disjoint variable condition, which does not require ax-13 2369, and removal of ax-13 2369 from hbs1 2270. (Contributed by BJ, 23-Jun-2019.) (Proof modification is discouraged.) |
⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑) | ||
Theorem | bj-nfs1v 34689* | Version of nfsb2 2484 with a disjoint variable condition, which does not require ax-13 2369, and removal of ax-13 2369 from nfs1v 2157. (Contributed by BJ, 24-Jun-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥[𝑦 / 𝑥]𝜑 | ||
Theorem | bj-hbsb2av 34690* | Version of hbsb2a 2485 with a disjoint variable condition, which does not require ax-13 2369. (Contributed by BJ, 11-Sep-2019.) (Proof modification is discouraged.) |
⊢ ([𝑦 / 𝑥]∀𝑦𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑) | ||
Theorem | bj-hbsb3v 34691* | Version of hbsb3 2488 with a disjoint variable condition, which does not require ax-13 2369. (Remark: the unbundled version of nfs1 2489 is given by bj-nfs1v 34689.) (Contributed by BJ, 11-Sep-2019.) (Proof modification is discouraged.) |
⊢ (𝜑 → ∀𝑦𝜑) ⇒ ⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑) | ||
Theorem | bj-nfsab1 34692* | Remove dependency on ax-13 2369 from nfsab1 2721. UPDATE / TODO: nfsab1 2721 does not use ax-13 2369 either anymore; bj-nfsab1 34692 is shorter than nfsab1 2721 but uses ax-12 2175. (Contributed by BJ, 23-Jun-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥 𝑦 ∈ {𝑥 ∣ 𝜑} | ||
Theorem | bj-dtru 34693* |
Remove dependency on ax-13 2369 from dtru 5252. (Contributed by BJ,
31-May-2019.)
TODO: This predates the removal of ax-13 2369 in dtru 5252. But actually, sn-dtru 39862 is better than either, so move it to Main with sn-el 39861 (and determine whether bj-dtru 34693 should be kept as ALT or deleted). (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ¬ ∀𝑥 𝑥 = 𝑦 | ||
Theorem | bj-dtrucor2v 34694* | Version of dtrucor2 5254 with a disjoint variable condition, which does not require ax-13 2369 (nor ax-4 1817, ax-5 1918, ax-7 2016, ax-12 2175). (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 34695 | Biconditional version of a form of hbae 2428 with commuted quantifiers, not requiring ax-11 2158. (Contributed by BJ, 12-Dec-2019.) (Proof modification is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 ↔ ∀𝑥∀𝑧 𝑥 = 𝑦) | ||
Theorem | bj-hbaeb 34696 | Biconditional version of hbae 2428. (Contributed by BJ, 6-Oct-2018.) (Proof modification is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 ↔ ∀𝑧∀𝑥 𝑥 = 𝑦) | ||
Theorem | bj-hbnaeb 34697 | Biconditional version of hbnae 2429 (to replace it?). (Contributed by BJ, 6-Oct-2018.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 ↔ ∀𝑧 ¬ ∀𝑥 𝑥 = 𝑦) | ||
Theorem | bj-dvv 34698 | A special instance of bj-hbaeb2 34695. 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 34466), then they should be added to the database. The present case is similar. Similar additions can be done regarding equsex 2415 (and equsalh 2417 and equsexh 2418). Even if only one of these two theorems holds, it should be added to the database. | ||
Theorem | bj-equsal1t 34699 | Duplication of wl-equsal1t 35394, with shorter proof. If one imposes a disjoint variable condition on x,y , then one can use alequexv 2009 and reduce axiom dependencies, and similarly for the following theorems. Note: wl-equsalcom 35395 is also interesting. (Contributed by BJ, 6-Oct-2018.) |
⊢ (Ⅎ𝑥𝜑 → (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜑)) | ||
Theorem | bj-equsal1ti 34700 | Inference associated with bj-equsal1t 34699. (Contributed by BJ, 30-Sep-2018.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜑) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |