P. 369 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 36801-36900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	bj-df-ifc 36801*	Candidate definition for the conditional operator for classes. This is in line with the definition of a class as the extension of a predicate in df-clab 2716. We reprove the current df-if 4482 from it in bj-dfif 36802. (Contributed by BJ, 20-Sep-2019.) (Proof modification is discouraged.)
⊢ if(𝜑, 𝐴, 𝐵) = {𝑥 ∣ if-(𝜑, 𝑥 ∈ 𝐴, 𝑥 ∈ 𝐵)}
Theorem	bj-dfif 36802*	Alternate definition of the conditional operator for classes, which used to be the main definition. (Contributed by BJ, 26-Dec-2023.) (Proof modification is discouraged.)
⊢ if(𝜑, 𝐴, 𝐵) = {𝑥 ∣ ((𝜑 ∧ 𝑥 ∈ 𝐴) ∨ (¬ 𝜑 ∧ 𝑥 ∈ 𝐵))}
Theorem	bj-ififc 36803	A biconditional connecting the conditional operator for propositions and the conditional operator for classes. Note that there is no sethood hypothesis on 𝑋: it is implied by either side. (Contributed by BJ, 24-Sep-2019.) Generalize statement from setvar 𝑥 to class 𝑋. (Revised by BJ, 26-Dec-2023.)
⊢ (𝑋 ∈ if(𝜑, 𝐴, 𝐵) ↔ if-(𝜑, 𝑋 ∈ 𝐴, 𝑋 ∈ 𝐵))
21.19.1.9  Propositional calculus: miscellaneous Miscellaneous theorems of propositional calculus.
Theorem	bj-imbi12 36804	Uncurried (imported) form of imbi12 346. (Contributed by BJ, 6-May-2019.)
⊢ (((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃)) → ((𝜑 → 𝜒) ↔ (𝜓 → 𝜃)))
Theorem	bj-falor 36805	Dual of truan 1553 (which has biconditional reversed). (Contributed by BJ, 26-Oct-2019.) (Proof modification is discouraged.)
⊢ (𝜑 ↔ (⊥ ∨ 𝜑))
Theorem	bj-falor2 36806	Dual of truan 1553. (Contributed by BJ, 26-Oct-2019.) (Proof modification is discouraged.)
⊢ ((⊥ ∨ 𝜑) ↔ 𝜑)
Theorem	bj-bibibi 36807	A property of the biconditional. (Contributed by BJ, 26-Oct-2019.) (Proof modification is discouraged.)
⊢ (𝜑 ↔ (𝜓 ↔ (𝜑 ↔ 𝜓)))
Theorem	bj-imn3ani 36808	Duplication of bnj1224 34976. Three-fold version of imnani 400. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Revised by BJ, 22-Oct-2019.) (Proof modification is discouraged.)
⊢ ¬ (𝜑 ∧ 𝜓 ∧ 𝜒)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → ¬ 𝜒)
Theorem	bj-andnotim 36809	Two ways of expressing a certain ternary connective. Note the respective positions of the three formulas on each side of the biconditional. (Contributed by BJ, 6-Oct-2018.)
⊢ (((𝜑 ∧ ¬ 𝜓) → 𝜒) ↔ ((𝜑 → 𝜓) ∨ 𝜒))
Theorem	bj-bi3ant 36810	This used to be in the main part. (Contributed by Wolf Lammen, 14-May-2013.) (Revised by BJ, 14-Jun-2019.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (((𝜃 → 𝜏) → 𝜑) → (((𝜏 → 𝜃) → 𝜓) → ((𝜃 ↔ 𝜏) → 𝜒)))
Theorem	bj-bisym 36811	This used to be in the main part. (Contributed by Wolf Lammen, 14-May-2013.) (Revised by BJ, 14-Jun-2019.)
⊢ (((𝜑 → 𝜓) → (𝜒 → 𝜃)) → (((𝜓 → 𝜑) → (𝜃 → 𝜒)) → ((𝜑 ↔ 𝜓) → (𝜒 ↔ 𝜃))))
Theorem	bj-bixor 36812	Equivalence of two ternary operations. Note the identical order and parenthesizing of the three arguments in both expressions. (Contributed by BJ, 31-Dec-2023.)
⊢ ((𝜑 ↔ (𝜓 ⊻ 𝜒)) ↔ (𝜑 ⊻ (𝜓 ↔ 𝜒)))
21.19.2  Modal logic In this section, we prove some theorems related to modal logic. For modal logic, we refer to https://en.wikipedia.org/wiki/Kripke_semantics, https://en.wikipedia.org/wiki/Modal_logic and https://plato.stanford.edu/entries/logic-modal/. Monadic first-order logic (i.e., with quantification over only one variable) is bi-interpretable with modal logic, by mapping ∀𝑥 to "necessity" (generally denoted by a box) and ∃𝑥 to "possibility" (generally denoted by a diamond). Therefore, we use these quantifiers so as not to introduce new symbols. (To be strictly within modal logic, we should add disjoint variable conditions between 𝑥 and any other metavariables appearing in the statements.) For instance, ax-gen 1797 corresponds to the necessitation rule of modal logic, and ax-4 1811 corresponds to the distributivity axiom (K) of modal logic, also called the Kripke scheme. Modal logics satisfying these rule and axiom are called "normal modal logics", of which the most important modal logics are. The minimal normal modal logic is also denoted by (K). Here are a few normal modal logics with their axiomatizations (on top of (K)): (K) axiomatized by no supplementary axioms; (T) axiomatized by the axiom T; (K4) axiomatized by the axiom 4; (S4) axiomatized by the axioms T,4; (S5) axiomatized by the axioms T,5 or D,B,4; (GL) axiomatized by the axiom GL. The last one, called Gödel–Löb logic or provability logic, is important because it describes exactly the properties of provability in Peano arithmetic, as proved by Robert Solovay. See for instance https://plato.stanford.edu/entries/logic-provability/ 1811. A basic result in this logic is bj-gl4 36816.
Theorem	bj-axdd2 36813	This implication, proved using only ax-gen 1797 and ax-4 1811 on top of propositional calculus (hence holding, up to the standard interpretation, in any normal modal logic), shows that the axiom scheme ⊢ ∃𝑥⊤ implies the axiom scheme ⊢ (∀𝑥𝜑 → ∃𝑥𝜑). These correspond to the modal axiom (D), and in predicate calculus, they assert that the universe of discourse is nonempty. For the converse, see bj-axd2d 36814. (Contributed by BJ, 16-May-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∃𝑥𝜑 → (∀𝑥𝜓 → ∃𝑥𝜓))
Theorem	bj-axd2d 36814	This implication, proved using only ax-gen 1797 on top of propositional calculus (hence holding, up to the standard interpretation, in any modal logic), shows that the axiom scheme ⊢ (∀𝑥𝜑 → ∃𝑥𝜑) implies the axiom scheme ⊢ ∃𝑥⊤ (substitute ⊤ for 𝜑). These correspond to the modal axiom (D), and in predicate calculus, they assert that the universe of discourse is nonempty. For the converse, see bj-axdd2 36813. (Contributed by BJ, 16-May-2019.) Generalize from its instance with ⊤ substituted for 𝜑. (Revised by BJ, 20-Mar-2022.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((∀𝑥⊤ → ∃𝑥𝜑) → ∃𝑥𝜑)
Theorem	bj-axtd 36815	This implication, proved from propositional calculus only (hence holding, up to the standard interpretation, in any modal logic), shows that the axiom scheme ⊢ (∀𝑥𝜑 → 𝜑) (modal T) implies the axiom scheme ⊢ (∀𝑥𝜑 → ∃𝑥𝜑) (modal D). See also bj-axdd2 36813 and bj-axd2d 36814. (Contributed by BJ, 16-May-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((∀𝑥 ¬ 𝜑 → ¬ 𝜑) → ((∀𝑥𝜑 → 𝜑) → (∀𝑥𝜑 → ∃𝑥𝜑)))
Theorem	bj-gl4 36816	In a normal modal logic, the modal axiom GL implies the modal axiom (4). Translated to first-order logic, Axiom GL reads ⊢ (∀𝑥(∀𝑥𝜑 → 𝜑) → ∀𝑥𝜑). Note that the antecedent of bj-gl4 36816 is an instance of the axiom GL, with 𝜑 replaced by (∀𝑥𝜑 ∧ 𝜑), which is a modality sometimes called the "strong necessity" of 𝜑. (Contributed by BJ, 12-Dec-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((∀𝑥(∀𝑥(∀𝑥𝜑 ∧ 𝜑) → (∀𝑥𝜑 ∧ 𝜑)) → ∀𝑥(∀𝑥𝜑 ∧ 𝜑)) → (∀𝑥𝜑 → ∀𝑥∀𝑥𝜑))
Theorem	bj-axc4 36817	Over minimal calculus, the modal axiom (4) (hba1 2300) and the modal axiom (K) (ax-4 1811) together imply axc4 2327. (Contributed by BJ, 29-Nov-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((∀𝑥𝜑 → ∀𝑥∀𝑥𝜑) → ((∀𝑥(∀𝑥𝜑 → 𝜓) → (∀𝑥∀𝑥𝜑 → ∀𝑥𝜓)) → (∀𝑥(∀𝑥𝜑 → 𝜓) → (∀𝑥𝜑 → ∀𝑥𝜓))))
21.19.3  Provability logic In this section, we assume that, on top of propositional calculus, there is given a provability predicate Prv satisfying the three axioms ax-prv1 36819 and ax-prv2 36820 and ax-prv3 36821. Note the similarity with ax-gen 1797, ax-4 1811 and hba1 2300 respectively. These three properties of Prv are often called the Hilbert–Bernays–Löb derivability conditions, or the Hilbert–Bernays provability conditions. This corresponds to the modal logic (K4) (see previous section for modal logic). The interpretation of provability logic is the following: we are given a background first-order theory T, the wff Prv 𝜑 means "𝜑 is provable in T", and the turnstile ⊢ indicates provability in T. Beware that "provability logic" often means (K) augmented with the Gödel–Löb axiom GL, which we do not assume here (at least for the moment). See for instance https://plato.stanford.edu/entries/logic-provability/ 2300. Provability logic is worth studying because whenever T is a first-order theory containing Robinson arithmetic (a fragment of Peano arithmetic), one can prove (using Gödel numbering, and in the much weaker primitive recursive arithmetic) that there exists in T a provability predicate Prv satisfying the above three axioms. (We do not construct this predicate in this section; this is still a project.) The main theorems of this section are the "easy parts" of the proofs of Gödel's second incompleteness theorem (bj-babygodel 36824) and Löb's theorem (bj-babylob 36825). See the comments of these theorems for details.
Syntax	cprvb 36818	Syntax for the provability predicate.
wff Prv 𝜑
Axiom	ax-prv1 36819	First property of three of the provability predicate. (Contributed by BJ, 3-Apr-2019.)
⊢ 𝜑    ⇒   ⊢ Prv 𝜑
Axiom	ax-prv2 36820	Second property of three of the provability predicate. (Contributed by BJ, 3-Apr-2019.)
⊢ (Prv (𝜑 → 𝜓) → (Prv 𝜑 → Prv 𝜓))
Axiom	ax-prv3 36821	Third property of three of the provability predicate. (Contributed by BJ, 3-Apr-2019.)
⊢ (Prv 𝜑 → Prv Prv 𝜑)
Theorem	prvlem1 36822	An elementary property of the provability predicate. (Contributed by BJ, 3-Apr-2019.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (Prv 𝜑 → Prv 𝜓)
Theorem	prvlem2 36823	An elementary property of the provability predicate. (Contributed by BJ, 3-Apr-2019.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (Prv 𝜑 → (Prv 𝜓 → Prv 𝜒))
Theorem	bj-babygodel 36824	See the section header comments for the context. The first hypothesis reads "𝜑 is true if and only if it is not provable in T" (and having this first hypothesis means that we can prove this fact in T). The wff 𝜑 is a formal version of the sentence "This sentence is not provable". The hard part of the proof of Gödel's theorem is to construct such a 𝜑, called a "Gödel–Rosser sentence", for a first-order theory T which is effectively axiomatizable and contains Robinson arithmetic, through Gödel diagonalization (this can be done in primitive recursive arithmetic). The second hypothesis means that ⊥ is not provable in T, that is, that the theory T is consistent (and having this second hypothesis means that we can prove in T that the theory T is consistent). The conclusion is the falsity, so having the conclusion means that T can prove the falsity, that is, T is inconsistent. Therefore, taking the contrapositive, this theorem expresses that if a first-order theory is consistent (and one can prove in it that some formula is true if and only if it is not provable in it), then this theory does not prove its own consistency. This proof is due to George Boolos, Gödel's Second Incompleteness Theorem Explained in Words of One Syllable, Mind, New Series, Vol. 103, No. 409 (January 1994), pp. 1--3. (Contributed by BJ, 3-Apr-2019.)
⊢ (𝜑 ↔ ¬ Prv 𝜑)    &   ⊢ ¬ Prv ⊥    ⇒   ⊢ ⊥
Theorem	bj-babylob 36825	See the section header comments for the context, as well as the comments for bj-babygodel 36824. Löb's theorem when the Löb sentence is given as a hypothesis (the hard part of the proof of Löb's theorem is to construct this Löb sentence; this can be done, using Gödel diagonalization, for any first-order effectively axiomatizable theory containing Robinson arithmetic). More precisely, the present theorem states that if a first-order theory proves that the provability of a given sentence entails its truth (and if one can construct in this theory a provability predicate and a Löb sentence, given here as the first hypothesis), then the theory actually proves that sentence. See for instance, Eliezer Yudkowsky, The Cartoon Guide to Löb's Theorem (available at http://yudkowsky.net/rational/lobs-theorem/ 36824). (Contributed by BJ, 20-Apr-2019.)
⊢ (𝜓 ↔ (Prv 𝜓 → 𝜑))    &   ⊢ (Prv 𝜑 → 𝜑)    ⇒   ⊢ 𝜑
Theorem	bj-godellob 36826	Proof of Gödel's theorem from Löb's theorem (see comments at bj-babygodel 36824 and bj-babylob 36825 for details). (Contributed by BJ, 20-Apr-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 ↔ ¬ Prv 𝜑)    &   ⊢ ¬ Prv ⊥    ⇒   ⊢ ⊥
21.19.4  First-order logic Utility lemmas or strengthenings of theorems in the main part (biconditional or closed forms, or fewer disjoint variable conditions, or disjoint variable conditions replaced with nonfreeness hypotheses...). Sorted in the same order as in the main part.
21.19.4.1  Universal and existential quantifiers, nonfreeness predicate
Theorem	bj-exexalal 36827	A lemma for changing bound variables. Only the forward implication is intuitionistic. (Contributed by BJ, 14-Mar-2026.)
⊢ ((∃𝑥𝜑 → ∃𝑦𝜓) ↔ (∀𝑦 ¬ 𝜓 → ∀𝑥 ¬ 𝜑))
21.19.4.2  Adding ax-gen
Theorem	bj-genr 36828	Generalization rule on the right conjunct. See 19.28 2236. (Contributed by BJ, 7-Jul-2021.)
⊢ (𝜑 ∧ 𝜓)    ⇒   ⊢ (𝜑 ∧ ∀𝑥𝜓)
Theorem	bj-genl 36829	Generalization rule on the left conjunct. See 19.27 2235. (Contributed by BJ, 7-Jul-2021.)
⊢ (𝜑 ∧ 𝜓)    ⇒   ⊢ (∀𝑥𝜑 ∧ 𝜓)
Theorem	bj-genan 36830	Generalization rule on a conjunction. Forward inference associated with 19.26 1872. (Contributed by BJ, 7-Jul-2021.)
⊢ (𝜑 ∧ 𝜓)    ⇒   ⊢ (∀𝑥𝜑 ∧ ∀𝑥𝜓)
Theorem	bj-mpgs 36831	From a closed form theorem (the major premise) with an antecedent in the "strong necessity" modality (in the language of modal logic), deduce the inference ⊢ 𝜑 ⇒ ⊢ 𝜓. Strong necessity is stronger than necessity, and equivalent to it when sp 2191 (modal T) is available. Therefore, this theorem is stronger than mpg 1799 when sp 2191 is not available. (Contributed by BJ, 1-Nov-2023.)
⊢ 𝜑    &   ⊢ ((𝜑 ∧ ∀𝑥𝜑) → 𝜓)    ⇒   ⊢ 𝜓
21.19.4.3  Adding ax-4
Theorem	bj-almp 36832	A quantified form of ax-mp 5. See also barbara 2664, bj-almpi 36834, and the inference associated with ala1 1815. (Contributed by BJ, 19-Mar-2026.) (Proof modification is discouraged.)
⊢ ∀𝑥(𝜓 → 𝜑)    &   ⊢ ∀𝑥𝜓    ⇒   ⊢ ∀𝑥𝜑
Theorem	bj-alimii 36833	Inference associated with alimi 1813. Double inference associated with alim 1812. The usual proof of an associated inference (here from alimi 1813 and ax-mp 5) has the same size and same number of steps. (Contributed by BJ, 19-Mar-2026.) (Proof modification is discouraged.)
⊢ (𝜓 → 𝜑)    &   ⊢ ∀𝑥𝜓    ⇒   ⊢ ∀𝑥𝜑
Theorem	bj-almpi 36834	A quantified form of mpi 20. See also barbara 2664, bj-almp 36832, and the inference associated with ala1 1815. (Contributed by BJ, 19-Mar-2026.) (Proof modification is discouraged.)
⊢ ∀𝑥(𝜑 → (𝜒 → 𝜓))    &   ⊢ ∀𝑥𝜒    ⇒   ⊢ ∀𝑥(𝜑 → 𝜓)
Theorem	bj-almpig 36835	A partially quantified form of mpi 20 similar to bj-almpi 36834. (Contributed by BJ, 19-Mar-2026.) (Proof modification is discouraged.)
⊢ (𝜑 → (𝜒 → 𝜓))    &   ⊢ ∀𝑥𝜒    ⇒   ⊢ ∀𝑥(𝜑 → 𝜓)
Theorem	bj-alsyl 36836	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 36837	Closed form of 2alimi 1814. (Contributed by BJ, 6-May-2019.)
⊢ (∀𝑥∀𝑦(𝜑 → 𝜓) → (∀𝑥∀𝑦𝜑 → ∀𝑥∀𝑦𝜓))
Theorem	bj-alanim 36838	Closed form of alanimi 1818. (Contributed by BJ, 6-May-2019.)
⊢ (∀𝑥((𝜑 ∧ 𝜓) → 𝜒) → ((∀𝑥𝜑 ∧ ∀𝑥𝜓) → ∀𝑥𝜒))
Theorem	bj-2albi 36839	Closed form of 2albii 1822. (Contributed by BJ, 6-May-2019.)
⊢ (∀𝑥∀𝑦(𝜑 ↔ 𝜓) → (∀𝑥∀𝑦𝜑 ↔ ∀𝑥∀𝑦𝜓))
Theorem	bj-notalbii 36840	Equivalence of universal quantification of negation of equivalent formulas. Shortens ab0 4334 (103>94), ballotlem2 34666 (2655>2648), bnj1143 34965 (522>519), hausdiag 23601 (2119>2104). (Contributed by BJ, 17-Jul-2021.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (∀𝑥 ¬ 𝜑 ↔ ∀𝑥 ¬ 𝜓)
Theorem	bj-sylggt 36841	Stronger form of sylgt 1824, closer to ax-2 7. (Contributed by BJ, 30-Jul-2025.)
⊢ ((𝜑 → ∀𝑥(𝜓 → 𝜒)) → ((𝜑 → ∀𝑥𝜓) → (𝜑 → ∀𝑥𝜒)))
Theorem	bj-sylgt2 36842	Uncurried (imported) form of sylgt 1824. (Contributed by BJ, 2-May-2019.)
⊢ ((∀𝑥(𝜓 → 𝜒) ∧ (𝜑 → ∀𝑥𝜓)) → (𝜑 → ∀𝑥𝜒))
Theorem	bj-2exim 36843	Closed form of 2eximi 1838. (Contributed by BJ, 6-May-2019.)
⊢ (∀𝑥∀𝑦(𝜑 → 𝜓) → (∃𝑥∃𝑦𝜑 → ∃𝑥∃𝑦𝜓))
Theorem	bj-2exbi 36844	Closed form of 2exbii 1851. (Contributed by BJ, 6-May-2019.)
⊢ (∀𝑥∀𝑦(𝜑 ↔ 𝜓) → (∃𝑥∃𝑦𝜑 ↔ ∃𝑥∃𝑦𝜓))
Theorem	bj-3exbi 36845	Closed form of 3exbii 1852. (Contributed by BJ, 6-May-2019.)
⊢ (∀𝑥∀𝑦∀𝑧(𝜑 ↔ 𝜓) → (∃𝑥∃𝑦∃𝑧𝜑 ↔ ∃𝑥∃𝑦∃𝑧𝜓))
Theorem	bj-alrimg 36846	The general form of the *alrim* 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 an antecedent, one can deduce from the universally quantified implication an implication where the consequent is universally quantified. Dual of bj-exlimg 36850. (Contributed by BJ, 9-Dec-2023.)
⊢ ((𝜑 → ∀𝑥𝜓) → (∀𝑥(𝜓 → 𝜒) → (𝜑 → ∀𝑥𝜒)))
Theorem	bj-alrimd 36847	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-sylget 36848	Dual statement of sylgt 1824. Closed form of bj-sylge 36851. (Contributed by BJ, 2-May-2019.)
⊢ (∀𝑥(𝜒 → 𝜑) → ((∃𝑥𝜑 → 𝜓) → (∃𝑥𝜒 → 𝜓)))
Theorem	bj-sylget2 36849	Uncurried (imported) form of bj-sylget 36848. (Contributed by BJ, 2-May-2019.)
⊢ ((∀𝑥(𝜑 → 𝜓) ∧ (∃𝑥𝜓 → 𝜒)) → (∃𝑥𝜑 → 𝜒))
Theorem	bj-exlimg 36850	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 36846. (Contributed by BJ, 9-Dec-2023.)
⊢ ((∃𝑥𝜑 → 𝜓) → (∀𝑥(𝜒 → 𝜑) → (∃𝑥𝜒 → 𝜓)))
Theorem	bj-sylge 36851	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 36852	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 36853	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 36846 and bj-exlimg 36850 (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 36854	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 36855. (Revised by BJ, 9-Dec-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓))
Theorem	bj-alexim 36855	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 36854). (Contributed by BJ, 8-Nov-2021.)
⊢ (∀𝑥(𝜑 → (𝜓 → 𝜒)) → (∀𝑥𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒)))
Theorem	bj-aleximiALT 36856	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-nexdh 36857	Closed form of nexdh 1867 (actually, its general instance). (Contributed by BJ, 6-May-2019.)
⊢ (∀𝑥(𝜑 → ¬ 𝜓) → ((𝜒 → ∀𝑥𝜑) → (𝜒 → ¬ ∃𝑥𝜓)))
Theorem	bj-nexdh2 36858	Uncurried (imported) form of bj-nexdh 36857. (Contributed by BJ, 6-May-2019.)
⊢ ((∀𝑥(𝜑 → ¬ 𝜓) ∧ (𝜒 → ∀𝑥𝜑)) → (𝜒 → ¬ ∃𝑥𝜓))
Theorem	bj-hbxfrbi 36859	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 36980) in order not to require sp 2191 (modal T). See bj-hbyfrbi 36860 for its version with existential quantifiers. (Contributed by BJ, 6-May-2019.)
⊢ (((𝜑 ↔ 𝜓) ∧ ∀𝑥(𝜑 ↔ 𝜓)) → ((𝜑 → ∀𝑥𝜑) ↔ (𝜓 → ∀𝑥𝜓)))
Theorem	bj-hbyfrbi 36860	Version of bj-hbxfrbi 36859 with existential quantifiers. (Contributed by BJ, 23-Aug-2023.)
⊢ (((𝜑 ↔ 𝜓) ∧ ∀𝑥(𝜑 ↔ 𝜓)) → ((∃𝑥𝜑 → 𝜑) ↔ (∃𝑥𝜓 → 𝜓)))
Theorem	bj-exalim 36861	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 36861, bj-exalimi 36862, bj-exalims 36863, bj-exalimsi 36864, bj-ax12i 36867, bj-ax12wlem 36882, bj-ax12w 36916. A new label is needed for bj-ax12i 36867 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 36862	An inference for distributing quantifiers over a nested implication. The canonical derivation from its closed form bj-exalim 36861 (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-exalims 36863	Distributing quantifiers over a nested implication. (Almost) the general statement that spimfw 1967 proves. (Contributed by BJ, 29-Sep-2019.)
⊢ (∃𝑥𝜑 → (¬ 𝜒 → ∀𝑥 ¬ 𝜒))    ⇒   ⊢ (∀𝑥(𝜑 → (𝜓 → 𝜒)) → (∃𝑥𝜑 → (∀𝑥𝜓 → 𝜒)))
Theorem	bj-exalimsi 36864	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 36865	Alternate proof of bj-axdd2 36813 (this should replace bj-axdd2 36813 when bj-exalimi 36862 is moved to the main section). (Contributed by BJ, 8-Mar-2026.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∃𝑥𝜑 → (∀𝑥𝜓 → ∃𝑥𝜓))
Theorem	bj-ax12ig 36866	A lemma used to prove a weak form of the axiom of substitution. A generalization of bj-ax12i 36867. (Contributed by BJ, 19-Dec-2020.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → (𝜒 → ∀𝑥𝜒))    ⇒   ⊢ (𝜑 → (𝜓 → ∀𝑥(𝜑 → 𝜓)))
Theorem	bj-ax12i 36867	A weakening of bj-ax12ig 36866 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 36868	Closed form of nfim 1898 and curried (exported) form of nfimt 1897. (Contributed by BJ, 20-Oct-2021.)
⊢ (Ⅎ𝑥𝜑 → (Ⅎ𝑥𝜓 → Ⅎ𝑥(𝜑 → 𝜓)))
Theorem	bj-cbvalimt 36869	A lemma in closed form used to prove bj-cbval 36887 in a weak axiomatization. (Contributed by BJ, 12-Mar-2023.) Do not use 19.35 1879 since only the direction of the biconditional used here holds in intuitionistic logic. (Proof modification is discouraged.)
⊢ (∀𝑦∃𝑥𝜒 → (∀𝑦∀𝑥(𝜒 → (𝜑 → 𝜓)) → ((∀𝑥𝜑 → ∀𝑦∀𝑥𝜑) → (∀𝑦(∃𝑥𝜓 → 𝜓) → (∀𝑥𝜑 → ∀𝑦𝜓)))))
Theorem	bj-cbveximt 36870	A lemma in closed form used to prove bj-cbvex 36888 in a weak axiomatization. (Contributed by BJ, 12-Mar-2023.) Do not use 19.35 1879 since only the direction of the biconditional used here holds in intuitionistic logic. (Proof modification is discouraged.)
⊢ (∀𝑥∃𝑦𝜒 → (∀𝑥∀𝑦(𝜒 → (𝜑 → 𝜓)) → (∀𝑥(𝜑 → ∀𝑦𝜑) → ((∃𝑥∃𝑦𝜓 → ∃𝑦𝜓) → (∃𝑥𝜑 → ∃𝑦𝜓)))))
Theorem	bj-eximcom 36871	A commuted form of exim 1836 which is sometimes posited as an axiom in instuitionistic modal logic. (Contributed by BJ, 9-Dec-2023.)
⊢ (∃𝑥(𝜑 → 𝜓) → (∀𝑥𝜑 → ∃𝑥𝜓))
21.19.4.4  Adding ax-5
Theorem	bj-spvw 36872*	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 36873*	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 36872 using duality, but that proof would not be intuitionistic, contrary to the present one. (Proof modification is discouraged.)
⊢ (∃𝑥𝜑 → (𝜓 ↔ ∃𝑥𝜓))
Theorem	bj-alextruim 36874*	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 36875 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 36875*	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 36874 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 36876*	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 36878 for a strengthening. (Contributed by BJ, 8-Mar-2026.) (Proof modification is discouraged.)
⊢ (∃𝑥𝜑 → (∀𝑥𝜓 → ∀𝑦𝜓))
Theorem	bj-cbvexvv 36877*	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 36879 for a strengthening. (Contributed by BJ, 8-Mar-2026.) (Proof modification is discouraged.)
⊢ (∃𝑥𝜑 → (∃𝑦𝜓 → ∃𝑥𝜓))
Theorem	bj-cbvaw 36878*	Universally quantifying over a non-occurring variable is independent from the variable, under a weaker condition than in bj-cbvalvv 36876. 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 36879*	Existentially quantifying over a non-occurring variable is independent from the variable, under a weaker condition than in bj-cbvexvv 36877. 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 36880*	Universally quantifying over a non-occurring variable is independent from the variable, under a weaker condition than in bj-cbvalvv 36876. (Contributed by BJ, 14-Mar-2026.) (Proof modification is discouraged.)
⊢ ((∃𝑥⊤ → ∃𝑦𝜑) → (∀𝑦𝜓 → ∀𝑥𝜓))
Theorem	bj-cbvaew 36881*	Exixtentially quantifying over a non-occurring variable is independent from the variable, under a weaker condition than in bj-cbvexvv 36877. (Contributed by BJ, 14-Mar-2026.) (Proof modification is discouraged.)
⊢ ((∀𝑥𝜑 → ∀𝑦⊥) → (∃𝑦𝜓 → ∃𝑥𝜓))
Theorem	bj-ax12wlem 36882*	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-cbvalim 36883*	A lemma used to prove bj-cbval 36887 in a weak axiomatization. (Contributed by BJ, 12-Mar-2023.) (Proof modification is discouraged.)
⊢ (∀𝑦∃𝑥𝜒 → (∀𝑦∀𝑥(𝜒 → (𝜑 → 𝜓)) → (∀𝑥𝜑 → ∀𝑦𝜓)))
Theorem	bj-cbvexim 36884*	A lemma used to prove bj-cbvex 36888 in a weak axiomatization. (Contributed by BJ, 12-Mar-2023.) (Proof modification is discouraged.)
⊢ (∀𝑥∃𝑦𝜒 → (∀𝑥∀𝑦(𝜒 → (𝜑 → 𝜓)) → (∃𝑥𝜑 → ∃𝑦𝜓)))
Theorem	bj-cbvalimi 36885*	An equality-free general instance of one half of a precise form of bj-cbval 36887. (Contributed by BJ, 12-Mar-2023.) (Proof modification is discouraged.)
⊢ (𝜒 → (𝜑 → 𝜓))    &   ⊢ ∀𝑦∃𝑥𝜒    ⇒   ⊢ (∀𝑥𝜑 → ∀𝑦𝜓)
Theorem	bj-cbveximi 36886*	An equality-free general instance of one half of a precise form of bj-cbvex 36888. (Contributed by BJ, 12-Mar-2023.) (Proof modification is discouraged.)
⊢ (𝜒 → (𝜑 → 𝜓))    &   ⊢ ∀𝑥∃𝑦𝜒    ⇒   ⊢ (∃𝑥𝜑 → ∃𝑦𝜓)
Theorem	bj-cbval 36887*	Changing a bound variable (universal quantification case) in a weak axiomatization, assuming that all variables denote (which is valid in inclusive free logic) and that equality is symmetric. (Contributed by BJ, 12-Mar-2023.) (Proof modification is discouraged.)
⊢ ∀𝑦∃𝑥 𝑥 = 𝑦    &   ⊢ ∀𝑥∃𝑦 𝑦 = 𝑥    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝑥 → 𝑥 = 𝑦)    ⇒   ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓)
Theorem	bj-cbvex 36888*	Changing a bound variable (existential quantification case) in a weak axiomatization, assuming that all variables denote (which is valid in inclusive free logic) and that equality is symmetric. (Contributed by BJ, 12-Mar-2023.) (Proof modification is discouraged.)
⊢ ∀𝑦∃𝑥 𝑥 = 𝑦    &   ⊢ ∀𝑥∃𝑦 𝑦 = 𝑥    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝑥 → 𝑥 = 𝑦)    ⇒   ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓)
Syntax	wmoo 36889	Syntax for BJ's version of the uniqueness quantifier.
wff ∃**𝑥𝜑
Definition	df-bj-mo 36890*	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 36891*	Proposed definition to replace df-sb 2069 and df-sbc 3743. 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. The equality 𝑦 = 𝑥 may seem "reversed", but it is written this way so that "substitution for oneself" does not require symmetry of equality to be seen to be the identity on propositions. (Contributed by BJ, 19-Feb-2026.)
⊢ ([𝐴 / 𝑥]𝜑 ↔ ∃𝑦(𝑦 = 𝐴 ∧ ∀𝑥(𝑦 = 𝑥 → 𝜑)))
Theorem	bj-ssbeq 36892*	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 36892 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 36893*	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 36894*	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 36895*	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 36896*	Remove a DV condition from bj-ax12v 36895 (using core axioms only). (Contributed by BJ, 26-Dec-2020.) (Proof modification is discouraged.)
⊢ ∀𝑥(𝑥 = 𝑡 → (𝜑 → ∀𝑥(𝑥 = 𝑡 → 𝜑)))
Theorem	bj-ax12ssb 36897*	Axiom bj-ax12 36896 expressed using substitution. (Contributed by BJ, 26-Dec-2020.) (Proof modification is discouraged.)
⊢ [𝑡 / 𝑥](𝜑 → [𝑡 / 𝑥]𝜑)
Theorem	bj-19.41al 36898	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 36899*	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 36900*	Proof of sbalex 2250 from core axioms, ax-10 2147 (modal5), and bj-ax12 36896. (Contributed by BJ, 29-Dec-2020.) (Proof modification is discouraged.)
⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑))