P. 375 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 37401-37500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	bj-ssbid2ALT 37401	Alternate proof of bj-ssbid2 37400, not using sbequ2 2286. (Contributed by BJ, 22-Dec-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ([𝑥 / 𝑥]𝜑 → 𝜑)
Theorem	bj-ssbid1 37402	A special case of sbequ1 2285. (Contributed by BJ, 22-Dec-2020.)
⊢ (𝜑 → [𝑥 / 𝑥]𝜑)
Theorem	bj-ssbid1ALT 37403	Alternate proof of bj-ssbid1 37402, not using sbequ1 2285. (Contributed by BJ, 22-Dec-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → [𝑥 / 𝑥]𝜑)
Theorem	bj-ax6elem1 37404*	Lemma for bj-ax6e 37406. (Contributed by BJ, 22-Dec-2020.) (Proof modification is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧))
Theorem	bj-ax6elem2 37405*	Lemma for bj-ax6e 37406. (Contributed by BJ, 22-Dec-2020.) (Proof modification is discouraged.)
⊢ (∀𝑥 𝑦 = 𝑧 → ∃𝑥 𝑥 = 𝑦)
Theorem	bj-ax6e 37406	Proof of ax6e 2414 (hence ax6 2415) from Tarski's system, ax-c9 39771, ax-c16 39773. Remark: ax-6 2000 is used only via its principal (unbundled) instance ax6v 2001. (Contributed by BJ, 22-Dec-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∃𝑥 𝑥 = 𝑦
21.19.4.6  Adding ax-6
Theorem	bj-spim0 37407*	A universal specialization result in deduction form, proved from ax-1 6 -- ax-6 2000, 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-spimvwt 37408*	Closed form of spimvw 2019. See also spimt 2417. (Contributed by BJ, 8-Nov-2021.)
⊢ (∀𝑥(𝑥 = 𝑦 → (𝜑 → 𝜓)) → (∀𝑥𝜑 → 𝜓))
Theorem	bj-spnfw 37409	Theorem close to a closed form of spnfw 2012. (Contributed by BJ, 12-May-2019.)
⊢ ((∃𝑥𝜑 → 𝜓) → (∀𝑥𝜑 → 𝜓))
Theorem	bj-cbvexiw 37410*	Change bound variable. This is to cbvexvw 2070 what cbvaliw 2039 is to cbvalvw 2069. TODO: move after cbvalivw 2040. (Contributed by BJ, 17-Mar-2020.)
⊢ (∃𝑥∃𝑦𝜓 → ∃𝑦𝜓)    &   ⊢ (𝜑 → ∀𝑦𝜑)    &   ⊢ (𝑦 = 𝑥 → (𝜑 → 𝜓))    ⇒   ⊢ (∃𝑥𝜑 → ∃𝑦𝜓)
Theorem	bj-cbvexivw 37411*	Change bound variable. This is to cbvexvw 2070 what cbvalivw 2040 is to cbvalvw 2069. TODO: move after cbvalivw 2040. (Contributed by BJ, 17-Mar-2020.)
⊢ (𝑦 = 𝑥 → (𝜑 → 𝜓))    ⇒   ⊢ (∃𝑥𝜑 → ∃𝑦𝜓)
Theorem	bj-modald 37412	A short form of the axiom D of modal logic. (Contributed by BJ, 4-Apr-2021.)
⊢ (∀𝑥 ¬ 𝜑 → ¬ ∀𝑥𝜑)
Theorem	bj-denot 37413*	A weakening of ax-6 2000 and ax6v 2001. (Contributed by BJ, 4-Apr-2021.) (New usage is discouraged.)
⊢ (𝑥 = 𝑥 → ¬ ∀𝑦 ¬ 𝑦 = 𝑥)
Theorem	bj-eqs 37414*	A lemma for substitutions, proved from Tarski's FOL. The version without DV (𝑥, 𝑦) is true but requires ax-13 2403. The disjoint variable condition DV (𝑥, 𝜑) is necessary for both directions: consider substituting 𝑥 = 𝑧 for 𝜑. (Contributed by BJ, 25-May-2021.)
⊢ (𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑))
21.19.4.7  Adding ax-7
Theorem	bj-cbvexw 37415*	Change bound variable. This is to cbvexvw 2070 what cbvalw 2068 is to cbvalvw 2069. (Contributed by BJ, 17-Mar-2020.)
⊢ (∃𝑥∃𝑦𝜓 → ∃𝑦𝜓)    &   ⊢ (𝜑 → ∀𝑦𝜑)    &   ⊢ (∃𝑦∃𝑥𝜑 → ∃𝑥𝜑)    &   ⊢ (𝜓 → ∀𝑥𝜓)    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓)
Theorem	bj-ax12w 37416*	The general statement that ax12w 2170 proves. (Contributed by BJ, 20-Mar-2020.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑦 = 𝑧 → (𝜓 ↔ 𝜃))    ⇒   ⊢ (𝜑 → (∀𝑦𝜓 → ∀𝑥(𝜑 → 𝜓)))
21.19.4.8  Membership predicate, ax-8 and ax-9
Theorem	bj-ax89 37417	A theorem which could be used as sole axiom for the non-logical predicate instead of ax-8 2147 and ax-9 2155. Indeed, it is implied over propositional calculus by the conjunction of ax-8 2147 and ax-9 2155, as proved here. In the other direction, one can prove ax-8 2147 (respectively ax-9 2155) from bj-ax89 37417 by using mpan2 704 (respectively mpan 703) and equid 2045. TODO: move to main part. (Contributed by BJ, 3-Oct-2019.)
⊢ ((𝑥 = 𝑦 ∧ 𝑧 = 𝑡) → (𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑡))
Theorem	bj-cleljusti 37418*	One direction of cleljust 2154, requiring only ax-1 6-- ax-5 1943 and ax8v1 2149. (Contributed by BJ, 31-Dec-2020.) (Proof modification is discouraged.)
⊢ (∃𝑧(𝑧 = 𝑥 ∧ 𝑧 ∈ 𝑦) → 𝑥 ∈ 𝑦)
21.19.4.9  Adding ax-11
Theorem	bj-alcomexcom 37419	Commutation of two existential quantifiers on a formula is equivalent to commutation of two universal quantifiers over the same variables on the negation of that formula. Can be placed in the ax-4 1842 section, soon after 2nexaln 1863, and used to prove excom 2199. (Contributed by BJ, 29-Nov-2020.) (Proof modification is discouraged.)
⊢ ((∀𝑥∀𝑦 ¬ 𝜑 → ∀𝑦∀𝑥 ¬ 𝜑) ↔ (∃𝑦∃𝑥𝜑 → ∃𝑥∃𝑦𝜑))
Theorem	bj-hbald 37420	General statement that hbald 2205 proves . (Contributed by BJ, 4-Apr-2026.)
⊢ (𝜑 → ∀𝑦𝜓)    &   ⊢ (𝜓 → (𝜒 → ∀𝑥𝜃))    ⇒   ⊢ (𝜑 → (∀𝑦𝜒 → ∀𝑥∀𝑦𝜃))
Theorem	bj-hbalt 37421	Closed form of (general instance of) hbal 2204. (Contributed by BJ, 2-May-2019.)
⊢ (∀𝑦(𝜑 → ∀𝑥𝜓) → (∀𝑦𝜑 → ∀𝑥∀𝑦𝜓))
Theorem	bj-hbal 37422	More general instance of hbal 2204. (Contributed by BJ, 4-Apr-2026.)
⊢ (𝜑 → ∀𝑥𝜓)    ⇒   ⊢ (∀𝑦𝜑 → ∀𝑥∀𝑦𝜓)
21.19.4.10  Adding ax-12
Theorem	axc11n11 37423	Proof of axc11n 2457 from { ax-1 6-- ax-7 2041, axc11 2461 } . Almost identical to axc11nfromc11 39807. (Contributed by NM, 6-Jul-2021.) (Proof modification is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥)
Theorem	axc11n11r 37424	Proof of axc11n 2457 from { ax-1 6-- ax-7 2041, axc9 2413, axc11r 2399 } (note that axc16 2297 is provable from { ax-1 6-- ax-7 2041, axc11r 2399 }). Note that axc11n 2457 proves (over minimal calculus) that axc11 2461 and axc11r 2399 are equivalent. Therefore, axc11n11 37423 and axc11n11r 37424 prove that one can use one or the other as an axiom, provided one assumes the axioms listed above (axc11 2461 appears slightly stronger since axc11n11r 37424 requires axc9 2413 while axc11n11 37423 does not). (Contributed by BJ, 6-Jul-2021.) (Proof modification is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥)
Theorem	bj-axc16g16 37425*	Proof of axc16g 2296 from { ax-1 6-- ax-7 2041, axc16 2297 }. (Contributed by BJ, 6-Jul-2021.) (Proof modification is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑧𝜑))
Theorem	bj-ax12v3 37426*	A weak version of ax-12 2215 which is stronger than ax12v 2216. Note that if one assumes reflexivity of equality ⊢ 𝑥 = 𝑥 (equid 2045), then bj-ax12v3 37426 implies ax-5 1943 over modal logic K (substitute 𝑥 for 𝑦). See also bj-ax12v3ALT 37427. (Contributed by BJ, 6-Jul-2021.) (Proof modification is discouraged.)
⊢ (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
Theorem	bj-ax12v3ALT 37427*	Alternate proof of bj-ax12v3 37426. Uses axc11r 2399 and axc15 2453 instead of ax-12 2215. (Contributed by BJ, 6-Jul-2021.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
Theorem	bj-sb 37428*	A weak variant of sbid2 2539 not requiring ax-13 2403 nor ax-10 2178. On top of Tarski's FOL, one implication requires only ax12v 2216, and the other requires only sp 2221. (Contributed by BJ, 25-May-2021.)
⊢ (𝜑 ↔ ∀𝑦(𝑦 = 𝑥 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
Theorem	bj-modalbe 37429	The predicate-calculus version of the axiom (B) of modal logic. See also modal-b 2351. (Contributed by BJ, 20-Oct-2019.)
⊢ (𝜑 → ∀𝑥∃𝑥𝜑)
Theorem	bj-spst 37430	Closed form of sps 2223. Once in main part, prove sps 2223 and spsd 2225 from it. (Contributed by BJ, 20-Oct-2019.)
⊢ ((𝜑 → 𝜓) → (∀𝑥𝜑 → 𝜓))
Theorem	bj-19.21bit 37431	Closed form of 19.21bi 2227. (Contributed by BJ, 20-Oct-2019.)
⊢ ((𝜑 → ∀𝑥𝜓) → (𝜑 → 𝜓))
Theorem	bj-19.23bit 37432	Closed form of 19.23bi 2229. (Contributed by BJ, 20-Oct-2019.)
⊢ ((∃𝑥𝜑 → 𝜓) → (𝜑 → 𝜓))
Theorem	bj-nexrt 37433	Closed form of nexr 2230. Contrapositive of 19.8a 2219. (Contributed by BJ, 20-Oct-2019.)
⊢ (¬ ∃𝑥𝜑 → ¬ 𝜑)
Theorem	bj-alrim 37434	Closed form of alrimi 2251. (Contributed by BJ, 2-May-2019.)
⊢ (Ⅎ𝑥𝜑 → (∀𝑥(𝜑 → 𝜓) → (𝜑 → ∀𝑥𝜓)))
Theorem	bj-alrim2 37435	Uncurried (imported) form of bj-alrim 37434. (Contributed by BJ, 2-May-2019.)
⊢ ((Ⅎ𝑥𝜑 ∧ ∀𝑥(𝜑 → 𝜓)) → (𝜑 → ∀𝑥𝜓))
Theorem	bj-nfdt0 37436	A theorem close to a closed form of nf5d 2319 and nf5dh 2184. (Contributed by BJ, 2-May-2019.)
⊢ (∀𝑥(𝜑 → (𝜓 → ∀𝑥𝜓)) → (∀𝑥𝜑 → Ⅎ𝑥𝜓))
Theorem	bj-nfdt 37437	Closed form of nf5d 2319 and nf5dh 2184. (Contributed by BJ, 2-May-2019.)
⊢ (∀𝑥(𝜑 → (𝜓 → ∀𝑥𝜓)) → ((𝜑 → ∀𝑥𝜑) → (𝜑 → Ⅎ𝑥𝜓)))
Theorem	bj-nexdt 37438	Closed form of nexd 2259. (Contributed by BJ, 20-Oct-2019.)
⊢ (Ⅎ𝑥𝜑 → (∀𝑥(𝜑 → ¬ 𝜓) → (𝜑 → ¬ ∃𝑥𝜓)))
Theorem	bj-nexdvt 37439*	Closed form of nexdv 1969. (Contributed by BJ, 20-Oct-2019.)
⊢ (∀𝑥(𝜑 → ¬ 𝜓) → (𝜑 → ¬ ∃𝑥𝜓))
Theorem	bj-alexbiex 37440	Adding a second quantifier over the same variable is a transparent operation, (∀∃ case). (Contributed by BJ, 20-Oct-2019.)
⊢ (∀𝑥∃𝑥𝜑 ↔ ∃𝑥𝜑)
Theorem	bj-exexbiex 37441	Adding a second quantifier over the same variable is a transparent operation, (∃∃ case). (Contributed by BJ, 20-Oct-2019.)
⊢ (∃𝑥∃𝑥𝜑 ↔ ∃𝑥𝜑)
Theorem	bj-alalbial 37442	Adding a second quantifier over the same variable is a transparent operation, (∀∀ case). (Contributed by BJ, 20-Oct-2019.)
⊢ (∀𝑥∀𝑥𝜑 ↔ ∀𝑥𝜑)
Theorem	bj-exalbial 37443	Adding a second quantifier over the same variable is a transparent operation, (∃∀ case). (Contributed by BJ, 20-Oct-2019.)
⊢ (∃𝑥∀𝑥𝜑 ↔ ∀𝑥𝜑)
Theorem	bj-19.9htbi 37444	Strengthening 19.9ht 2352 by replacing its consequent with a biconditional (19.9t 2242 does have a biconditional consequent). This propagates. (Contributed by BJ, 20-Oct-2019.)
⊢ (∀𝑥(𝜑 → ∀𝑥𝜑) → (∃𝑥𝜑 ↔ 𝜑))
Theorem	bj-hbntbi 37445	Strengthening hbnt 2329 by replacing its consequent with a biconditional. See also hbntg 36390 and hbntal 45384. (Contributed by BJ, 20-Oct-2019.) Proved from bj-19.9htbi 37444. (Proof modification is discouraged.)
⊢ (∀𝑥(𝜑 → ∀𝑥𝜑) → (¬ 𝜑 ↔ ∀𝑥 ¬ 𝜑))
Theorem	bj-biexal1 37446	A general FOL biconditional that generalizes 19.9ht 2352 among others. For this and the following theorems, see also 19.35 1910, 19.21 2245, 19.23 2249. When 𝜑 is substituted for 𝜓, both sides express a form of nonfreeness. (Contributed by BJ, 20-Oct-2019.)
⊢ (∀𝑥(𝜑 → ∀𝑥𝜓) ↔ (∃𝑥𝜑 → ∀𝑥𝜓))
Theorem	bj-biexal2 37447	When 𝜑 is substituted for 𝜓, both sides express a form of nonfreeness. (Contributed by BJ, 20-Oct-2019.)
⊢ (∀𝑥(∃𝑥𝜑 → 𝜓) ↔ (∃𝑥𝜑 → ∀𝑥𝜓))
Theorem	bj-biexal3 37448	When 𝜑 is substituted for 𝜓, both sides express a form of nonfreeness. (Contributed by BJ, 20-Oct-2019.)
⊢ (∀𝑥(𝜑 → ∀𝑥𝜓) ↔ ∀𝑥(∃𝑥𝜑 → 𝜓))
Theorem	bj-bialal 37449	When 𝜑 is substituted for 𝜓, both sides express a form of nonfreeness. (Contributed by BJ, 20-Oct-2019.)
⊢ (∀𝑥(∀𝑥𝜑 → 𝜓) ↔ (∀𝑥𝜑 → ∀𝑥𝜓))
Theorem	bj-biexex 37450	When 𝜑 is substituted for 𝜓, both sides express a form of nonfreeness. (Contributed by BJ, 20-Oct-2019.)
⊢ (∀𝑥(𝜑 → ∃𝑥𝜓) ↔ (∃𝑥𝜑 → ∃𝑥𝜓))
Theorem	bj-hbexd 37451	A more general instance of the deduction form of hbex 2357. (Contributed by BJ, 4-Apr-2026.)
⊢ (𝜑 → ∀𝑦𝜓)    &   ⊢ (𝜓 → (𝜒 → ∀𝑥𝜃))    ⇒   ⊢ (𝜑 → (∃𝑦𝜒 → ∀𝑥∃𝑦𝜃))
Theorem	bj-hbext 37452	Closed form of bj-hbex 37453 and hbex 2357. (Contributed by BJ, 10-Oct-2019.)
⊢ (∀𝑦∀𝑥(𝜑 → ∀𝑥𝜓) → (∃𝑦𝜑 → ∀𝑥∃𝑦𝜓))
Theorem	bj-hbex 37453	A more general instance of hbex 2357. (Contributed by BJ, 4-Apr-2026.)
⊢ (𝜑 → ∀𝑥𝜓)    ⇒   ⊢ (∃𝑦𝜑 → ∀𝑥∃𝑦𝜓)
Theorem	bj-nfalt 37454	Closed form of nfal 2355. (Contributed by BJ, 2-May-2019.)
⊢ (∀𝑥Ⅎ𝑦𝜑 → Ⅎ𝑦∀𝑥𝜑)
Theorem	bj-nfext 37455	Closed form of nfex 2356. (Contributed by BJ, 10-Oct-2019.)
⊢ (∀𝑥Ⅎ𝑦𝜑 → Ⅎ𝑦∃𝑥𝜑)
Theorem	bj-eeanvw 37456*	Version of exdistrv 1988 with a disjoint variable condition on 𝑥, 𝑦 not requiring ax-11 2194. (The same can be done with eeeanv 2381 and ee4anv 2382.) (Contributed by BJ, 29-Sep-2019.) (Proof modification is discouraged.)
⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ ∃𝑦𝜓))
Theorem	bj-modal4 37457	First-order logic form of the modal axiom (4). See hba1 2328. This is the standard proof of the implication in modal logic (B5 ⇒ 4). Its dual statement is bj-modal4e 37458. (Contributed by BJ, 12-Aug-2023.) (Proof modification is discouraged.)
⊢ (∀𝑥𝜑 → ∀𝑥∀𝑥𝜑)
Theorem	bj-modal4e 37458	First-order logic form of the modal axiom (4) using existential quantifiers. Dual statement of bj-modal4 37457 (hba1 2328). (Contributed by BJ, 21-Dec-2020.) (Proof modification is discouraged.)
⊢ (∃𝑥∃𝑥𝜑 → ∃𝑥𝜑)
Theorem	bj-modalb 37459	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 37460	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 37461	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 37462	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 37463	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 37464	See 19.12 2359. Could be labeled "exalimalex" for "'there exists for all' implies 'for all there exists'". This proof is from excom 2199 and modal (B) on top of modalK logic. (Contributed by BJ, 12-Aug-2023.) The proof should not rely on df-nf 1817 or df-bj-nnf 37468, 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 2215, actually only require sp 2221 (which is proved using ax-12 2215).
Theorem	bj-substax12 37465	Equivalent form of the axiom of substitution bj-ax12 37395. Although both sides need a DV condition on 𝑥, 𝑡 (or as in bj-ax12v3 37426 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 37466. Note that in the LHS, the reverse implication holds by equs4 2447 (or equs4v 2033 if a DV condition is added on 𝑥, 𝑡 as in bj-ax12 37395), and the forward implication is sbalex 2280. 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 37466*	Weak form of the LHS of bj-substax12 37465 proved from the core axiom schemes. Compare ax12w 2170. (Contributed by BJ, 26-May-2024.) (Proof modification is discouraged.)
⊢ (𝑥 = 𝑡 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥(𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑))
21.19.4.12  Nonfreeness
Syntax	wnnf 37467	Syntax for the nonfreeness quantifier.
wff Ⅎ'𝑥𝜑
Definition	df-bj-nnf 37468	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 1943 and ax5e 1945. 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 37509, 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 2196 and excom 2199 (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 1943, ax5e 1945, ax5ea 1946. 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 37488 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 23, or have variables all in OC(PHI) ∖ {𝜑}, so (Ⅎ'𝑥 PHI, {{𝑥, 𝑎} ∣ 𝑎 ∈ OC(PHI) ∖ {𝜑}}) by bj-nnfv 37509, 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 37493, bj-nnfnt 37491, bj-nnfan 37495, bj-nnfor 37497, bj-nnfbit 37499, bj-nnfalt 37531, bj-nnfext 37532. 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 37493 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 37531 yields ((∀𝑦∀𝑥1 ...∀𝑥m Ⅎ'𝑥𝜑 → Ⅎ'𝑥∀𝑦 PHI), {{𝑥, 𝑎} ∣ 𝑎 ∈ OC(∀𝑦 PHI) ∖ {𝜑}}) and similarly for antecedents which are conjunctions as in the statement of the lemma. Note bj-nnfalt 37531 and bj-nnfext 37532 are proved from positive propositional calculus with alcom 2196 and excom 2199 (possibly weakened by a DV condition on the quantifying variables), and modalB (via bj-19.12 37464). 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 1943 or ax5e 1945 or ax5ea 1946. 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 37469 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 1945 or ax5ea 1946, we would use bj-nnfe 37472 or bj-nnfea 37475 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 1828, by bj-nnf-alrim 37486 and bj-nnfa1 37525 (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 2014. QED Compared with df-nf 1817, the present definition is stricter on positive propositional calculus (bj-nnfnfTEMP 37481) and equivalent on core FOL plus sp 2221 (bj-nfnnfTEMP 37523). While being stricter, it still holds for non-occurring variables (bj-nnfv 37509), 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 2178 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 37469	Nonfreeness implies the equivalent of ax-5 1943. See nf5r 2232. (Contributed by BJ, 28-Jul-2023.)
⊢ (Ⅎ'𝑥𝜑 → (𝜑 → ∀𝑥𝜑))
Theorem	bj-nnfad 37470	Nonfreeness implies the equivalent of ax-5 1943, deduction form. See nf5rd 2234. (Contributed by BJ, 2-Dec-2023.)
⊢ (𝜑 → Ⅎ'𝑥𝜓)    ⇒   ⊢ (𝜑 → (𝜓 → ∀𝑥𝜓))
Theorem	bj-nnfai 37471	Nonfreeness implies the equivalent of ax-5 1943, inference form. See nf5ri 2233. (Contributed by BJ, 22-Sep-2024.)
⊢ Ⅎ'𝑥𝜑    ⇒   ⊢ (𝜑 → ∀𝑥𝜑)
Theorem	bj-nnfe 37472	Nonfreeness implies the equivalent of ax5e 1945. (Contributed by BJ, 28-Jul-2023.)
⊢ (Ⅎ'𝑥𝜑 → (∃𝑥𝜑 → 𝜑))
Theorem	bj-nnfed 37473	Nonfreeness implies the equivalent of ax5e 1945, deduction form. (Contributed by BJ, 2-Dec-2023.)
⊢ (𝜑 → Ⅎ'𝑥𝜓)    ⇒   ⊢ (𝜑 → (∃𝑥𝜓 → 𝜓))
Theorem	bj-nnfei 37474	Nonfreeness implies the equivalent of ax5e 1945, inference form. (Contributed by BJ, 22-Sep-2024.)
⊢ Ⅎ'𝑥𝜑    ⇒   ⊢ (∃𝑥𝜑 → 𝜑)
Theorem	bj-nnfea 37475	Nonfreeness implies the equivalent of ax5ea 1946. (Contributed by BJ, 28-Jul-2023.)
⊢ (Ⅎ'𝑥𝜑 → (∃𝑥𝜑 → ∀𝑥𝜑))
Theorem	bj-nnfead 37476	Nonfreeness implies the equivalent of ax5ea 1946, deduction form. (Contributed by BJ, 2-Dec-2023.)
⊢ (𝜑 → Ⅎ'𝑥𝜓)    ⇒   ⊢ (𝜑 → (∃𝑥𝜓 → ∀𝑥𝜓))
Theorem	bj-nnfeai 37477	Nonfreeness implies the equivalent of ax5ea 1946, inference form. (Contributed by BJ, 22-Sep-2024.)
⊢ Ⅎ'𝑥𝜑    ⇒   ⊢ (∃𝑥𝜑 → ∀𝑥𝜑)
Theorem	bj-alnnf 37478	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 37479	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 37480	Alternate definition of df-bj-nnf 37468 using only primitive symbols (→, ¬, ∀) in each conjunct. (Contributed by BJ, 20-Aug-2023.)
⊢ (Ⅎ'𝑥𝜑 ↔ ((𝜑 → ∀𝑥𝜑) ∧ (¬ 𝜑 → ∀𝑥 ¬ 𝜑)))
Theorem	bj-nnfnfTEMP 37481	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 1817 except via df-nf 1817 directly. (Proof modification is discouraged.)
⊢ (Ⅎ'𝑥𝜑 → Ⅎ𝑥𝜑)
Theorem	bj-nnfim1 37482	A consequence of nonfreeness in the antecedent and the consequent of an implication. (Contributed by BJ, 27-Aug-2023.)
⊢ ((Ⅎ'𝑥𝜑 ∧ Ⅎ'𝑥𝜓) → ((𝜑 → 𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓)))
Theorem	bj-nnfim2 37483	A consequence of nonfreeness in the antecedent and the consequent of an implication. (Contributed by BJ, 27-Aug-2023.)
⊢ ((Ⅎ'𝑥𝜑 ∧ Ⅎ'𝑥𝜓) → ((∀𝑥𝜑 → ∃𝑥𝜓) → (𝜑 → 𝜓)))
Theorem	bj-nnftht 37484	A variable is nonfree in a theorem. The antecedent is in the "strong necessity" modality of modal logic in order not to require sp 2221 (modal T), as in bj-nnfbi 37488. (Contributed by BJ, 28-Jul-2023.)
⊢ ((𝜑 ∧ ∀𝑥𝜑) → Ⅎ'𝑥𝜑)
Theorem	bj-nnfth 37485	A variable is nonfree in a theorem, inference form. (Contributed by BJ, 28-Jul-2023.)
⊢ 𝜑    ⇒   ⊢ Ⅎ'𝑥𝜑
Theorem	bj-nnf-alrim 37486	Proof of the closed form of alrimi 2251 from modalK (compare alrimiv 1960). See also bj-alrim 37434. Actually, most proofs between 19.3t 2239 and 2sbbid 2284 could be proved without ax-12 2215. (Contributed by BJ, 20-Aug-2023.)
⊢ (Ⅎ'𝑥𝜑 → (∀𝑥(𝜑 → 𝜓) → (𝜑 → ∀𝑥𝜓)))
Theorem	bj-stdpc5t 37487	Alias of bj-nnf-alrim 37486 for labeling consistency (a standard predicate calculus axiom). Closed form of stdpc5 2246 proved from modalK (obsoleting stdpc5v 1971). (Contributed by BJ, 2-Dec-2023.) Use bj-nnf-alrim 37486 instead. (New usaged is discouraged.)
⊢ (Ⅎ'𝑥𝜑 → (∀𝑥(𝜑 → 𝜓) → (𝜑 → ∀𝑥𝜓)))
Theorem	bj-nnfbi 37488	If two formulas are equivalent, then nonfreeness of a variable in one of them is equivalent to nonfreeness in the other. Compare nfbiit 1884. From this and bj-nnfim 37493 and bj-nnfnt 37491, 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 37484) in order not to require sp 2221 (modal T). (Contributed by BJ, 27-Aug-2023.)
⊢ (((𝜑 ↔ 𝜓) ∧ ∀𝑥(𝜑 ↔ 𝜓)) → (Ⅎ'𝑥𝜑 ↔ Ⅎ'𝑥𝜓))
Theorem	bj-nnfbd0 37489	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 37484) in order not to require sp 2221 (modal T). See bj-nnfbi 37488. (Contributed by BJ, 21-Mar-2026.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ ((𝜑 ∧ ∀𝑥𝜑) → (Ⅎ'𝑥𝜓 ↔ Ⅎ'𝑥𝜒))
Theorem	bj-nnfbii 37490	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 37488. (Contributed by BJ, 18-Nov-2023.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (Ⅎ'𝑥𝜑 ↔ Ⅎ'𝑥𝜓)
Theorem	bj-nnfnt 37491	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 37493). Intuitionistically, ⊢ (Ⅎ'𝑥¬ 𝜑 ↔ Ⅎ'𝑥¬ ¬ 𝜑). See nfnt 1889. (Contributed by BJ, 28-Jul-2023.)
⊢ (Ⅎ'𝑥𝜑 ↔ Ⅎ'𝑥 ¬ 𝜑)
Theorem	bj-nnfnth 37492	A variable is nonfree in the negation of a theorem, inference form. (Contributed by BJ, 27-Aug-2023.)
⊢ ¬ 𝜑    ⇒   ⊢ Ⅎ'𝑥𝜑
Theorem	bj-nnfim 37493	Nonfreeness in the antecedent and the consequent of an implication implies nonfreeness in the implication. (Contributed by BJ, 27-Aug-2023.)
⊢ ((Ⅎ'𝑥𝜑 ∧ Ⅎ'𝑥𝜓) → Ⅎ'𝑥(𝜑 → 𝜓))
Theorem	bj-nnfimd 37494	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 37495	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 37493, bj-nnfnt 37491 and bj-nnfbi 37488, but we want a proof valid in intuitionistic logic. (Proof modification is discouraged.)
⊢ ((Ⅎ'𝑥𝜑 ∧ Ⅎ'𝑥𝜓) → Ⅎ'𝑥(𝜑 ∧ 𝜓))
Theorem	bj-nnfand 37496	Nonfreeness in both conjuncts implies nonfreeness in the conjunction, deduction form. Note: compared with the proof of bj-nnfan 37495, 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 37495 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 37496 will generally be easier to understand). (Contributed by BJ, 19-Nov-2023.) (Proof modification is discouraged.)
⊢ (𝜑 → Ⅎ'𝑥𝜓)    &   ⊢ (𝜑 → Ⅎ'𝑥𝜒)    ⇒   ⊢ (𝜑 → Ⅎ'𝑥(𝜓 ∧ 𝜒))
Theorem	bj-nnfor 37497	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 37493, bj-nnfnt 37491 and bj-nnfbi 37488, but we want a proof valid in intuitionistic logic. (Proof modification is discouraged.)
⊢ ((Ⅎ'𝑥𝜑 ∧ Ⅎ'𝑥𝜓) → Ⅎ'𝑥(𝜑 ∨ 𝜓))
Theorem	bj-nnford 37498	Nonfreeness in both disjuncts implies nonfreeness in the disjunction, deduction form. See comments for bj-nnfor 37497 and bj-nnfand 37496. (Contributed by BJ, 2-Dec-2023.) (Proof modification is discouraged.)
⊢ (𝜑 → Ⅎ'𝑥𝜓)    &   ⊢ (𝜑 → Ⅎ'𝑥𝜒)    ⇒   ⊢ (𝜑 → Ⅎ'𝑥(𝜓 ∨ 𝜒))
Theorem	bj-nnfbit 37499	Nonfreeness in both sides implies nonfreeness in the biconditional. (Contributed by BJ, 2-Dec-2023.) (Proof modification is discouraged.)
⊢ ((Ⅎ'𝑥𝜑 ∧ Ⅎ'𝑥𝜓) → Ⅎ'𝑥(𝜑 ↔ 𝜓))
Theorem	bj-nnfbid 37500	Nonfreeness in both sides implies nonfreeness in the biconditional, deduction form. (Contributed by BJ, 2-Dec-2023.) (Proof modification is discouraged.)
⊢ (𝜑 → Ⅎ'𝑥𝜓)    &   ⊢ (𝜑 → Ⅎ'𝑥𝜒)    ⇒   ⊢ (𝜑 → Ⅎ'𝑥(𝜓 ↔ 𝜒))