P. 371 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 37001-37100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	bj-modalbe 37001	The predicate-calculus version of the axiom (B) of modal logic. See also modal-b 2325. (Contributed by BJ, 20-Oct-2019.)
⊢ (𝜑 → ∀𝑥∃𝑥𝜑)
Theorem	bj-spst 37002	Closed form of sps 2193. Once in main part, prove sps 2193 and spsd 2195 from it. (Contributed by BJ, 20-Oct-2019.)
⊢ ((𝜑 → 𝜓) → (∀𝑥𝜑 → 𝜓))
Theorem	bj-19.21bit 37003	Closed form of 19.21bi 2197. (Contributed by BJ, 20-Oct-2019.)
⊢ ((𝜑 → ∀𝑥𝜓) → (𝜑 → 𝜓))
Theorem	bj-19.23bit 37004	Closed form of 19.23bi 2199. (Contributed by BJ, 20-Oct-2019.)
⊢ ((∃𝑥𝜑 → 𝜓) → (𝜑 → 𝜓))
Theorem	bj-nexrt 37005	Closed form of nexr 2200. Contrapositive of 19.8a 2189. (Contributed by BJ, 20-Oct-2019.)
⊢ (¬ ∃𝑥𝜑 → ¬ 𝜑)
Theorem	bj-alrim 37006	Closed form of alrimi 2221. (Contributed by BJ, 2-May-2019.)
⊢ (Ⅎ𝑥𝜑 → (∀𝑥(𝜑 → 𝜓) → (𝜑 → ∀𝑥𝜓)))
Theorem	bj-alrim2 37007	Uncurried (imported) form of bj-alrim 37006. (Contributed by BJ, 2-May-2019.)
⊢ ((Ⅎ𝑥𝜑 ∧ ∀𝑥(𝜑 → 𝜓)) → (𝜑 → ∀𝑥𝜓))
Theorem	bj-nfdt0 37008	A theorem close to a closed form of nf5d 2291 and nf5dh 2153. (Contributed by BJ, 2-May-2019.)
⊢ (∀𝑥(𝜑 → (𝜓 → ∀𝑥𝜓)) → (∀𝑥𝜑 → Ⅎ𝑥𝜓))
Theorem	bj-nfdt 37009	Closed form of nf5d 2291 and nf5dh 2153. (Contributed by BJ, 2-May-2019.)
⊢ (∀𝑥(𝜑 → (𝜓 → ∀𝑥𝜓)) → ((𝜑 → ∀𝑥𝜑) → (𝜑 → Ⅎ𝑥𝜓)))
Theorem	bj-nexdt 37010	Closed form of nexd 2229. (Contributed by BJ, 20-Oct-2019.)
⊢ (Ⅎ𝑥𝜑 → (∀𝑥(𝜑 → ¬ 𝜓) → (𝜑 → ¬ ∃𝑥𝜓)))
Theorem	bj-nexdvt 37011*	Closed form of nexdv 1938. (Contributed by BJ, 20-Oct-2019.)
⊢ (∀𝑥(𝜑 → ¬ 𝜓) → (𝜑 → ¬ ∃𝑥𝜓))
Theorem	bj-alexbiex 37012	Adding a second quantifier over the same variable is a transparent operation, (∀∃ case). (Contributed by BJ, 20-Oct-2019.)
⊢ (∀𝑥∃𝑥𝜑 ↔ ∃𝑥𝜑)
Theorem	bj-exexbiex 37013	Adding a second quantifier over the same variable is a transparent operation, (∃∃ case). (Contributed by BJ, 20-Oct-2019.)
⊢ (∃𝑥∃𝑥𝜑 ↔ ∃𝑥𝜑)
Theorem	bj-alalbial 37014	Adding a second quantifier over the same variable is a transparent operation, (∀∀ case). (Contributed by BJ, 20-Oct-2019.)
⊢ (∀𝑥∀𝑥𝜑 ↔ ∀𝑥𝜑)
Theorem	bj-exalbial 37015	Adding a second quantifier over the same variable is a transparent operation, (∃∀ case). (Contributed by BJ, 20-Oct-2019.)
⊢ (∃𝑥∀𝑥𝜑 ↔ ∀𝑥𝜑)
Theorem	bj-19.9htbi 37016	Strengthening 19.9ht 2326 by replacing its consequent with a biconditional (19.9t 2212 does have a biconditional consequent). This propagates. (Contributed by BJ, 20-Oct-2019.)
⊢ (∀𝑥(𝜑 → ∀𝑥𝜑) → (∃𝑥𝜑 ↔ 𝜑))
Theorem	bj-hbntbi 37017	Strengthening hbnt 2301 by replacing its consequent with a biconditional. See also hbntg 36001 and hbntal 44998. (Contributed by BJ, 20-Oct-2019.) Proved from bj-19.9htbi 37016. (Proof modification is discouraged.)
⊢ (∀𝑥(𝜑 → ∀𝑥𝜑) → (¬ 𝜑 ↔ ∀𝑥 ¬ 𝜑))
Theorem	bj-biexal1 37018	A general FOL biconditional that generalizes 19.9ht 2326 among others. For this and the following theorems, see also 19.35 1879, 19.21 2215, 19.23 2219. When 𝜑 is substituted for 𝜓, both sides express a form of nonfreeness. (Contributed by BJ, 20-Oct-2019.)
⊢ (∀𝑥(𝜑 → ∀𝑥𝜓) ↔ (∃𝑥𝜑 → ∀𝑥𝜓))
Theorem	bj-biexal2 37019	When 𝜑 is substituted for 𝜓, both sides express a form of nonfreeness. (Contributed by BJ, 20-Oct-2019.)
⊢ (∀𝑥(∃𝑥𝜑 → 𝜓) ↔ (∃𝑥𝜑 → ∀𝑥𝜓))
Theorem	bj-biexal3 37020	When 𝜑 is substituted for 𝜓, both sides express a form of nonfreeness. (Contributed by BJ, 20-Oct-2019.)
⊢ (∀𝑥(𝜑 → ∀𝑥𝜓) ↔ ∀𝑥(∃𝑥𝜑 → 𝜓))
Theorem	bj-bialal 37021	When 𝜑 is substituted for 𝜓, both sides express a form of nonfreeness. (Contributed by BJ, 20-Oct-2019.)
⊢ (∀𝑥(∀𝑥𝜑 → 𝜓) ↔ (∀𝑥𝜑 → ∀𝑥𝜓))
Theorem	bj-biexex 37022	When 𝜑 is substituted for 𝜓, both sides express a form of nonfreeness. (Contributed by BJ, 20-Oct-2019.)
⊢ (∀𝑥(𝜑 → ∃𝑥𝜓) ↔ (∃𝑥𝜑 → ∃𝑥𝜓))
Theorem	bj-hbexd 37023	A more general instance of the deduction form of hbex 2331. (Contributed by BJ, 4-Apr-2026.)
⊢ (𝜑 → ∀𝑦𝜓)    &   ⊢ (𝜓 → (𝜒 → ∀𝑥𝜃))    ⇒   ⊢ (𝜑 → (∃𝑦𝜒 → ∀𝑥∃𝑦𝜃))
Theorem	bj-hbext 37024	Closed form of bj-hbex 37025 and hbex 2331. (Contributed by BJ, 10-Oct-2019.)
⊢ (∀𝑦∀𝑥(𝜑 → ∀𝑥𝜓) → (∃𝑦𝜑 → ∀𝑥∃𝑦𝜓))
Theorem	bj-hbex 37025	A more general instance of hbex 2331. (Contributed by BJ, 4-Apr-2026.)
⊢ (𝜑 → ∀𝑥𝜓)    ⇒   ⊢ (∃𝑦𝜑 → ∀𝑥∃𝑦𝜓)
Theorem	bj-nfalt 37026	Closed form of nfal 2329. (Contributed by BJ, 2-May-2019.)
⊢ (∀𝑥Ⅎ𝑦𝜑 → Ⅎ𝑦∀𝑥𝜑)
Theorem	bj-nfext 37027	Closed form of nfex 2330. (Contributed by BJ, 10-Oct-2019.)
⊢ (∀𝑥Ⅎ𝑦𝜑 → Ⅎ𝑦∃𝑥𝜑)
Theorem	bj-eeanvw 37028*	Version of exdistrv 1957 with a disjoint variable condition on 𝑥, 𝑦 not requiring ax-11 2163. (The same can be done with eeeanv 2355 and ee4anv 2356.) (Contributed by BJ, 29-Sep-2019.) (Proof modification is discouraged.)
⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ ∃𝑦𝜓))
Theorem	bj-modal4 37029	First-order logic form of the modal axiom (4). See hba1 2300. This is the standard proof of the implication in modal logic (B5 ⇒ 4). Its dual statement is bj-modal4e 37030. (Contributed by BJ, 12-Aug-2023.) (Proof modification is discouraged.)
⊢ (∀𝑥𝜑 → ∀𝑥∀𝑥𝜑)
Theorem	bj-modal4e 37030	First-order logic form of the modal axiom (4) using existential quantifiers. Dual statement of bj-modal4 37029 (hba1 2300). (Contributed by BJ, 21-Dec-2020.) (Proof modification is discouraged.)
⊢ (∃𝑥∃𝑥𝜑 → ∃𝑥𝜑)
Theorem	bj-modalb 37031	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 37032	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 37033	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 37034	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 37035	When 𝜑 is substituted for 𝜓, this statement expresses that weak nonfreeness implies the existential form of nonfreeness. (Contributed by BJ, 9-Dec-2023.)
⊢ ((∃𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(∃𝑥𝜑 → 𝜓))
Theorem	bj-19.12 37036	See 19.12 2333. Could be labeled "exalimalex" for "'there exists for all' implies 'for all there exists'". This proof is from excom 2168 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 37040, directly or indirectly. (Proof modification is discouraged.)
⊢ (∃𝑥∀𝑦𝜑 → ∀𝑦∃𝑥𝜑)
21.19.4.11  Really adding ax-12 The results in the previous section, as actually many theorems of the main part using ax-12 2185, actually only require sp 2191 (which is proved using ax-12 2185).
Theorem	bj-substax12 37037	Equivalent form of the axiom of substitution bj-ax12 36967. Although both sides need a DV condition on 𝑥, 𝑡 (or as in bj-ax12v3 36998 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 37038. Note that in the LHS, the reverse implication holds by equs4 2421 (or equs4v 2002 if a DV condition is added on 𝑥, 𝑡 as in bj-ax12 36967), and the forward implication is sbalex 2250. 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 37038*	Weak form of the LHS of bj-substax12 37037 proved from the core axiom schemes. Compare ax12w 2139. (Contributed by BJ, 26-May-2024.) (Proof modification is discouraged.)
⊢ (𝑥 = 𝑡 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥(𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑))
21.19.4.12  Nonfreeness
Syntax	wnnf 37039	Syntax for the nonfreeness quantifier.
wff Ⅎ'𝑥𝜑
Definition	df-bj-nnf 37040	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 1912 and ax5e 1914. 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 37081, 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 2165 and excom 2168 (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 1912, ax5e 1914, ax5ea 1915. 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 37060 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 37081, 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 37065, bj-nnfnt 37063, bj-nnfan 37067, bj-nnfor 37069, bj-nnfbit 37071, bj-nnfalt 37103, bj-nnfext 37104. 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 37065 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 37103 yields ((∀𝑦∀𝑥1 ...∀𝑥m Ⅎ'𝑥𝜑 → Ⅎ'𝑥∀𝑦 PHI), {{𝑥, 𝑎} ∣ 𝑎 ∈ OC(∀𝑦 PHI) ∖ {𝜑}}) and similarly for antecedents which are conjunctions as in the statement of the lemma. Note bj-nnfalt 37103 and bj-nnfext 37104 are proved from positive propositional calculus with alcom 2165 and excom 2168 (possibly weakened by a DV condition on the quantifying variables), and modalB (via bj-19.12 37036). 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 1912 or ax5e 1914 or ax5ea 1915. 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 37041 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 1914 or ax5ea 1915, we would use bj-nnfe 37044 or bj-nnfea 37047 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 1797, by bj-nnf-alrim 37058 and bj-nnfa1 37097 (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 1983. QED Compared with df-nf 1786, the present definition is stricter on positive propositional calculus (bj-nnfnfTEMP 37053) and equivalent on core FOL plus sp 2191 (bj-nfnnfTEMP 37095). While being stricter, it still holds for non-occurring variables (bj-nnfv 37081), 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 2147 to work with), and also not to have redundant conjuncts when full metacomplete FOL= is developed. (Contributed by BJ, 28-Jul-2023.)
⊢ (Ⅎ'𝑥𝜑 ↔ ((∃𝑥𝜑 → 𝜑) ∧ (𝜑 → ∀𝑥𝜑)))
Theorem	bj-nnfa 37041	Nonfreeness implies the equivalent of ax-5 1912. See nf5r 2202. (Contributed by BJ, 28-Jul-2023.)
⊢ (Ⅎ'𝑥𝜑 → (𝜑 → ∀𝑥𝜑))
Theorem	bj-nnfad 37042	Nonfreeness implies the equivalent of ax-5 1912, deduction form. See nf5rd 2204. (Contributed by BJ, 2-Dec-2023.)
⊢ (𝜑 → Ⅎ'𝑥𝜓)    ⇒   ⊢ (𝜑 → (𝜓 → ∀𝑥𝜓))
Theorem	bj-nnfai 37043	Nonfreeness implies the equivalent of ax-5 1912, inference form. See nf5ri 2203. (Contributed by BJ, 22-Sep-2024.)
⊢ Ⅎ'𝑥𝜑    ⇒   ⊢ (𝜑 → ∀𝑥𝜑)
Theorem	bj-nnfe 37044	Nonfreeness implies the equivalent of ax5e 1914. (Contributed by BJ, 28-Jul-2023.)
⊢ (Ⅎ'𝑥𝜑 → (∃𝑥𝜑 → 𝜑))
Theorem	bj-nnfed 37045	Nonfreeness implies the equivalent of ax5e 1914, deduction form. (Contributed by BJ, 2-Dec-2023.)
⊢ (𝜑 → Ⅎ'𝑥𝜓)    ⇒   ⊢ (𝜑 → (∃𝑥𝜓 → 𝜓))
Theorem	bj-nnfei 37046	Nonfreeness implies the equivalent of ax5e 1914, inference form. (Contributed by BJ, 22-Sep-2024.)
⊢ Ⅎ'𝑥𝜑    ⇒   ⊢ (∃𝑥𝜑 → 𝜑)
Theorem	bj-nnfea 37047	Nonfreeness implies the equivalent of ax5ea 1915. (Contributed by BJ, 28-Jul-2023.)
⊢ (Ⅎ'𝑥𝜑 → (∃𝑥𝜑 → ∀𝑥𝜑))
Theorem	bj-nnfead 37048	Nonfreeness implies the equivalent of ax5ea 1915, deduction form. (Contributed by BJ, 2-Dec-2023.)
⊢ (𝜑 → Ⅎ'𝑥𝜓)    ⇒   ⊢ (𝜑 → (∃𝑥𝜓 → ∀𝑥𝜓))
Theorem	bj-nnfeai 37049	Nonfreeness implies the equivalent of ax5ea 1915, inference form. (Contributed by BJ, 22-Sep-2024.)
⊢ Ⅎ'𝑥𝜑    ⇒   ⊢ (∃𝑥𝜑 → ∀𝑥𝜑)
Theorem	bj-alnnf 37050	In deduction-style proofs, it is equivalent to assert that the context holds for all values of a variable, or that is does not depend on that variable. (Contributed by BJ, 28-Mar-2026.)
⊢ ((𝜑 → ∀𝑥𝜑) ↔ (𝜑 → Ⅎ'𝑥𝜑))
Theorem	bj-alnnf2 37051	If a proposition holds, then it holds for all values of a given variable if and only if it does not depend on that variable. (Contributed by BJ, 28-Mar-2026.)
⊢ (𝜑 → (∀𝑥𝜑 ↔ Ⅎ'𝑥𝜑))
Theorem	bj-dfnnf2 37052	Alternate definition of df-bj-nnf 37040 using only primitive symbols (→, ¬, ∀) in each conjunct. (Contributed by BJ, 20-Aug-2023.)
⊢ (Ⅎ'𝑥𝜑 ↔ ((𝜑 → ∀𝑥𝜑) ∧ (¬ 𝜑 → ∀𝑥 ¬ 𝜑)))
Theorem	bj-nnfnfTEMP 37053	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-nnfim1 37054	A consequence of nonfreeness in the antecedent and the consequent of an implication. (Contributed by BJ, 27-Aug-2023.)
⊢ ((Ⅎ'𝑥𝜑 ∧ Ⅎ'𝑥𝜓) → ((𝜑 → 𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓)))
Theorem	bj-nnfim2 37055	A consequence of nonfreeness in the antecedent and the consequent of an implication. (Contributed by BJ, 27-Aug-2023.)
⊢ ((Ⅎ'𝑥𝜑 ∧ Ⅎ'𝑥𝜓) → ((∀𝑥𝜑 → ∃𝑥𝜓) → (𝜑 → 𝜓)))
Theorem	bj-nnftht 37056	A variable is nonfree in a theorem. The antecedent is in the "strong necessity" modality of modal logic in order not to require sp 2191 (modal T), as in bj-nnfbi 37060. (Contributed by BJ, 28-Jul-2023.)
⊢ ((𝜑 ∧ ∀𝑥𝜑) → Ⅎ'𝑥𝜑)
Theorem	bj-nnfth 37057	A variable is nonfree in a theorem, inference form. (Contributed by BJ, 28-Jul-2023.)
⊢ 𝜑    ⇒   ⊢ Ⅎ'𝑥𝜑
Theorem	bj-nnf-alrim 37058	Proof of the closed form of alrimi 2221 from modalK (compare alrimiv 1929). See also bj-alrim 37006. Actually, most proofs between 19.3t 2209 and 2sbbid 2255 could be proved without ax-12 2185. (Contributed by BJ, 20-Aug-2023.)
⊢ (Ⅎ'𝑥𝜑 → (∀𝑥(𝜑 → 𝜓) → (𝜑 → ∀𝑥𝜓)))
Theorem	bj-stdpc5t 37059	Alias of bj-nnf-alrim 37058 for labeling consistency (a standard predicate calculus axiom). Closed form of stdpc5 2216 proved from modalK (obsoleting stdpc5v 1940). (Contributed by BJ, 2-Dec-2023.) Use bj-nnf-alrim 37058 instead. (New usaged is discouraged.)
⊢ (Ⅎ'𝑥𝜑 → (∀𝑥(𝜑 → 𝜓) → (𝜑 → ∀𝑥𝜓)))
Theorem	bj-nnfbi 37060	If two formulas are equivalent, then nonfreeness of a variable in one of them is equivalent to nonfreeness in the other. Compare nfbiit 1853. From this and bj-nnfim 37065 and bj-nnfnt 37063, 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 37056) in order not to require sp 2191 (modal T). (Contributed by BJ, 27-Aug-2023.)
⊢ (((𝜑 ↔ 𝜓) ∧ ∀𝑥(𝜑 ↔ 𝜓)) → (Ⅎ'𝑥𝜑 ↔ Ⅎ'𝑥𝜓))
Theorem	bj-nnfbd0 37061	If two formulas are equivalent, then nonfreeness of a variable in one of them is equivalent to nonfreeness in the other, deduction form. The antecedent of the conclusion is in the "strong necessity" modality of modal logic (see also bj-nnftht 37056) in order not to require sp 2191 (modal T). See bj-nnfbi 37060. (Contributed by BJ, 21-Mar-2026.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ ((𝜑 ∧ ∀𝑥𝜑) → (Ⅎ'𝑥𝜓 ↔ Ⅎ'𝑥𝜒))
Theorem	bj-nnfbii 37062	If two formulas are equivalent, then nonfreeness of a variable in one of them is equivalent to nonfreeness in the other, inference form. See bj-nnfbi 37060. (Contributed by BJ, 18-Nov-2023.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (Ⅎ'𝑥𝜑 ↔ Ⅎ'𝑥𝜓)
Theorem	bj-nnfnt 37063	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 37065). Intuitionistically, ⊢ (Ⅎ'𝑥¬ 𝜑 ↔ Ⅎ'𝑥¬ ¬ 𝜑). See nfnt 1858. (Contributed by BJ, 28-Jul-2023.)
⊢ (Ⅎ'𝑥𝜑 ↔ Ⅎ'𝑥 ¬ 𝜑)
Theorem	bj-nnfnth 37064	A variable is nonfree in the negation of a theorem, inference form. (Contributed by BJ, 27-Aug-2023.)
⊢ ¬ 𝜑    ⇒   ⊢ Ⅎ'𝑥𝜑
Theorem	bj-nnfim 37065	Nonfreeness in the antecedent and the consequent of an implication implies nonfreeness in the implication. (Contributed by BJ, 27-Aug-2023.)
⊢ ((Ⅎ'𝑥𝜑 ∧ Ⅎ'𝑥𝜓) → Ⅎ'𝑥(𝜑 → 𝜓))
Theorem	bj-nnfimd 37066	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 37067	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 37065, bj-nnfnt 37063 and bj-nnfbi 37060, but we want a proof valid in intuitionistic logic. (Proof modification is discouraged.)
⊢ ((Ⅎ'𝑥𝜑 ∧ Ⅎ'𝑥𝜓) → Ⅎ'𝑥(𝜑 ∧ 𝜓))
Theorem	bj-nnfand 37068	Nonfreeness in both conjuncts implies nonfreeness in the conjunction, deduction form. Note: compared with the proof of bj-nnfan 37067, 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 37067 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 37068 will generally be easier to understand). (Contributed by BJ, 19-Nov-2023.) (Proof modification is discouraged.)
⊢ (𝜑 → Ⅎ'𝑥𝜓)    &   ⊢ (𝜑 → Ⅎ'𝑥𝜒)    ⇒   ⊢ (𝜑 → Ⅎ'𝑥(𝜓 ∧ 𝜒))
Theorem	bj-nnfor 37069	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 37065, bj-nnfnt 37063 and bj-nnfbi 37060, but we want a proof valid in intuitionistic logic. (Proof modification is discouraged.)
⊢ ((Ⅎ'𝑥𝜑 ∧ Ⅎ'𝑥𝜓) → Ⅎ'𝑥(𝜑 ∨ 𝜓))
Theorem	bj-nnford 37070	Nonfreeness in both disjuncts implies nonfreeness in the disjunction, deduction form. See comments for bj-nnfor 37069 and bj-nnfand 37068. (Contributed by BJ, 2-Dec-2023.) (Proof modification is discouraged.)
⊢ (𝜑 → Ⅎ'𝑥𝜓)    &   ⊢ (𝜑 → Ⅎ'𝑥𝜒)    ⇒   ⊢ (𝜑 → Ⅎ'𝑥(𝜓 ∨ 𝜒))
Theorem	bj-nnfbit 37071	Nonfreeness in both sides implies nonfreeness in the biconditional. (Contributed by BJ, 2-Dec-2023.) (Proof modification is discouraged.)
⊢ ((Ⅎ'𝑥𝜑 ∧ Ⅎ'𝑥𝜓) → Ⅎ'𝑥(𝜑 ↔ 𝜓))
Theorem	bj-nnfbid 37072	Nonfreeness in both sides implies nonfreeness in the biconditional, deduction form. (Contributed by BJ, 2-Dec-2023.) (Proof modification is discouraged.)
⊢ (𝜑 → Ⅎ'𝑥𝜓)    &   ⊢ (𝜑 → Ⅎ'𝑥𝜒)    ⇒   ⊢ (𝜑 → Ⅎ'𝑥(𝜓 ↔ 𝜒))
Theorem	bj-nnf-exlim 37073	Proof of the closed form of exlimi 2225 from modalK (compare exlimiv 1932). See also bj-sylget2 36915. (Contributed by BJ, 2-Dec-2023.)
⊢ (Ⅎ'𝑥𝜓 → (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → 𝜓)))
Theorem	bj-19.21t 37074	Statement 19.21t 2214 proved from modalK (obsoleting 19.21v 1941). (Contributed by BJ, 2-Dec-2023.)
⊢ (Ⅎ'𝑥𝜑 → (∀𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥𝜓)))
Theorem	bj-19.23t 37075	Statement 19.23t 2218 proved from modalK (obsoleting 19.23v 1944). (Contributed by BJ, 2-Dec-2023.)
⊢ (Ⅎ'𝑥𝜓 → (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜓)))
Theorem	bj-19.36im 37076	One direction of 19.36 2238 from the same axioms as 19.36imv 1947. (Contributed by BJ, 2-Dec-2023.)
⊢ (Ⅎ'𝑥𝜓 → (∃𝑥(𝜑 → 𝜓) → (∀𝑥𝜑 → 𝜓)))
Theorem	bj-19.37im 37077	One direction of 19.37 2240 from the same axioms as 19.37imv 1949. (Contributed by BJ, 2-Dec-2023.)
⊢ (Ⅎ'𝑥𝜑 → (∃𝑥(𝜑 → 𝜓) → (𝜑 → ∃𝑥𝜓)))
Theorem	bj-19.42t 37078	Closed form of 19.42 2244 from the same axioms as 19.42v 1955. (Contributed by BJ, 2-Dec-2023.)
⊢ (Ⅎ'𝑥𝜑 → (∃𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥𝜓)))
Theorem	bj-19.41t 37079	Closed form of 19.41 2243 from the same axioms as 19.41v 1951. The same is doable with 19.27 2235, 19.28 2236, 19.31 2242, 19.32 2241, 19.44 2245, 19.45 2246. (Contributed by BJ, 2-Dec-2023.)
⊢ (Ⅎ'𝑥𝜓 → (∃𝑥(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ 𝜓)))
Theorem	bj-pm11.53vw 37080	Version of pm11.53v 1946 with nonfreeness antecedents. One can also prove the theorem with antecedent (Ⅎ'𝑦∀𝑥𝜑 ∧ ∀𝑦Ⅎ'𝑥𝜓). (Contributed by BJ, 7-Oct-2024.)
⊢ ((∀𝑥Ⅎ'𝑦𝜑 ∧ Ⅎ'𝑥∀𝑦𝜓) → (∀𝑥∀𝑦(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → ∀𝑦𝜓)))
Theorem	bj-nnfv 37081*	A non-occurring variable is nonfree in a formula. (Contributed by BJ, 28-Jul-2023.)
⊢ Ⅎ'𝑥𝜑
Theorem	bj-nnfbd 37082*	If two formulas are equivalent, then nonfreeness of a variable in one of them is equivalent to nonfreeness in the other, deduction form. See bj-nnfbi 37060. (Contributed by BJ, 27-Aug-2023.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (Ⅎ'𝑥𝜓 ↔ Ⅎ'𝑥𝜒))
Theorem	bj-pm11.53a 37083*	A variant of pm11.53v 1946. One can similarly prove a variant with DV (𝑦, 𝜑) and ∀𝑦Ⅎ'𝑥𝜓 instead of DV (𝑥, 𝜓) and ∀𝑥Ⅎ'𝑦𝜑. (Contributed by BJ, 7-Oct-2024.)
⊢ (∀𝑥Ⅎ'𝑦𝜑 → (∀𝑥∀𝑦(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → ∀𝑦𝜓)))
Theorem	bj-equsvt 37084*	A variant of equsv 2005. (Contributed by BJ, 7-Oct-2024.)
⊢ (Ⅎ'𝑥𝜑 → (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜑))
Theorem	bj-equsalvwd 37085*	Variant of equsalvw 2006. (Contributed by BJ, 7-Oct-2024.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → Ⅎ'𝑥𝜒)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥(𝑥 = 𝑦 → 𝜓) ↔ 𝜒))
Theorem	bj-equsexvwd 37086*	Variant of equsexvw 2007. (Contributed by BJ, 7-Oct-2024.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → Ⅎ'𝑥𝜒)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥(𝑥 = 𝑦 ∧ 𝜓) ↔ 𝜒))
Theorem	bj-nnf-spim 37087*	A universal specialization result in deduction form, proved from ax-1 6 -- ax-6 1969, where the only DV condition is on 𝑥, 𝑦 and where 𝑥 should be nonfree in the new proposition 𝜒 (and in the context 𝜑). (Contributed by BJ, 4-Apr-2026.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → Ⅎ'𝑥𝜒)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 → 𝜒))
Theorem	bj-nnf-spime 37088*	An existential generalization result in deduction form, from ax-1 6-- ax-6 1969, where the only DV condition is on 𝑥, 𝑦, and where 𝑥 should be nonfree in the new proposition 𝜒 (and in the context 𝜑). (Contributed by BJ, 4-Apr-2026.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → Ⅎ'𝑥𝜓)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (𝜓 → ∃𝑥𝜒))
Theorem	bj-nnf-cbvaliv 37089*	The only DV conditions are those saying that 𝑦 is a fresh variable used to construct 𝜒. (Contributed by BJ, 4-Apr-2026.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → Ⅎ'𝑥𝜒)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 → ∀𝑦𝜒))
Theorem	bj-sbievwd 37090*	Variant of sbievw 2099. (Contributed by BJ, 7-Oct-2024.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → Ⅎ'𝑥𝜒)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ([𝑦 / 𝑥]𝜓 ↔ 𝜒))
Theorem	bj-sbft 37091	Version of sbft 2277 using Ⅎ', proved from core axioms. (Contributed by BJ, 19-Nov-2023.)
⊢ (Ⅎ'𝑥𝜑 → ([𝑡 / 𝑥]𝜑 ↔ 𝜑))
Theorem	bj-nnf-cbvali 37092*	Compared with bj-nnf-cbvaliv 37089, replacing the DV condition on 𝑦, 𝜓 with the nonfreeness condition requires ax-11 2163. (Contributed by BJ, 4-Apr-2026.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → ∀𝑦𝜑)    &   ⊢ (𝜑 → Ⅎ'𝑦𝜓)    &   ⊢ (𝜑 → Ⅎ'𝑥𝜒)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 → ∀𝑦𝜒))
Theorem	bj-nnf-cbval 37093*	Compared with cbvalv1 2346, this saves ax-12 2185. (Contributed by BJ, 4-Apr-2026.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → ∀𝑦𝜑)    &   ⊢ (𝜑 → Ⅎ'𝑦𝜓)    &   ⊢ (𝜑 → Ⅎ'𝑥𝜒)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒))
Theorem	bj-dfnnf3 37094	Alternate definition of nonfreeness when sp 2191 is available. (Contributed by BJ, 28-Jul-2023.) The proof should not rely on df-nf 1786. (Proof modification is discouraged.)
⊢ (Ⅎ'𝑥𝜑 ↔ (∃𝑥𝜑 → ∀𝑥𝜑))
Theorem	bj-nfnnfTEMP 37095	New nonfreeness is equivalent to old nonfreeness on core FOL axioms plus sp 2191. (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 37096	When 𝜑 is substituted for 𝜓, this statement expresses nonfreeness in the weak form of nonfreeness (∃ → ∀). Note that this could also be proved from bj-nnfim 37065, bj-nnfe1 37098 and bj-nnfa1 37097. (Contributed by BJ, 9-Dec-2023.)
⊢ Ⅎ'𝑥(∃𝑥𝜑 → ∀𝑥𝜓)
Theorem	bj-nnfa1 37097	See nfa1 2157. (Contributed by BJ, 12-Aug-2023.) (Proof modification is discouraged.)
⊢ Ⅎ'𝑥∀𝑥𝜑
Theorem	bj-nnfe1 37098	See nfe1 2156. (Contributed by BJ, 12-Aug-2023.) (Proof modification is discouraged.)
⊢ Ⅎ'𝑥∃𝑥𝜑
Theorem	bj-nnflemaa 37099	One of four lemmas for nonfreeness: antecedent and consequent both expressed using universal quantifier. Note: this is bj-hbalt 36993. (Contributed by BJ, 12-Aug-2023.) (Proof modification is discouraged.)
⊢ (∀𝑥(𝜑 → ∀𝑦𝜓) → (∀𝑥𝜑 → ∀𝑦∀𝑥𝜓))
Theorem	bj-nnflemee 37100	One of four lemmas for nonfreeness: antecedent and consequent both expressed using existential quantifier. (Contributed by BJ, 12-Aug-2023.) (Proof modification is discouraged.)
⊢ (∀𝑥(∃𝑦𝜑 → 𝜓) → (∃𝑦∃𝑥𝜑 → ∃𝑥𝜓))