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-dfbi6 37201	Alternate definition of the biconditional. (Contributed by BJ, 4-Oct-2019.)
⊢ ((𝜑 ↔ 𝜓) ↔ ((𝜑 ∨ 𝜓) ↔ (𝜑 ∧ 𝜓)))
Theorem	bj-bijust0ALT 37202	Alternate proof of bijust0 207; shorter but using additional intermediate results. (Contributed by NM, 11-May-1999.) (Proof shortened by Josh Purinton, 29-Dec-2000.) (Revised by BJ, 19-Mar-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ¬ ((𝜑 → 𝜑) → ¬ (𝜑 → 𝜑))
Theorem	bj-bijust00 37203	A self-implication does not imply the negation of a self-implication. Most general theorem of which bijust 208 is an instance (bijust0 207 and bj-bijust0ALT 37202 are therefore also instances of it). (Contributed by BJ, 7-Sep-2022.)
⊢ ¬ ((𝜑 → 𝜑) → ¬ (𝜓 → 𝜓))
21.19.1.8  The conditional operator for propositions
Theorem	bj-consensus 37204	Version of consensus 1068 expressed using the conditional operator. (Remark: it may be better to express it as consensus 1068, using only binary connectives, and hinting at the fact that it is a Boolean algebra identity, like the absorption identities.) (Contributed by BJ, 30-Sep-2019.)
⊢ ((if-(𝜑, 𝜓, 𝜒) ∨ (𝜓 ∧ 𝜒)) ↔ if-(𝜑, 𝜓, 𝜒))
Theorem	bj-consensusALT 37205	Alternate proof of bj-consensus 37204. (Contributed by BJ, 30-Sep-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((if-(𝜑, 𝜓, 𝜒) ∨ (𝜓 ∧ 𝜒)) ↔ if-(𝜑, 𝜓, 𝜒))
Theorem	bj-df-ifc 37206*	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 2744. We reprove the current df-if 4490 from it in bj-dfif 37207. (Contributed by BJ, 20-Sep-2019.) (Proof modification is discouraged.)
⊢ if(𝜑, 𝐴, 𝐵) = {𝑥 ∣ if-(𝜑, 𝑥 ∈ 𝐴, 𝑥 ∈ 𝐵)}
Theorem	bj-dfif 37207*	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 37208	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 37209	Uncurried (imported) form of imbi12 349. (Contributed by BJ, 6-May-2019.)
⊢ (((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃)) → ((𝜑 → 𝜒) ↔ (𝜓 → 𝜃)))
Theorem	bj-falor 37210	Dual of truan 1581 (which has biconditional reversed). (Contributed by BJ, 26-Oct-2019.) (Proof modification is discouraged.)
⊢ (𝜑 ↔ (⊥ ∨ 𝜑))
Theorem	bj-falor2 37211	Dual of truan 1581. (Contributed by BJ, 26-Oct-2019.) (Proof modification is discouraged.)
⊢ ((⊥ ∨ 𝜑) ↔ 𝜑)
Theorem	bj-bibibi 37212	A property of the biconditional. (Contributed by BJ, 26-Oct-2019.) (Proof modification is discouraged.)
⊢ (𝜑 ↔ (𝜓 ↔ (𝜑 ↔ 𝜓)))
Theorem	bj-imn3ani 37213	Duplication of bnj1224 35213. Three-fold version of imnani 406. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Revised by BJ, 22-Oct-2019.) (Proof modification is discouraged.)
⊢ ¬ (𝜑 ∧ 𝜓 ∧ 𝜒)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → ¬ 𝜒)
Theorem	bj-andnotim 37214	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 37215	This used to be in the main part. (Contributed by Wolf Lammen, 14-May-2013.) (Revised by BJ, 14-Jun-2019.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (((𝜃 → 𝜏) → 𝜑) → (((𝜏 → 𝜃) → 𝜓) → ((𝜃 ↔ 𝜏) → 𝜒)))
Theorem	bj-bisym 37216	This used to be in the main part. (Contributed by Wolf Lammen, 14-May-2013.) (Revised by BJ, 14-Jun-2019.)
⊢ (((𝜑 → 𝜓) → (𝜒 → 𝜃)) → (((𝜓 → 𝜑) → (𝜃 → 𝜒)) → ((𝜑 ↔ 𝜓) → (𝜒 ↔ 𝜃))))
Theorem	bj-bixor 37217	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 1828 corresponds to the necessitation rule of modal logic, and ax-4 1842 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/ 1842. A basic result in this logic is bj-gl4 37221.
Theorem	bj-axdd2 37218	This implication, proved using only ax-gen 1828 and ax-4 1842 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 37219. (Contributed by BJ, 16-May-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∃𝑥𝜑 → (∀𝑥𝜓 → ∃𝑥𝜓))
Theorem	bj-axd2d 37219	This implication, proved using only ax-gen 1828 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 37218. (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 37220	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 37218 and bj-axd2d 37219. (Contributed by BJ, 16-May-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((∀𝑥 ¬ 𝜑 → ¬ 𝜑) → ((∀𝑥𝜑 → 𝜑) → (∀𝑥𝜑 → ∃𝑥𝜑)))
Theorem	bj-gl4 37221	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 37221 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 37222	Over minimal calculus, the modal axiom (4) (hba1 2330) and the modal axiom (K) (ax-4 1842) together imply axc4 2356. (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 37224 and ax-prv2 37225 and ax-prv3 37226. Note the similarity with ax-gen 1828, ax-4 1842 and hba1 2330 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/ 2330. 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 37229) and Löb's theorem (bj-babylob 37230). See the comments of these theorems for details.
Syntax	cprvb 37223	Syntax for the provability predicate.
wff Prv 𝜑
Axiom	ax-prv1 37224	First property of three of the provability predicate. (Contributed by BJ, 3-Apr-2019.)
⊢ 𝜑    ⇒   ⊢ Prv 𝜑
Axiom	ax-prv2 37225	Second property of three of the provability predicate. (Contributed by BJ, 3-Apr-2019.)
⊢ (Prv (𝜑 → 𝜓) → (Prv 𝜑 → Prv 𝜓))
Axiom	ax-prv3 37226	Third property of three of the provability predicate. (Contributed by BJ, 3-Apr-2019.)
⊢ (Prv 𝜑 → Prv Prv 𝜑)
Theorem	prvlem1 37227	An elementary property of the provability predicate. (Contributed by BJ, 3-Apr-2019.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (Prv 𝜑 → Prv 𝜓)
Theorem	prvlem2 37228	An elementary property of the provability predicate. (Contributed by BJ, 3-Apr-2019.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (Prv 𝜑 → (Prv 𝜓 → Prv 𝜒))
Theorem	bj-babygodel 37229	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 37230	See the section header comments for the context, as well as the comments for bj-babygodel 37229. 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/ 37229). (Contributed by BJ, 20-Apr-2019.)
⊢ (𝜓 ↔ (Prv 𝜓 → 𝜑))    &   ⊢ (Prv 𝜑 → 𝜑)    ⇒   ⊢ 𝜑
Theorem	bj-godellob 37231	Proof of Gödel's theorem from Löb's theorem (see comments at bj-babygodel 37229 and bj-babylob 37230 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 37232	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 37233	Generalization rule on the right conjunct. See 19.28 2267. (Contributed by BJ, 7-Jul-2021.)
⊢ (𝜑 ∧ 𝜓)    ⇒   ⊢ (𝜑 ∧ ∀𝑥𝜓)
Theorem	bj-genl 37234	Generalization rule on the left conjunct. See 19.27 2266. (Contributed by BJ, 7-Jul-2021.)
⊢ (𝜑 ∧ 𝜓)    ⇒   ⊢ (∀𝑥𝜑 ∧ 𝜓)
Theorem	bj-genan 37235	Generalization rule on a conjunction. Forward inference associated with 19.26 1903. (Contributed by BJ, 7-Jul-2021.)
⊢ (𝜑 ∧ 𝜓)    ⇒   ⊢ (∀𝑥𝜑 ∧ ∀𝑥𝜓)
Theorem	bj-mpgs 37236	From a closed form theorem (the major premise) with an antecedent in the "strong necessity" modality (in the language of modal logic), deduce the associated inference. Strong necessity is stronger than necessity, and equivalent to it when sp 2222 (modal T) is available. Therefore, this theorem is stronger than mpg 1830, and strictly stronger when sp 2222 is not available. (Contributed by BJ, 1-Nov-2023.)
⊢ ((𝜑 ∧ ∀𝑥𝜑) → 𝜓)    &   ⊢ 𝜑    ⇒   ⊢ 𝜓
21.19.4.3  Adding ax-4
Theorem	bj-almp 37237	A quantified form of ax-mp 5. See also barbara 2692, bj-ala1i 37244, bj-almpi 37245. (Contributed by BJ, 19-Mar-2026.)
⊢ ∀𝑥(𝜓 → 𝜑)    &   ⊢ ∀𝑥𝜓    ⇒   ⊢ ∀𝑥𝜑
Theorem	bj-sylggt 37238	Stronger form of sylgt 1855, closer to ax-2 7. (Contributed by BJ, 30-Jul-2025.)
⊢ ((𝜑 → ∀𝑥(𝜓 → 𝜒)) → ((𝜑 → ∀𝑥𝜓) → (𝜑 → ∀𝑥𝜒)))
Theorem	bj-alrimg 37239	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 37261. (Contributed by BJ, 9-Dec-2023.)
⊢ ((𝜑 → ∀𝑥𝜓) → (∀𝑥(𝜓 → 𝜒) → (𝜑 → ∀𝑥𝜒)))
Theorem	bj-sylgt2 37240	Uncurried (imported) form of sylgt 1855. (Contributed by BJ, 2-May-2019.)
⊢ ((∀𝑥(𝜓 → 𝜒) ∧ (𝜑 → ∀𝑥𝜓)) → (𝜑 → ∀𝑥𝜒))
Theorem	bj-nexdh 37241	Closed form of nexdh 1898 (actually, its general instance). (Contributed by BJ, 6-May-2019.)
⊢ (∀𝑥(𝜑 → ¬ 𝜓) → ((𝜒 → ∀𝑥𝜑) → (𝜒 → ¬ ∃𝑥𝜓)))
Theorem	bj-nexdh2 37242	Uncurried (imported) form of bj-nexdh 37241. (Contributed by BJ, 6-May-2019.)
⊢ ((∀𝑥(𝜑 → ¬ 𝜓) ∧ (𝜒 → ∀𝑥𝜑)) → (𝜒 → ¬ ∃𝑥𝜓))
Theorem	bj-alimii 37243	Inference associated with alimi 1844. Double inference associated with alim 1843. The usual proof of an associated inference (here from alimi 1844 and ax-mp 5) has the same size and same number of steps. (Contributed by BJ, 19-Mar-2026.)
⊢ (𝜓 → 𝜑)    &   ⊢ ∀𝑥𝜓    ⇒   ⊢ ∀𝑥𝜑
Theorem	bj-ala1i 37244	Add an antecedent in a universally quantified formula. Inference associated with ala1 1846. (Contributed by BJ, 6-Oct-2018.)
⊢ ∀𝑥𝜑    ⇒   ⊢ ∀𝑥(𝜓 → 𝜑)
Theorem	bj-almpi 37245	A quantified form of mpi 21. See also barbara 2692, bj-ala1i 37244, bj-almp 37237. (Contributed by BJ, 19-Mar-2026.)
⊢ ∀𝑥(𝜑 → (𝜒 → 𝜓))    &   ⊢ ∀𝑥𝜒    ⇒   ⊢ ∀𝑥(𝜑 → 𝜓)
Theorem	bj-almpig 37246	A partially quantified form of mpi 21 similar to bj-almpi 37245. (Contributed by BJ, 19-Mar-2026.)
⊢ (𝜑 → (𝜒 → 𝜓))    &   ⊢ ∀𝑥𝜒    ⇒   ⊢ ∀𝑥(𝜑 → 𝜓)
Theorem	bj-alsyl 37247	Syllogism under the universal quantifier, in the curried form appearing as Theorem *10.3 of [WhiteheadRussell] p. 145. See alsyl 1926 for the uncurried form. (Contributed by BJ, 28-Mar-2026.)
⊢ (∀𝑥(𝜑 → 𝜓) → (∀𝑥(𝜓 → 𝜒) → ∀𝑥(𝜑 → 𝜒)))
Theorem	bj-2alim 37248	Closed form of 2alimi 1845. (Contributed by BJ, 6-May-2019.)
⊢ (∀𝑥∀𝑦(𝜑 → 𝜓) → (∀𝑥∀𝑦𝜑 → ∀𝑥∀𝑦𝜓))
Theorem	bj-alimdh 37249	General instance of alimdh 1850. (Contributed by NM, 4-Jan-2002.) State the most general derivable instance. (Revised by BJ, 5-Apr-2026.)
⊢ (𝜑 → ∀𝑥𝜓)    &   ⊢ (𝜓 → (𝜒 → 𝜃))    ⇒   ⊢ (𝜑 → (∀𝑥𝜒 → ∀𝑥𝜃))
Theorem	bj-alrimdh 37250	Deduction form of Theorem 19.21 of [Margaris] p. 90, see 19.21 2246 and 19.21h 2324. (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 37251	A slightly more general alrimd 2254. A common usage will have 𝜑 substituted for 𝜓 and 𝜒 substituted for 𝜃, giving a form closer to alrimd 2254. (Contributed by BJ, 25-Dec-2023.)
⊢ (𝜑 → ∀𝑥𝜓)    &   ⊢ (𝜑 → (𝜒 → ∀𝑥𝜃))    &   ⊢ (𝜓 → (𝜃 → 𝜏))    ⇒   ⊢ (𝜑 → (𝜒 → ∀𝑥𝜏))
Theorem	bj-exa1i 37252	Add an antecedent in an existentially quantified formula. Inference associated with exa1 1871. (Contributed by BJ, 6-Oct-2018.)
⊢ ∃𝑥𝜑    ⇒   ⊢ ∃𝑥(𝜓 → 𝜑)
Theorem	bj-alanim 37253	Closed form of alanimi 1849. (Contributed by BJ, 6-May-2019.)
⊢ (∀𝑥((𝜑 ∧ 𝜓) → 𝜒) → ((∀𝑥𝜑 ∧ ∀𝑥𝜓) → ∀𝑥𝜒))
Theorem	bj-2albi 37254	Closed form of 2albii 1853. (Contributed by BJ, 6-May-2019.)
⊢ (∀𝑥∀𝑦(𝜑 ↔ 𝜓) → (∀𝑥∀𝑦𝜑 ↔ ∀𝑥∀𝑦𝜓))
Theorem	bj-notalbii 37255	Equivalence of universal quantification of negation of equivalent formulas. Shortens ab0 4336 (103>94), ballotlem2 34903 (2655>2648), bnj1143 35202 (522>519), hausdiag 23831 (2119>2104). (Contributed by BJ, 17-Jul-2021.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (∀𝑥 ¬ 𝜑 ↔ ∀𝑥 ¬ 𝜓)
Theorem	bj-2exim 37256	Closed form of 2eximi 1869. (Contributed by BJ, 6-May-2019.)
⊢ (∀𝑥∀𝑦(𝜑 → 𝜓) → (∃𝑥∃𝑦𝜑 → ∃𝑥∃𝑦𝜓))
Theorem	bj-2exbi 37257	Closed form of 2exbii 1882. (Contributed by BJ, 6-May-2019.)
⊢ (∀𝑥∀𝑦(𝜑 ↔ 𝜓) → (∃𝑥∃𝑦𝜑 ↔ ∃𝑥∃𝑦𝜓))
Theorem	bj-3exbi 37258	Closed form of 3exbii 1883. (Contributed by BJ, 6-May-2019.)
⊢ (∀𝑥∀𝑦∀𝑧(𝜑 ↔ 𝜓) → (∃𝑥∃𝑦∃𝑧𝜑 ↔ ∃𝑥∃𝑦∃𝑧𝜓))
Theorem	bj-sylget 37259	Dual statement of sylgt 1855. Closed form of bj-sylge 37262. (Contributed by BJ, 2-May-2019.)
⊢ (∀𝑥(𝜒 → 𝜑) → ((∃𝑥𝜑 → 𝜓) → (∃𝑥𝜒 → 𝜓)))
Theorem	bj-sylget2 37260	Uncurried (imported) form of bj-sylget 37259. (Contributed by BJ, 2-May-2019.)
⊢ ((∀𝑥(𝜑 → 𝜓) ∧ (∃𝑥𝜓 → 𝜒)) → (∃𝑥𝜑 → 𝜒))
Theorem	bj-exlimg 37261	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 37239. (Contributed by BJ, 9-Dec-2023.)
⊢ ((∃𝑥𝜑 → 𝜓) → (∀𝑥(𝜒 → 𝜑) → (∃𝑥𝜒 → 𝜓)))
Theorem	bj-sylge 37262	Dual statement of sylg 1856 (the final "e" in the label stands for "existential (version of sylg 1856)". Variant of exlimih 2326. (Contributed by BJ, 25-Dec-2023.)
⊢ (∃𝑥𝜑 → 𝜓)    &   ⊢ (𝜒 → 𝜑)    ⇒   ⊢ (∃𝑥𝜒 → 𝜓)
Theorem	bj-exlimd 37263	A slightly more general exlimd 2257. A common usage will have 𝜑 substituted for 𝜓 and 𝜃 substituted for 𝜏, giving a form closer to exlimd 2257. (Contributed by BJ, 25-Dec-2023.)
⊢ (𝜑 → ∀𝑥𝜓)    &   ⊢ (𝜑 → (∃𝑥𝜃 → 𝜏))    &   ⊢ (𝜓 → (𝜒 → 𝜃))    ⇒   ⊢ (𝜑 → (∃𝑥𝜒 → 𝜏))
Theorem	bj-nfimexal 37264	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 1872) and the converse implication is the join of instances of bj-alrimg 37239 and bj-exlimg 37261 (see 19.38a 1873 and 19.38b 1874). TODO: prove a version where the antecedents use the nonfreeness quantifier. (Contributed by BJ, 9-Dec-2023.)
⊢ (((∃𝑥𝜑 → ∀𝑥𝜑) ∨ (∃𝑥𝜓 → ∀𝑥𝜓)) → ((∃𝑥𝜑 → ∀𝑥𝜓) ↔ ∀𝑥(𝜑 → 𝜓)))
Theorem	bj-exim 37265	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 1843 to allow use in bj-alexim 37266. (Revised by BJ, 9-Dec-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓))
Theorem	bj-alexim 37266	Closed form of aleximi 1865. Note: this proof is shorter, so aleximi 1865 could be deduced from it (exim 1867 would have to be proved first, see bj-exim 37265). (Contributed by BJ, 8-Nov-2021.)
⊢ (∀𝑥(𝜑 → (𝜓 → 𝜒)) → (∀𝑥𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒)))
Theorem	bj-aleximiALT 37267	Alternate proof of aleximi 1865 from exim 1867, 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 37268	Closed form of hbxfrbi 1858. Note: it is less important than nfbiit 1884. The antecedent is in the "strong necessity" modality of modal logic (see also bj-nnftht 37401) in order not to require sp 2222 (modal T). See bj-hbyfrbi 37269 for its version with existential quantifiers. (Contributed by BJ, 6-May-2019.)
⊢ (((𝜑 ↔ 𝜓) ∧ ∀𝑥(𝜑 ↔ 𝜓)) → ((𝜑 → ∀𝑥𝜑) ↔ (𝜓 → ∀𝑥𝜓)))
Theorem	bj-hbyfrbi 37269	Version of bj-hbxfrbi 37268 with existential quantifiers. (Contributed by BJ, 23-Aug-2023.)
⊢ (((𝜑 ↔ 𝜓) ∧ ∀𝑥(𝜑 ↔ 𝜓)) → ((∃𝑥𝜑 → 𝜑) ↔ (∃𝑥𝜓 → 𝜓)))
Theorem	bj-exalim 37270	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 1943. I propose to move to the main part: bj-exalim 37270, bj-exalimi 37271, bj-eximcom 37272 bj-exalims 37273, bj-exalimsi 37274, bj-ax12i 37277, bj-ax12wlem 37300, bj-ax12w 37333. A new label is needed for bj-ax12i 37277 and label suggestions are welcome for the others. I also propose to change ¬ ∀𝑥¬ to ∃𝑥 in speimfw 1996 and spimfw 1998 (other spim* theorems use ∃𝑥 and very few theorems in set.mm use ¬ ∀𝑥¬). (Contributed by BJ, 8-Nov-2021.)
⊢ (∀𝑥(𝜑 → (𝜓 → 𝜒)) → (∃𝑥𝜑 → (∀𝑥𝜓 → ∃𝑥𝜒)))
Theorem	bj-exalimi 37271	An inference for distributing quantifiers over a nested implication. The canonical derivation from its closed form bj-exalim 37270 (using mpg 1830) has fewer essential steps, but more steps in total (yielding a longer compressed proof). (Almost) the general statement that speimfw 1996 proves. (Contributed by BJ, 29-Sep-2019.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (∃𝑥𝜑 → (∀𝑥𝜓 → ∃𝑥𝜒))
Theorem	bj-eximcom 37272	A commuted form of exim 1867 which is sometimes posited as an axiom in instuitionistic modal logic. Forward implication of 19.35 1910. Its converse is not intuitionistic. (Contributed by BJ, 9-Dec-2023.)
⊢ (∃𝑥(𝜑 → 𝜓) → (∀𝑥𝜑 → ∃𝑥𝜓))
Theorem	bj-exalims 37273	Distributing quantifiers over a nested implication. (Almost) the general statement that spimfw 1998 proves. (Contributed by BJ, 29-Sep-2019.)
⊢ (∃𝑥𝜑 → (¬ 𝜒 → ∀𝑥 ¬ 𝜒))    ⇒   ⊢ (∀𝑥(𝜑 → (𝜓 → 𝜒)) → (∃𝑥𝜑 → (∀𝑥𝜓 → 𝜒)))
Theorem	bj-exalimsi 37274	An inference for distributing quantifiers over a nested implication. (Almost) the general statement that spimfw 1998 proves. (Contributed by BJ, 29-Sep-2019.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (∃𝑥𝜑 → (¬ 𝜒 → ∀𝑥 ¬ 𝜒))    ⇒   ⊢ (∃𝑥𝜑 → (∀𝑥𝜓 → 𝜒))
Theorem	bj-axdd2ALT 37275	Alternate proof of bj-axdd2 37218 (this should replace bj-axdd2 37218 when bj-exalimi 37271 is moved to the main section). (Contributed by BJ, 8-Mar-2026.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∃𝑥𝜑 → (∀𝑥𝜓 → ∃𝑥𝜓))
Theorem	bj-ax12ig 37276	A lemma used to prove a weak form of the axiom of substitution. A generalization of bj-ax12i 37277. (Contributed by BJ, 19-Dec-2020.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → (𝜒 → ∀𝑥𝜒))    ⇒   ⊢ (𝜑 → (𝜓 → ∀𝑥(𝜑 → 𝜓)))
Theorem	bj-ax12i 37277	A weakening of bj-ax12ig 37276 that is sufficient to prove a weak form of the axiom of substitution ax-12 2216. The general statement of which ax12i 1999 is an instance. (Contributed by BJ, 29-Sep-2019.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜒 → ∀𝑥𝜒)    ⇒   ⊢ (𝜑 → (𝜓 → ∀𝑥(𝜑 → 𝜓)))
Theorem	bj-nfimt 37278	Closed form of nfim 1929 and curried (exported) form of nfimt 1928. (Contributed by BJ, 20-Oct-2021.) Proof should not use 19.35 1910. (Proof modification is discouraged.)
⊢ (Ⅎ𝑥𝜑 → (Ⅎ𝑥𝜓 → Ⅎ𝑥(𝜑 → 𝜓)))
Theorem	bj-spimnfe 37279	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 2270, bj-19.36im 37421, 19.36imv 1978, spimfw 1998... (Contributed by BJ, 3-Apr-2026.) Proof should not use 19.35 1910. (Proof modification is discouraged.)
⊢ ((∃𝑥𝜓 → 𝜓) → (∃𝑥(𝜑 → 𝜓) → (∀𝑥𝜑 → 𝜓)))
Theorem	bj-spimenfa 37280	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 1910. (Proof modification is discouraged.)
⊢ ((𝜑 → ∀𝑥𝜑) → (∃𝑥(𝜑 → 𝜓) → (𝜑 → ∃𝑥𝜓)))
Theorem	bj-spim 37281	A lemma for universal specification. In applications, 𝑥 = 𝑦 will be substituted for 𝜓 and ax6ev 2002 will prove Hypothesis bj-spim.denote. (Contributed by BJ, 4-Apr-2026.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → (∃𝑥𝜃 → 𝜃))    &   ⊢ (𝜑 → ∃𝑥𝜓)    &   ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))    ⇒   ⊢ (𝜑 → (∀𝑥𝜒 → 𝜃))
Theorem	bj-spime 37282	A lemma for existential generalization. In applications, 𝑥 = 𝑦 will be substituted for 𝜓 and ax6ev 2002 will prove Hypothesis bj-spime.denote. (Contributed by BJ, 4-Apr-2026.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → (𝜒 → ∀𝑥𝜒))    &   ⊢ (𝜑 → ∃𝑥𝜓)    &   ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))    ⇒   ⊢ (𝜑 → (𝜒 → ∃𝑥𝜃))
Theorem	bj-cbvalimd0 37283	A lemma for alpha-renaming of variables bound by a universal quantifier. In applications, 𝑥 = 𝑦 will be substituted for 𝜓 and ax6ev 2002 will prove Hypothesis bj-cbvalimd0.denote. When ax6ev 2002 is not available but only its universal closure is, then bj-cbvalimd 37286 or bj-cbvalimdv 37288 should be used (see bj-cbvalimdlem 37284, bj-cbval 37301). (Contributed by BJ, 4-Apr-2026.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → ∀𝑦𝜑)    &   ⊢ (𝜑 → (𝜒 → ∀𝑦𝜒))    &   ⊢ (𝜑 → (∃𝑥𝜃 → 𝜃))    &   ⊢ (𝜑 → ∃𝑥𝜓)    &   ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))    ⇒   ⊢ (𝜑 → (∀𝑥𝜒 → ∀𝑦𝜃))
Theorem	bj-cbvalimdlem 37284	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 37288 or from a nonfreeness condition and alcom 2197 as in bj-cbvalimd 37286. Hypothesis bj-cbvalimdlem.denote is weaker than the corresponding hypothesis of bj-cbvalimd0 37283, and this proof is therefore a bit longer, not using bj-spim 37281 but bj-eximcom 37272. (Contributed by BJ, 12-Mar-2023.) Proof should not use 19.35 1910. (Proof modification is discouraged.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → ∀𝑦𝜑)    &   ⊢ (𝜑 → (∀𝑥𝜒 → ∀𝑦∀𝑥𝜒))    &   ⊢ (𝜑 → (∃𝑥𝜃 → 𝜃))    &   ⊢ (𝜑 → ∀𝑦∃𝑥𝜓)    &   ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))    ⇒   ⊢ (𝜑 → (∀𝑥𝜒 → ∀𝑦𝜃))
Theorem	bj-cbveximdlem 37285	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 37289 or from a nonfreeness condition and excom 2200 as in bj-cbveximd 37287. 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 37282 but bj-eximcom 37272. (Contributed by BJ, 12-Mar-2023.) Proof should not use 19.35 1910. (Proof modification is discouraged.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → ∀𝑦𝜑)    &   ⊢ (𝜑 → (𝜒 → ∀𝑦𝜒))    &   ⊢ (𝜑 → (∃𝑥∃𝑦𝜃 → ∃𝑦𝜃))    &   ⊢ (𝜑 → ∀𝑥∃𝑦𝜓)    &   ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))    ⇒   ⊢ (𝜑 → (∃𝑥𝜒 → ∃𝑦𝜃))
Theorem	bj-cbvalimd 37286	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 37287	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 37288*	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 37289*	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 37290*	Version of spvw 2014 and 19.3v 2015 proved from ax-1 6-- ax-5 1943. The antecedent can for instance be proved with the existence axiom extru 2008. (Contributed by BJ, 8-Mar-2026.) (Proof modification is discouraged.)
⊢ (∃𝑥𝜑 → (𝜓 ↔ ∀𝑥𝜓))
Theorem	bj-spvew 37291*	Version of 19.8v 2016 and 19.9v 2017 proved from ax-1 6-- ax-5 1943. The antecedent can for instance be proved with the existence axiom extru 2008. (Contributed by BJ, 8-Mar-2026.) This could also be proved from bj-spvw 37290 using duality, but that proof would not be intuitionistic, contrary to the present one. (Proof modification is discouraged.)
⊢ (∃𝑥𝜑 → (𝜓 ↔ ∃𝑥𝜓))
Theorem	bj-alextruim 37292*	An equivalent expression for universal quantification over a non-occurring variable proved over ax-1 6-- ax-5 1943. The forward implication can be strengthened when ax-6 2000 is posited (which implies that models are non-empty), see spvw 2014. The reverse implication can be seen as a strengthening of ax-5 1943 (since the antecedent of the implication is weakened). See bj-exextruan 37293 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 37293*	An equivalent expression for existential quantification over a non-occurring variable proved over ax-1 6-- ax-5 1943. The forward implication can be seen as a strengthening of ax-5 1943 (a conjunct is added to the consequent of the implication). The reverse implication can be strengthened when ax-6 2000 is posited (which implies that models are non-empty), see 19.8v 2016. See bj-alextruim 37292 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 37294*	Universally quantifying over a non-occurring variable is independent of that variable, over ax-1 6-- ax-5 1943 and the existence axiom extru 2008. See bj-cbvaw 37296 for a strengthening. (Contributed by BJ, 8-Mar-2026.) (Proof modification is discouraged.)
⊢ (∃𝑥𝜑 → (∀𝑥𝜓 → ∀𝑦𝜓))
Theorem	bj-cbvexvv 37295*	Existentially quantifying over a non-occurring variable is independent of that variable, over ax-1 6-- ax-5 1943 and the existence axiom extru 2008. See bj-cbvew 37297 for a strengthening. (Contributed by BJ, 8-Mar-2026.) (Proof modification is discouraged.)
⊢ (∃𝑥𝜑 → (∃𝑦𝜓 → ∃𝑥𝜓))
Theorem	bj-cbvaw 37296*	Universally quantifying over a non-occurring variable is independent from the variable, under a weaker condition than in bj-cbvalvv 37294. 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 867). (Proof modification is discouraged.)
⊢ ((∀𝑥𝜑 → ∀𝑦⊥) → (∀𝑥𝜓 → ∀𝑦𝜓))
Theorem	bj-cbvew 37297*	Existentially quantifying over a non-occurring variable is independent from the variable, under a weaker condition than in bj-cbvexvv 37295. 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 37298*	Universally quantifying over a non-occurring variable is independent from the variable, under a weaker condition than in bj-cbvalvv 37294. (Contributed by BJ, 14-Mar-2026.) (Proof modification is discouraged.)
⊢ ((∃𝑥⊤ → ∃𝑦𝜑) → (∀𝑦𝜓 → ∀𝑥𝜓))
Theorem	bj-cbvaew 37299*	Exixtentially quantifying over a non-occurring variable is independent from the variable, under a weaker condition than in bj-cbvexvv 37295. (Contributed by BJ, 14-Mar-2026.) (Proof modification is discouraged.)
⊢ ((∀𝑥𝜑 → ∀𝑦⊥) → (∃𝑦𝜓 → ∃𝑥𝜓))
Theorem	bj-ax12wlem 37300*	A lemma used to prove a weak version of the axiom of substitution ax-12 2216. (Temporary comment: The general statement that ax12wlem 2170 proves.) (Contributed by BJ, 20-Mar-2020.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (𝜓 → ∀𝑥(𝜑 → 𝜓)))