P. 370 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 36901-37000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	bj-exexbiex 36901	Adding a second quantifier over the same variable is a transparent operation, (∃∃ case). (Contributed by BJ, 20-Oct-2019.)
⊢ (∃𝑥∃𝑥𝜑 ↔ ∃𝑥𝜑)
Theorem	bj-alalbial 36902	Adding a second quantifier over the same variable is a transparent operation, (∀∀ case). (Contributed by BJ, 20-Oct-2019.)
⊢ (∀𝑥∀𝑥𝜑 ↔ ∀𝑥𝜑)
Theorem	bj-exalbial 36903	Adding a second quantifier over the same variable is a transparent operation, (∃∀ case). (Contributed by BJ, 20-Oct-2019.)
⊢ (∃𝑥∀𝑥𝜑 ↔ ∀𝑥𝜑)
Theorem	bj-19.9htbi 36904	Strengthening 19.9ht 2325 by replacing its consequent with a biconditional (19.9t 2211 does have a biconditional consequent). This propagates. (Contributed by BJ, 20-Oct-2019.)
⊢ (∀𝑥(𝜑 → ∀𝑥𝜑) → (∃𝑥𝜑 ↔ 𝜑))
Theorem	bj-hbntbi 36905	Strengthening hbnt 2300 by replacing its consequent with a biconditional. See also hbntg 35997 and hbntal 44790. (Contributed by BJ, 20-Oct-2019.) Proved from bj-19.9htbi 36904. (Proof modification is discouraged.)
⊢ (∀𝑥(𝜑 → ∀𝑥𝜑) → (¬ 𝜑 ↔ ∀𝑥 ¬ 𝜑))
Theorem	bj-biexal1 36906	A general FOL biconditional that generalizes 19.9ht 2325 among others. For this and the following theorems, see also 19.35 1878, 19.21 2214, 19.23 2218. When 𝜑 is substituted for 𝜓, both sides express a form of nonfreeness. (Contributed by BJ, 20-Oct-2019.)
⊢ (∀𝑥(𝜑 → ∀𝑥𝜓) ↔ (∃𝑥𝜑 → ∀𝑥𝜓))
Theorem	bj-biexal2 36907	When 𝜑 is substituted for 𝜓, both sides express a form of nonfreeness. (Contributed by BJ, 20-Oct-2019.)
⊢ (∀𝑥(∃𝑥𝜑 → 𝜓) ↔ (∃𝑥𝜑 → ∀𝑥𝜓))
Theorem	bj-biexal3 36908	When 𝜑 is substituted for 𝜓, both sides express a form of nonfreeness. (Contributed by BJ, 20-Oct-2019.)
⊢ (∀𝑥(𝜑 → ∀𝑥𝜓) ↔ ∀𝑥(∃𝑥𝜑 → 𝜓))
Theorem	bj-bialal 36909	When 𝜑 is substituted for 𝜓, both sides express a form of nonfreeness. (Contributed by BJ, 20-Oct-2019.)
⊢ (∀𝑥(∀𝑥𝜑 → 𝜓) ↔ (∀𝑥𝜑 → ∀𝑥𝜓))
Theorem	bj-biexex 36910	When 𝜑 is substituted for 𝜓, both sides express a form of nonfreeness. (Contributed by BJ, 20-Oct-2019.)
⊢ (∀𝑥(𝜑 → ∃𝑥𝜓) ↔ (∃𝑥𝜑 → ∃𝑥𝜓))
Theorem	bj-hbext 36911	Closed form of hbex 2330. (Contributed by BJ, 10-Oct-2019.)
⊢ (∀𝑦∀𝑥(𝜑 → ∀𝑥𝜑) → (∃𝑦𝜑 → ∀𝑥∃𝑦𝜑))
Theorem	bj-nfalt 36912	Closed form of nfal 2328. (Contributed by BJ, 2-May-2019.)
⊢ (∀𝑥Ⅎ𝑦𝜑 → Ⅎ𝑦∀𝑥𝜑)
Theorem	bj-nfext 36913	Closed form of nfex 2329. (Contributed by BJ, 10-Oct-2019.)
⊢ (∀𝑥Ⅎ𝑦𝜑 → Ⅎ𝑦∃𝑥𝜑)
Theorem	bj-eeanvw 36914*	Version of exdistrv 1956 with a disjoint variable condition on 𝑥, 𝑦 not requiring ax-11 2162. (The same can be done with eeeanv 2354 and ee4anv 2355.) (Contributed by BJ, 29-Sep-2019.) (Proof modification is discouraged.)
⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ ∃𝑦𝜓))
Theorem	bj-modal4 36915	First-order logic form of the modal axiom (4). See hba1 2299. This is the standard proof of the implication in modal logic (B5 ⇒ 4). Its dual statement is bj-modal4e 36916. (Contributed by BJ, 12-Aug-2023.) (Proof modification is discouraged.)
⊢ (∀𝑥𝜑 → ∀𝑥∀𝑥𝜑)
Theorem	bj-modal4e 36916	First-order logic form of the modal axiom (4) using existential quantifiers. Dual statement of bj-modal4 36915 (hba1 2299). (Contributed by BJ, 21-Dec-2020.) (Proof modification is discouraged.)
⊢ (∃𝑥∃𝑥𝜑 → ∃𝑥𝜑)
Theorem	bj-modalb 36917	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 36918	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 36919	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 36920	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 36921	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 36922	Equivalent form of the axiom of substitution bj-ax12 36858. Although both sides need a DV condition on 𝑥, 𝑡 (or as in bj-ax12v3 36886 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 36923. Note that in the LHS, the reverse implication holds by equs4 2420 (or equs4v 2001 if a DV condition is added on 𝑥, 𝑡 as in bj-ax12 36858), and the forward implication is sbalex 2249. 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 36923*	Weak form of the LHS of bj-substax12 36922 proved from the core axiom schemes. Compare ax12w 2138. (Contributed by BJ, 26-May-2024.) (Proof modification is discouraged.)
⊢ (𝑥 = 𝑡 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥(𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑))
21.19.4.10  Nonfreeness
Syntax	wnnf 36924	Syntax for the nonfreeness quantifier.
wff Ⅎ'𝑥𝜑
Definition	df-bj-nnf 36925	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 1911 and ax5e 1913. 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 36955, 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 2164 and excom 2167 (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 1911, ax5e 1913, ax5ea 1914. 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 36926 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 36955, 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 36947, bj-nnfnt 36941, bj-nnfan 36949, bj-nnfor 36951, bj-nnfbit 36953, bj-nnfalt 36967, bj-nnfext 36968. 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 36947 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 36967 yields ((∀𝑦∀𝑥1 ...∀𝑥m Ⅎ'𝑥𝜑 → Ⅎ'𝑥∀𝑦 PHI), {{𝑥, 𝑎} ∣ 𝑎 ∈ OC(∀𝑦 PHI) ∖ {𝜑}}) and similarly for antecedents which are conjunctions as in the statement of the lemma. Note bj-nnfalt 36967 and bj-nnfext 36968 are proved from positive propositional calculus with alcom 2164 and excom 2167 (possibly weakened by a DV condition on the quantifying variables), and modalB (via bj-19.12 36962). 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 1911 or ax5e 1913 or ax5ea 1914. 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 36929 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 1913 or ax5ea 1914, we would use bj-nnfe 36932 or bj-nnfea 36935 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 1796, by bj-nnf-alrim 36956 and bj-nnfa1 36960 (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 1982. QED Compared with df-nf 1785, the present definition is stricter on positive propositional calculus (bj-nnfnfTEMP 36939) and equivalent on core FOL plus sp 2190 (bj-nfnnfTEMP 36959). While being stricter, it still holds for non-occurring variables (bj-nnfv 36955), 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 2146 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 36926	If two formulas are equivalent for all 𝑥, then nonfreeness of 𝑥 in one of them is equivalent to nonfreeness in the other. Compare nfbiit 1852. From this and bj-nnfim 36947 and bj-nnfnt 36941, 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 36942) in order not to require sp 2190 (modal T). (Contributed by BJ, 27-Aug-2023.)
⊢ (((𝜑 ↔ 𝜓) ∧ ∀𝑥(𝜑 ↔ 𝜓)) → (Ⅎ'𝑥𝜑 ↔ Ⅎ'𝑥𝜓))
Theorem	bj-nnfbd 36927*	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 36926. (Contributed by BJ, 27-Aug-2023.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (Ⅎ'𝑥𝜓 ↔ Ⅎ'𝑥𝜒))
Theorem	bj-nnfbii 36928	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 36926. (Contributed by BJ, 18-Nov-2023.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (Ⅎ'𝑥𝜑 ↔ Ⅎ'𝑥𝜓)
Theorem	bj-nnfa 36929	Nonfreeness implies the equivalent of ax-5 1911. See nf5r 2201. (Contributed by BJ, 28-Jul-2023.)
⊢ (Ⅎ'𝑥𝜑 → (𝜑 → ∀𝑥𝜑))
Theorem	bj-nnfad 36930	Nonfreeness implies the equivalent of ax-5 1911, deduction form. See nf5rd 2203. (Contributed by BJ, 2-Dec-2023.)
⊢ (𝜑 → Ⅎ'𝑥𝜓)    ⇒   ⊢ (𝜑 → (𝜓 → ∀𝑥𝜓))
Theorem	bj-nnfai 36931	Nonfreeness implies the equivalent of ax-5 1911, inference form. See nf5ri 2202. (Contributed by BJ, 22-Sep-2024.)
⊢ Ⅎ'𝑥𝜑    ⇒   ⊢ (𝜑 → ∀𝑥𝜑)
Theorem	bj-nnfe 36932	Nonfreeness implies the equivalent of ax5e 1913. (Contributed by BJ, 28-Jul-2023.)
⊢ (Ⅎ'𝑥𝜑 → (∃𝑥𝜑 → 𝜑))
Theorem	bj-nnfed 36933	Nonfreeness implies the equivalent of ax5e 1913, deduction form. (Contributed by BJ, 2-Dec-2023.)
⊢ (𝜑 → Ⅎ'𝑥𝜓)    ⇒   ⊢ (𝜑 → (∃𝑥𝜓 → 𝜓))
Theorem	bj-nnfei 36934	Nonfreeness implies the equivalent of ax5e 1913, inference form. (Contributed by BJ, 22-Sep-2024.)
⊢ Ⅎ'𝑥𝜑    ⇒   ⊢ (∃𝑥𝜑 → 𝜑)
Theorem	bj-nnfea 36935	Nonfreeness implies the equivalent of ax5ea 1914. (Contributed by BJ, 28-Jul-2023.)
⊢ (Ⅎ'𝑥𝜑 → (∃𝑥𝜑 → ∀𝑥𝜑))
Theorem	bj-nnfead 36936	Nonfreeness implies the equivalent of ax5ea 1914, deduction form. (Contributed by BJ, 2-Dec-2023.)
⊢ (𝜑 → Ⅎ'𝑥𝜓)    ⇒   ⊢ (𝜑 → (∃𝑥𝜓 → ∀𝑥𝜓))
Theorem	bj-nnfeai 36937	Nonfreeness implies the equivalent of ax5ea 1914, inference form. (Contributed by BJ, 22-Sep-2024.)
⊢ Ⅎ'𝑥𝜑    ⇒   ⊢ (∃𝑥𝜑 → ∀𝑥𝜑)
Theorem	bj-dfnnf2 36938	Alternate definition of df-bj-nnf 36925 using only primitive symbols (→, ¬, ∀) in each conjunct. (Contributed by BJ, 20-Aug-2023.)
⊢ (Ⅎ'𝑥𝜑 ↔ ((𝜑 → ∀𝑥𝜑) ∧ (¬ 𝜑 → ∀𝑥 ¬ 𝜑)))
Theorem	bj-nnfnfTEMP 36939	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 1785 except via df-nf 1785 directly. (Proof modification is discouraged.)
⊢ (Ⅎ'𝑥𝜑 → Ⅎ𝑥𝜑)
Theorem	bj-wnfnf 36940	When 𝜑 is substituted for 𝜓, this statement expresses nonfreeness in the weak form of nonfreeness (∃ → ∀). Note that this could also be proved from bj-nnfim 36947, bj-nnfe1 36961 and bj-nnfa1 36960. (Contributed by BJ, 9-Dec-2023.)
⊢ Ⅎ'𝑥(∃𝑥𝜑 → ∀𝑥𝜓)
Theorem	bj-nnfnt 36941	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 36947). Intuitionistically, ⊢ (Ⅎ'𝑥¬ 𝜑 ↔ Ⅎ'𝑥¬ ¬ 𝜑). See nfnt 1857. (Contributed by BJ, 28-Jul-2023.)
⊢ (Ⅎ'𝑥𝜑 ↔ Ⅎ'𝑥 ¬ 𝜑)
Theorem	bj-nnftht 36942	A variable is nonfree in a theorem. The antecedent is in the "strong necessity" modality of modal logic in order not to require sp 2190 (modal T), as in bj-nnfbi 36926. (Contributed by BJ, 28-Jul-2023.)
⊢ ((𝜑 ∧ ∀𝑥𝜑) → Ⅎ'𝑥𝜑)
Theorem	bj-nnfth 36943	A variable is nonfree in a theorem, inference form. (Contributed by BJ, 28-Jul-2023.)
⊢ 𝜑    ⇒   ⊢ Ⅎ'𝑥𝜑
Theorem	bj-nnfnth 36944	A variable is nonfree in the negation of a theorem, inference form. (Contributed by BJ, 27-Aug-2023.)
⊢ ¬ 𝜑    ⇒   ⊢ Ⅎ'𝑥𝜑
Theorem	bj-nnfim1 36945	A consequence of nonfreeness in the antecedent and the consequent of an implication. (Contributed by BJ, 27-Aug-2023.)
⊢ ((Ⅎ'𝑥𝜑 ∧ Ⅎ'𝑥𝜓) → ((𝜑 → 𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓)))
Theorem	bj-nnfim2 36946	A consequence of nonfreeness in the antecedent and the consequent of an implication. (Contributed by BJ, 27-Aug-2023.)
⊢ ((Ⅎ'𝑥𝜑 ∧ Ⅎ'𝑥𝜓) → ((∀𝑥𝜑 → ∃𝑥𝜓) → (𝜑 → 𝜓)))
Theorem	bj-nnfim 36947	Nonfreeness in the antecedent and the consequent of an implication implies nonfreeness in the implication. (Contributed by BJ, 27-Aug-2023.)
⊢ ((Ⅎ'𝑥𝜑 ∧ Ⅎ'𝑥𝜓) → Ⅎ'𝑥(𝜑 → 𝜓))
Theorem	bj-nnfimd 36948	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 36949	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 36947, bj-nnfnt 36941 and bj-nnfbi 36926, but we want a proof valid in intuitionistic logic. (Proof modification is discouraged.)
⊢ ((Ⅎ'𝑥𝜑 ∧ Ⅎ'𝑥𝜓) → Ⅎ'𝑥(𝜑 ∧ 𝜓))
Theorem	bj-nnfand 36950	Nonfreeness in both conjuncts implies nonfreeness in the conjunction, deduction form. Note: compared with the proof of bj-nnfan 36949, 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 36949 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 36950 will generally be easier to understand). (Contributed by BJ, 19-Nov-2023.) (Proof modification is discouraged.)
⊢ (𝜑 → Ⅎ'𝑥𝜓)    &   ⊢ (𝜑 → Ⅎ'𝑥𝜒)    ⇒   ⊢ (𝜑 → Ⅎ'𝑥(𝜓 ∧ 𝜒))
Theorem	bj-nnfor 36951	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 36947, bj-nnfnt 36941 and bj-nnfbi 36926, but we want a proof valid in intuitionistic logic. (Proof modification is discouraged.)
⊢ ((Ⅎ'𝑥𝜑 ∧ Ⅎ'𝑥𝜓) → Ⅎ'𝑥(𝜑 ∨ 𝜓))
Theorem	bj-nnford 36952	Nonfreeness in both disjuncts implies nonfreeness in the disjunction, deduction form. See comments for bj-nnfor 36951 and bj-nnfand 36950. (Contributed by BJ, 2-Dec-2023.) (Proof modification is discouraged.)
⊢ (𝜑 → Ⅎ'𝑥𝜓)    &   ⊢ (𝜑 → Ⅎ'𝑥𝜒)    ⇒   ⊢ (𝜑 → Ⅎ'𝑥(𝜓 ∨ 𝜒))
Theorem	bj-nnfbit 36953	Nonfreeness in both sides implies nonfreeness in the biconditional. (Contributed by BJ, 2-Dec-2023.) (Proof modification is discouraged.)
⊢ ((Ⅎ'𝑥𝜑 ∧ Ⅎ'𝑥𝜓) → Ⅎ'𝑥(𝜑 ↔ 𝜓))
Theorem	bj-nnfbid 36954	Nonfreeness in both sides implies nonfreeness in the biconditional, deduction form. (Contributed by BJ, 2-Dec-2023.) (Proof modification is discouraged.)
⊢ (𝜑 → Ⅎ'𝑥𝜓)    &   ⊢ (𝜑 → Ⅎ'𝑥𝜒)    ⇒   ⊢ (𝜑 → Ⅎ'𝑥(𝜓 ↔ 𝜒))
Theorem	bj-nnfv 36955*	A non-occurring variable is nonfree in a formula. (Contributed by BJ, 28-Jul-2023.)
⊢ Ⅎ'𝑥𝜑
Theorem	bj-nnf-alrim 36956	Proof of the closed form of alrimi 2220 from modalK (compare alrimiv 1928). See also bj-alrim 36894. Actually, most proofs between 19.3t 2208 and 2sbbid 2254 could be proved without ax-12 2184. (Contributed by BJ, 20-Aug-2023.)
⊢ (Ⅎ'𝑥𝜑 → (∀𝑥(𝜑 → 𝜓) → (𝜑 → ∀𝑥𝜓)))
Theorem	bj-nnf-exlim 36957	Proof of the closed form of exlimi 2224 from modalK (compare exlimiv 1931). See also bj-sylget2 36822. (Contributed by BJ, 2-Dec-2023.)
⊢ (Ⅎ'𝑥𝜓 → (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → 𝜓)))
Theorem	bj-dfnnf3 36958	Alternate definition of nonfreeness when sp 2190 is available. (Contributed by BJ, 28-Jul-2023.) The proof should not rely on df-nf 1785. (Proof modification is discouraged.)
⊢ (Ⅎ'𝑥𝜑 ↔ (∃𝑥𝜑 → ∀𝑥𝜑))
Theorem	bj-nfnnfTEMP 36959	New nonfreeness is equivalent to old nonfreeness on core FOL axioms plus sp 2190. (Contributed by BJ, 28-Jul-2023.) The proof should not rely on df-nf 1785 except via df-nf 1785 directly. (Proof modification is discouraged.)
⊢ (Ⅎ'𝑥𝜑 ↔ Ⅎ𝑥𝜑)
Theorem	bj-nnfa1 36960	See nfa1 2156. (Contributed by BJ, 12-Aug-2023.) (Proof modification is discouraged.)
⊢ Ⅎ'𝑥∀𝑥𝜑
Theorem	bj-nnfe1 36961	See nfe1 2155. (Contributed by BJ, 12-Aug-2023.) (Proof modification is discouraged.)
⊢ Ⅎ'𝑥∃𝑥𝜑
Theorem	bj-19.12 36962	See 19.12 2332. Could be labeled "exalimalex" for "'there exists for all' implies 'for all there exists'". This proof is from excom 2167 and modal (B) on top of modalK logic. (Contributed by BJ, 12-Aug-2023.) The proof should not rely on df-nf 1785 or df-bj-nnf 36925, directly or indirectly. (Proof modification is discouraged.)
⊢ (∃𝑥∀𝑦𝜑 → ∀𝑦∃𝑥𝜑)
Theorem	bj-nnflemaa 36963	One of four lemmas for nonfreeness: antecedent and consequent both expressed using universal quantifier. Note: this is bj-hbalt 36882. (Contributed by BJ, 12-Aug-2023.) (Proof modification is discouraged.)
⊢ (∀𝑥(𝜑 → ∀𝑦𝜑) → (∀𝑥𝜑 → ∀𝑦∀𝑥𝜑))
Theorem	bj-nnflemee 36964	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 36965	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 36966	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 36967	See nfal 2328 and bj-nfalt 36912. (Contributed by BJ, 12-Aug-2023.) (Proof modification is discouraged.)
⊢ (∀𝑥Ⅎ'𝑦𝜑 → Ⅎ'𝑦∀𝑥𝜑)
Theorem	bj-nnfext 36968	See nfex 2329 and bj-nfext 36913. (Contributed by BJ, 12-Aug-2023.) (Proof modification is discouraged.)
⊢ (∀𝑥Ⅎ'𝑦𝜑 → Ⅎ'𝑦∃𝑥𝜑)
Theorem	bj-stdpc5t 36969	Alias of bj-nnf-alrim 36956 for labeling consistency (a standard predicate calculus axiom). Closed form of stdpc5 2215 proved from modalK (obsoleting stdpc5v 1939). (Contributed by BJ, 2-Dec-2023.) Use bj-nnf-alrim 36956 instead. (New usaged is discouraged.)
⊢ (Ⅎ'𝑥𝜑 → (∀𝑥(𝜑 → 𝜓) → (𝜑 → ∀𝑥𝜓)))
Theorem	bj-19.21t 36970	Statement 19.21t 2213 proved from modalK (obsoleting 19.21v 1940). (Contributed by BJ, 2-Dec-2023.)
⊢ (Ⅎ'𝑥𝜑 → (∀𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥𝜓)))
Theorem	bj-19.23t 36971	Statement 19.23t 2217 proved from modalK (obsoleting 19.23v 1943). (Contributed by BJ, 2-Dec-2023.)
⊢ (Ⅎ'𝑥𝜓 → (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜓)))
Theorem	bj-19.36im 36972	One direction of 19.36 2237 from the same axioms as 19.36imv 1946. (Contributed by BJ, 2-Dec-2023.)
⊢ (Ⅎ'𝑥𝜓 → (∃𝑥(𝜑 → 𝜓) → (∀𝑥𝜑 → 𝜓)))
Theorem	bj-19.37im 36973	One direction of 19.37 2239 from the same axioms as 19.37imv 1948. (Contributed by BJ, 2-Dec-2023.)
⊢ (Ⅎ'𝑥𝜑 → (∃𝑥(𝜑 → 𝜓) → (𝜑 → ∃𝑥𝜓)))
Theorem	bj-19.42t 36974	Closed form of 19.42 2243 from the same axioms as 19.42v 1954. (Contributed by BJ, 2-Dec-2023.)
⊢ (Ⅎ'𝑥𝜑 → (∃𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥𝜓)))
Theorem	bj-19.41t 36975	Closed form of 19.41 2242 from the same axioms as 19.41v 1950. The same is doable with 19.27 2234, 19.28 2235, 19.31 2241, 19.32 2240, 19.44 2244, 19.45 2245. (Contributed by BJ, 2-Dec-2023.)
⊢ (Ⅎ'𝑥𝜓 → (∃𝑥(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ 𝜓)))
Theorem	bj-sbft 36976	Version of sbft 2276 using Ⅎ', proved from core axioms. (Contributed by BJ, 19-Nov-2023.)
⊢ (Ⅎ'𝑥𝜑 → ([𝑡 / 𝑥]𝜑 ↔ 𝜑))
Theorem	bj-pm11.53vw 36977	Version of pm11.53v 1945 with nonfreeness antecedents. One can also prove the theorem with antecedent (Ⅎ'𝑦∀𝑥𝜑 ∧ ∀𝑦Ⅎ'𝑥𝜓). (Contributed by BJ, 7-Oct-2024.)
⊢ ((∀𝑥Ⅎ'𝑦𝜑 ∧ Ⅎ'𝑥∀𝑦𝜓) → (∀𝑥∀𝑦(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → ∀𝑦𝜓)))
Theorem	bj-pm11.53v 36978	Version of pm11.53v 1945 with nonfreeness antecedents. (Contributed by BJ, 7-Oct-2024.)
⊢ ((∀𝑥Ⅎ'𝑦𝜑 ∧ ∀𝑦Ⅎ'𝑥𝜓) → (∀𝑥∀𝑦(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → ∀𝑦𝜓)))
Theorem	bj-pm11.53a 36979*	A variant of pm11.53v 1945. One can similarly prove a variant with DV (𝑦, 𝜑) and ∀𝑦Ⅎ'𝑥𝜓 instead of DV (𝑥, 𝜓) and ∀𝑥Ⅎ'𝑦𝜑. (Contributed by BJ, 7-Oct-2024.)
⊢ (∀𝑥Ⅎ'𝑦𝜑 → (∀𝑥∀𝑦(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → ∀𝑦𝜓)))
Theorem	bj-equsvt 36980*	A variant of equsv 2004. (Contributed by BJ, 7-Oct-2024.)
⊢ (Ⅎ'𝑥𝜑 → (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜑))
Theorem	bj-equsalvwd 36981*	Variant of equsalvw 2005. (Contributed by BJ, 7-Oct-2024.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → Ⅎ'𝑥𝜒)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥(𝑥 = 𝑦 → 𝜓) ↔ 𝜒))
Theorem	bj-equsexvwd 36982*	Variant of equsexvw 2006. (Contributed by BJ, 7-Oct-2024.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → Ⅎ'𝑥𝜒)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥(𝑥 = 𝑦 ∧ 𝜓) ↔ 𝜒))
Theorem	bj-sbievwd 36983*	Variant of sbievw 2098. (Contributed by BJ, 7-Oct-2024.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → Ⅎ'𝑥𝜒)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ([𝑦 / 𝑥]𝜓 ↔ 𝜒))
21.19.4.11  Adding ax-13
Theorem	bj-axc10 36984	Alternate proof of axc10 2389. Shorter. One can prove a version with DV (𝑥, 𝑦) without ax-13 2376, by using ax6ev 1970 instead of ax6e 2387. (Contributed by BJ, 31-Mar-2021.) (Proof modification is discouraged.)
⊢ (∀𝑥(𝑥 = 𝑦 → ∀𝑥𝜑) → 𝜑)
Theorem	bj-alequex 36985	A fol lemma. See alequexv 2002 for a version with a disjoint variable condition requiring fewer axioms. Can be used to reduce the proof of spimt 2390 from 133 to 112 bytes. (Contributed by BJ, 6-Oct-2018.)
⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → ∃𝑥𝜑)
Theorem	bj-spimt2 36986	A step in the proof of spimt 2390. (Contributed by BJ, 2-May-2019.)
⊢ (∀𝑥(𝑥 = 𝑦 → (𝜑 → 𝜓)) → ((∃𝑥𝜓 → 𝜓) → (∀𝑥𝜑 → 𝜓)))
Theorem	bj-cbv3ta 36987	Closed form of cbv3 2401. (Contributed by BJ, 2-May-2019.)
⊢ (∀𝑥∀𝑦(𝑥 = 𝑦 → (𝜑 → 𝜓)) → ((∀𝑦(∃𝑥𝜓 → 𝜓) ∧ ∀𝑥(𝜑 → ∀𝑦𝜑)) → (∀𝑥𝜑 → ∀𝑦𝜓)))
Theorem	bj-cbv3tb 36988	Closed form of cbv3 2401. (Contributed by BJ, 2-May-2019.)
⊢ (∀𝑥∀𝑦(𝑥 = 𝑦 → (𝜑 → 𝜓)) → ((∀𝑦Ⅎ𝑥𝜓 ∧ ∀𝑥Ⅎ𝑦𝜑) → (∀𝑥𝜑 → ∀𝑦𝜓)))
Theorem	bj-hbsb3t 36989	A theorem close to a closed form of hbsb3 2491. (Contributed by BJ, 2-May-2019.)
⊢ (∀𝑥(𝜑 → ∀𝑦𝜑) → ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑))
Theorem	bj-hbsb3 36990	Shorter proof of hbsb3 2491. (Contributed by BJ, 2-May-2019.) (Proof modification is discouraged.)
⊢ (𝜑 → ∀𝑦𝜑)    ⇒   ⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑)
Theorem	bj-nfs1t 36991	A theorem close to a closed form of nfs1 2492. (Contributed by BJ, 2-May-2019.)
⊢ (∀𝑥(𝜑 → ∀𝑦𝜑) → Ⅎ𝑥[𝑦 / 𝑥]𝜑)
Theorem	bj-nfs1t2 36992	A theorem close to a closed form of nfs1 2492. (Contributed by BJ, 2-May-2019.)
⊢ (∀𝑥Ⅎ𝑦𝜑 → Ⅎ𝑥[𝑦 / 𝑥]𝜑)
Theorem	bj-nfs1 36993	Shorter proof of nfs1 2492 (three essential steps instead of four). (Contributed by BJ, 2-May-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ Ⅎ𝑥[𝑦 / 𝑥]𝜑
21.19.4.12  Removing dependencies on ax-13 (and ax-11) It is known that ax-13 2376 is logically redundant (see ax13w 2141 and the head comment of the section "Logical redundancy of ax-10--13"). More precisely, one can remove dependency on ax-13 2376 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 2376 with ax13w 2141. This section is an experiment to see in practice if (partially) unbundled versions of existing theorems can be proved more efficiently without ax-13 2376 (and using ax6v 1969 / ax6ev 1970 instead of ax-6 1968 / ax6e 2387, as is currently done). One reason to be optimistic is that the first few utility theorems using ax-13 2376 (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 2376, labeled bj-xxxv (we follow the proof of xxx but use ax6v 1969 and ax6ev 1970 instead of ax-6 1968 and ax6e 2387, and ax-5 1911 instead of ax13v 2377; 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 2376, so as to remove dependencies on ax-13 2376 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 2162, typically by replacing a nonfree hypothesis with a disjoint variable condition (see cbv3v2 2248 and following theorems).
Theorem	bj-axc10v 36994*	Version of axc10 2389 with a disjoint variable condition, which does not require ax-13 2376. (Contributed by BJ, 14-Jun-2019.) (Proof modification is discouraged.)
⊢ (∀𝑥(𝑥 = 𝑦 → ∀𝑥𝜑) → 𝜑)
Theorem	bj-spimtv 36995*	Version of spimt 2390 with a disjoint variable condition, which does not require ax-13 2376. (Contributed by BJ, 14-Jun-2019.) (Proof modification is discouraged.)
⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝑦 → (𝜑 → 𝜓))) → (∀𝑥𝜑 → 𝜓))
Theorem	bj-cbv3hv2 36996*	Version of cbv3h 2408 with two disjoint variable conditions, which does not require ax-11 2162 nor ax-13 2376. (Contributed by BJ, 24-Jun-2019.) (Proof modification is discouraged.)
⊢ (𝜓 → ∀𝑥𝜓)    &   ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))    ⇒   ⊢ (∀𝑥𝜑 → ∀𝑦𝜓)
Theorem	bj-cbv1hv 36997*	Version of cbv1h 2409 with a disjoint variable condition, which does not require ax-13 2376. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ (𝜑 → (𝜓 → ∀𝑦𝜓))    &   ⊢ (𝜑 → (𝜒 → ∀𝑥𝜒))    &   ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 → 𝜒)))    ⇒   ⊢ (∀𝑥∀𝑦𝜑 → (∀𝑥𝜓 → ∀𝑦𝜒))
Theorem	bj-cbv2hv 36998*	Version of cbv2h 2410 with a disjoint variable condition, which does not require ax-13 2376. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ (𝜑 → (𝜓 → ∀𝑦𝜓))    &   ⊢ (𝜑 → (𝜒 → ∀𝑥𝜒))    &   ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (∀𝑥∀𝑦𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒))
Theorem	bj-cbv2v 36999*	Version of cbv2 2407 with a disjoint variable condition, which does not require ax-13 2376. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑦𝜓)    &   ⊢ (𝜑 → Ⅎ𝑥𝜒)    &   ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒))
Theorem	bj-cbvaldv 37000*	Version of cbvald 2411 with a disjoint variable condition, which does not require ax-13 2376. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑦𝜓)    &   ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒))