P. 373 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 37201-37300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	bj-alanim 37201	Closed form of alanimi 1846. (Contributed by BJ, 6-May-2019.)
⊢ (∀𝑥((𝜑 ∧ 𝜓) → 𝜒) → ((∀𝑥𝜑 ∧ ∀𝑥𝜓) → ∀𝑥𝜒))
Theorem	bj-2albi 37202	Closed form of 2albii 1850. (Contributed by BJ, 6-May-2019.)
⊢ (∀𝑥∀𝑦(𝜑 ↔ 𝜓) → (∀𝑥∀𝑦𝜑 ↔ ∀𝑥∀𝑦𝜓))
Theorem	bj-notalbii 37203	Equivalence of universal quantification of negation of equivalent formulas. Shortens ab0 4337 (103>94), ballotlem2 34860 (2655>2648), bnj1143 35159 (522>519), hausdiag 23783 (2119>2104). (Contributed by BJ, 17-Jul-2021.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (∀𝑥 ¬ 𝜑 ↔ ∀𝑥 ¬ 𝜓)
Theorem	bj-2exim 37204	Closed form of 2eximi 1866. (Contributed by BJ, 6-May-2019.)
⊢ (∀𝑥∀𝑦(𝜑 → 𝜓) → (∃𝑥∃𝑦𝜑 → ∃𝑥∃𝑦𝜓))
Theorem	bj-2exbi 37205	Closed form of 2exbii 1879. (Contributed by BJ, 6-May-2019.)
⊢ (∀𝑥∀𝑦(𝜑 ↔ 𝜓) → (∃𝑥∃𝑦𝜑 ↔ ∃𝑥∃𝑦𝜓))
Theorem	bj-3exbi 37206	Closed form of 3exbii 1880. (Contributed by BJ, 6-May-2019.)
⊢ (∀𝑥∀𝑦∀𝑧(𝜑 ↔ 𝜓) → (∃𝑥∃𝑦∃𝑧𝜑 ↔ ∃𝑥∃𝑦∃𝑧𝜓))
Theorem	bj-sylget 37207	Dual statement of sylgt 1852. Closed form of bj-sylge 37210. (Contributed by BJ, 2-May-2019.)
⊢ (∀𝑥(𝜒 → 𝜑) → ((∃𝑥𝜑 → 𝜓) → (∃𝑥𝜒 → 𝜓)))
Theorem	bj-sylget2 37208	Uncurried (imported) form of bj-sylget 37207. (Contributed by BJ, 2-May-2019.)
⊢ ((∀𝑥(𝜑 → 𝜓) ∧ (∃𝑥𝜓 → 𝜒)) → (∃𝑥𝜑 → 𝜒))
Theorem	bj-exlimg 37209	The general form of the *exlim* family of theorems: if 𝜑 is substituted for 𝜓, then the antecedent expresses a form of nonfreeness of 𝑥 in 𝜑, so the theorem means that under a nonfreeness condition in a consequent, one can deduce from the universally quantified implication an implication where the antecedent is existentially quantified. Dual of bj-alrimg 37187. (Contributed by BJ, 9-Dec-2023.)
⊢ ((∃𝑥𝜑 → 𝜓) → (∀𝑥(𝜒 → 𝜑) → (∃𝑥𝜒 → 𝜓)))
Theorem	bj-sylge 37210	Dual statement of sylg 1853 (the final "e" in the label stands for "existential (version of sylg 1853)". Variant of exlimih 2324. (Contributed by BJ, 25-Dec-2023.)
⊢ (∃𝑥𝜑 → 𝜓)    &   ⊢ (𝜒 → 𝜑)    ⇒   ⊢ (∃𝑥𝜒 → 𝜓)
Theorem	bj-exlimd 37211	A slightly more general exlimd 2254. A common usage will have 𝜑 substituted for 𝜓 and 𝜃 substituted for 𝜏, giving a form closer to exlimd 2254. (Contributed by BJ, 25-Dec-2023.)
⊢ (𝜑 → ∀𝑥𝜓)    &   ⊢ (𝜑 → (∃𝑥𝜃 → 𝜏))    &   ⊢ (𝜓 → (𝜒 → 𝜃))    ⇒   ⊢ (𝜑 → (∃𝑥𝜒 → 𝜏))
Theorem	bj-nfimexal 37212	A weak from of nonfreeness in either an antecedent or a consequent implies that a universally quantified implication is equivalent to the associated implication where the antecedent is existentially quantified and the consequent is universally quantified. The forward implication always holds (this is 19.38 1869) and the converse implication is the join of instances of bj-alrimg 37187 and bj-exlimg 37209 (see 19.38a 1870 and 19.38b 1871). TODO: prove a version where the antecedents use the nonfreeness quantifier. (Contributed by BJ, 9-Dec-2023.)
⊢ (((∃𝑥𝜑 → ∀𝑥𝜑) ∨ (∃𝑥𝜓 → ∀𝑥𝜓)) → ((∃𝑥𝜑 → ∀𝑥𝜓) ↔ ∀𝑥(𝜑 → 𝜓)))
Theorem	bj-exim 37213	Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 10-Jan-1993.) (Proof shortened by Wolf Lammen, 4-Jul-2014.) Prove it directly from alim 1840 to allow use in bj-alexim 37214. (Revised by BJ, 9-Dec-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓))
Theorem	bj-alexim 37214	Closed form of aleximi 1862. Note: this proof is shorter, so aleximi 1862 could be deduced from it (exim 1864 would have to be proved first, see bj-exim 37213). (Contributed by BJ, 8-Nov-2021.)
⊢ (∀𝑥(𝜑 → (𝜓 → 𝜒)) → (∀𝑥𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒)))
Theorem	bj-aleximiALT 37215	Alternate proof of aleximi 1862 from exim 1864, which is sometimes used as an axiom in instuitionistic modal logic. (Contributed by BJ, 9-Dec-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (∀𝑥𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))
Theorem	bj-hbxfrbi 37216	Closed form of hbxfrbi 1855. Note: it is less important than nfbiit 1881. The antecedent is in the "strong necessity" modality of modal logic (see also bj-nnftht 37349) in order not to require sp 2219 (modal T). See bj-hbyfrbi 37217 for its version with existential quantifiers. (Contributed by BJ, 6-May-2019.)
⊢ (((𝜑 ↔ 𝜓) ∧ ∀𝑥(𝜑 ↔ 𝜓)) → ((𝜑 → ∀𝑥𝜑) ↔ (𝜓 → ∀𝑥𝜓)))
Theorem	bj-hbyfrbi 37217	Version of bj-hbxfrbi 37216 with existential quantifiers. (Contributed by BJ, 23-Aug-2023.)
⊢ (((𝜑 ↔ 𝜓) ∧ ∀𝑥(𝜑 ↔ 𝜓)) → ((∃𝑥𝜑 → 𝜑) ↔ (∃𝑥𝜓 → 𝜓)))
Theorem	bj-exalim 37218	Distribute quantifiers over a nested implication. This and the following theorems are the general instances of already proved theorems. They could be moved to the main part, before ax-5 1940. I propose to move to the main part: bj-exalim 37218, bj-exalimi 37219, bj-eximcom 37220 bj-exalims 37221, bj-exalimsi 37222, bj-ax12i 37225, bj-ax12wlem 37248, bj-ax12w 37281. A new label is needed for bj-ax12i 37225 and label suggestions are welcome for the others. I also propose to change ¬ ∀𝑥¬ to ∃𝑥 in speimfw 1993 and spimfw 1995 (other spim* theorems use ∃𝑥 and very few theorems in set.mm use ¬ ∀𝑥¬). (Contributed by BJ, 8-Nov-2021.)
⊢ (∀𝑥(𝜑 → (𝜓 → 𝜒)) → (∃𝑥𝜑 → (∀𝑥𝜓 → ∃𝑥𝜒)))
Theorem	bj-exalimi 37219	An inference for distributing quantifiers over a nested implication. The canonical derivation from its closed form bj-exalim 37218 (using mpg 1827) has fewer essential steps, but more steps in total (yielding a longer compressed proof). (Almost) the general statement that speimfw 1993 proves. (Contributed by BJ, 29-Sep-2019.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (∃𝑥𝜑 → (∀𝑥𝜓 → ∃𝑥𝜒))
Theorem	bj-eximcom 37220	A commuted form of exim 1864 which is sometimes posited as an axiom in instuitionistic modal logic. Forward implication of 19.35 1907. Its converse is not intuitionistic. (Contributed by BJ, 9-Dec-2023.)
⊢ (∃𝑥(𝜑 → 𝜓) → (∀𝑥𝜑 → ∃𝑥𝜓))
Theorem	bj-exalims 37221	Distributing quantifiers over a nested implication. (Almost) the general statement that spimfw 1995 proves. (Contributed by BJ, 29-Sep-2019.)
⊢ (∃𝑥𝜑 → (¬ 𝜒 → ∀𝑥 ¬ 𝜒))    ⇒   ⊢ (∀𝑥(𝜑 → (𝜓 → 𝜒)) → (∃𝑥𝜑 → (∀𝑥𝜓 → 𝜒)))
Theorem	bj-exalimsi 37222	An inference for distributing quantifiers over a nested implication. (Almost) the general statement that spimfw 1995 proves. (Contributed by BJ, 29-Sep-2019.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (∃𝑥𝜑 → (¬ 𝜒 → ∀𝑥 ¬ 𝜒))    ⇒   ⊢ (∃𝑥𝜑 → (∀𝑥𝜓 → 𝜒))
Theorem	bj-axdd2ALT 37223	Alternate proof of bj-axdd2 37166 (this should replace bj-axdd2 37166 when bj-exalimi 37219 is moved to the main section). (Contributed by BJ, 8-Mar-2026.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∃𝑥𝜑 → (∀𝑥𝜓 → ∃𝑥𝜓))
Theorem	bj-ax12ig 37224	A lemma used to prove a weak form of the axiom of substitution. A generalization of bj-ax12i 37225. (Contributed by BJ, 19-Dec-2020.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → (𝜒 → ∀𝑥𝜒))    ⇒   ⊢ (𝜑 → (𝜓 → ∀𝑥(𝜑 → 𝜓)))
Theorem	bj-ax12i 37225	A weakening of bj-ax12ig 37224 that is sufficient to prove a weak form of the axiom of substitution ax-12 2213. The general statement of which ax12i 1996 is an instance. (Contributed by BJ, 29-Sep-2019.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜒 → ∀𝑥𝜒)    ⇒   ⊢ (𝜑 → (𝜓 → ∀𝑥(𝜑 → 𝜓)))
Theorem	bj-nfimt 37226	Closed form of nfim 1926 and curried (exported) form of nfimt 1925. (Contributed by BJ, 20-Oct-2021.) Proof should not use 19.35 1907. (Proof modification is discouraged.)
⊢ (Ⅎ𝑥𝜑 → (Ⅎ𝑥𝜓 → Ⅎ𝑥(𝜑 → 𝜓)))
Theorem	bj-spimnfe 37227	A universal specification result: if 𝜑 is true for all values of 𝑥 and implies 𝜓 for at least one value, and if furthermore 𝑥 is ∃-weakly nonfree in 𝜓, then 𝜓 follows. An intermediate result on the way to prove 19.36i 2267, bj-19.36im 37369, 19.36imv 1975, spimfw 1995... (Contributed by BJ, 3-Apr-2026.) Proof should not use 19.35 1907. (Proof modification is discouraged.)
⊢ ((∃𝑥𝜓 → 𝜓) → (∃𝑥(𝜑 → 𝜓) → (∀𝑥𝜑 → 𝜓)))
Theorem	bj-spimenfa 37228	An existential generalization result: if 𝜑 holds and implies 𝜓 for at least one value of 𝑥, and if furthermore 𝑥 is ∀ -weakly nonfree in 𝜑, then 𝜓 holds for at least one value of 𝑥. (Contributed by BJ, 3-Apr-2026.) Proof should not use 19.35 1907. (Proof modification is discouraged.)
⊢ ((𝜑 → ∀𝑥𝜑) → (∃𝑥(𝜑 → 𝜓) → (𝜑 → ∃𝑥𝜓)))
Theorem	bj-spim 37229	A lemma for universal specification. In applications, 𝑥 = 𝑦 will be substituted for 𝜓 and ax6ev 1999 will prove Hypothesis bj-spim.denote. (Contributed by BJ, 4-Apr-2026.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → (∃𝑥𝜃 → 𝜃))    &   ⊢ (𝜑 → ∃𝑥𝜓)    &   ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))    ⇒   ⊢ (𝜑 → (∀𝑥𝜒 → 𝜃))
Theorem	bj-spime 37230	A lemma for existential generalization. In applications, 𝑥 = 𝑦 will be substituted for 𝜓 and ax6ev 1999 will prove Hypothesis bj-spime.denote. (Contributed by BJ, 4-Apr-2026.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → (𝜒 → ∀𝑥𝜒))    &   ⊢ (𝜑 → ∃𝑥𝜓)    &   ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))    ⇒   ⊢ (𝜑 → (𝜒 → ∃𝑥𝜃))
Theorem	bj-cbvalimd0 37231	A lemma for alpha-renaming of variables bound by a universal quantifier. In applications, 𝑥 = 𝑦 will be substituted for 𝜓 and ax6ev 1999 will prove Hypothesis bj-cbvalimd0.denote. When ax6ev 1999 is not available but only its universal closure is, then bj-cbvalimd 37234 or bj-cbvalimdv 37236 should be used (see bj-cbvalimdlem 37232, bj-cbval 37249). (Contributed by BJ, 4-Apr-2026.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → ∀𝑦𝜑)    &   ⊢ (𝜑 → (𝜒 → ∀𝑦𝜒))    &   ⊢ (𝜑 → (∃𝑥𝜃 → 𝜃))    &   ⊢ (𝜑 → ∃𝑥𝜓)    &   ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))    ⇒   ⊢ (𝜑 → (∀𝑥𝜒 → ∀𝑦𝜃))
Theorem	bj-cbvalimdlem 37232	A lemma for alpha-renaming of variables bound by a universal quantifier. Hypothesis bj-cbvalimdlem.nfch can be proved either from DV conditions as in bj-cbvalimdv 37236 or from a nonfreeness condition and alcom 2194 as in bj-cbvalimd 37234. Hypothesis bj-cbvalimdlem.denote is weaker than the corresponding hypothesis of bj-cbvalimd0 37231, and this proof is therefore a bit longer, not using bj-spim 37229 but bj-eximcom 37220. (Contributed by BJ, 12-Mar-2023.) Proof should not use 19.35 1907. (Proof modification is discouraged.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → ∀𝑦𝜑)    &   ⊢ (𝜑 → (∀𝑥𝜒 → ∀𝑦∀𝑥𝜒))    &   ⊢ (𝜑 → (∃𝑥𝜃 → 𝜃))    &   ⊢ (𝜑 → ∀𝑦∃𝑥𝜓)    &   ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))    ⇒   ⊢ (𝜑 → (∀𝑥𝜒 → ∀𝑦𝜃))
Theorem	bj-cbveximdlem 37233	A lemma for alpha-renaming of variables bound by an existential quantifier. Hypothesis bj-cbveximdlem.nfth can be proved either from DV conditions as in bj-cbveximdv 37237 or from a nonfreeness condition and excom 2197 as in bj-cbveximd 37235. Hypothesis bj-cbveximdlem.denote is weaker than the corresponding hypothesis of ~ bj-cbveximd0 , and this proof is therefore a bit longer, not using bj-spime 37230 but bj-eximcom 37220. (Contributed by BJ, 12-Mar-2023.) Proof should not use 19.35 1907. (Proof modification is discouraged.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → ∀𝑦𝜑)    &   ⊢ (𝜑 → (𝜒 → ∀𝑦𝜒))    &   ⊢ (𝜑 → (∃𝑥∃𝑦𝜃 → ∃𝑦𝜃))    &   ⊢ (𝜑 → ∀𝑥∃𝑦𝜓)    &   ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))    ⇒   ⊢ (𝜑 → (∃𝑥𝜒 → ∃𝑦𝜃))
Theorem	bj-cbvalimd 37234	A lemma for alpha-renaming of variables bound by a universal quantifier. (Contributed by BJ, 4-Apr-2026.) (Proof modification is discouraged.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → ∀𝑦𝜑)    &   ⊢ (𝜑 → (𝜒 → ∀𝑦𝜒))    &   ⊢ (𝜑 → (∃𝑥𝜃 → 𝜃))    &   ⊢ (𝜑 → ∀𝑦∃𝑥𝜓)    &   ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))    ⇒   ⊢ (𝜑 → (∀𝑥𝜒 → ∀𝑦𝜃))
Theorem	bj-cbveximd 37235	A lemma for alpha-renaming of variables bound by an existential quantifier. (Contributed by BJ, 4-Apr-2026.) (Proof modification is discouraged.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → ∀𝑦𝜑)    &   ⊢ (𝜑 → (𝜒 → ∀𝑦𝜒))    &   ⊢ (𝜑 → (∃𝑥𝜃 → 𝜃))    &   ⊢ (𝜑 → ∀𝑥∃𝑦𝜓)    &   ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))    ⇒   ⊢ (𝜑 → (∃𝑥𝜒 → ∃𝑦𝜃))
Theorem	bj-cbvalimdv 37236*	A lemma for alpha-renaming of variables bound by a universal quantifier. (Contributed by BJ, 4-Apr-2026.) (Proof modification is discouraged.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → ∀𝑦𝜑)    &   ⊢ (𝜑 → (∃𝑥𝜃 → 𝜃))    &   ⊢ (𝜑 → ∀𝑦∃𝑥𝜓)    &   ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))    ⇒   ⊢ (𝜑 → (∀𝑥𝜒 → ∀𝑦𝜃))
Theorem	bj-cbveximdv 37237*	A lemma for alpha-renaming of variables bound by an existential quantifier. (Contributed by BJ, 4-Apr-2026.) (Proof modification is discouraged.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → ∀𝑦𝜑)    &   ⊢ (𝜑 → (𝜒 → ∀𝑦𝜒))    &   ⊢ (𝜑 → ∀𝑥∃𝑦𝜓)    &   ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))    ⇒   ⊢ (𝜑 → (∃𝑥𝜒 → ∃𝑦𝜃))
21.19.4.4  Adding ax-5
Theorem	bj-spvw 37238*	Version of spvw 2011 and 19.3v 2012 proved from ax-1 6-- ax-5 1940. The antecedent can for instance be proved with the existence axiom extru 2005. (Contributed by BJ, 8-Mar-2026.) (Proof modification is discouraged.)
⊢ (∃𝑥𝜑 → (𝜓 ↔ ∀𝑥𝜓))
Theorem	bj-spvew 37239*	Version of 19.8v 2013 and 19.9v 2014 proved from ax-1 6-- ax-5 1940. The antecedent can for instance be proved with the existence axiom extru 2005. (Contributed by BJ, 8-Mar-2026.) This could also be proved from bj-spvw 37238 using duality, but that proof would not be intuitionistic, contrary to the present one. (Proof modification is discouraged.)
⊢ (∃𝑥𝜑 → (𝜓 ↔ ∃𝑥𝜓))
Theorem	bj-alextruim 37240*	An equivalent expression for universal quantification over a non-occurring variable proved over ax-1 6-- ax-5 1940. The forward implication can be strengthened when ax-6 1997 is posited (which implies that models are non-empty), see spvw 2011. The reverse implication can be seen as a strengthening of ax-5 1940 (since the antecedent of the implication is weakened). See bj-exextruan 37241 for a dual statement. An approximate meaning is: the universal quantification of a proposition over a non-occurring variable holds if and only if the proposition holds in nonempty universes. (Contributed by BJ, 14-Mar-2026.) (Proof modification is discouraged.)
⊢ (∀𝑥𝜑 ↔ (∃𝑥⊤ → 𝜑))
Theorem	bj-exextruan 37241*	An equivalent expression for existential quantification over a non-occurring variable proved over ax-1 6-- ax-5 1940. The forward implication can be seen as a strengthening of ax-5 1940 (a conjunct is added to the consequent of the implication). The reverse implication can be strengthened when ax-6 1997 is posited (which implies that models are non-empty), see 19.8v 2013. See bj-alextruim 37240 for a dual statement. An approximate meaning is: the existential quantification of a proposition over a non-occurring variable holds if and only if the proposition holds and the universe is nonempty. (Contributed by BJ, 14-Mar-2026.) (Proof modification is discouraged.)
⊢ (∃𝑥𝜑 ↔ (∃𝑥⊤ ∧ 𝜑))
Theorem	bj-cbvalvv 37242*	Universally quantifying over a non-occurring variable is independent of that variable, over ax-1 6-- ax-5 1940 and the existence axiom extru 2005. See bj-cbvaw 37244 for a strengthening. (Contributed by BJ, 8-Mar-2026.) (Proof modification is discouraged.)
⊢ (∃𝑥𝜑 → (∀𝑥𝜓 → ∀𝑦𝜓))
Theorem	bj-cbvexvv 37243*	Existentially quantifying over a non-occurring variable is independent of that variable, over ax-1 6-- ax-5 1940 and the existence axiom extru 2005. See bj-cbvew 37245 for a strengthening. (Contributed by BJ, 8-Mar-2026.) (Proof modification is discouraged.)
⊢ (∃𝑥𝜑 → (∃𝑦𝜓 → ∃𝑥𝜓))
Theorem	bj-cbvaw 37244*	Universally quantifying over a non-occurring variable is independent from the variable, under a weaker condition than in bj-cbvalvv 37242. If ⊥ is substituted for 𝜑, then the statement reads: "universally quantifying over a non-occurring variable is independent from the variable as soon as that result is true for the False truth constant". The label "cbvaw" means "'change bound variable' theorem, 'all' quantifier, weak version". (Contributed by BJ, 14-Mar-2026.) This proof is not intuitionistic (it uses ja 188); an intuitionistically valid statement is obtained by expressing the antecedent as a disjunction (classically equivalent through imor 866). (Proof modification is discouraged.)
⊢ ((∀𝑥𝜑 → ∀𝑦⊥) → (∀𝑥𝜓 → ∀𝑦𝜓))
Theorem	bj-cbvew 37245*	Existentially quantifying over a non-occurring variable is independent from the variable, under a weaker condition than in bj-cbvexvv 37243. If ⊤ is substituted for 𝜑, then the statement reads: "existentially quantifying over a non-occurring variable is independent from the variable as soon as that result is true for the True truth constant. The label "cbvew" means "'change bound variable' theorem, 'exists' quantifier, weak version". (Contributed by BJ, 14-Mar-2026.) This proof is intuitionistic. (Proof modification is discouraged.)
⊢ ((∃𝑥⊤ → ∃𝑦𝜑) → (∃𝑥𝜓 → ∃𝑦𝜓))
Theorem	bj-cbveaw 37246*	Universally quantifying over a non-occurring variable is independent from the variable, under a weaker condition than in bj-cbvalvv 37242. (Contributed by BJ, 14-Mar-2026.) (Proof modification is discouraged.)
⊢ ((∃𝑥⊤ → ∃𝑦𝜑) → (∀𝑦𝜓 → ∀𝑥𝜓))
Theorem	bj-cbvaew 37247*	Exixtentially quantifying over a non-occurring variable is independent from the variable, under a weaker condition than in bj-cbvexvv 37243. (Contributed by BJ, 14-Mar-2026.) (Proof modification is discouraged.)
⊢ ((∀𝑥𝜑 → ∀𝑦⊥) → (∃𝑦𝜓 → ∃𝑥𝜓))
Theorem	bj-ax12wlem 37248*	A lemma used to prove a weak version of the axiom of substitution ax-12 2213. (Temporary comment: The general statement that ax12wlem 2167 proves.) (Contributed by BJ, 20-Mar-2020.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (𝜓 → ∀𝑥(𝜑 → 𝜓)))
Theorem	bj-cbval 37249*	Changing a bound variable (universal quantification case) in a weak axiomatization that assumes that all variables denote (which is valid in inclusive free logic) and that equality is symmetric. (Contributed by BJ, 12-Mar-2023.) Proved from ax-1 6-- ax-5 1940. (Proof modification is discouraged.)
⊢ ∀𝑦∃𝑥 𝑥 = 𝑦    &   ⊢ ∀𝑥∃𝑦 𝑦 = 𝑥    &   ⊢ (𝑦 = 𝑥 → 𝑥 = 𝑦)    &   ⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → ∀𝑦𝜑)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒))
Theorem	bj-cbvex 37250*	Changing a bound variable (existential quantification case) in a weak axiomatization that assumes that all variables denote (which is valid in inclusive free logic) and that equality is symmetric. (Contributed by BJ, 12-Mar-2023.) Proved from ax-1 6-- ax-5 1940. (Proof modification is discouraged.)
⊢ ∀𝑦∃𝑥 𝑥 = 𝑦    &   ⊢ ∀𝑥∃𝑦 𝑦 = 𝑥    &   ⊢ (𝑦 = 𝑥 → 𝑥 = 𝑦)    &   ⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → ∀𝑦𝜑)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑦𝜒))
Syntax	wmoo 37251	Syntax for BJ's version of the uniqueness quantifier.
wff ∃**𝑥𝜑
Definition	df-bj-mo 37252*	Definition of the uniqueness quantifier which is correct on the empty domain. Instead of the fresh variable 𝑧, one could save a dummy variable by using 𝑥 or 𝑦 at the cost of having nested quantifiers on the same variable. (Contributed by BJ, 12-Mar-2023.)
⊢ (∃**𝑥𝜑 ↔ ∀𝑧∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦))
21.19.4.5  Equality and substitution
Theorem	bj-df-sb 37253*	Proposed definition to replace df-sb 2097 and df-sbc 3746. Proof is therefore unimportant. Contrary to df-sb 2097, this definition makes a substituted formula false when one substitutes a non-existent object for a variable: this is better suited to the "Levy-style" treatment of classes as virtual objects adopted by set.mm. That difference is unimportant since as soon as ax6ev 1999 is posited, all variables "exist". (Contributed by BJ, 19-Feb-2026.)
⊢ ([𝐴 / 𝑥]𝜑 ↔ ∃𝑦(𝑦 = 𝐴 ∧ ∀𝑥(𝑥 = 𝑦 → 𝜑)))
Theorem	bj-sbcex 37254	Proof of sbcex 3755 when taking bj-df-sb 37253 as definition. (Contributed by BJ, 19-Feb-2026.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ([𝐴 / 𝑥]𝜑 → 𝐴 ∈ V)
Theorem	bj-dfsbc 37255	Proof of df-sbc 3746 when taking bj-df-sb 37253 as definition. (Contributed by BJ, 19-Feb-2026.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ [𝐴 / 𝑥]𝜑)
Theorem	bj-ssbeq 37256*	Substitution in an equality, disjoint variables case. Uses only ax-1 6 through ax-6 1997. It might be shorter to prove the result about composition of two substitutions and prove bj-ssbeq 37256 first with a DV condition on 𝑥, 𝑡, and then in the general case. (Contributed by BJ, 22-Dec-2020.) (Proof modification is discouraged.)
⊢ ([𝑡 / 𝑥]𝑦 = 𝑧 ↔ 𝑦 = 𝑧)
Theorem	bj-ssblem1 37257*	A lemma for the definiens of df-sb 2097. An instance of sp 2219 proved without it. Note: it has a common subproof with sbjust 2095. (Contributed by BJ, 22-Dec-2020.) (Proof modification is discouraged.)
⊢ (∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑)) → (𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
Theorem	bj-ssblem2 37258*	An instance of ax-11 2192 proved without it. The converse may not be provable without ax-11 2192 (since using alcomimw 2073 would require a DV on 𝜑, 𝑥, which defeats the purpose). (Contributed by BJ, 22-Dec-2020.) (Proof modification is discouraged.)
⊢ (∀𝑥∀𝑦(𝑦 = 𝑡 → (𝑥 = 𝑦 → 𝜑)) → ∀𝑦∀𝑥(𝑦 = 𝑡 → (𝑥 = 𝑦 → 𝜑)))
Theorem	bj-ax12v 37259*	A weaker form of ax-12 2213 and ax12v 2214, namely the generalization over 𝑥 of the latter. In this statement, all occurrences of 𝑥 are bound. (Contributed by BJ, 26-Dec-2020.) (Proof modification is discouraged.)
⊢ ∀𝑥(𝑥 = 𝑡 → (𝜑 → ∀𝑥(𝑥 = 𝑡 → 𝜑)))
Theorem	bj-ax12 37260*	Remove a DV condition from bj-ax12v 37259 (using core axioms only). (Contributed by BJ, 26-Dec-2020.) (Proof modification is discouraged.)
⊢ ∀𝑥(𝑥 = 𝑡 → (𝜑 → ∀𝑥(𝑥 = 𝑡 → 𝜑)))
Theorem	bj-ax12ssb 37261*	Axiom bj-ax12 37260 expressed using substitution. (Contributed by BJ, 26-Dec-2020.) (Proof modification is discouraged.)
⊢ [𝑡 / 𝑥](𝜑 → [𝑡 / 𝑥]𝜑)
Theorem	bj-19.41al 37262	Special case of 19.41 2271 proved from core axioms, ax-10 2176 (modal5), and hba1 2328 (modal4). (Contributed by BJ, 29-Dec-2020.) (Proof modification is discouraged.)
⊢ (∃𝑥(𝜑 ∧ ∀𝑥𝜓) ↔ (∃𝑥𝜑 ∧ ∀𝑥𝜓))
Theorem	bj-equsexval 37263*	Special case of equsexv 2304 proved from core axioms, ax-10 2176 (modal5), and hba1 2328 (modal4). (Contributed by BJ, 29-Dec-2020.) (Proof modification is discouraged.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ ∀𝑥𝜓))    ⇒   ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ ∀𝑥𝜓)
Theorem	bj-subst 37264*	Proof of sbalex 2278 from core axioms, ax-10 2176 (modal5), and bj-ax12 37260. (Contributed by BJ, 29-Dec-2020.) (Proof modification is discouraged.)
⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑))
Theorem	bj-ssbid2 37265	A special case of sbequ2 2285. (Contributed by BJ, 22-Dec-2020.)
⊢ ([𝑥 / 𝑥]𝜑 → 𝜑)
Theorem	bj-ssbid2ALT 37266	Alternate proof of bj-ssbid2 37265, not using sbequ2 2285. (Contributed by BJ, 22-Dec-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ([𝑥 / 𝑥]𝜑 → 𝜑)
Theorem	bj-ssbid1 37267	A special case of sbequ1 2284. (Contributed by BJ, 22-Dec-2020.)
⊢ (𝜑 → [𝑥 / 𝑥]𝜑)
Theorem	bj-ssbid1ALT 37268	Alternate proof of bj-ssbid1 37267, not using sbequ1 2284. (Contributed by BJ, 22-Dec-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → [𝑥 / 𝑥]𝜑)
Theorem	bj-ax6elem1 37269*	Lemma for bj-ax6e 37271. (Contributed by BJ, 22-Dec-2020.) (Proof modification is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧))
Theorem	bj-ax6elem2 37270*	Lemma for bj-ax6e 37271. (Contributed by BJ, 22-Dec-2020.) (Proof modification is discouraged.)
⊢ (∀𝑥 𝑦 = 𝑧 → ∃𝑥 𝑥 = 𝑦)
Theorem	bj-ax6e 37271	Proof of ax6e 2415 (hence ax6 2416) from Tarski's system, ax-c9 39645, ax-c16 39647. Remark: ax-6 1997 is used only via its principal (unbundled) instance ax6v 1998. (Contributed by BJ, 22-Dec-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∃𝑥 𝑥 = 𝑦
21.19.4.6  Adding ax-6
Theorem	bj-spim0 37272*	A universal specialization result in deduction form, proved from ax-1 6 -- ax-6 1997, 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 37273*	Closed form of spimvw 2016. See also spimt 2418. (Contributed by BJ, 8-Nov-2021.)
⊢ (∀𝑥(𝑥 = 𝑦 → (𝜑 → 𝜓)) → (∀𝑥𝜑 → 𝜓))
Theorem	bj-spnfw 37274	Theorem close to a closed form of spnfw 2009. (Contributed by BJ, 12-May-2019.)
⊢ ((∃𝑥𝜑 → 𝜓) → (∀𝑥𝜑 → 𝜓))
Theorem	bj-cbvexiw 37275*	Change bound variable. This is to cbvexvw 2067 what cbvaliw 2036 is to cbvalvw 2066. TODO: move after cbvalivw 2037. (Contributed by BJ, 17-Mar-2020.)
⊢ (∃𝑥∃𝑦𝜓 → ∃𝑦𝜓)    &   ⊢ (𝜑 → ∀𝑦𝜑)    &   ⊢ (𝑦 = 𝑥 → (𝜑 → 𝜓))    ⇒   ⊢ (∃𝑥𝜑 → ∃𝑦𝜓)
Theorem	bj-cbvexivw 37276*	Change bound variable. This is to cbvexvw 2067 what cbvalivw 2037 is to cbvalvw 2066. TODO: move after cbvalivw 2037. (Contributed by BJ, 17-Mar-2020.)
⊢ (𝑦 = 𝑥 → (𝜑 → 𝜓))    ⇒   ⊢ (∃𝑥𝜑 → ∃𝑦𝜓)
Theorem	bj-modald 37277	A short form of the axiom D of modal logic. (Contributed by BJ, 4-Apr-2021.)
⊢ (∀𝑥 ¬ 𝜑 → ¬ ∀𝑥𝜑)
Theorem	bj-denot 37278*	A weakening of ax-6 1997 and ax6v 1998. (Contributed by BJ, 4-Apr-2021.) (New usage is discouraged.)
⊢ (𝑥 = 𝑥 → ¬ ∀𝑦 ¬ 𝑦 = 𝑥)
Theorem	bj-eqs 37279*	A lemma for substitutions, proved from Tarski's FOL. The version without DV (𝑥, 𝑦) is true but requires ax-13 2404. 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 37280*	Change bound variable. This is to cbvexvw 2067 what cbvalw 2065 is to cbvalvw 2066. (Contributed by BJ, 17-Mar-2020.)
⊢ (∃𝑥∃𝑦𝜓 → ∃𝑦𝜓)    &   ⊢ (𝜑 → ∀𝑦𝜑)    &   ⊢ (∃𝑦∃𝑥𝜑 → ∃𝑥𝜑)    &   ⊢ (𝜓 → ∀𝑥𝜓)    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓)
Theorem	bj-ax12w 37281*	The general statement that ax12w 2168 proves. (Contributed by BJ, 20-Mar-2020.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑦 = 𝑧 → (𝜓 ↔ 𝜃))    ⇒   ⊢ (𝜑 → (∀𝑦𝜓 → ∀𝑥(𝜑 → 𝜓)))
21.19.4.8  Membership predicate, ax-8 and ax-9
Theorem	bj-ax89 37282	A theorem which could be used as sole axiom for the non-logical predicate instead of ax-8 2145 and ax-9 2153. Indeed, it is implied over propositional calculus by the conjunction of ax-8 2145 and ax-9 2153, as proved here. In the other direction, one can prove ax-8 2145 (respectively ax-9 2153) from bj-ax89 37282 by using mpan2 703 (respectively mpan 702) and equid 2042. TODO: move to main part. (Contributed by BJ, 3-Oct-2019.)
⊢ ((𝑥 = 𝑦 ∧ 𝑧 = 𝑡) → (𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑡))
Theorem	bj-cleljusti 37283*	One direction of cleljust 2152, requiring only ax-1 6-- ax-5 1940 and ax8v1 2147. (Contributed by BJ, 31-Dec-2020.) (Proof modification is discouraged.)
⊢ (∃𝑧(𝑧 = 𝑥 ∧ 𝑧 ∈ 𝑦) → 𝑥 ∈ 𝑦)
21.19.4.9  Adding ax-11
Theorem	bj-alcomexcom 37284	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 1839 section, soon after 2nexaln 1860, and used to prove excom 2197. (Contributed by BJ, 29-Nov-2020.) (Proof modification is discouraged.)
⊢ ((∀𝑥∀𝑦 ¬ 𝜑 → ∀𝑦∀𝑥 ¬ 𝜑) ↔ (∃𝑦∃𝑥𝜑 → ∃𝑥∃𝑦𝜑))
Theorem	bj-hbald 37285	General statement that hbald 2203 proves . (Contributed by BJ, 4-Apr-2026.)
⊢ (𝜑 → ∀𝑦𝜓)    &   ⊢ (𝜓 → (𝜒 → ∀𝑥𝜃))    ⇒   ⊢ (𝜑 → (∀𝑦𝜒 → ∀𝑥∀𝑦𝜃))
Theorem	bj-hbalt 37286	Closed form of (general instance of) hbal 2202. (Contributed by BJ, 2-May-2019.)
⊢ (∀𝑦(𝜑 → ∀𝑥𝜓) → (∀𝑦𝜑 → ∀𝑥∀𝑦𝜓))
Theorem	bj-hbal 37287	More general instance of hbal 2202. (Contributed by BJ, 4-Apr-2026.)
⊢ (𝜑 → ∀𝑥𝜓)    ⇒   ⊢ (∀𝑦𝜑 → ∀𝑥∀𝑦𝜓)
21.19.4.10  Adding ax-12
Theorem	axc11n11 37288	Proof of axc11n 2458 from { ax-1 6-- ax-7 2038, axc11 2462 } . Almost identical to axc11nfromc11 39681. (Contributed by NM, 6-Jul-2021.) (Proof modification is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥)
Theorem	axc11n11r 37289	Proof of axc11n 2458 from { ax-1 6-- ax-7 2038, axc9 2414, axc11r 2400 } (note that axc16 2297 is provable from { ax-1 6-- ax-7 2038, axc11r 2400 }). Note that axc11n 2458 proves (over minimal calculus) that axc11 2462 and axc11r 2400 are equivalent. Therefore, axc11n11 37288 and axc11n11r 37289 prove that one can use one or the other as an axiom, provided one assumes the axioms listed above (axc11 2462 appears slightly stronger since axc11n11r 37289 requires axc9 2414 while axc11n11 37288 does not). (Contributed by BJ, 6-Jul-2021.) (Proof modification is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥)
Theorem	bj-axc16g16 37290*	Proof of axc16g 2296 from { ax-1 6-- ax-7 2038, axc16 2297 }. (Contributed by BJ, 6-Jul-2021.) (Proof modification is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑧𝜑))
Theorem	bj-ax12v3 37291*	A weak version of ax-12 2213 which is stronger than ax12v 2214. Note that if one assumes reflexivity of equality ⊢ 𝑥 = 𝑥 (equid 2042), then bj-ax12v3 37291 implies ax-5 1940 over modal logic K (substitute 𝑥 for 𝑦). See also bj-ax12v3ALT 37292. (Contributed by BJ, 6-Jul-2021.) (Proof modification is discouraged.)
⊢ (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
Theorem	bj-ax12v3ALT 37292*	Alternate proof of bj-ax12v3 37291. Uses axc11r 2400 and axc15 2454 instead of ax-12 2213. (Contributed by BJ, 6-Jul-2021.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
Theorem	bj-sb 37293*	A weak variant of sbid2 2540 not requiring ax-13 2404 nor ax-10 2176. On top of Tarski's FOL, one implication requires only ax12v 2214, and the other requires only sp 2219. (Contributed by BJ, 25-May-2021.)
⊢ (𝜑 ↔ ∀𝑦(𝑦 = 𝑥 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
Theorem	bj-modalbe 37294	The predicate-calculus version of the axiom (B) of modal logic. See also modal-b 2352. (Contributed by BJ, 20-Oct-2019.)
⊢ (𝜑 → ∀𝑥∃𝑥𝜑)
Theorem	bj-spst 37295	Closed form of sps 2221. Once in main part, prove sps 2221 and spsd 2223 from it. (Contributed by BJ, 20-Oct-2019.)
⊢ ((𝜑 → 𝜓) → (∀𝑥𝜑 → 𝜓))
Theorem	bj-19.21bit 37296	Closed form of 19.21bi 2225. (Contributed by BJ, 20-Oct-2019.)
⊢ ((𝜑 → ∀𝑥𝜓) → (𝜑 → 𝜓))
Theorem	bj-19.23bit 37297	Closed form of 19.23bi 2227. (Contributed by BJ, 20-Oct-2019.)
⊢ ((∃𝑥𝜑 → 𝜓) → (𝜑 → 𝜓))
Theorem	bj-nexrt 37298	Closed form of nexr 2228. Contrapositive of 19.8a 2217. (Contributed by BJ, 20-Oct-2019.)
⊢ (¬ ∃𝑥𝜑 → ¬ 𝜑)
Theorem	bj-alrim 37299	Closed form of alrimi 2249. (Contributed by BJ, 2-May-2019.)
⊢ (Ⅎ𝑥𝜑 → (∀𝑥(𝜑 → 𝜓) → (𝜑 → ∀𝑥𝜓)))
Theorem	bj-alrim2 37300	Uncurried (imported) form of bj-alrim 37299. (Contributed by BJ, 2-May-2019.)
⊢ ((Ⅎ𝑥𝜑 ∧ ∀𝑥(𝜑 → 𝜓)) → (𝜑 → ∀𝑥𝜓))