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-almpig 36901	A partially quantified form of mpi 20 similar to bj-almpi 36900. (Contributed by BJ, 19-Mar-2026.)
⊢ (𝜑 → (𝜒 → 𝜓))    &   ⊢ ∀𝑥𝜒    ⇒   ⊢ ∀𝑥(𝜑 → 𝜓)
Theorem	bj-alsyl 36902	Syllogism under the universal quantifier, in the curried form appearing as Theorem *10.3 of [WhiteheadRussell] p. 145. See alsyl 1895 for the uncurried form. (Contributed by BJ, 28-Mar-2026.)
⊢ (∀𝑥(𝜑 → 𝜓) → (∀𝑥(𝜓 → 𝜒) → ∀𝑥(𝜑 → 𝜒)))
Theorem	bj-2alim 36903	Closed form of 2alimi 1814. (Contributed by BJ, 6-May-2019.)
⊢ (∀𝑥∀𝑦(𝜑 → 𝜓) → (∀𝑥∀𝑦𝜑 → ∀𝑥∀𝑦𝜓))
Theorem	bj-alimdh 36904	General instance of alimdh 1819. (Contributed by NM, 4-Jan-2002.) State the most general derivable instance. (Revised by BJ, 5-Apr-2026.)
⊢ (𝜑 → ∀𝑥𝜓)    &   ⊢ (𝜓 → (𝜒 → 𝜃))    ⇒   ⊢ (𝜑 → (∀𝑥𝜒 → ∀𝑥𝜃))
Theorem	bj-alrimdh 36905	Deduction form of Theorem 19.21 of [Margaris] p. 90, see 19.21 2215 and 19.21h 2294. (Contributed by NM, 10-Feb-1997.) (Proof shortened by Andrew Salmon, 13-May-2011.) State the most general derivable instance. (Revised by BJ, 5-Apr-2026.)
⊢ (𝜑 → ∀𝑥𝜓)    &   ⊢ (𝜒 → ∀𝑥𝜃)    &   ⊢ (𝜓 → (𝜃 → 𝜏))    ⇒   ⊢ (𝜑 → (𝜒 → ∀𝑥𝜏))
Theorem	bj-alrimd 36906	A slightly more general alrimd 2223. A common usage will have 𝜑 substituted for 𝜓 and 𝜒 substituted for 𝜃, giving a form closer to alrimd 2223. (Contributed by BJ, 25-Dec-2023.)
⊢ (𝜑 → ∀𝑥𝜓)    &   ⊢ (𝜑 → (𝜒 → ∀𝑥𝜃))    &   ⊢ (𝜓 → (𝜃 → 𝜏))    ⇒   ⊢ (𝜑 → (𝜒 → ∀𝑥𝜏))
Theorem	bj-exa1i 36907	Add an antecedent in an existentially quantified formula. Inference associated with exa1 1840. (Contributed by BJ, 6-Oct-2018.)
⊢ ∃𝑥𝜑    ⇒   ⊢ ∃𝑥(𝜓 → 𝜑)
Theorem	bj-alanim 36908	Closed form of alanimi 1818. (Contributed by BJ, 6-May-2019.)
⊢ (∀𝑥((𝜑 ∧ 𝜓) → 𝜒) → ((∀𝑥𝜑 ∧ ∀𝑥𝜓) → ∀𝑥𝜒))
Theorem	bj-2albi 36909	Closed form of 2albii 1822. (Contributed by BJ, 6-May-2019.)
⊢ (∀𝑥∀𝑦(𝜑 ↔ 𝜓) → (∀𝑥∀𝑦𝜑 ↔ ∀𝑥∀𝑦𝜓))
Theorem	bj-notalbii 36910	Equivalence of universal quantification of negation of equivalent formulas. Shortens ab0 4321 (103>94), ballotlem2 34649 (2655>2648), bnj1143 34948 (522>519), hausdiag 23620 (2119>2104). (Contributed by BJ, 17-Jul-2021.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (∀𝑥 ¬ 𝜑 ↔ ∀𝑥 ¬ 𝜓)
Theorem	bj-2exim 36911	Closed form of 2eximi 1838. (Contributed by BJ, 6-May-2019.)
⊢ (∀𝑥∀𝑦(𝜑 → 𝜓) → (∃𝑥∃𝑦𝜑 → ∃𝑥∃𝑦𝜓))
Theorem	bj-2exbi 36912	Closed form of 2exbii 1851. (Contributed by BJ, 6-May-2019.)
⊢ (∀𝑥∀𝑦(𝜑 ↔ 𝜓) → (∃𝑥∃𝑦𝜑 ↔ ∃𝑥∃𝑦𝜓))
Theorem	bj-3exbi 36913	Closed form of 3exbii 1852. (Contributed by BJ, 6-May-2019.)
⊢ (∀𝑥∀𝑦∀𝑧(𝜑 ↔ 𝜓) → (∃𝑥∃𝑦∃𝑧𝜑 ↔ ∃𝑥∃𝑦∃𝑧𝜓))
Theorem	bj-sylget 36914	Dual statement of sylgt 1824. Closed form of bj-sylge 36917. (Contributed by BJ, 2-May-2019.)
⊢ (∀𝑥(𝜒 → 𝜑) → ((∃𝑥𝜑 → 𝜓) → (∃𝑥𝜒 → 𝜓)))
Theorem	bj-sylget2 36915	Uncurried (imported) form of bj-sylget 36914. (Contributed by BJ, 2-May-2019.)
⊢ ((∀𝑥(𝜑 → 𝜓) ∧ (∃𝑥𝜓 → 𝜒)) → (∃𝑥𝜑 → 𝜒))
Theorem	bj-exlimg 36916	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 36894. (Contributed by BJ, 9-Dec-2023.)
⊢ ((∃𝑥𝜑 → 𝜓) → (∀𝑥(𝜒 → 𝜑) → (∃𝑥𝜒 → 𝜓)))
Theorem	bj-sylge 36917	Dual statement of sylg 1825 (the final "e" in the label stands for "existential (version of sylg 1825)". Variant of exlimih 2296. (Contributed by BJ, 25-Dec-2023.)
⊢ (∃𝑥𝜑 → 𝜓)    &   ⊢ (𝜒 → 𝜑)    ⇒   ⊢ (∃𝑥𝜒 → 𝜓)
Theorem	bj-exlimd 36918	A slightly more general exlimd 2226. A common usage will have 𝜑 substituted for 𝜓 and 𝜃 substituted for 𝜏, giving a form closer to exlimd 2226. (Contributed by BJ, 25-Dec-2023.)
⊢ (𝜑 → ∀𝑥𝜓)    &   ⊢ (𝜑 → (∃𝑥𝜃 → 𝜏))    &   ⊢ (𝜓 → (𝜒 → 𝜃))    ⇒   ⊢ (𝜑 → (∃𝑥𝜒 → 𝜏))
Theorem	bj-nfimexal 36919	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 1841) and the converse implication is the join of instances of bj-alrimg 36894 and bj-exlimg 36916 (see 19.38a 1842 and 19.38b 1843). TODO: prove a version where the antecedents use the nonfreeness quantifier. (Contributed by BJ, 9-Dec-2023.)
⊢ (((∃𝑥𝜑 → ∀𝑥𝜑) ∨ (∃𝑥𝜓 → ∀𝑥𝜓)) → ((∃𝑥𝜑 → ∀𝑥𝜓) ↔ ∀𝑥(𝜑 → 𝜓)))
Theorem	bj-exim 36920	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 1812 to allow use in bj-alexim 36921. (Revised by BJ, 9-Dec-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓))
Theorem	bj-alexim 36921	Closed form of aleximi 1834. Note: this proof is shorter, so aleximi 1834 could be deduced from it (exim 1836 would have to be proved first, see bj-exim 36920). (Contributed by BJ, 8-Nov-2021.)
⊢ (∀𝑥(𝜑 → (𝜓 → 𝜒)) → (∀𝑥𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒)))
Theorem	bj-aleximiALT 36922	Alternate proof of aleximi 1834 from exim 1836, 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 36923	Closed form of hbxfrbi 1827. Note: it is less important than nfbiit 1853. 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). See bj-hbyfrbi 36924 for its version with existential quantifiers. (Contributed by BJ, 6-May-2019.)
⊢ (((𝜑 ↔ 𝜓) ∧ ∀𝑥(𝜑 ↔ 𝜓)) → ((𝜑 → ∀𝑥𝜑) ↔ (𝜓 → ∀𝑥𝜓)))
Theorem	bj-hbyfrbi 36924	Version of bj-hbxfrbi 36923 with existential quantifiers. (Contributed by BJ, 23-Aug-2023.)
⊢ (((𝜑 ↔ 𝜓) ∧ ∀𝑥(𝜑 ↔ 𝜓)) → ((∃𝑥𝜑 → 𝜑) ↔ (∃𝑥𝜓 → 𝜓)))
Theorem	bj-exalim 36925	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 1912. I propose to move to the main part: bj-exalim 36925, bj-exalimi 36926, bj-eximcom 36927 bj-exalims 36928, bj-exalimsi 36929, bj-ax12i 36932, bj-ax12wlem 36955, bj-ax12w 36988. A new label is needed for bj-ax12i 36932 and label suggestions are welcome for the others. I also propose to change ¬ ∀𝑥¬ to ∃𝑥 in speimfw 1965 and spimfw 1967 (other spim* theorems use ∃𝑥 and very few theorems in set.mm use ¬ ∀𝑥¬). (Contributed by BJ, 8-Nov-2021.)
⊢ (∀𝑥(𝜑 → (𝜓 → 𝜒)) → (∃𝑥𝜑 → (∀𝑥𝜓 → ∃𝑥𝜒)))
Theorem	bj-exalimi 36926	An inference for distributing quantifiers over a nested implication. The canonical derivation from its closed form bj-exalim 36925 (using mpg 1799) has fewer essential steps, but more steps in total (yielding a longer compressed proof). (Almost) the general statement that speimfw 1965 proves. (Contributed by BJ, 29-Sep-2019.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (∃𝑥𝜑 → (∀𝑥𝜓 → ∃𝑥𝜒))
Theorem	bj-eximcom 36927	A commuted form of exim 1836 which is sometimes posited as an axiom in instuitionistic modal logic. Forward implication of 19.35 1879. Its converse is not intuitionistic. (Contributed by BJ, 9-Dec-2023.)
⊢ (∃𝑥(𝜑 → 𝜓) → (∀𝑥𝜑 → ∃𝑥𝜓))
Theorem	bj-exalims 36928	Distributing quantifiers over a nested implication. (Almost) the general statement that spimfw 1967 proves. (Contributed by BJ, 29-Sep-2019.)
⊢ (∃𝑥𝜑 → (¬ 𝜒 → ∀𝑥 ¬ 𝜒))    ⇒   ⊢ (∀𝑥(𝜑 → (𝜓 → 𝜒)) → (∃𝑥𝜑 → (∀𝑥𝜓 → 𝜒)))
Theorem	bj-exalimsi 36929	An inference for distributing quantifiers over a nested implication. (Almost) the general statement that spimfw 1967 proves. (Contributed by BJ, 29-Sep-2019.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (∃𝑥𝜑 → (¬ 𝜒 → ∀𝑥 ¬ 𝜒))    ⇒   ⊢ (∃𝑥𝜑 → (∀𝑥𝜓 → 𝜒))
Theorem	bj-axdd2ALT 36930	Alternate proof of bj-axdd2 36873 (this should replace bj-axdd2 36873 when bj-exalimi 36926 is moved to the main section). (Contributed by BJ, 8-Mar-2026.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∃𝑥𝜑 → (∀𝑥𝜓 → ∃𝑥𝜓))
Theorem	bj-ax12ig 36931	A lemma used to prove a weak form of the axiom of substitution. A generalization of bj-ax12i 36932. (Contributed by BJ, 19-Dec-2020.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → (𝜒 → ∀𝑥𝜒))    ⇒   ⊢ (𝜑 → (𝜓 → ∀𝑥(𝜑 → 𝜓)))
Theorem	bj-ax12i 36932	A weakening of bj-ax12ig 36931 that is sufficient to prove a weak form of the axiom of substitution ax-12 2185. The general statement of which ax12i 1968 is an instance. (Contributed by BJ, 29-Sep-2019.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜒 → ∀𝑥𝜒)    ⇒   ⊢ (𝜑 → (𝜓 → ∀𝑥(𝜑 → 𝜓)))
Theorem	bj-nfimt 36933	Closed form of nfim 1898 and curried (exported) form of nfimt 1897. (Contributed by BJ, 20-Oct-2021.) Proof should not use 19.35 1879. (Proof modification is discouraged.)
⊢ (Ⅎ𝑥𝜑 → (Ⅎ𝑥𝜓 → Ⅎ𝑥(𝜑 → 𝜓)))
Theorem	bj-spimnfe 36934	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 2239, bj-19.36im 37076, 19.36imv 1947, spimfw 1967... (Contributed by BJ, 3-Apr-2026.) Proof should not use 19.35 1879. (Proof modification is discouraged.)
⊢ ((∃𝑥𝜓 → 𝜓) → (∃𝑥(𝜑 → 𝜓) → (∀𝑥𝜑 → 𝜓)))
Theorem	bj-spimenfa 36935	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 1879. (Proof modification is discouraged.)
⊢ ((𝜑 → ∀𝑥𝜑) → (∃𝑥(𝜑 → 𝜓) → (𝜑 → ∃𝑥𝜓)))
Theorem	bj-spim 36936	A lemma for universal specification. In applications, 𝑥 = 𝑦 will be substituted for 𝜓 and ax6ev 1971 will prove Hypothesis bj-spim.denote. (Contributed by BJ, 4-Apr-2026.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → (∃𝑥𝜃 → 𝜃))    &   ⊢ (𝜑 → ∃𝑥𝜓)    &   ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))    ⇒   ⊢ (𝜑 → (∀𝑥𝜒 → 𝜃))
Theorem	bj-spime 36937	A lemma for existential generalization. In applications, 𝑥 = 𝑦 will be substituted for 𝜓 and ax6ev 1971 will prove Hypothesis bj-spime.denote. (Contributed by BJ, 4-Apr-2026.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → (𝜒 → ∀𝑥𝜒))    &   ⊢ (𝜑 → ∃𝑥𝜓)    &   ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))    ⇒   ⊢ (𝜑 → (𝜒 → ∃𝑥𝜃))
Theorem	bj-cbvalimd0 36938	A lemma for alpha-renaming of variables bound by a universal quantifier. In applications, 𝑥 = 𝑦 will be substituted for 𝜓 and ax6ev 1971 will prove Hypothesis bj-cbvalimd0.denote. When ax6ev 1971 is not available but only its universal closure is, then bj-cbvalimd 36941 or bj-cbvalimdv 36943 should be used (see bj-cbvalimdlem 36939, bj-cbval 36956). (Contributed by BJ, 4-Apr-2026.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → ∀𝑦𝜑)    &   ⊢ (𝜑 → (𝜒 → ∀𝑦𝜒))    &   ⊢ (𝜑 → (∃𝑥𝜃 → 𝜃))    &   ⊢ (𝜑 → ∃𝑥𝜓)    &   ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))    ⇒   ⊢ (𝜑 → (∀𝑥𝜒 → ∀𝑦𝜃))
Theorem	bj-cbvalimdlem 36939	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 36943 or from a nonfreeness condition and alcom 2165 as in bj-cbvalimd 36941. Hypothesis bj-cbvalimdlem.denote is weaker than the corresponding hypothesis of bj-cbvalimd0 36938, and this proof is therefore a bit longer, not using bj-spim 36936 but bj-eximcom 36927. (Contributed by BJ, 12-Mar-2023.) Proof should not use 19.35 1879. (Proof modification is discouraged.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → ∀𝑦𝜑)    &   ⊢ (𝜑 → (∀𝑥𝜒 → ∀𝑦∀𝑥𝜒))    &   ⊢ (𝜑 → (∃𝑥𝜃 → 𝜃))    &   ⊢ (𝜑 → ∀𝑦∃𝑥𝜓)    &   ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))    ⇒   ⊢ (𝜑 → (∀𝑥𝜒 → ∀𝑦𝜃))
Theorem	bj-cbveximdlem 36940	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 36944 or from a nonfreeness condition and excom 2168 as in bj-cbveximd 36942. 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 36937 but bj-eximcom 36927. (Contributed by BJ, 12-Mar-2023.) Proof should not use 19.35 1879. (Proof modification is discouraged.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → ∀𝑦𝜑)    &   ⊢ (𝜑 → (𝜒 → ∀𝑦𝜒))    &   ⊢ (𝜑 → (∃𝑥∃𝑦𝜃 → ∃𝑦𝜃))    &   ⊢ (𝜑 → ∀𝑥∃𝑦𝜓)    &   ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))    ⇒   ⊢ (𝜑 → (∃𝑥𝜒 → ∃𝑦𝜃))
Theorem	bj-cbvalimd 36941	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 36942	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 36943*	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 36944*	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 36945*	Version of spvw 1983 and 19.3v 1984 proved from ax-1 6-- ax-5 1912. The antecedent can for instance be proved with the existence axiom extru 1977. (Contributed by BJ, 8-Mar-2026.) (Proof modification is discouraged.)
⊢ (∃𝑥𝜑 → (𝜓 ↔ ∀𝑥𝜓))
Theorem	bj-spvew 36946*	Version of 19.8v 1985 and 19.9v 1986 proved from ax-1 6-- ax-5 1912. The antecedent can for instance be proved with the existence axiom extru 1977. (Contributed by BJ, 8-Mar-2026.) This could also be proved from bj-spvw 36945 using duality, but that proof would not be intuitionistic, contrary to the present one. (Proof modification is discouraged.)
⊢ (∃𝑥𝜑 → (𝜓 ↔ ∃𝑥𝜓))
Theorem	bj-alextruim 36947*	An equivalent expression for universal quantification over a non-occurring variable proved over ax-1 6-- ax-5 1912. The forward implication can be strengthened when ax-6 1969 is posited (which implies that models are non-empty), see spvw 1983. The reverse implication can be seen as a strengthening of ax-5 1912 (since the antecedent of the implication is weakened). See bj-exextruan 36948 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 36948*	An equivalent expression for existential quantification over a non-occurring variable proved over ax-1 6-- ax-5 1912. The forward implication can be seen as a strengthening of ax-5 1912 (a conjunct is added to the consequent of the implication). The reverse implication can be strengthened when ax-6 1969 is posited (which implies that models are non-empty), see 19.8v 1985. See bj-alextruim 36947 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 36949*	Universally quantifying over a non-occurring variable is independent of that variable, over ax-1 6-- ax-5 1912 and the existence axiom extru 1977. See bj-cbvaw 36951 for a strengthening. (Contributed by BJ, 8-Mar-2026.) (Proof modification is discouraged.)
⊢ (∃𝑥𝜑 → (∀𝑥𝜓 → ∀𝑦𝜓))
Theorem	bj-cbvexvv 36950*	Existentially quantifying over a non-occurring variable is independent of that variable, over ax-1 6-- ax-5 1912 and the existence axiom extru 1977. See bj-cbvew 36952 for a strengthening. (Contributed by BJ, 8-Mar-2026.) (Proof modification is discouraged.)
⊢ (∃𝑥𝜑 → (∃𝑦𝜓 → ∃𝑥𝜓))
Theorem	bj-cbvaw 36951*	Universally quantifying over a non-occurring variable is independent from the variable, under a weaker condition than in bj-cbvalvv 36949. 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 186); an intuitionistically valid statement is obtained by expressing the antecedent as a disjunction (classically equivalent through imor 854). (Proof modification is discouraged.)
⊢ ((∀𝑥𝜑 → ∀𝑦⊥) → (∀𝑥𝜓 → ∀𝑦𝜓))
Theorem	bj-cbvew 36952*	Existentially quantifying over a non-occurring variable is independent from the variable, under a weaker condition than in bj-cbvexvv 36950. 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 36953*	Universally quantifying over a non-occurring variable is independent from the variable, under a weaker condition than in bj-cbvalvv 36949. (Contributed by BJ, 14-Mar-2026.) (Proof modification is discouraged.)
⊢ ((∃𝑥⊤ → ∃𝑦𝜑) → (∀𝑦𝜓 → ∀𝑥𝜓))
Theorem	bj-cbvaew 36954*	Exixtentially quantifying over a non-occurring variable is independent from the variable, under a weaker condition than in bj-cbvexvv 36950. (Contributed by BJ, 14-Mar-2026.) (Proof modification is discouraged.)
⊢ ((∀𝑥𝜑 → ∀𝑦⊥) → (∃𝑦𝜓 → ∃𝑥𝜓))
Theorem	bj-ax12wlem 36955*	A lemma used to prove a weak version of the axiom of substitution ax-12 2185. (Temporary comment: The general statement that ax12wlem 2138 proves.) (Contributed by BJ, 20-Mar-2020.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (𝜓 → ∀𝑥(𝜑 → 𝜓)))
Theorem	bj-cbval 36956*	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 1912. (Proof modification is discouraged.)
⊢ ∀𝑦∃𝑥 𝑥 = 𝑦    &   ⊢ ∀𝑥∃𝑦 𝑦 = 𝑥    &   ⊢ (𝑦 = 𝑥 → 𝑥 = 𝑦)    &   ⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → ∀𝑦𝜑)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒))
Theorem	bj-cbvex 36957*	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 1912. (Proof modification is discouraged.)
⊢ ∀𝑦∃𝑥 𝑥 = 𝑦    &   ⊢ ∀𝑥∃𝑦 𝑦 = 𝑥    &   ⊢ (𝑦 = 𝑥 → 𝑥 = 𝑦)    &   ⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → ∀𝑦𝜑)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑦𝜒))
Syntax	wmoo 36958	Syntax for BJ's version of the uniqueness quantifier.
wff ∃**𝑥𝜑
Definition	df-bj-mo 36959*	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 36960*	Proposed definition to replace df-sb 2069 and df-sbc 3730. Proof is therefore unimportant. Contrary to df-sb 2069, 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 1971 is posited, all variables "exist". (Contributed by BJ, 19-Feb-2026.)
⊢ ([𝐴 / 𝑥]𝜑 ↔ ∃𝑦(𝑦 = 𝐴 ∧ ∀𝑥(𝑥 = 𝑦 → 𝜑)))
Theorem	bj-sbcex 36961	Proof of sbcex 3739 when taking bj-df-sb 36960 as definition. (Contributed by BJ, 19-Feb-2026.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ([𝐴 / 𝑥]𝜑 → 𝐴 ∈ V)
Theorem	bj-dfsbc 36962	Proof of df-sbc 3730 when taking bj-df-sb 36960 as definition. (Contributed by BJ, 19-Feb-2026.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ [𝐴 / 𝑥]𝜑)
Theorem	bj-ssbeq 36963*	Substitution in an equality, disjoint variables case. Uses only ax-1 6 through ax-6 1969. It might be shorter to prove the result about composition of two substitutions and prove bj-ssbeq 36963 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 36964*	A lemma for the definiens of df-sb 2069. An instance of sp 2191 proved without it. Note: it has a common subproof with sbjust 2067. (Contributed by BJ, 22-Dec-2020.) (Proof modification is discouraged.)
⊢ (∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑)) → (𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
Theorem	bj-ssblem2 36965*	An instance of ax-11 2163 proved without it. The converse may not be provable without ax-11 2163 (since using alcomimw 2045 would require a DV on 𝜑, 𝑥, which defeats the purpose). (Contributed by BJ, 22-Dec-2020.) (Proof modification is discouraged.)
⊢ (∀𝑥∀𝑦(𝑦 = 𝑡 → (𝑥 = 𝑦 → 𝜑)) → ∀𝑦∀𝑥(𝑦 = 𝑡 → (𝑥 = 𝑦 → 𝜑)))
Theorem	bj-ax12v 36966*	A weaker form of ax-12 2185 and ax12v 2186, 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 36967*	Remove a DV condition from bj-ax12v 36966 (using core axioms only). (Contributed by BJ, 26-Dec-2020.) (Proof modification is discouraged.)
⊢ ∀𝑥(𝑥 = 𝑡 → (𝜑 → ∀𝑥(𝑥 = 𝑡 → 𝜑)))
Theorem	bj-ax12ssb 36968*	Axiom bj-ax12 36967 expressed using substitution. (Contributed by BJ, 26-Dec-2020.) (Proof modification is discouraged.)
⊢ [𝑡 / 𝑥](𝜑 → [𝑡 / 𝑥]𝜑)
Theorem	bj-19.41al 36969	Special case of 19.41 2243 proved from core axioms, ax-10 2147 (modal5), and hba1 2300 (modal4). (Contributed by BJ, 29-Dec-2020.) (Proof modification is discouraged.)
⊢ (∃𝑥(𝜑 ∧ ∀𝑥𝜓) ↔ (∃𝑥𝜑 ∧ ∀𝑥𝜓))
Theorem	bj-equsexval 36970*	Special case of equsexv 2276 proved from core axioms, ax-10 2147 (modal5), and hba1 2300 (modal4). (Contributed by BJ, 29-Dec-2020.) (Proof modification is discouraged.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ ∀𝑥𝜓))    ⇒   ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ ∀𝑥𝜓)
Theorem	bj-subst 36971*	Proof of sbalex 2250 from core axioms, ax-10 2147 (modal5), and bj-ax12 36967. (Contributed by BJ, 29-Dec-2020.) (Proof modification is discouraged.)
⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑))
Theorem	bj-ssbid2 36972	A special case of sbequ2 2257. (Contributed by BJ, 22-Dec-2020.)
⊢ ([𝑥 / 𝑥]𝜑 → 𝜑)
Theorem	bj-ssbid2ALT 36973	Alternate proof of bj-ssbid2 36972, not using sbequ2 2257. (Contributed by BJ, 22-Dec-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ([𝑥 / 𝑥]𝜑 → 𝜑)
Theorem	bj-ssbid1 36974	A special case of sbequ1 2256. (Contributed by BJ, 22-Dec-2020.)
⊢ (𝜑 → [𝑥 / 𝑥]𝜑)
Theorem	bj-ssbid1ALT 36975	Alternate proof of bj-ssbid1 36974, not using sbequ1 2256. (Contributed by BJ, 22-Dec-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → [𝑥 / 𝑥]𝜑)
Theorem	bj-ax6elem1 36976*	Lemma for bj-ax6e 36978. (Contributed by BJ, 22-Dec-2020.) (Proof modification is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧))
Theorem	bj-ax6elem2 36977*	Lemma for bj-ax6e 36978. (Contributed by BJ, 22-Dec-2020.) (Proof modification is discouraged.)
⊢ (∀𝑥 𝑦 = 𝑧 → ∃𝑥 𝑥 = 𝑦)
Theorem	bj-ax6e 36978	Proof of ax6e 2388 (hence ax6 2389) from Tarski's system, ax-c9 39350, ax-c16 39352. Remark: ax-6 1969 is used only via its principal (unbundled) instance ax6v 1970. (Contributed by BJ, 22-Dec-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∃𝑥 𝑥 = 𝑦
21.19.4.6  Adding ax-6
Theorem	bj-spim0 36979*	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-spimvwt 36980*	Closed form of spimvw 1988. See also spimt 2391. (Contributed by BJ, 8-Nov-2021.)
⊢ (∀𝑥(𝑥 = 𝑦 → (𝜑 → 𝜓)) → (∀𝑥𝜑 → 𝜓))
Theorem	bj-spnfw 36981	Theorem close to a closed form of spnfw 1981. (Contributed by BJ, 12-May-2019.)
⊢ ((∃𝑥𝜑 → 𝜓) → (∀𝑥𝜑 → 𝜓))
Theorem	bj-cbvexiw 36982*	Change bound variable. This is to cbvexvw 2039 what cbvaliw 2008 is to cbvalvw 2038. TODO: move after cbvalivw 2009. (Contributed by BJ, 17-Mar-2020.)
⊢ (∃𝑥∃𝑦𝜓 → ∃𝑦𝜓)    &   ⊢ (𝜑 → ∀𝑦𝜑)    &   ⊢ (𝑦 = 𝑥 → (𝜑 → 𝜓))    ⇒   ⊢ (∃𝑥𝜑 → ∃𝑦𝜓)
Theorem	bj-cbvexivw 36983*	Change bound variable. This is to cbvexvw 2039 what cbvalivw 2009 is to cbvalvw 2038. TODO: move after cbvalivw 2009. (Contributed by BJ, 17-Mar-2020.)
⊢ (𝑦 = 𝑥 → (𝜑 → 𝜓))    ⇒   ⊢ (∃𝑥𝜑 → ∃𝑦𝜓)
Theorem	bj-modald 36984	A short form of the axiom D of modal logic. (Contributed by BJ, 4-Apr-2021.)
⊢ (∀𝑥 ¬ 𝜑 → ¬ ∀𝑥𝜑)
Theorem	bj-denot 36985*	A weakening of ax-6 1969 and ax6v 1970. (Contributed by BJ, 4-Apr-2021.) (New usage is discouraged.)
⊢ (𝑥 = 𝑥 → ¬ ∀𝑦 ¬ 𝑦 = 𝑥)
Theorem	bj-eqs 36986*	A lemma for substitutions, proved from Tarski's FOL. The version without DV (𝑥, 𝑦) is true but requires ax-13 2377. 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 36987*	Change bound variable. This is to cbvexvw 2039 what cbvalw 2037 is to cbvalvw 2038. (Contributed by BJ, 17-Mar-2020.)
⊢ (∃𝑥∃𝑦𝜓 → ∃𝑦𝜓)    &   ⊢ (𝜑 → ∀𝑦𝜑)    &   ⊢ (∃𝑦∃𝑥𝜑 → ∃𝑥𝜑)    &   ⊢ (𝜓 → ∀𝑥𝜓)    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓)
Theorem	bj-ax12w 36988*	The general statement that ax12w 2139 proves. (Contributed by BJ, 20-Mar-2020.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑦 = 𝑧 → (𝜓 ↔ 𝜃))    ⇒   ⊢ (𝜑 → (∀𝑦𝜓 → ∀𝑥(𝜑 → 𝜓)))
21.19.4.8  Membership predicate, ax-8 and ax-9
Theorem	bj-ax89 36989	A theorem which could be used as sole axiom for the non-logical predicate instead of ax-8 2116 and ax-9 2124. Indeed, it is implied over propositional calculus by the conjunction of ax-8 2116 and ax-9 2124, as proved here. In the other direction, one can prove ax-8 2116 (respectively ax-9 2124) from bj-ax89 36989 by using mpan2 692 (respectively mpan 691) and equid 2014. TODO: move to main part. (Contributed by BJ, 3-Oct-2019.)
⊢ ((𝑥 = 𝑦 ∧ 𝑧 = 𝑡) → (𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑡))
Theorem	bj-cleljusti 36990*	One direction of cleljust 2123, requiring only ax-1 6-- ax-5 1912 and ax8v1 2118. (Contributed by BJ, 31-Dec-2020.) (Proof modification is discouraged.)
⊢ (∃𝑧(𝑧 = 𝑥 ∧ 𝑧 ∈ 𝑦) → 𝑥 ∈ 𝑦)
21.19.4.9  Adding ax-11
Theorem	bj-alcomexcom 36991	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 1811 section, soon after 2nexaln 1832, and used to prove excom 2168. (Contributed by BJ, 29-Nov-2020.) (Proof modification is discouraged.)
⊢ ((∀𝑥∀𝑦 ¬ 𝜑 → ∀𝑦∀𝑥 ¬ 𝜑) ↔ (∃𝑦∃𝑥𝜑 → ∃𝑥∃𝑦𝜑))
Theorem	bj-hbald 36992	General statement that hbald 2174 proves . (Contributed by BJ, 4-Apr-2026.)
⊢ (𝜑 → ∀𝑦𝜓)    &   ⊢ (𝜓 → (𝜒 → ∀𝑥𝜃))    ⇒   ⊢ (𝜑 → (∀𝑦𝜒 → ∀𝑥∀𝑦𝜃))
Theorem	bj-hbalt 36993	Closed form of (general instance of) hbal 2173. (Contributed by BJ, 2-May-2019.)
⊢ (∀𝑦(𝜑 → ∀𝑥𝜓) → (∀𝑦𝜑 → ∀𝑥∀𝑦𝜓))
Theorem	bj-hbal 36994	More general instance of hbal 2173. (Contributed by BJ, 4-Apr-2026.)
⊢ (𝜑 → ∀𝑥𝜓)    ⇒   ⊢ (∀𝑦𝜑 → ∀𝑥∀𝑦𝜓)
21.19.4.10  Adding ax-12
Theorem	axc11n11 36995	Proof of axc11n 2431 from { ax-1 6-- ax-7 2010, axc11 2435 } . Almost identical to axc11nfromc11 39386. (Contributed by NM, 6-Jul-2021.) (Proof modification is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥)
Theorem	axc11n11r 36996	Proof of axc11n 2431 from { ax-1 6-- ax-7 2010, axc9 2387, axc11r 2373 } (note that axc16 2269 is provable from { ax-1 6-- ax-7 2010, axc11r 2373 }). Note that axc11n 2431 proves (over minimal calculus) that axc11 2435 and axc11r 2373 are equivalent. Therefore, axc11n11 36995 and axc11n11r 36996 prove that one can use one or the other as an axiom, provided one assumes the axioms listed above (axc11 2435 appears slightly stronger since axc11n11r 36996 requires axc9 2387 while axc11n11 36995 does not). (Contributed by BJ, 6-Jul-2021.) (Proof modification is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥)
Theorem	bj-axc16g16 36997*	Proof of axc16g 2268 from { ax-1 6-- ax-7 2010, axc16 2269 }. (Contributed by BJ, 6-Jul-2021.) (Proof modification is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑧𝜑))
Theorem	bj-ax12v3 36998*	A weak version of ax-12 2185 which is stronger than ax12v 2186. Note that if one assumes reflexivity of equality ⊢ 𝑥 = 𝑥 (equid 2014), then bj-ax12v3 36998 implies ax-5 1912 over modal logic K (substitute 𝑥 for 𝑦). See also bj-ax12v3ALT 36999. (Contributed by BJ, 6-Jul-2021.) (Proof modification is discouraged.)
⊢ (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
Theorem	bj-ax12v3ALT 36999*	Alternate proof of bj-ax12v3 36998. Uses axc11r 2373 and axc15 2427 instead of ax-12 2185. (Contributed by BJ, 6-Jul-2021.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
Theorem	bj-sb 37000*	A weak variant of sbid2 2513 not requiring ax-13 2377 nor ax-10 2147. On top of Tarski's FOL, one implication requires only ax12v 2186, and the other requires only sp 2191. (Contributed by BJ, 25-May-2021.)
⊢ (𝜑 ↔ ∀𝑦(𝑦 = 𝑥 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))