P. 349 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 34801-34900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	bj-nexrt 34801	Closed form of nexr 2187. Contrapositive of 19.8a 2176. (Contributed by BJ, 20-Oct-2019.)
⊢ (¬ ∃𝑥𝜑 → ¬ 𝜑)
Theorem	bj-alrim 34802	Closed form of alrimi 2209. (Contributed by BJ, 2-May-2019.)
⊢ (Ⅎ𝑥𝜑 → (∀𝑥(𝜑 → 𝜓) → (𝜑 → ∀𝑥𝜓)))
Theorem	bj-alrim2 34803	Uncurried (imported) form of bj-alrim 34802. (Contributed by BJ, 2-May-2019.)
⊢ ((Ⅎ𝑥𝜑 ∧ ∀𝑥(𝜑 → 𝜓)) → (𝜑 → ∀𝑥𝜓))
Theorem	bj-nfdt0 34804	A theorem close to a closed form of nf5d 2284 and nf5dh 2145. (Contributed by BJ, 2-May-2019.)
⊢ (∀𝑥(𝜑 → (𝜓 → ∀𝑥𝜓)) → (∀𝑥𝜑 → Ⅎ𝑥𝜓))
Theorem	bj-nfdt 34805	Closed form of nf5d 2284 and nf5dh 2145. (Contributed by BJ, 2-May-2019.)
⊢ (∀𝑥(𝜑 → (𝜓 → ∀𝑥𝜓)) → ((𝜑 → ∀𝑥𝜑) → (𝜑 → Ⅎ𝑥𝜓)))
Theorem	bj-nexdt 34806	Closed form of nexd 2217. (Contributed by BJ, 20-Oct-2019.)
⊢ (Ⅎ𝑥𝜑 → (∀𝑥(𝜑 → ¬ 𝜓) → (𝜑 → ¬ ∃𝑥𝜓)))
Theorem	bj-nexdvt 34807*	Closed form of nexdv 1940. (Contributed by BJ, 20-Oct-2019.)
⊢ (∀𝑥(𝜑 → ¬ 𝜓) → (𝜑 → ¬ ∃𝑥𝜓))
Theorem	bj-alexbiex 34808	Adding a second quantifier over the same variable is a transparent operation, (∀∃ case). (Contributed by BJ, 20-Oct-2019.)
⊢ (∀𝑥∃𝑥𝜑 ↔ ∃𝑥𝜑)
Theorem	bj-exexbiex 34809	Adding a second quantifier over the same variable is a transparent operation, (∃∃ case). (Contributed by BJ, 20-Oct-2019.)
⊢ (∃𝑥∃𝑥𝜑 ↔ ∃𝑥𝜑)
Theorem	bj-alalbial 34810	Adding a second quantifier over the same variable is a transparent operation, (∀∀ case). (Contributed by BJ, 20-Oct-2019.)
⊢ (∀𝑥∀𝑥𝜑 ↔ ∀𝑥𝜑)
Theorem	bj-exalbial 34811	Adding a second quantifier over the same variable is a transparent operation, (∃∀ case). (Contributed by BJ, 20-Oct-2019.)
⊢ (∃𝑥∀𝑥𝜑 ↔ ∀𝑥𝜑)
Theorem	bj-19.9htbi 34812	Strengthening 19.9ht 2318 by replacing its consequent with a biconditional (19.9t 2200 does have a biconditional consequent). This propagates. (Contributed by BJ, 20-Oct-2019.)
⊢ (∀𝑥(𝜑 → ∀𝑥𝜑) → (∃𝑥𝜑 ↔ 𝜑))
Theorem	bj-hbntbi 34813	Strengthening hbnt 2294 by replacing its consequent with a biconditional. See also hbntg 33687 and hbntal 42062. (Contributed by BJ, 20-Oct-2019.) Proved from bj-19.9htbi 34812. (Proof modification is discouraged.)
⊢ (∀𝑥(𝜑 → ∀𝑥𝜑) → (¬ 𝜑 ↔ ∀𝑥 ¬ 𝜑))
Theorem	bj-biexal1 34814	A general FOL biconditional that generalizes 19.9ht 2318 among others. For this and the following theorems, see also 19.35 1881, 19.21 2203, 19.23 2207. When 𝜑 is substituted for 𝜓, both sides express a form of nonfreeness. (Contributed by BJ, 20-Oct-2019.)
⊢ (∀𝑥(𝜑 → ∀𝑥𝜓) ↔ (∃𝑥𝜑 → ∀𝑥𝜓))
Theorem	bj-biexal2 34815	When 𝜑 is substituted for 𝜓, both sides express a form of nonfreeness. (Contributed by BJ, 20-Oct-2019.)
⊢ (∀𝑥(∃𝑥𝜑 → 𝜓) ↔ (∃𝑥𝜑 → ∀𝑥𝜓))
Theorem	bj-biexal3 34816	When 𝜑 is substituted for 𝜓, both sides express a form of nonfreeness. (Contributed by BJ, 20-Oct-2019.)
⊢ (∀𝑥(𝜑 → ∀𝑥𝜓) ↔ ∀𝑥(∃𝑥𝜑 → 𝜓))
Theorem	bj-bialal 34817	When 𝜑 is substituted for 𝜓, both sides express a form of nonfreeness. (Contributed by BJ, 20-Oct-2019.)
⊢ (∀𝑥(∀𝑥𝜑 → 𝜓) ↔ (∀𝑥𝜑 → ∀𝑥𝜓))
Theorem	bj-biexex 34818	When 𝜑 is substituted for 𝜓, both sides express a form of nonfreeness. (Contributed by BJ, 20-Oct-2019.)
⊢ (∀𝑥(𝜑 → ∃𝑥𝜓) ↔ (∃𝑥𝜑 → ∃𝑥𝜓))
Theorem	bj-hbext 34819	Closed form of hbex 2323. (Contributed by BJ, 10-Oct-2019.)
⊢ (∀𝑦∀𝑥(𝜑 → ∀𝑥𝜑) → (∃𝑦𝜑 → ∀𝑥∃𝑦𝜑))
Theorem	bj-nfalt 34820	Closed form of nfal 2321. (Contributed by BJ, 2-May-2019.)
⊢ (∀𝑥Ⅎ𝑦𝜑 → Ⅎ𝑦∀𝑥𝜑)
Theorem	bj-nfext 34821	Closed form of nfex 2322. (Contributed by BJ, 10-Oct-2019.)
⊢ (∀𝑥Ⅎ𝑦𝜑 → Ⅎ𝑦∃𝑥𝜑)
Theorem	bj-eeanvw 34822*	Version of exdistrv 1960 with a disjoint variable condition on 𝑥, 𝑦 not requiring ax-11 2156. (The same can be done with eeeanv 2350 and ee4anv 2351.) (Contributed by BJ, 29-Sep-2019.) (Proof modification is discouraged.)
⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ ∃𝑦𝜓))
Theorem	bj-modal4 34823	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 34824. (Contributed by BJ, 12-Aug-2023.) (Proof modification is discouraged.)
⊢ (∀𝑥𝜑 → ∀𝑥∀𝑥𝜑)
Theorem	bj-modal4e 34824	First-order logic form of the modal axiom (4) using existential quantifiers. Dual statement of bj-modal4 34823 (hba1 2293). (Contributed by BJ, 21-Dec-2020.) (Proof modification is discouraged.)
⊢ (∃𝑥∃𝑥𝜑 → ∃𝑥𝜑)
Theorem	bj-modalb 34825	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 34826	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 34827	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 34828	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 34829	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 34830	Equivalent form of the axiom of substitution bj-ax12 34765. Although both sides need a DV condition on 𝑥, 𝑡 (or as in bj-ax12v3 34794 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 34831. 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 34765). 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 34831*	Weak form of the LHS of bj-substax12 34830 proved from the core axiom schemes. Compare ax12w 2131. (Contributed by BJ, 26-May-2024.) (Proof modification is discouraged.)
⊢ (𝑥 = 𝑡 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥(𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑))
20.15.4.10  Nonfreeness
Syntax	wnnf 34832	Syntax for the nonfreeness quantifier.
wff Ⅎ'𝑥𝜑
Definition	df-bj-nnf 34833	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 34863, 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 2158 and excom 2164 (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 34834 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 34863, 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 34855, bj-nnfnt 34849, bj-nnfan 34857, bj-nnfor 34859, bj-nnfbit 34861, bj-nnfalt 34875, bj-nnfext 34876. 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 34855 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 34875 yields ((∀𝑦∀𝑥1 ...∀𝑥m Ⅎ'𝑥𝜑 → Ⅎ'𝑥∀𝑦 PHI), {{𝑥, 𝑎} ∣ 𝑎 ∈ OC(∀𝑦 PHI) ∖ {𝜑}}) and similarly for antecedents which are conjunctions as in the statement of the lemma. Note bj-nnfalt 34875 and bj-nnfext 34876 are proved from positive propositional calculus with alcom 2158 and excom 2164 (possibly weakened by a DV condition on the quantifying variables), and modalB (via bj-19.12 34870). 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 34837 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 34840 or bj-nnfea 34843 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 1799, by bj-nnf-alrim 34864 and bj-nnfa1 34868 (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 1788, the present definition is stricter on positive propositional calculus (bj-nnfnfTEMP 34847) and equivalent on core FOL plus sp 2178 (bj-nfnnfTEMP 34867). While being stricter, it still holds for non-occurring variables (bj-nnfv 34863), 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 2139 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 34834	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 34855 and bj-nnfnt 34849, 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 34850) in order not to require sp 2178 (modal T). (Contributed by BJ, 27-Aug-2023.)
⊢ (((𝜑 ↔ 𝜓) ∧ ∀𝑥(𝜑 ↔ 𝜓)) → (Ⅎ'𝑥𝜑 ↔ Ⅎ'𝑥𝜓))
Theorem	bj-nnfbd 34835*	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 34834. (Contributed by BJ, 27-Aug-2023.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (Ⅎ'𝑥𝜓 ↔ Ⅎ'𝑥𝜒))
Theorem	bj-nnfbii 34836	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 34834. (Contributed by BJ, 18-Nov-2023.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (Ⅎ'𝑥𝜑 ↔ Ⅎ'𝑥𝜓)
Theorem	bj-nnfa 34837	Nonfreeness implies the equivalent of ax-5 1914. See nf5r 2189. (Contributed by BJ, 28-Jul-2023.)
⊢ (Ⅎ'𝑥𝜑 → (𝜑 → ∀𝑥𝜑))
Theorem	bj-nnfad 34838	Nonfreeness implies the equivalent of ax-5 1914, deduction form. See nf5rd 2192. (Contributed by BJ, 2-Dec-2023.)
⊢ (𝜑 → Ⅎ'𝑥𝜓)    ⇒   ⊢ (𝜑 → (𝜓 → ∀𝑥𝜓))
Theorem	bj-nnfai 34839	Nonfreeness implies the equivalent of ax-5 1914, inference form. See nf5ri 2191. (Contributed by BJ, 22-Sep-2024.)
⊢ Ⅎ'𝑥𝜑    ⇒   ⊢ (𝜑 → ∀𝑥𝜑)
Theorem	bj-nnfe 34840	Nonfreeness implies the equivalent of ax5e 1916. (Contributed by BJ, 28-Jul-2023.)
⊢ (Ⅎ'𝑥𝜑 → (∃𝑥𝜑 → 𝜑))
Theorem	bj-nnfed 34841	Nonfreeness implies the equivalent of ax5e 1916, deduction form. (Contributed by BJ, 2-Dec-2023.)
⊢ (𝜑 → Ⅎ'𝑥𝜓)    ⇒   ⊢ (𝜑 → (∃𝑥𝜓 → 𝜓))
Theorem	bj-nnfei 34842	Nonfreeness implies the equivalent of ax5e 1916, inference form. (Contributed by BJ, 22-Sep-2024.)
⊢ Ⅎ'𝑥𝜑    ⇒   ⊢ (∃𝑥𝜑 → 𝜑)
Theorem	bj-nnfea 34843	Nonfreeness implies the equivalent of ax5ea 1917. (Contributed by BJ, 28-Jul-2023.)
⊢ (Ⅎ'𝑥𝜑 → (∃𝑥𝜑 → ∀𝑥𝜑))
Theorem	bj-nnfead 34844	Nonfreeness implies the equivalent of ax5ea 1917, deduction form. (Contributed by BJ, 2-Dec-2023.)
⊢ (𝜑 → Ⅎ'𝑥𝜓)    ⇒   ⊢ (𝜑 → (∃𝑥𝜓 → ∀𝑥𝜓))
Theorem	bj-nnfeai 34845	Nonfreeness implies the equivalent of ax5ea 1917, inference form. (Contributed by BJ, 22-Sep-2024.)
⊢ Ⅎ'𝑥𝜑    ⇒   ⊢ (∃𝑥𝜑 → ∀𝑥𝜑)
Theorem	bj-dfnnf2 34846	Alternate definition of df-bj-nnf 34833 using only primitive symbols (→, ¬, ∀) in each conjunct. (Contributed by BJ, 20-Aug-2023.)
⊢ (Ⅎ'𝑥𝜑 ↔ ((𝜑 → ∀𝑥𝜑) ∧ (¬ 𝜑 → ∀𝑥 ¬ 𝜑)))
Theorem	bj-nnfnfTEMP 34847	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 1788 except via df-nf 1788 directly. (Proof modification is discouraged.)
⊢ (Ⅎ'𝑥𝜑 → Ⅎ𝑥𝜑)
Theorem	bj-wnfnf 34848	When 𝜑 is substituted for 𝜓, this statement expresses nonfreeness in the weak form of nonfreeness (∃ → ∀). Note that this could also be proved from bj-nnfim 34855, bj-nnfe1 34869 and bj-nnfa1 34868. (Contributed by BJ, 9-Dec-2023.)
⊢ Ⅎ'𝑥(∃𝑥𝜑 → ∀𝑥𝜓)
Theorem	bj-nnfnt 34849	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 34855). Intuitionistically, ⊢ (Ⅎ'𝑥¬ 𝜑 ↔ Ⅎ'𝑥¬ ¬ 𝜑). See nfnt 1860. (Contributed by BJ, 28-Jul-2023.)
⊢ (Ⅎ'𝑥𝜑 ↔ Ⅎ'𝑥 ¬ 𝜑)
Theorem	bj-nnftht 34850	A variable is nonfree in a theorem. The antecedent is in the "strong necessity" modality of modal logic in order not to require sp 2178 (modal T), as in bj-nnfbi 34834. (Contributed by BJ, 28-Jul-2023.)
⊢ ((𝜑 ∧ ∀𝑥𝜑) → Ⅎ'𝑥𝜑)
Theorem	bj-nnfth 34851	A variable is nonfree in a theorem, inference form. (Contributed by BJ, 28-Jul-2023.)
⊢ 𝜑    ⇒   ⊢ Ⅎ'𝑥𝜑
Theorem	bj-nnfnth 34852	A variable is nonfree in the negation of a theorem, inference form. (Contributed by BJ, 27-Aug-2023.)
⊢ ¬ 𝜑    ⇒   ⊢ Ⅎ'𝑥𝜑
Theorem	bj-nnfim1 34853	A consequence of nonfreeness in the antecedent and the consequent of an implication. (Contributed by BJ, 27-Aug-2023.)
⊢ ((Ⅎ'𝑥𝜑 ∧ Ⅎ'𝑥𝜓) → ((𝜑 → 𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓)))
Theorem	bj-nnfim2 34854	A consequence of nonfreeness in the antecedent and the consequent of an implication. (Contributed by BJ, 27-Aug-2023.)
⊢ ((Ⅎ'𝑥𝜑 ∧ Ⅎ'𝑥𝜓) → ((∀𝑥𝜑 → ∃𝑥𝜓) → (𝜑 → 𝜓)))
Theorem	bj-nnfim 34855	Nonfreeness in the antecedent and the consequent of an implication implies nonfreeness in the implication. (Contributed by BJ, 27-Aug-2023.)
⊢ ((Ⅎ'𝑥𝜑 ∧ Ⅎ'𝑥𝜓) → Ⅎ'𝑥(𝜑 → 𝜓))
Theorem	bj-nnfimd 34856	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 34857	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 34855, bj-nnfnt 34849 and bj-nnfbi 34834, but we want a proof valid in intuitionistic logic. (Proof modification is discouraged.)
⊢ ((Ⅎ'𝑥𝜑 ∧ Ⅎ'𝑥𝜓) → Ⅎ'𝑥(𝜑 ∧ 𝜓))
Theorem	bj-nnfand 34858	Nonfreeness in both conjuncts implies nonfreeness in the conjunction, deduction form. Note: compared with the proof of bj-nnfan 34857, 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 34857 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 34858 will generally be easier to understand). (Contributed by BJ, 19-Nov-2023.) (Proof modification is discouraged.)
⊢ (𝜑 → Ⅎ'𝑥𝜓)    &   ⊢ (𝜑 → Ⅎ'𝑥𝜒)    ⇒   ⊢ (𝜑 → Ⅎ'𝑥(𝜓 ∧ 𝜒))
Theorem	bj-nnfor 34859	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 34855, bj-nnfnt 34849 and bj-nnfbi 34834, but we want a proof valid in intuitionistic logic. (Proof modification is discouraged.)
⊢ ((Ⅎ'𝑥𝜑 ∧ Ⅎ'𝑥𝜓) → Ⅎ'𝑥(𝜑 ∨ 𝜓))
Theorem	bj-nnford 34860	Nonfreeness in both disjuncts implies nonfreeness in the disjunction, deduction form. See comments for bj-nnfor 34859 and bj-nnfand 34858. (Contributed by BJ, 2-Dec-2023.) (Proof modification is discouraged.)
⊢ (𝜑 → Ⅎ'𝑥𝜓)    &   ⊢ (𝜑 → Ⅎ'𝑥𝜒)    ⇒   ⊢ (𝜑 → Ⅎ'𝑥(𝜓 ∨ 𝜒))
Theorem	bj-nnfbit 34861	Nonfreeness in both sides implies nonfreeness in the biconditional. (Contributed by BJ, 2-Dec-2023.) (Proof modification is discouraged.)
⊢ ((Ⅎ'𝑥𝜑 ∧ Ⅎ'𝑥𝜓) → Ⅎ'𝑥(𝜑 ↔ 𝜓))
Theorem	bj-nnfbid 34862	Nonfreeness in both sides implies nonfreeness in the biconditional, deduction form. (Contributed by BJ, 2-Dec-2023.) (Proof modification is discouraged.)
⊢ (𝜑 → Ⅎ'𝑥𝜓)    &   ⊢ (𝜑 → Ⅎ'𝑥𝜒)    ⇒   ⊢ (𝜑 → Ⅎ'𝑥(𝜓 ↔ 𝜒))
Theorem	bj-nnfv 34863*	A non-occurring variable is nonfree in a formula. (Contributed by BJ, 28-Jul-2023.)
⊢ Ⅎ'𝑥𝜑
Theorem	bj-nnf-alrim 34864	Proof of the closed form of alrimi 2209 from modalK (compare alrimiv 1931). See also bj-alrim 34802. Actually, most proofs between 19.3t 2197 and 2sbbid 2242 could be proved without ax-12 2173. (Contributed by BJ, 20-Aug-2023.)
⊢ (Ⅎ'𝑥𝜑 → (∀𝑥(𝜑 → 𝜓) → (𝜑 → ∀𝑥𝜓)))
Theorem	bj-nnf-exlim 34865	Proof of the closed form of exlimi 2213 from modalK (compare exlimiv 1934). See also bj-sylget2 34730. (Contributed by BJ, 2-Dec-2023.)
⊢ (Ⅎ'𝑥𝜓 → (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → 𝜓)))
Theorem	bj-dfnnf3 34866	Alternate definition of nonfreeness when sp 2178 is available. (Contributed by BJ, 28-Jul-2023.) The proof should not rely on df-nf 1788. (Proof modification is discouraged.)
⊢ (Ⅎ'𝑥𝜑 ↔ (∃𝑥𝜑 → ∀𝑥𝜑))
Theorem	bj-nfnnfTEMP 34867	New nonfreeness is equivalent to old nonfreeness on core FOL axioms plus sp 2178. (Contributed by BJ, 28-Jul-2023.) The proof should not rely on df-nf 1788 except via df-nf 1788 directly. (Proof modification is discouraged.)
⊢ (Ⅎ'𝑥𝜑 ↔ Ⅎ𝑥𝜑)
Theorem	bj-nnfa1 34868	See nfa1 2150. (Contributed by BJ, 12-Aug-2023.) (Proof modification is discouraged.)
⊢ Ⅎ'𝑥∀𝑥𝜑
Theorem	bj-nnfe1 34869	See nfe1 2149. (Contributed by BJ, 12-Aug-2023.) (Proof modification is discouraged.)
⊢ Ⅎ'𝑥∃𝑥𝜑
Theorem	bj-19.12 34870	See 19.12 2325. Could be labeled "exalimalex" for "'there exists for all' implies 'for all there exists'". This proof is from excom 2164 and modal (B) on top of modalK logic. (Contributed by BJ, 12-Aug-2023.) The proof should not rely on df-nf 1788 or df-bj-nnf 34833, directly or indirectly. (Proof modification is discouraged.)
⊢ (∃𝑥∀𝑦𝜑 → ∀𝑦∃𝑥𝜑)
Theorem	bj-nnflemaa 34871	One of four lemmas for nonfreeness: antecedent and consequent both expressed using universal quantifier. Note: this is bj-hbalt 34790. (Contributed by BJ, 12-Aug-2023.) (Proof modification is discouraged.)
⊢ (∀𝑥(𝜑 → ∀𝑦𝜑) → (∀𝑥𝜑 → ∀𝑦∀𝑥𝜑))
Theorem	bj-nnflemee 34872	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 34873	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 34874	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 34875	See nfal 2321 and bj-nfalt 34820. (Contributed by BJ, 12-Aug-2023.) (Proof modification is discouraged.)
⊢ (∀𝑥Ⅎ'𝑦𝜑 → Ⅎ'𝑦∀𝑥𝜑)
Theorem	bj-nnfext 34876	See nfex 2322 and bj-nfext 34821. (Contributed by BJ, 12-Aug-2023.) (Proof modification is discouraged.)
⊢ (∀𝑥Ⅎ'𝑦𝜑 → Ⅎ'𝑦∃𝑥𝜑)
Theorem	bj-stdpc5t 34877	Alias of bj-nnf-alrim 34864 for labeling consistency (a standard predicate calculus axiom). Closed form of stdpc5 2204 proved from modalK (obsoleting stdpc5v 1942). (Contributed by BJ, 2-Dec-2023.) Use bj-nnf-alrim 34864 instead. (New usaged is discouraged.)
⊢ (Ⅎ'𝑥𝜑 → (∀𝑥(𝜑 → 𝜓) → (𝜑 → ∀𝑥𝜓)))
Theorem	bj-19.21t 34878	Statement 19.21t 2202 proved from modalK (obsoleting 19.21v 1943). (Contributed by BJ, 2-Dec-2023.)
⊢ (Ⅎ'𝑥𝜑 → (∀𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥𝜓)))
Theorem	bj-19.23t 34879	Statement 19.23t 2206 proved from modalK (obsoleting 19.23v 1946). (Contributed by BJ, 2-Dec-2023.)
⊢ (Ⅎ'𝑥𝜓 → (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜓)))
Theorem	bj-19.36im 34880	One direction of 19.36 2226 from the same axioms as 19.36imv 1949. (Contributed by BJ, 2-Dec-2023.)
⊢ (Ⅎ'𝑥𝜓 → (∃𝑥(𝜑 → 𝜓) → (∀𝑥𝜑 → 𝜓)))
Theorem	bj-19.37im 34881	One direction of 19.37 2228 from the same axioms as 19.37imv 1952. (Contributed by BJ, 2-Dec-2023.)
⊢ (Ⅎ'𝑥𝜑 → (∃𝑥(𝜑 → 𝜓) → (𝜑 → ∃𝑥𝜓)))
Theorem	bj-19.42t 34882	Closed form of 19.42 2232 from the same axioms as 19.42v 1958. (Contributed by BJ, 2-Dec-2023.)
⊢ (Ⅎ'𝑥𝜑 → (∃𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥𝜓)))
Theorem	bj-19.41t 34883	Closed form of 19.41 2231 from the same axioms as 19.41v 1954. The same is doable with 19.27 2223, 19.28 2224, 19.31 2230, 19.32 2229, 19.44 2233, 19.45 2234. (Contributed by BJ, 2-Dec-2023.)
⊢ (Ⅎ'𝑥𝜓 → (∃𝑥(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ 𝜓)))
Theorem	bj-sbft 34884	Version of sbft 2265 using Ⅎ', proved from core axioms. (Contributed by BJ, 19-Nov-2023.)
⊢ (Ⅎ'𝑥𝜑 → ([𝑡 / 𝑥]𝜑 ↔ 𝜑))
Theorem	bj-pm11.53vw 34885	Version of pm11.53v 1948 with nonfreeness antecedents. One can also prove the theorem with antecedent (Ⅎ'𝑦∀𝑥𝜑 ∧ ∀𝑦Ⅎ'𝑥𝜓). (Contributed by BJ, 7-Oct-2024.)
⊢ ((∀𝑥Ⅎ'𝑦𝜑 ∧ Ⅎ'𝑥∀𝑦𝜓) → (∀𝑥∀𝑦(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → ∀𝑦𝜓)))
Theorem	bj-pm11.53v 34886	Version of pm11.53v 1948 with nonfreeness antecedents. (Contributed by BJ, 7-Oct-2024.)
⊢ ((∀𝑥Ⅎ'𝑦𝜑 ∧ ∀𝑦Ⅎ'𝑥𝜓) → (∀𝑥∀𝑦(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → ∀𝑦𝜓)))
Theorem	bj-pm11.53a 34887*	A variant of pm11.53v 1948. One can similarly prove a variant with DV (𝑦, 𝜑) and ∀𝑦Ⅎ'𝑥𝜓 instead of DV (𝑥, 𝜓) and ∀𝑥Ⅎ'𝑦𝜑. (Contributed by BJ, 7-Oct-2024.)
⊢ (∀𝑥Ⅎ'𝑦𝜑 → (∀𝑥∀𝑦(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → ∀𝑦𝜓)))
Theorem	bj-equsvt 34888*	A variant of equsv 2007. (Contributed by BJ, 7-Oct-2024.)
⊢ (Ⅎ'𝑥𝜑 → (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜑))
Theorem	bj-equsalvwd 34889*	Variant of equsalvw 2008. (Contributed by BJ, 7-Oct-2024.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → Ⅎ'𝑥𝜒)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥(𝑥 = 𝑦 → 𝜓) ↔ 𝜒))
Theorem	bj-equsexvwd 34890*	Variant of equsexvw 2009. (Contributed by BJ, 7-Oct-2024.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → Ⅎ'𝑥𝜒)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥(𝑥 = 𝑦 ∧ 𝜓) ↔ 𝜒))
Theorem	bj-sbievwd 34891*	Variant of sbievw 2097. (Contributed by BJ, 7-Oct-2024.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → Ⅎ'𝑥𝜒)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ([𝑦 / 𝑥]𝜓 ↔ 𝜒))
20.15.4.11  Adding ax-13
Theorem	bj-axc10 34892	Alternate proof of axc10 2385. Shorter. One can prove a version with DV (𝑥, 𝑦) without ax-13 2372, by using ax6ev 1974 instead of ax6e 2383. (Contributed by BJ, 31-Mar-2021.) (Proof modification is discouraged.)
⊢ (∀𝑥(𝑥 = 𝑦 → ∀𝑥𝜑) → 𝜑)
Theorem	bj-alequex 34893	A fol lemma. See alequexv 2005 for a version with a disjoint variable condition requiring fewer axioms. Can be used to reduce the proof of spimt 2386 from 133 to 112 bytes. (Contributed by BJ, 6-Oct-2018.)
⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → ∃𝑥𝜑)
Theorem	bj-spimt2 34894	A step in the proof of spimt 2386. (Contributed by BJ, 2-May-2019.)
⊢ (∀𝑥(𝑥 = 𝑦 → (𝜑 → 𝜓)) → ((∃𝑥𝜓 → 𝜓) → (∀𝑥𝜑 → 𝜓)))
Theorem	bj-cbv3ta 34895	Closed form of cbv3 2397. (Contributed by BJ, 2-May-2019.)
⊢ (∀𝑥∀𝑦(𝑥 = 𝑦 → (𝜑 → 𝜓)) → ((∀𝑦(∃𝑥𝜓 → 𝜓) ∧ ∀𝑥(𝜑 → ∀𝑦𝜑)) → (∀𝑥𝜑 → ∀𝑦𝜓)))
Theorem	bj-cbv3tb 34896	Closed form of cbv3 2397. (Contributed by BJ, 2-May-2019.)
⊢ (∀𝑥∀𝑦(𝑥 = 𝑦 → (𝜑 → 𝜓)) → ((∀𝑦Ⅎ𝑥𝜓 ∧ ∀𝑥Ⅎ𝑦𝜑) → (∀𝑥𝜑 → ∀𝑦𝜓)))
Theorem	bj-hbsb3t 34897	A theorem close to a closed form of hbsb3 2491. (Contributed by BJ, 2-May-2019.)
⊢ (∀𝑥(𝜑 → ∀𝑦𝜑) → ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑))
Theorem	bj-hbsb3 34898	Shorter proof of hbsb3 2491. (Contributed by BJ, 2-May-2019.) (Proof modification is discouraged.)
⊢ (𝜑 → ∀𝑦𝜑)    ⇒   ⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑)
Theorem	bj-nfs1t 34899	A theorem close to a closed form of nfs1 2492. (Contributed by BJ, 2-May-2019.)
⊢ (∀𝑥(𝜑 → ∀𝑦𝜑) → Ⅎ𝑥[𝑦 / 𝑥]𝜑)
Theorem	bj-nfs1t2 34900	A theorem close to a closed form of nfs1 2492. (Contributed by BJ, 2-May-2019.)
⊢ (∀𝑥Ⅎ𝑦𝜑 → Ⅎ𝑥[𝑦 / 𝑥]𝜑)