| Metamath
Proof Explorer Theorem List (p. 368 of 494) | < 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-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | bj-exexbiex 36701 | Adding a second quantifier over the same variable is a transparent operation, (∃∃ case). (Contributed by BJ, 20-Oct-2019.) |
| ⊢ (∃𝑥∃𝑥𝜑 ↔ ∃𝑥𝜑) | ||
| Theorem | bj-alalbial 36702 | Adding a second quantifier over the same variable is a transparent operation, (∀∀ case). (Contributed by BJ, 20-Oct-2019.) |
| ⊢ (∀𝑥∀𝑥𝜑 ↔ ∀𝑥𝜑) | ||
| Theorem | bj-exalbial 36703 | Adding a second quantifier over the same variable is a transparent operation, (∃∀ case). (Contributed by BJ, 20-Oct-2019.) |
| ⊢ (∃𝑥∀𝑥𝜑 ↔ ∀𝑥𝜑) | ||
| Theorem | bj-19.9htbi 36704 | Strengthening 19.9ht 2320 by replacing its consequent with a biconditional (19.9t 2204 does have a biconditional consequent). This propagates. (Contributed by BJ, 20-Oct-2019.) |
| ⊢ (∀𝑥(𝜑 → ∀𝑥𝜑) → (∃𝑥𝜑 ↔ 𝜑)) | ||
| Theorem | bj-hbntbi 36705 | Strengthening hbnt 2294 by replacing its consequent with a biconditional. See also hbntg 35806 and hbntal 44573. (Contributed by BJ, 20-Oct-2019.) Proved from bj-19.9htbi 36704. (Proof modification is discouraged.) |
| ⊢ (∀𝑥(𝜑 → ∀𝑥𝜑) → (¬ 𝜑 ↔ ∀𝑥 ¬ 𝜑)) | ||
| Theorem | bj-biexal1 36706 | A general FOL biconditional that generalizes 19.9ht 2320 among others. For this and the following theorems, see also 19.35 1877, 19.21 2207, 19.23 2211. When 𝜑 is substituted for 𝜓, both sides express a form of nonfreeness. (Contributed by BJ, 20-Oct-2019.) |
| ⊢ (∀𝑥(𝜑 → ∀𝑥𝜓) ↔ (∃𝑥𝜑 → ∀𝑥𝜓)) | ||
| Theorem | bj-biexal2 36707 | When 𝜑 is substituted for 𝜓, both sides express a form of nonfreeness. (Contributed by BJ, 20-Oct-2019.) |
| ⊢ (∀𝑥(∃𝑥𝜑 → 𝜓) ↔ (∃𝑥𝜑 → ∀𝑥𝜓)) | ||
| Theorem | bj-biexal3 36708 | When 𝜑 is substituted for 𝜓, both sides express a form of nonfreeness. (Contributed by BJ, 20-Oct-2019.) |
| ⊢ (∀𝑥(𝜑 → ∀𝑥𝜓) ↔ ∀𝑥(∃𝑥𝜑 → 𝜓)) | ||
| Theorem | bj-bialal 36709 | When 𝜑 is substituted for 𝜓, both sides express a form of nonfreeness. (Contributed by BJ, 20-Oct-2019.) |
| ⊢ (∀𝑥(∀𝑥𝜑 → 𝜓) ↔ (∀𝑥𝜑 → ∀𝑥𝜓)) | ||
| Theorem | bj-biexex 36710 | When 𝜑 is substituted for 𝜓, both sides express a form of nonfreeness. (Contributed by BJ, 20-Oct-2019.) |
| ⊢ (∀𝑥(𝜑 → ∃𝑥𝜓) ↔ (∃𝑥𝜑 → ∃𝑥𝜓)) | ||
| Theorem | bj-hbext 36711 | Closed form of hbex 2325. (Contributed by BJ, 10-Oct-2019.) |
| ⊢ (∀𝑦∀𝑥(𝜑 → ∀𝑥𝜑) → (∃𝑦𝜑 → ∀𝑥∃𝑦𝜑)) | ||
| Theorem | bj-nfalt 36712 | Closed form of nfal 2323. (Contributed by BJ, 2-May-2019.) |
| ⊢ (∀𝑥Ⅎ𝑦𝜑 → Ⅎ𝑦∀𝑥𝜑) | ||
| Theorem | bj-nfext 36713 | Closed form of nfex 2324. (Contributed by BJ, 10-Oct-2019.) |
| ⊢ (∀𝑥Ⅎ𝑦𝜑 → Ⅎ𝑦∃𝑥𝜑) | ||
| Theorem | bj-eeanvw 36714* | Version of exdistrv 1955 with a disjoint variable condition on 𝑥, 𝑦 not requiring ax-11 2157. (The same can be done with eeeanv 2352 and ee4anv 2353.) (Contributed by BJ, 29-Sep-2019.) (Proof modification is discouraged.) |
| ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ ∃𝑦𝜓)) | ||
| Theorem | bj-modal4 36715 | First-order logic form of the modal axiom (4). See hba1 2293. This is the standard proof of the implication in modal logic (B5 ⇒ 4). Its dual statement is bj-modal4e 36716. (Contributed by BJ, 12-Aug-2023.) (Proof modification is discouraged.) |
| ⊢ (∀𝑥𝜑 → ∀𝑥∀𝑥𝜑) | ||
| Theorem | bj-modal4e 36716 | First-order logic form of the modal axiom (4) using existential quantifiers. Dual statement of bj-modal4 36715 (hba1 2293). (Contributed by BJ, 21-Dec-2020.) (Proof modification is discouraged.) |
| ⊢ (∃𝑥∃𝑥𝜑 → ∃𝑥𝜑) | ||
| Theorem | bj-modalb 36717 | 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 36718 | 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 36719 | 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 36720 | 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 36721 | 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 36722 |
Equivalent form of the axiom of substitution bj-ax12 36658. Although both
sides need a DV condition on 𝑥, 𝑡 (or as in bj-ax12v3 36686 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 36723. Note that in the LHS, the reverse
implication holds by equs4 2421 (or equs4v 1999 if a DV condition is added on
𝑥,
𝑡 as in bj-ax12 36658), and the forward implication is sbalex 2242.
The LHS can be read as saying that if there exists a variable equal to a given term witnessing a given formula, then all variables equal to that term also witness that formula. The equivalent form of the LHS using only primitive symbols is (∀𝑥(𝑥 = 𝑡 → 𝜑) ∨ ∀𝑥(𝑥 = 𝑡 → ¬ 𝜑)), which expresses that a given formula is true at all variables equal to a given term, or false at all these variables. An equivalent form of the LHS using only the existential quantifier is ¬ (∃𝑥(𝑥 = 𝑡 ∧ 𝜑) ∧ ∃𝑥(𝑥 = 𝑡 ∧ ¬ 𝜑)), which expresses that there can be no two variables both equal to a given term, one witnessing a formula and the other witnessing its negation. These equivalences do not hold in intuitionistic logic. The LHS should be the preferred form, and has the advantage of having no negation nor nested quantifiers. (Contributed by BJ, 21-May-2024.) (Proof modification is discouraged.) |
| ⊢ ((∃𝑥(𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑)) ↔ ∀𝑥(𝑥 = 𝑡 → (𝜑 → ∀𝑥(𝑥 = 𝑡 → 𝜑)))) | ||
| Theorem | bj-substw 36723* | Weak form of the LHS of bj-substax12 36722 proved from the core axiom schemes. Compare ax12w 2133. (Contributed by BJ, 26-May-2024.) (Proof modification is discouraged.) |
| ⊢ (𝑥 = 𝑡 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥(𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑)) | ||
| Syntax | wnnf 36724 | Syntax for the nonfreeness quantifier. |
| wff Ⅎ'𝑥𝜑 | ||
| Definition | df-bj-nnf 36725 |
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 1910 and ax5e 1912. 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 36755, 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 2159 and excom 2162 (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 1910, ax5e 1912, ax5ea 1913. 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 36726 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 36755, 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 36747, bj-nnfnt 36741, bj-nnfan 36749, bj-nnfor 36751, bj-nnfbit 36753, bj-nnfalt 36767, bj-nnfext 36768. 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 36747 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 36767 yields ((∀𝑦∀𝑥1 ...∀𝑥m Ⅎ'𝑥𝜑 → Ⅎ'𝑥∀𝑦 PHI), {{𝑥, 𝑎} ∣ 𝑎 ∈ OC(∀𝑦 PHI) ∖ {𝜑}}) and similarly for antecedents which are conjunctions as in the statement of the lemma. Note bj-nnfalt 36767 and bj-nnfext 36768 are proved from positive propositional calculus with alcom 2159 and excom 2162 (possibly weakened by a DV condition on the quantifying variables), and modalB (via bj-19.12 36762). 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 1910 or ax5e 1912 or ax5ea 1913. 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 36729 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 1912 or ax5ea 1913, we would use bj-nnfe 36732 or bj-nnfea 36735 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 1795, by bj-nnf-alrim 36756 and bj-nnfa1 36760 (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 1980. QED Compared with df-nf 1784, the present definition is stricter on positive propositional calculus (bj-nnfnfTEMP 36739) and equivalent on core FOL plus sp 2183 (bj-nfnnfTEMP 36759). While being stricter, it still holds for non-occurring variables (bj-nnfv 36755), 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 2141 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 36726 | If two formulas are equivalent for all 𝑥, then nonfreeness of 𝑥 in one of them is equivalent to nonfreeness in the other. Compare nfbiit 1851. From this and bj-nnfim 36747 and bj-nnfnt 36741, 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 36742) in order not to require sp 2183 (modal T). (Contributed by BJ, 27-Aug-2023.) |
| ⊢ (((𝜑 ↔ 𝜓) ∧ ∀𝑥(𝜑 ↔ 𝜓)) → (Ⅎ'𝑥𝜑 ↔ Ⅎ'𝑥𝜓)) | ||
| Theorem | bj-nnfbd 36727* | 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 36726. (Contributed by BJ, 27-Aug-2023.) |
| ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (Ⅎ'𝑥𝜓 ↔ Ⅎ'𝑥𝜒)) | ||
| Theorem | bj-nnfbii 36728 | 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 36726. (Contributed by BJ, 18-Nov-2023.) |
| ⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (Ⅎ'𝑥𝜑 ↔ Ⅎ'𝑥𝜓) | ||
| Theorem | bj-nnfa 36729 | Nonfreeness implies the equivalent of ax-5 1910. See nf5r 2194. (Contributed by BJ, 28-Jul-2023.) |
| ⊢ (Ⅎ'𝑥𝜑 → (𝜑 → ∀𝑥𝜑)) | ||
| Theorem | bj-nnfad 36730 | Nonfreeness implies the equivalent of ax-5 1910, deduction form. See nf5rd 2196. (Contributed by BJ, 2-Dec-2023.) |
| ⊢ (𝜑 → Ⅎ'𝑥𝜓) ⇒ ⊢ (𝜑 → (𝜓 → ∀𝑥𝜓)) | ||
| Theorem | bj-nnfai 36731 | Nonfreeness implies the equivalent of ax-5 1910, inference form. See nf5ri 2195. (Contributed by BJ, 22-Sep-2024.) |
| ⊢ Ⅎ'𝑥𝜑 ⇒ ⊢ (𝜑 → ∀𝑥𝜑) | ||
| Theorem | bj-nnfe 36732 | Nonfreeness implies the equivalent of ax5e 1912. (Contributed by BJ, 28-Jul-2023.) |
| ⊢ (Ⅎ'𝑥𝜑 → (∃𝑥𝜑 → 𝜑)) | ||
| Theorem | bj-nnfed 36733 | Nonfreeness implies the equivalent of ax5e 1912, deduction form. (Contributed by BJ, 2-Dec-2023.) |
| ⊢ (𝜑 → Ⅎ'𝑥𝜓) ⇒ ⊢ (𝜑 → (∃𝑥𝜓 → 𝜓)) | ||
| Theorem | bj-nnfei 36734 | Nonfreeness implies the equivalent of ax5e 1912, inference form. (Contributed by BJ, 22-Sep-2024.) |
| ⊢ Ⅎ'𝑥𝜑 ⇒ ⊢ (∃𝑥𝜑 → 𝜑) | ||
| Theorem | bj-nnfea 36735 | Nonfreeness implies the equivalent of ax5ea 1913. (Contributed by BJ, 28-Jul-2023.) |
| ⊢ (Ⅎ'𝑥𝜑 → (∃𝑥𝜑 → ∀𝑥𝜑)) | ||
| Theorem | bj-nnfead 36736 | Nonfreeness implies the equivalent of ax5ea 1913, deduction form. (Contributed by BJ, 2-Dec-2023.) |
| ⊢ (𝜑 → Ⅎ'𝑥𝜓) ⇒ ⊢ (𝜑 → (∃𝑥𝜓 → ∀𝑥𝜓)) | ||
| Theorem | bj-nnfeai 36737 | Nonfreeness implies the equivalent of ax5ea 1913, inference form. (Contributed by BJ, 22-Sep-2024.) |
| ⊢ Ⅎ'𝑥𝜑 ⇒ ⊢ (∃𝑥𝜑 → ∀𝑥𝜑) | ||
| Theorem | bj-dfnnf2 36738 | Alternate definition of df-bj-nnf 36725 using only primitive symbols (→, ¬, ∀) in each conjunct. (Contributed by BJ, 20-Aug-2023.) |
| ⊢ (Ⅎ'𝑥𝜑 ↔ ((𝜑 → ∀𝑥𝜑) ∧ (¬ 𝜑 → ∀𝑥 ¬ 𝜑))) | ||
| Theorem | bj-nnfnfTEMP 36739 | 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 1784 except via df-nf 1784 directly. (Proof modification is discouraged.) |
| ⊢ (Ⅎ'𝑥𝜑 → Ⅎ𝑥𝜑) | ||
| Theorem | bj-wnfnf 36740 | When 𝜑 is substituted for 𝜓, this statement expresses nonfreeness in the weak form of nonfreeness (∃ → ∀). Note that this could also be proved from bj-nnfim 36747, bj-nnfe1 36761 and bj-nnfa1 36760. (Contributed by BJ, 9-Dec-2023.) |
| ⊢ Ⅎ'𝑥(∃𝑥𝜑 → ∀𝑥𝜓) | ||
| Theorem | bj-nnfnt 36741 | 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 36747). Intuitionistically, ⊢ (Ⅎ'𝑥¬ 𝜑 ↔ Ⅎ'𝑥¬ ¬ 𝜑). See nfnt 1856. (Contributed by BJ, 28-Jul-2023.) |
| ⊢ (Ⅎ'𝑥𝜑 ↔ Ⅎ'𝑥 ¬ 𝜑) | ||
| Theorem | bj-nnftht 36742 | A variable is nonfree in a theorem. The antecedent is in the "strong necessity" modality of modal logic in order not to require sp 2183 (modal T), as in bj-nnfbi 36726. (Contributed by BJ, 28-Jul-2023.) |
| ⊢ ((𝜑 ∧ ∀𝑥𝜑) → Ⅎ'𝑥𝜑) | ||
| Theorem | bj-nnfth 36743 | A variable is nonfree in a theorem, inference form. (Contributed by BJ, 28-Jul-2023.) |
| ⊢ 𝜑 ⇒ ⊢ Ⅎ'𝑥𝜑 | ||
| Theorem | bj-nnfnth 36744 | A variable is nonfree in the negation of a theorem, inference form. (Contributed by BJ, 27-Aug-2023.) |
| ⊢ ¬ 𝜑 ⇒ ⊢ Ⅎ'𝑥𝜑 | ||
| Theorem | bj-nnfim1 36745 | A consequence of nonfreeness in the antecedent and the consequent of an implication. (Contributed by BJ, 27-Aug-2023.) |
| ⊢ ((Ⅎ'𝑥𝜑 ∧ Ⅎ'𝑥𝜓) → ((𝜑 → 𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓))) | ||
| Theorem | bj-nnfim2 36746 | A consequence of nonfreeness in the antecedent and the consequent of an implication. (Contributed by BJ, 27-Aug-2023.) |
| ⊢ ((Ⅎ'𝑥𝜑 ∧ Ⅎ'𝑥𝜓) → ((∀𝑥𝜑 → ∃𝑥𝜓) → (𝜑 → 𝜓))) | ||
| Theorem | bj-nnfim 36747 | Nonfreeness in the antecedent and the consequent of an implication implies nonfreeness in the implication. (Contributed by BJ, 27-Aug-2023.) |
| ⊢ ((Ⅎ'𝑥𝜑 ∧ Ⅎ'𝑥𝜓) → Ⅎ'𝑥(𝜑 → 𝜓)) | ||
| Theorem | bj-nnfimd 36748 | 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 36749 | 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 36747, bj-nnfnt 36741 and bj-nnfbi 36726, but we want a proof valid in intuitionistic logic. (Proof modification is discouraged.) |
| ⊢ ((Ⅎ'𝑥𝜑 ∧ Ⅎ'𝑥𝜓) → Ⅎ'𝑥(𝜑 ∧ 𝜓)) | ||
| Theorem | bj-nnfand 36750 | Nonfreeness in both conjuncts implies nonfreeness in the conjunction, deduction form. Note: compared with the proof of bj-nnfan 36749, 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 36749 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 36750 will generally be easier to understand). (Contributed by BJ, 19-Nov-2023.) (Proof modification is discouraged.) |
| ⊢ (𝜑 → Ⅎ'𝑥𝜓) & ⊢ (𝜑 → Ⅎ'𝑥𝜒) ⇒ ⊢ (𝜑 → Ⅎ'𝑥(𝜓 ∧ 𝜒)) | ||
| Theorem | bj-nnfor 36751 | 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 36747, bj-nnfnt 36741 and bj-nnfbi 36726, but we want a proof valid in intuitionistic logic. (Proof modification is discouraged.) |
| ⊢ ((Ⅎ'𝑥𝜑 ∧ Ⅎ'𝑥𝜓) → Ⅎ'𝑥(𝜑 ∨ 𝜓)) | ||
| Theorem | bj-nnford 36752 | Nonfreeness in both disjuncts implies nonfreeness in the disjunction, deduction form. See comments for bj-nnfor 36751 and bj-nnfand 36750. (Contributed by BJ, 2-Dec-2023.) (Proof modification is discouraged.) |
| ⊢ (𝜑 → Ⅎ'𝑥𝜓) & ⊢ (𝜑 → Ⅎ'𝑥𝜒) ⇒ ⊢ (𝜑 → Ⅎ'𝑥(𝜓 ∨ 𝜒)) | ||
| Theorem | bj-nnfbit 36753 | Nonfreeness in both sides implies nonfreeness in the biconditional. (Contributed by BJ, 2-Dec-2023.) (Proof modification is discouraged.) |
| ⊢ ((Ⅎ'𝑥𝜑 ∧ Ⅎ'𝑥𝜓) → Ⅎ'𝑥(𝜑 ↔ 𝜓)) | ||
| Theorem | bj-nnfbid 36754 | Nonfreeness in both sides implies nonfreeness in the biconditional, deduction form. (Contributed by BJ, 2-Dec-2023.) (Proof modification is discouraged.) |
| ⊢ (𝜑 → Ⅎ'𝑥𝜓) & ⊢ (𝜑 → Ⅎ'𝑥𝜒) ⇒ ⊢ (𝜑 → Ⅎ'𝑥(𝜓 ↔ 𝜒)) | ||
| Theorem | bj-nnfv 36755* | A non-occurring variable is nonfree in a formula. (Contributed by BJ, 28-Jul-2023.) |
| ⊢ Ⅎ'𝑥𝜑 | ||
| Theorem | bj-nnf-alrim 36756 | Proof of the closed form of alrimi 2213 from modalK (compare alrimiv 1927). See also bj-alrim 36694. Actually, most proofs between 19.3t 2201 and 2sbbid 2247 could be proved without ax-12 2177. (Contributed by BJ, 20-Aug-2023.) |
| ⊢ (Ⅎ'𝑥𝜑 → (∀𝑥(𝜑 → 𝜓) → (𝜑 → ∀𝑥𝜓))) | ||
| Theorem | bj-nnf-exlim 36757 | Proof of the closed form of exlimi 2217 from modalK (compare exlimiv 1930). See also bj-sylget2 36623. (Contributed by BJ, 2-Dec-2023.) |
| ⊢ (Ⅎ'𝑥𝜓 → (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → 𝜓))) | ||
| Theorem | bj-dfnnf3 36758 | Alternate definition of nonfreeness when sp 2183 is available. (Contributed by BJ, 28-Jul-2023.) The proof should not rely on df-nf 1784. (Proof modification is discouraged.) |
| ⊢ (Ⅎ'𝑥𝜑 ↔ (∃𝑥𝜑 → ∀𝑥𝜑)) | ||
| Theorem | bj-nfnnfTEMP 36759 | New nonfreeness is equivalent to old nonfreeness on core FOL axioms plus sp 2183. (Contributed by BJ, 28-Jul-2023.) The proof should not rely on df-nf 1784 except via df-nf 1784 directly. (Proof modification is discouraged.) |
| ⊢ (Ⅎ'𝑥𝜑 ↔ Ⅎ𝑥𝜑) | ||
| Theorem | bj-nnfa1 36760 | See nfa1 2151. (Contributed by BJ, 12-Aug-2023.) (Proof modification is discouraged.) |
| ⊢ Ⅎ'𝑥∀𝑥𝜑 | ||
| Theorem | bj-nnfe1 36761 | See nfe1 2150. (Contributed by BJ, 12-Aug-2023.) (Proof modification is discouraged.) |
| ⊢ Ⅎ'𝑥∃𝑥𝜑 | ||
| Theorem | bj-19.12 36762 | See 19.12 2327. 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 1784 or df-bj-nnf 36725, directly or indirectly. (Proof modification is discouraged.) |
| ⊢ (∃𝑥∀𝑦𝜑 → ∀𝑦∃𝑥𝜑) | ||
| Theorem | bj-nnflemaa 36763 | One of four lemmas for nonfreeness: antecedent and consequent both expressed using universal quantifier. Note: this is bj-hbalt 36682. (Contributed by BJ, 12-Aug-2023.) (Proof modification is discouraged.) |
| ⊢ (∀𝑥(𝜑 → ∀𝑦𝜑) → (∀𝑥𝜑 → ∀𝑦∀𝑥𝜑)) | ||
| Theorem | bj-nnflemee 36764 | 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 36765 | 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 36766 | 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 36767 | See nfal 2323 and bj-nfalt 36712. (Contributed by BJ, 12-Aug-2023.) (Proof modification is discouraged.) |
| ⊢ (∀𝑥Ⅎ'𝑦𝜑 → Ⅎ'𝑦∀𝑥𝜑) | ||
| Theorem | bj-nnfext 36768 | See nfex 2324 and bj-nfext 36713. (Contributed by BJ, 12-Aug-2023.) (Proof modification is discouraged.) |
| ⊢ (∀𝑥Ⅎ'𝑦𝜑 → Ⅎ'𝑦∃𝑥𝜑) | ||
| Theorem | bj-stdpc5t 36769 | Alias of bj-nnf-alrim 36756 for labeling consistency (a standard predicate calculus axiom). Closed form of stdpc5 2208 proved from modalK (obsoleting stdpc5v 1938). (Contributed by BJ, 2-Dec-2023.) Use bj-nnf-alrim 36756 instead. (New usaged is discouraged.) |
| ⊢ (Ⅎ'𝑥𝜑 → (∀𝑥(𝜑 → 𝜓) → (𝜑 → ∀𝑥𝜓))) | ||
| Theorem | bj-19.21t 36770 | Statement 19.21t 2206 proved from modalK (obsoleting 19.21v 1939). (Contributed by BJ, 2-Dec-2023.) |
| ⊢ (Ⅎ'𝑥𝜑 → (∀𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥𝜓))) | ||
| Theorem | bj-19.23t 36771 | Statement 19.23t 2210 proved from modalK (obsoleting 19.23v 1942). (Contributed by BJ, 2-Dec-2023.) |
| ⊢ (Ⅎ'𝑥𝜓 → (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜓))) | ||
| Theorem | bj-19.36im 36772 | One direction of 19.36 2230 from the same axioms as 19.36imv 1945. (Contributed by BJ, 2-Dec-2023.) |
| ⊢ (Ⅎ'𝑥𝜓 → (∃𝑥(𝜑 → 𝜓) → (∀𝑥𝜑 → 𝜓))) | ||
| Theorem | bj-19.37im 36773 | One direction of 19.37 2232 from the same axioms as 19.37imv 1947. (Contributed by BJ, 2-Dec-2023.) |
| ⊢ (Ⅎ'𝑥𝜑 → (∃𝑥(𝜑 → 𝜓) → (𝜑 → ∃𝑥𝜓))) | ||
| Theorem | bj-19.42t 36774 | Closed form of 19.42 2236 from the same axioms as 19.42v 1953. (Contributed by BJ, 2-Dec-2023.) |
| ⊢ (Ⅎ'𝑥𝜑 → (∃𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥𝜓))) | ||
| Theorem | bj-19.41t 36775 | Closed form of 19.41 2235 from the same axioms as 19.41v 1949. The same is doable with 19.27 2227, 19.28 2228, 19.31 2234, 19.32 2233, 19.44 2237, 19.45 2238. (Contributed by BJ, 2-Dec-2023.) |
| ⊢ (Ⅎ'𝑥𝜓 → (∃𝑥(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ 𝜓))) | ||
| Theorem | bj-sbft 36776 | Version of sbft 2270 using Ⅎ', proved from core axioms. (Contributed by BJ, 19-Nov-2023.) |
| ⊢ (Ⅎ'𝑥𝜑 → ([𝑡 / 𝑥]𝜑 ↔ 𝜑)) | ||
| Theorem | bj-pm11.53vw 36777 | Version of pm11.53v 1944 with nonfreeness antecedents. One can also prove the theorem with antecedent (Ⅎ'𝑦∀𝑥𝜑 ∧ ∀𝑦Ⅎ'𝑥𝜓). (Contributed by BJ, 7-Oct-2024.) |
| ⊢ ((∀𝑥Ⅎ'𝑦𝜑 ∧ Ⅎ'𝑥∀𝑦𝜓) → (∀𝑥∀𝑦(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → ∀𝑦𝜓))) | ||
| Theorem | bj-pm11.53v 36778 | Version of pm11.53v 1944 with nonfreeness antecedents. (Contributed by BJ, 7-Oct-2024.) |
| ⊢ ((∀𝑥Ⅎ'𝑦𝜑 ∧ ∀𝑦Ⅎ'𝑥𝜓) → (∀𝑥∀𝑦(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → ∀𝑦𝜓))) | ||
| Theorem | bj-pm11.53a 36779* | A variant of pm11.53v 1944. One can similarly prove a variant with DV (𝑦, 𝜑) and ∀𝑦Ⅎ'𝑥𝜓 instead of DV (𝑥, 𝜓) and ∀𝑥Ⅎ'𝑦𝜑. (Contributed by BJ, 7-Oct-2024.) |
| ⊢ (∀𝑥Ⅎ'𝑦𝜑 → (∀𝑥∀𝑦(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → ∀𝑦𝜓))) | ||
| Theorem | bj-equsvt 36780* | A variant of equsv 2002. (Contributed by BJ, 7-Oct-2024.) |
| ⊢ (Ⅎ'𝑥𝜑 → (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜑)) | ||
| Theorem | bj-equsalvwd 36781* | Variant of equsalvw 2003. (Contributed by BJ, 7-Oct-2024.) |
| ⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜑 → Ⅎ'𝑥𝜒) & ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥(𝑥 = 𝑦 → 𝜓) ↔ 𝜒)) | ||
| Theorem | bj-equsexvwd 36782* | Variant of equsexvw 2004. (Contributed by BJ, 7-Oct-2024.) |
| ⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜑 → Ⅎ'𝑥𝜒) & ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥(𝑥 = 𝑦 ∧ 𝜓) ↔ 𝜒)) | ||
| Theorem | bj-sbievwd 36783* | Variant of sbievw 2093. (Contributed by BJ, 7-Oct-2024.) |
| ⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜑 → Ⅎ'𝑥𝜒) & ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ([𝑦 / 𝑥]𝜓 ↔ 𝜒)) | ||
| Theorem | bj-axc10 36784 | Alternate proof of axc10 2390. Shorter. One can prove a version with DV (𝑥, 𝑦) without ax-13 2377, by using ax6ev 1969 instead of ax6e 2388. (Contributed by BJ, 31-Mar-2021.) (Proof modification is discouraged.) |
| ⊢ (∀𝑥(𝑥 = 𝑦 → ∀𝑥𝜑) → 𝜑) | ||
| Theorem | bj-alequex 36785 | A fol lemma. See alequexv 2000 for a version with a disjoint variable condition requiring fewer axioms. Can be used to reduce the proof of spimt 2391 from 133 to 112 bytes. (Contributed by BJ, 6-Oct-2018.) |
| ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → ∃𝑥𝜑) | ||
| Theorem | bj-spimt2 36786 | A step in the proof of spimt 2391. (Contributed by BJ, 2-May-2019.) |
| ⊢ (∀𝑥(𝑥 = 𝑦 → (𝜑 → 𝜓)) → ((∃𝑥𝜓 → 𝜓) → (∀𝑥𝜑 → 𝜓))) | ||
| Theorem | bj-cbv3ta 36787 | Closed form of cbv3 2402. (Contributed by BJ, 2-May-2019.) |
| ⊢ (∀𝑥∀𝑦(𝑥 = 𝑦 → (𝜑 → 𝜓)) → ((∀𝑦(∃𝑥𝜓 → 𝜓) ∧ ∀𝑥(𝜑 → ∀𝑦𝜑)) → (∀𝑥𝜑 → ∀𝑦𝜓))) | ||
| Theorem | bj-cbv3tb 36788 | Closed form of cbv3 2402. (Contributed by BJ, 2-May-2019.) |
| ⊢ (∀𝑥∀𝑦(𝑥 = 𝑦 → (𝜑 → 𝜓)) → ((∀𝑦Ⅎ𝑥𝜓 ∧ ∀𝑥Ⅎ𝑦𝜑) → (∀𝑥𝜑 → ∀𝑦𝜓))) | ||
| Theorem | bj-hbsb3t 36789 | A theorem close to a closed form of hbsb3 2492. (Contributed by BJ, 2-May-2019.) |
| ⊢ (∀𝑥(𝜑 → ∀𝑦𝜑) → ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑)) | ||
| Theorem | bj-hbsb3 36790 | Shorter proof of hbsb3 2492. (Contributed by BJ, 2-May-2019.) (Proof modification is discouraged.) |
| ⊢ (𝜑 → ∀𝑦𝜑) ⇒ ⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑) | ||
| Theorem | bj-nfs1t 36791 | A theorem close to a closed form of nfs1 2493. (Contributed by BJ, 2-May-2019.) |
| ⊢ (∀𝑥(𝜑 → ∀𝑦𝜑) → Ⅎ𝑥[𝑦 / 𝑥]𝜑) | ||
| Theorem | bj-nfs1t2 36792 | A theorem close to a closed form of nfs1 2493. (Contributed by BJ, 2-May-2019.) |
| ⊢ (∀𝑥Ⅎ𝑦𝜑 → Ⅎ𝑥[𝑦 / 𝑥]𝜑) | ||
| Theorem | bj-nfs1 36793 | Shorter proof of nfs1 2493 (three essential steps instead of four). (Contributed by BJ, 2-May-2019.) (Proof modification is discouraged.) |
| ⊢ Ⅎ𝑦𝜑 ⇒ ⊢ Ⅎ𝑥[𝑦 / 𝑥]𝜑 | ||
It is known that ax-13 2377 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 2377 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 2377 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 2377 (and using ax6v 1968 / ax6ev 1969 instead of ax-6 1967 / ax6e 2388, as is currently done). One reason to be optimistic is that the first few utility theorems using ax-13 2377 (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 2377, labeled bj-xxxv (we follow the proof of xxx but use ax6v 1968 and ax6ev 1969 instead of ax-6 1967 and ax6e 2388, and ax-5 1910 instead of ax13v 2378; 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 dispense with ax-13 2377, so as to remove dependencies on ax-13 2377 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 2157, typically by replacing a nonfree hypothesis with a disjoint variable condition (see cbv3v2 2241 and following theorems). | ||
| Theorem | bj-axc10v 36794* | Version of axc10 2390 with a disjoint variable condition, which does not require ax-13 2377. (Contributed by BJ, 14-Jun-2019.) (Proof modification is discouraged.) |
| ⊢ (∀𝑥(𝑥 = 𝑦 → ∀𝑥𝜑) → 𝜑) | ||
| Theorem | bj-spimtv 36795* | Version of spimt 2391 with a disjoint variable condition, which does not require ax-13 2377. (Contributed by BJ, 14-Jun-2019.) (Proof modification is discouraged.) |
| ⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝑦 → (𝜑 → 𝜓))) → (∀𝑥𝜑 → 𝜓)) | ||
| Theorem | bj-cbv3hv2 36796* | Version of cbv3h 2409 with two disjoint variable conditions, which does not require ax-11 2157 nor ax-13 2377. (Contributed by BJ, 24-Jun-2019.) (Proof modification is discouraged.) |
| ⊢ (𝜓 → ∀𝑥𝜓) & ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) ⇒ ⊢ (∀𝑥𝜑 → ∀𝑦𝜓) | ||
| Theorem | bj-cbv1hv 36797* | Version of cbv1h 2410 with a disjoint variable condition, which does not require ax-13 2377. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.) |
| ⊢ (𝜑 → (𝜓 → ∀𝑦𝜓)) & ⊢ (𝜑 → (𝜒 → ∀𝑥𝜒)) & ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 → 𝜒))) ⇒ ⊢ (∀𝑥∀𝑦𝜑 → (∀𝑥𝜓 → ∀𝑦𝜒)) | ||
| Theorem | bj-cbv2hv 36798* | Version of cbv2h 2411 with a disjoint variable condition, which does not require ax-13 2377. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.) |
| ⊢ (𝜑 → (𝜓 → ∀𝑦𝜓)) & ⊢ (𝜑 → (𝜒 → ∀𝑥𝜒)) & ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))) ⇒ ⊢ (∀𝑥∀𝑦𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒)) | ||
| Theorem | bj-cbv2v 36799* | Version of cbv2 2408 with a disjoint variable condition, which does not require ax-13 2377. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑦𝜓) & ⊢ (𝜑 → Ⅎ𝑥𝜒) & ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))) ⇒ ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒)) | ||
| Theorem | bj-cbvaldv 36800* | Version of cbvald 2412 with a disjoint variable condition, which does not require ax-13 2377. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.) |
| ⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑦𝜓) & ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))) ⇒ ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |