P. 360 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 35901-36000   *Has distinct variable group(s)

Type	Label	Description
Statement
21.17.1.5  Implication and negation
Theorem	bj-con2com 35901	A commuted form of the contrapositive, true in minimal calculus. (Contributed by BJ, 19-Mar-2020.)
⊢ (𝜑 → ((𝜓 → ¬ 𝜑) → ¬ 𝜓))
Theorem	bj-con2comi 35902	Inference associated with bj-con2com 35901. Its associated inference is mt2 199. TODO: when in the main part, add to mt2 199 that it is the inference associated with bj-con2comi 35902. (Contributed by BJ, 19-Mar-2020.)
⊢ 𝜑    ⇒   ⊢ ((𝜓 → ¬ 𝜑) → ¬ 𝜓)
Theorem	bj-pm2.01i 35903	Inference associated with the weak Clavius law pm2.01 188. (Contributed by BJ, 30-Mar-2020.)
⊢ (𝜑 → ¬ 𝜑)    ⇒   ⊢ ¬ 𝜑
Theorem	bj-nimn 35904	If a formula is true, then it does not imply its negation. (Contributed by BJ, 19-Mar-2020.) A shorter proof is possible using id 22 and jc 161, however, the present proof uses theorems that are more basic than jc 161. (Proof modification is discouraged.)
⊢ (𝜑 → ¬ (𝜑 → ¬ 𝜑))
Theorem	bj-nimni 35905	Inference associated with bj-nimn 35904. (Contributed by BJ, 19-Mar-2020.)
⊢ 𝜑    ⇒   ⊢ ¬ (𝜑 → ¬ 𝜑)
Theorem	bj-peircei 35906	Inference associated with peirce 201. (Contributed by BJ, 30-Mar-2020.)
⊢ ((𝜑 → 𝜓) → 𝜑)    ⇒   ⊢ 𝜑
Theorem	bj-looinvi 35907	Inference associated with looinv 202. Its associated inference is bj-looinvii 35908. (Contributed by BJ, 30-Mar-2020.)
⊢ ((𝜑 → 𝜓) → 𝜓)    ⇒   ⊢ ((𝜓 → 𝜑) → 𝜑)
Theorem	bj-looinvii 35908	Inference associated with bj-looinvi 35907. (Contributed by BJ, 30-Mar-2020.)
⊢ ((𝜑 → 𝜓) → 𝜓)    &   ⊢ (𝜓 → 𝜑)    ⇒   ⊢ 𝜑
Theorem	bj-mt2bi 35909	Version of mt2 199 where the major premise is a biconditional. Another proof is also possible via con2bii 357 and mpbi 229. The current mt2bi 363 should be relabeled, maybe to imfal. (Contributed by BJ, 5-Oct-2024.)
⊢ 𝜑    &   ⊢ (𝜓 ↔ ¬ 𝜑)    ⇒   ⊢ ¬ 𝜓
Theorem	bj-ntrufal 35910	The negation of a theorem is equivalent to false. This can shorten dfnul2 4325. (Contributed by BJ, 5-Oct-2024.)
⊢ 𝜑    ⇒   ⊢ (¬ 𝜑 ↔ ⊥)
Theorem	bj-fal 35911	Shortening of fal 1554 using bj-mt2bi 35909. (Contributed by Anthony Hart, 22-Oct-2010.) (Proof shortened by Mel L. O'Cat, 11-Mar-2012.) (Proof modification is discouraged.)
⊢ ¬ ⊥
21.17.1.6  Disjunction A few lemmas about disjunction. The fundamental theorems in this family are the dual statements pm4.71 557 and pm4.72 947. See also biort 933 and biorf 934.
Theorem	bj-jaoi1 35912	Shortens orfa2 37418 (58>53), pm1.2 901 (20>18), pm1.2 901 (20>18), pm2.4 904 (31>25), pm2.41 905 (31>25), pm2.42 940 (38>32), pm3.2ni 878 (43>39), pm4.44 994 (55>51). (Contributed by BJ, 30-Sep-2019.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ ((𝜑 ∨ 𝜓) → 𝜓)
Theorem	bj-jaoi2 35913	Shortens consensus 1050 (110>106), elnn0z 12578 (336>329), pm1.2 901 (20>19), pm3.2ni 878 (43>39), pm4.44 994 (55>51). (Contributed by BJ, 30-Sep-2019.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ ((𝜓 ∨ 𝜑) → 𝜓)
21.17.1.7  Logical equivalence A few other characterizations of the bicondional. The inter-definability of logical connectives offers many ways to express a given statement. Some useful theorems in this regard are df-or 845, df-an 396, pm4.64 846, imor 850, pm4.62 853 through pm4.67 398, and, for the De Morgan laws, ianor 979 through pm4.57 988.
Theorem	bj-dfbi4 35914	Alternate definition of the biconditional. (Contributed by BJ, 4-Oct-2019.)
⊢ ((𝜑 ↔ 𝜓) ↔ ((𝜑 ∧ 𝜓) ∨ ¬ (𝜑 ∨ 𝜓)))
Theorem	bj-dfbi5 35915	Alternate definition of the biconditional. (Contributed by BJ, 4-Oct-2019.)
⊢ ((𝜑 ↔ 𝜓) ↔ ((𝜑 ∨ 𝜓) → (𝜑 ∧ 𝜓)))
Theorem	bj-dfbi6 35916	Alternate definition of the biconditional. (Contributed by BJ, 4-Oct-2019.)
⊢ ((𝜑 ↔ 𝜓) ↔ ((𝜑 ∨ 𝜓) ↔ (𝜑 ∧ 𝜓)))
Theorem	bj-bijust0ALT 35917	Alternate proof of bijust0 203; 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 35918	A self-implication does not imply the negation of a self-implication. Most general theorem of which bijust 204 is an instance (bijust0 203 and bj-bijust0ALT 35917 are therefore also instances of it). (Contributed by BJ, 7-Sep-2022.)
⊢ ¬ ((𝜑 → 𝜑) → ¬ (𝜓 → 𝜓))
21.17.1.8  The conditional operator for propositions
Theorem	bj-consensus 35919	Version of consensus 1050 expressed using the conditional operator. (Remark: it may be better to express it as consensus 1050, 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 35920	Alternate proof of bj-consensus 35919. (Contributed by BJ, 30-Sep-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((if-(𝜑, 𝜓, 𝜒) ∨ (𝜓 ∧ 𝜒)) ↔ if-(𝜑, 𝜓, 𝜒))
Theorem	bj-df-ifc 35921*	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 2709. We reprove the current df-if 4529 from it in bj-dfif 35922. (Contributed by BJ, 20-Sep-2019.) (Proof modification is discouraged.)
⊢ if(𝜑, 𝐴, 𝐵) = {𝑥 ∣ if-(𝜑, 𝑥 ∈ 𝐴, 𝑥 ∈ 𝐵)}
Theorem	bj-dfif 35922*	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 35923	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.17.1.9  Propositional calculus: miscellaneous Miscellaneous theorems of propositional calculus.
Theorem	bj-imbi12 35924	Uncurried (imported) form of imbi12 346. (Contributed by BJ, 6-May-2019.)
⊢ (((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃)) → ((𝜑 → 𝜒) ↔ (𝜓 → 𝜃)))
Theorem	bj-biorfi 35925	This should be labeled "biorfi" while the current biorfi 936 should be labeled "biorfri". The dual of biorf 934 is not biantr 803 but iba 527 (and ibar 528). So there should also be a "biorfr". (Note that these four statements can actually be strengthened to biconditionals.) (Contributed by BJ, 26-Oct-2019.) (Proof modification is discouraged.)
⊢ ¬ 𝜑    ⇒   ⊢ (𝜓 ↔ (𝜑 ∨ 𝜓))
Theorem	bj-falor 35926	Dual of truan 1551 (which has biconditional reversed). (Contributed by BJ, 26-Oct-2019.) (Proof modification is discouraged.)
⊢ (𝜑 ↔ (⊥ ∨ 𝜑))
Theorem	bj-falor2 35927	Dual of truan 1551. (Contributed by BJ, 26-Oct-2019.) (Proof modification is discouraged.)
⊢ ((⊥ ∨ 𝜑) ↔ 𝜑)
Theorem	bj-bibibi 35928	A property of the biconditional. (Contributed by BJ, 26-Oct-2019.) (Proof modification is discouraged.)
⊢ (𝜑 ↔ (𝜓 ↔ (𝜑 ↔ 𝜓)))
Theorem	bj-imn3ani 35929	Duplication of bnj1224 34276. 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 35930	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 35931	This used to be in the main part. (Contributed by Wolf Lammen, 14-May-2013.) (Revised by BJ, 14-Jun-2019.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (((𝜃 → 𝜏) → 𝜑) → (((𝜏 → 𝜃) → 𝜓) → ((𝜃 ↔ 𝜏) → 𝜒)))
Theorem	bj-bisym 35932	This used to be in the main part. (Contributed by Wolf Lammen, 14-May-2013.) (Revised by BJ, 14-Jun-2019.)
⊢ (((𝜑 → 𝜓) → (𝜒 → 𝜃)) → (((𝜓 → 𝜑) → (𝜃 → 𝜒)) → ((𝜑 ↔ 𝜓) → (𝜒 ↔ 𝜃))))
Theorem	bj-bixor 35933	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.17.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 1796 corresponds to the necessitation rule of modal logic, and ax-4 1810 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/ 1810. A basic result in this logic is bj-gl4 35937.
Theorem	bj-axdd2 35934	This implication, proved using only ax-gen 1796 and ax-4 1810 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 35935. (Contributed by BJ, 16-May-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∃𝑥𝜑 → (∀𝑥𝜓 → ∃𝑥𝜓))
Theorem	bj-axd2d 35935	This implication, proved using only ax-gen 1796 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 ⊢ ∃𝑥⊤. 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 35934. (Contributed by BJ, 16-May-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((∀𝑥⊤ → ∃𝑥⊤) → ∃𝑥⊤)
Theorem	bj-axtd 35936	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 35934 and bj-axd2d 35935. (Contributed by BJ, 16-May-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((∀𝑥 ¬ 𝜑 → ¬ 𝜑) → ((∀𝑥𝜑 → 𝜑) → (∀𝑥𝜑 → ∃𝑥𝜑)))
Theorem	bj-gl4 35937	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 35937 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 35938	Over minimal calculus, the modal axiom (4) (hba1 2288) and the modal axiom (K) (ax-4 1810) together imply axc4 2313. (Contributed by BJ, 29-Nov-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((∀𝑥𝜑 → ∀𝑥∀𝑥𝜑) → ((∀𝑥(∀𝑥𝜑 → 𝜓) → (∀𝑥∀𝑥𝜑 → ∀𝑥𝜓)) → (∀𝑥(∀𝑥𝜑 → 𝜓) → (∀𝑥𝜑 → ∀𝑥𝜓))))
21.17.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 35940 and ax-prv2 35941 and ax-prv3 35942. Note the similarity with ax-gen 1796, ax-4 1810 and hba1 2288 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/ 2288. 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 35945) and Löb's theorem (bj-babylob 35946). See the comments of these theorems for details.
Syntax	cprvb 35939	Syntax for the provability predicate.
wff Prv 𝜑
Axiom	ax-prv1 35940	First property of three of the provability predicate. (Contributed by BJ, 3-Apr-2019.)
⊢ 𝜑    ⇒   ⊢ Prv 𝜑
Axiom	ax-prv2 35941	Second property of three of the provability predicate. (Contributed by BJ, 3-Apr-2019.)
⊢ (Prv (𝜑 → 𝜓) → (Prv 𝜑 → Prv 𝜓))
Axiom	ax-prv3 35942	Third property of three of the provability predicate. (Contributed by BJ, 3-Apr-2019.)
⊢ (Prv 𝜑 → Prv Prv 𝜑)
Theorem	prvlem1 35943	An elementary property of the provability predicate. (Contributed by BJ, 3-Apr-2019.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (Prv 𝜑 → Prv 𝜓)
Theorem	prvlem2 35944	An elementary property of the provability predicate. (Contributed by BJ, 3-Apr-2019.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (Prv 𝜑 → (Prv 𝜓 → Prv 𝜒))
Theorem	bj-babygodel 35945	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 35946	See the section header comments for the context, as well as the comments for bj-babygodel 35945. 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/ 35945). (Contributed by BJ, 20-Apr-2019.)
⊢ (𝜓 ↔ (Prv 𝜓 → 𝜑))    &   ⊢ (Prv 𝜑 → 𝜑)    ⇒   ⊢ 𝜑
Theorem	bj-godellob 35947	Proof of Gödel's theorem from Löb's theorem (see comments at bj-babygodel 35945 and bj-babylob 35946 for details). (Contributed by BJ, 20-Apr-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 ↔ ¬ Prv 𝜑)    &   ⊢ ¬ Prv ⊥    ⇒   ⊢ ⊥
21.17.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.17.4.1  Adding ax-gen
Theorem	bj-genr 35948	Generalization rule on the right conjunct. See 19.28 2220. (Contributed by BJ, 7-Jul-2021.)
⊢ (𝜑 ∧ 𝜓)    ⇒   ⊢ (𝜑 ∧ ∀𝑥𝜓)
Theorem	bj-genl 35949	Generalization rule on the left conjunct. See 19.27 2219. (Contributed by BJ, 7-Jul-2021.)
⊢ (𝜑 ∧ 𝜓)    ⇒   ⊢ (∀𝑥𝜑 ∧ 𝜓)
Theorem	bj-genan 35950	Generalization rule on a conjunction. Forward inference associated with 19.26 1872. (Contributed by BJ, 7-Jul-2021.)
⊢ (𝜑 ∧ 𝜓)    ⇒   ⊢ (∀𝑥𝜑 ∧ ∀𝑥𝜓)
Theorem	bj-mpgs 35951	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 2175 (modal T) is available. Therefore, this theorem is stronger than mpg 1798 when sp 2175 is not available. (Contributed by BJ, 1-Nov-2023.)
⊢ 𝜑    &   ⊢ ((𝜑 ∧ ∀𝑥𝜑) → 𝜓)    ⇒   ⊢ 𝜓
21.17.4.2  Adding ax-4
Theorem	bj-2alim 35952	Closed form of 2alimi 1813. (Contributed by BJ, 6-May-2019.)
⊢ (∀𝑥∀𝑦(𝜑 → 𝜓) → (∀𝑥∀𝑦𝜑 → ∀𝑥∀𝑦𝜓))
Theorem	bj-2exim 35953	Closed form of 2eximi 1837. (Contributed by BJ, 6-May-2019.)
⊢ (∀𝑥∀𝑦(𝜑 → 𝜓) → (∃𝑥∃𝑦𝜑 → ∃𝑥∃𝑦𝜓))
Theorem	bj-alanim 35954	Closed form of alanimi 1817. (Contributed by BJ, 6-May-2019.)
⊢ (∀𝑥((𝜑 ∧ 𝜓) → 𝜒) → ((∀𝑥𝜑 ∧ ∀𝑥𝜓) → ∀𝑥𝜒))
Theorem	bj-2albi 35955	Closed form of 2albii 1821. (Contributed by BJ, 6-May-2019.)
⊢ (∀𝑥∀𝑦(𝜑 ↔ 𝜓) → (∀𝑥∀𝑦𝜑 ↔ ∀𝑥∀𝑦𝜓))
Theorem	bj-notalbii 35956	Equivalence of universal quantification of negation of equivalent formulas. Shortens ab0 4374 (103>94), ballotlem2 33951 (2655>2648), bnj1143 34265 (522>519), hausdiag 23469 (2119>2104). (Contributed by BJ, 17-Jul-2021.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (∀𝑥 ¬ 𝜑 ↔ ∀𝑥 ¬ 𝜓)
Theorem	bj-2exbi 35957	Closed form of 2exbii 1850. (Contributed by BJ, 6-May-2019.)
⊢ (∀𝑥∀𝑦(𝜑 ↔ 𝜓) → (∃𝑥∃𝑦𝜑 ↔ ∃𝑥∃𝑦𝜓))
Theorem	bj-3exbi 35958	Closed form of 3exbii 1851. (Contributed by BJ, 6-May-2019.)
⊢ (∀𝑥∀𝑦∀𝑧(𝜑 ↔ 𝜓) → (∃𝑥∃𝑦∃𝑧𝜑 ↔ ∃𝑥∃𝑦∃𝑧𝜓))
Theorem	bj-sylgt2 35959	Uncurried (imported) form of sylgt 1823. (Contributed by BJ, 2-May-2019.)
⊢ ((∀𝑥(𝜓 → 𝜒) ∧ (𝜑 → ∀𝑥𝜓)) → (𝜑 → ∀𝑥𝜒))
Theorem	bj-alrimg 35960	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 35964. (Contributed by BJ, 9-Dec-2023.)
⊢ ((𝜑 → ∀𝑥𝜓) → (∀𝑥(𝜓 → 𝜒) → (𝜑 → ∀𝑥𝜒)))
Theorem	bj-alrimd 35961	A slightly more general alrimd 2207. A common usage will have 𝜑 substituted for 𝜓 and 𝜒 substituted for 𝜃, giving a form closer to alrimd 2207. (Contributed by BJ, 25-Dec-2023.)
⊢ (𝜑 → ∀𝑥𝜓)    &   ⊢ (𝜑 → (𝜒 → ∀𝑥𝜃))    &   ⊢ (𝜓 → (𝜃 → 𝜏))    ⇒   ⊢ (𝜑 → (𝜒 → ∀𝑥𝜏))
Theorem	bj-sylget 35962	Dual statement of sylgt 1823. Closed form of bj-sylge 35965. (Contributed by BJ, 2-May-2019.)
⊢ (∀𝑥(𝜒 → 𝜑) → ((∃𝑥𝜑 → 𝜓) → (∃𝑥𝜒 → 𝜓)))
Theorem	bj-sylget2 35963	Uncurried (imported) form of bj-sylget 35962. (Contributed by BJ, 2-May-2019.)
⊢ ((∀𝑥(𝜑 → 𝜓) ∧ (∃𝑥𝜓 → 𝜒)) → (∃𝑥𝜑 → 𝜒))
Theorem	bj-exlimg 35964	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 35960. (Contributed by BJ, 9-Dec-2023.)
⊢ ((∃𝑥𝜑 → 𝜓) → (∀𝑥(𝜒 → 𝜑) → (∃𝑥𝜒 → 𝜓)))
Theorem	bj-sylge 35965	Dual statement of sylg 1824 (the final "e" in the label stands for "existential (version of sylg 1824)". Variant of exlimih 2284. (Contributed by BJ, 25-Dec-2023.)
⊢ (∃𝑥𝜑 → 𝜓)    &   ⊢ (𝜒 → 𝜑)    ⇒   ⊢ (∃𝑥𝜒 → 𝜓)
Theorem	bj-exlimd 35966	A slightly more general exlimd 2210. A common usage will have 𝜑 substituted for 𝜓 and 𝜃 substituted for 𝜏, giving a form closer to exlimd 2210. (Contributed by BJ, 25-Dec-2023.)
⊢ (𝜑 → ∀𝑥𝜓)    &   ⊢ (𝜑 → (∃𝑥𝜃 → 𝜏))    &   ⊢ (𝜓 → (𝜒 → 𝜃))    ⇒   ⊢ (𝜑 → (∃𝑥𝜒 → 𝜏))
Theorem	bj-nfimexal 35967	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 1840) and the converse implication is the join of instances of bj-alrimg 35960 and bj-exlimg 35964 (see 19.38a 1841 and 19.38b 1842). TODO: prove a version where the antecedents use the nonfreeness quantifier. (Contributed by BJ, 9-Dec-2023.)
⊢ (((∃𝑥𝜑 → ∀𝑥𝜑) ∨ (∃𝑥𝜓 → ∀𝑥𝜓)) → ((∃𝑥𝜑 → ∀𝑥𝜓) ↔ ∀𝑥(𝜑 → 𝜓)))
Theorem	bj-alexim 35968	Closed form of aleximi 1833. Note: this proof is shorter, so aleximi 1833 could be deduced from it (exim 1835 would have to be proved first, see bj-eximALT 35982 but its proof is shorter (currently almost a subproof of aleximi 1833)). (Contributed by BJ, 8-Nov-2021.)
⊢ (∀𝑥(𝜑 → (𝜓 → 𝜒)) → (∀𝑥𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒)))
Theorem	bj-nexdh 35969	Closed form of nexdh 1867 (actually, its general instance). (Contributed by BJ, 6-May-2019.)
⊢ (∀𝑥(𝜑 → ¬ 𝜓) → ((𝜒 → ∀𝑥𝜑) → (𝜒 → ¬ ∃𝑥𝜓)))
Theorem	bj-nexdh2 35970	Uncurried (imported) form of bj-nexdh 35969. (Contributed by BJ, 6-May-2019.)
⊢ ((∀𝑥(𝜑 → ¬ 𝜓) ∧ (𝜒 → ∀𝑥𝜑)) → (𝜒 → ¬ ∃𝑥𝜓))
Theorem	bj-hbxfrbi 35971	Closed form of hbxfrbi 1826. Note: it is less important than nfbiit 1852. The antecedent is in the "strong necessity" modality of modal logic (see also bj-nnftht 36083) in order not to require sp 2175 (modal T). See bj-hbyfrbi 35972 for its version with existential quantifiers. (Contributed by BJ, 6-May-2019.)
⊢ (((𝜑 ↔ 𝜓) ∧ ∀𝑥(𝜑 ↔ 𝜓)) → ((𝜑 → ∀𝑥𝜑) ↔ (𝜓 → ∀𝑥𝜓)))
Theorem	bj-hbyfrbi 35972	Version of bj-hbxfrbi 35971 with existential quantifiers. (Contributed by BJ, 23-Aug-2023.)
⊢ (((𝜑 ↔ 𝜓) ∧ ∀𝑥(𝜑 ↔ 𝜓)) → ((∃𝑥𝜑 → 𝜑) ↔ (∃𝑥𝜓 → 𝜓)))
Theorem	bj-exalim 35973	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 35973, bj-exalimi 35974, bj-exalims 35975, bj-exalimsi 35976, bj-ax12i 35978, bj-ax12wlem 35985, bj-ax12w 36018. A new label is needed for bj-ax12i 35978 and label suggestions are welcome for the others. I also propose to change ¬ ∀𝑥¬ to ∃𝑥 in speimfw 1966 and spimfw 1968 (other spim* theorems use ∃𝑥 and very few theorems in set.mm use ¬ ∀𝑥¬). (Contributed by BJ, 8-Nov-2021.)
⊢ (∀𝑥(𝜑 → (𝜓 → 𝜒)) → (∃𝑥𝜑 → (∀𝑥𝜓 → ∃𝑥𝜒)))
Theorem	bj-exalimi 35974	An inference for distributing quantifiers over a nested implication. The canonical derivation from its closed form bj-exalim 35973 (using mpg 1798) has fewer essential steps, but more steps in total (yielding a longer compressed proof). (Almost) the general statement that speimfw 1966 proves. (Contributed by BJ, 29-Sep-2019.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (∃𝑥𝜑 → (∀𝑥𝜓 → ∃𝑥𝜒))
Theorem	bj-exalims 35975	Distributing quantifiers over a nested implication. (Almost) the general statement that spimfw 1968 proves. (Contributed by BJ, 29-Sep-2019.)
⊢ (∃𝑥𝜑 → (¬ 𝜒 → ∀𝑥 ¬ 𝜒))    ⇒   ⊢ (∀𝑥(𝜑 → (𝜓 → 𝜒)) → (∃𝑥𝜑 → (∀𝑥𝜓 → 𝜒)))
Theorem	bj-exalimsi 35976	An inference for distributing quantifiers over a nested implication. (Almost) the general statement that spimfw 1968 proves. (Contributed by BJ, 29-Sep-2019.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (∃𝑥𝜑 → (¬ 𝜒 → ∀𝑥 ¬ 𝜒))    ⇒   ⊢ (∃𝑥𝜑 → (∀𝑥𝜓 → 𝜒))
Theorem	bj-ax12ig 35977	A lemma used to prove a weak form of the axiom of substitution. A generalization of bj-ax12i 35978. (Contributed by BJ, 19-Dec-2020.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → (𝜒 → ∀𝑥𝜒))    ⇒   ⊢ (𝜑 → (𝜓 → ∀𝑥(𝜑 → 𝜓)))
Theorem	bj-ax12i 35978	A weakening of bj-ax12ig 35977 that is sufficient to prove a weak form of the axiom of substitution ax-12 2170. The general statement of which ax12i 1969 is an instance. (Contributed by BJ, 29-Sep-2019.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜒 → ∀𝑥𝜒)    ⇒   ⊢ (𝜑 → (𝜓 → ∀𝑥(𝜑 → 𝜓)))
Theorem	bj-nfimt 35979	Closed form of nfim 1898 and curried (exported) form of nfimt 1897. (Contributed by BJ, 20-Oct-2021.)
⊢ (Ⅎ𝑥𝜑 → (Ⅎ𝑥𝜓 → Ⅎ𝑥(𝜑 → 𝜓)))
Theorem	bj-cbvalimt 35980	A lemma in closed form used to prove bj-cbval 35990 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 35981	A lemma in closed form used to prove bj-cbvex 35991 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-eximALT 35982	Alternate proof of exim 1835 directly from alim 1811 by using df-ex 1781 (using duality of ∀ and ∃. (Contributed by BJ, 9-Dec-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓))
Theorem	bj-aleximiALT 35983	Alternate proof of aleximi 1833 from exim 1835, 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-eximcom 35984	A commuted form of exim 1835 which is sometimes posited as an axiom in instuitionistic modal logic. (Contributed by BJ, 9-Dec-2023.)
⊢ (∃𝑥(𝜑 → 𝜓) → (∀𝑥𝜑 → ∃𝑥𝜓))
21.17.4.3  Adding ax-5
Theorem	bj-ax12wlem 35985*	A lemma used to prove a weak version of the axiom of substitution ax-12 2170. (Temporary comment: The general statement that ax12wlem 2127 proves.) (Contributed by BJ, 20-Mar-2020.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (𝜓 → ∀𝑥(𝜑 → 𝜓)))
Theorem	bj-cbvalim 35986*	A lemma used to prove bj-cbval 35990 in a weak axiomatization. (Contributed by BJ, 12-Mar-2023.) (Proof modification is discouraged.)
⊢ (∀𝑦∃𝑥𝜒 → (∀𝑦∀𝑥(𝜒 → (𝜑 → 𝜓)) → (∀𝑥𝜑 → ∀𝑦𝜓)))
Theorem	bj-cbvexim 35987*	A lemma used to prove bj-cbvex 35991 in a weak axiomatization. (Contributed by BJ, 12-Mar-2023.) (Proof modification is discouraged.)
⊢ (∀𝑥∃𝑦𝜒 → (∀𝑥∀𝑦(𝜒 → (𝜑 → 𝜓)) → (∃𝑥𝜑 → ∃𝑦𝜓)))
Theorem	bj-cbvalimi 35988*	An equality-free general instance of one half of a precise form of bj-cbval 35990. (Contributed by BJ, 12-Mar-2023.) (Proof modification is discouraged.)
⊢ (𝜒 → (𝜑 → 𝜓))    &   ⊢ ∀𝑦∃𝑥𝜒    ⇒   ⊢ (∀𝑥𝜑 → ∀𝑦𝜓)
Theorem	bj-cbveximi 35989*	An equality-free general instance of one half of a precise form of bj-cbvex 35991. (Contributed by BJ, 12-Mar-2023.) (Proof modification is discouraged.)
⊢ (𝜒 → (𝜑 → 𝜓))    &   ⊢ ∀𝑥∃𝑦𝜒    ⇒   ⊢ (∃𝑥𝜑 → ∃𝑦𝜓)
Theorem	bj-cbval 35990*	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 35991*	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 35992	Syntax for BJ's version of the uniqueness quantifier.
wff ∃**𝑥𝜑
Definition	df-bj-mo 35993*	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.17.4.4  Equality and substitution
Theorem	bj-ssbeq 35994*	Substitution in an equality, disjoint variables case. Uses only ax-1 6 through ax-6 1970. It might be shorter to prove the result about composition of two substitutions and prove bj-ssbeq 35994 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 35995*	A lemma for the definiens of df-sb 2067. An instance of sp 2175 proved without it. Note: it has a common subproof with sbjust 2065. (Contributed by BJ, 22-Dec-2020.) (Proof modification is discouraged.)
⊢ (∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑)) → (𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
Theorem	bj-ssblem2 35996*	An instance of ax-11 2153 proved without it. The converse may not be provable without ax-11 2153 (since using alcomiw 2045 would require a DV on 𝜑, 𝑥, which defeats the purpose). (Contributed by BJ, 22-Dec-2020.) (Proof modification is discouraged.)
⊢ (∀𝑥∀𝑦(𝑦 = 𝑡 → (𝑥 = 𝑦 → 𝜑)) → ∀𝑦∀𝑥(𝑦 = 𝑡 → (𝑥 = 𝑦 → 𝜑)))
Theorem	bj-ax12v 35997*	A weaker form of ax-12 2170 and ax12v 2171, 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 35998*	Remove a DV condition from bj-ax12v 35997 (using core axioms only). (Contributed by BJ, 26-Dec-2020.) (Proof modification is discouraged.)
⊢ ∀𝑥(𝑥 = 𝑡 → (𝜑 → ∀𝑥(𝑥 = 𝑡 → 𝜑)))
Theorem	bj-ax12ssb 35999*	Axiom bj-ax12 35998 expressed using substitution. (Contributed by BJ, 26-Dec-2020.) (Proof modification is discouraged.)
⊢ [𝑡 / 𝑥](𝜑 → [𝑡 / 𝑥]𝜑)
Theorem	bj-19.41al 36000	Special case of 19.41 2227 proved from core axioms, ax-10 2136 (modal5), and hba1 2288 (modal4). (Contributed by BJ, 29-Dec-2020.) (Proof modification is discouraged.)
⊢ (∃𝑥(𝜑 ∧ ∀𝑥𝜓) ↔ (∃𝑥𝜑 ∧ ∀𝑥𝜓))