P. 371 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 37001-37100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	bj-19.37im 37001	One direction of 19.37 2240 from the same axioms as 19.37imv 1949. (Contributed by BJ, 2-Dec-2023.)
⊢ (Ⅎ'𝑥𝜑 → (∃𝑥(𝜑 → 𝜓) → (𝜑 → ∃𝑥𝜓)))
Theorem	bj-19.42t 37002	Closed form of 19.42 2244 from the same axioms as 19.42v 1955. (Contributed by BJ, 2-Dec-2023.)
⊢ (Ⅎ'𝑥𝜑 → (∃𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥𝜓)))
Theorem	bj-19.41t 37003	Closed form of 19.41 2243 from the same axioms as 19.41v 1951. The same is doable with 19.27 2235, 19.28 2236, 19.31 2242, 19.32 2241, 19.44 2245, 19.45 2246. (Contributed by BJ, 2-Dec-2023.)
⊢ (Ⅎ'𝑥𝜓 → (∃𝑥(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ 𝜓)))
Theorem	bj-pm11.53vw 37004	Version of pm11.53v 1946 with nonfreeness antecedents. One can also prove the theorem with antecedent (Ⅎ'𝑦∀𝑥𝜑 ∧ ∀𝑦Ⅎ'𝑥𝜓). (Contributed by BJ, 7-Oct-2024.)
⊢ ((∀𝑥Ⅎ'𝑦𝜑 ∧ Ⅎ'𝑥∀𝑦𝜓) → (∀𝑥∀𝑦(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → ∀𝑦𝜓)))
Theorem	bj-nnfv 37005*	A non-occurring variable is nonfree in a formula. (Contributed by BJ, 28-Jul-2023.)
⊢ Ⅎ'𝑥𝜑
Theorem	bj-nnfbd 37006*	If two formulas are equivalent, then nonfreeness of a variable in one of them is equivalent to nonfreeness in the other, deduction form. See bj-nnfbi 36982. (Contributed by BJ, 27-Aug-2023.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (Ⅎ'𝑥𝜓 ↔ Ⅎ'𝑥𝜒))
Theorem	bj-pm11.53a 37007*	A variant of pm11.53v 1946. One can similarly prove a variant with DV (𝑦, 𝜑) and ∀𝑦Ⅎ'𝑥𝜓 instead of DV (𝑥, 𝜓) and ∀𝑥Ⅎ'𝑦𝜑. (Contributed by BJ, 7-Oct-2024.)
⊢ (∀𝑥Ⅎ'𝑦𝜑 → (∀𝑥∀𝑦(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → ∀𝑦𝜓)))
Theorem	bj-equsvt 37008*	A variant of equsv 2005. (Contributed by BJ, 7-Oct-2024.)
⊢ (Ⅎ'𝑥𝜑 → (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜑))
Theorem	bj-equsalvwd 37009*	Variant of equsalvw 2006. (Contributed by BJ, 7-Oct-2024.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → Ⅎ'𝑥𝜒)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥(𝑥 = 𝑦 → 𝜓) ↔ 𝜒))
Theorem	bj-equsexvwd 37010*	Variant of equsexvw 2007. (Contributed by BJ, 7-Oct-2024.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → Ⅎ'𝑥𝜒)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥(𝑥 = 𝑦 ∧ 𝜓) ↔ 𝜒))
Theorem	bj-sbievwd 37011*	Variant of sbievw 2099. (Contributed by BJ, 7-Oct-2024.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → Ⅎ'𝑥𝜒)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ([𝑦 / 𝑥]𝜓 ↔ 𝜒))
Theorem	bj-sbft 37012	Version of sbft 2277 using Ⅎ', proved from core axioms. (Contributed by BJ, 19-Nov-2023.)
⊢ (Ⅎ'𝑥𝜑 → ([𝑡 / 𝑥]𝜑 ↔ 𝜑))
Theorem	bj-dfnnf3 37013	Alternate definition of nonfreeness when sp 2191 is available. (Contributed by BJ, 28-Jul-2023.) The proof should not rely on df-nf 1786. (Proof modification is discouraged.)
⊢ (Ⅎ'𝑥𝜑 ↔ (∃𝑥𝜑 → ∀𝑥𝜑))
Theorem	bj-nfnnfTEMP 37014	New nonfreeness is equivalent to old nonfreeness on core FOL axioms plus sp 2191. (Contributed by BJ, 28-Jul-2023.) The proof should not rely on df-nf 1786 except via df-nf 1786 directly. (Proof modification is discouraged.)
⊢ (Ⅎ'𝑥𝜑 ↔ Ⅎ𝑥𝜑)
Theorem	bj-wnfnf 37015	When 𝜑 is substituted for 𝜓, this statement expresses nonfreeness in the weak form of nonfreeness (∃ → ∀). Note that this could also be proved from bj-nnfim 36987, bj-nnfe1 37017 and bj-nnfa1 37016. (Contributed by BJ, 9-Dec-2023.)
⊢ Ⅎ'𝑥(∃𝑥𝜑 → ∀𝑥𝜓)
Theorem	bj-nnfa1 37016	See nfa1 2157. (Contributed by BJ, 12-Aug-2023.) (Proof modification is discouraged.)
⊢ Ⅎ'𝑥∀𝑥𝜑
Theorem	bj-nnfe1 37017	See nfe1 2156. (Contributed by BJ, 12-Aug-2023.) (Proof modification is discouraged.)
⊢ Ⅎ'𝑥∃𝑥𝜑
Theorem	bj-nnflemaa 37018	One of four lemmas for nonfreeness: antecedent and consequent both expressed using universal quantifier. Note: this is bj-hbalt 36920. (Contributed by BJ, 12-Aug-2023.) (Proof modification is discouraged.)
⊢ (∀𝑥(𝜑 → ∀𝑦𝜑) → (∀𝑥𝜑 → ∀𝑦∀𝑥𝜑))
Theorem	bj-nnflemee 37019	One of four lemmas for nonfreeness: antecedent and consequent both expressed using existential quantifier. (Contributed by BJ, 12-Aug-2023.) (Proof modification is discouraged.)
⊢ (∀𝑥(∃𝑦𝜑 → 𝜑) → (∃𝑦∃𝑥𝜑 → ∃𝑥𝜑))
Theorem	bj-nnflemae 37020	One of four lemmas for nonfreeness: antecedent expressed with universal quantifier and consequent expressed with existential quantifier. (Contributed by BJ, 12-Aug-2023.) (Proof modification is discouraged.)
⊢ (∀𝑥(𝜑 → ∀𝑦𝜑) → (∃𝑥𝜑 → ∀𝑦∃𝑥𝜑))
Theorem	bj-nnflemea 37021	One of four lemmas for nonfreeness: antecedent expressed with existential quantifier and consequent expressed with universal quantifier. (Contributed by BJ, 12-Aug-2023.) (Proof modification is discouraged.)
⊢ (∀𝑥(∃𝑦𝜑 → 𝜑) → (∃𝑦∀𝑥𝜑 → ∀𝑥𝜑))
Theorem	bj-nnfalt 37022	See nfal 2329 and bj-nfalt 36950. (Contributed by BJ, 12-Aug-2023.) (Proof modification is discouraged.)
⊢ (∀𝑥Ⅎ'𝑦𝜑 → Ⅎ'𝑦∀𝑥𝜑)
Theorem	bj-nnfext 37023	See nfex 2330 and bj-nfext 36951. (Contributed by BJ, 12-Aug-2023.) (Proof modification is discouraged.)
⊢ (∀𝑥Ⅎ'𝑦𝜑 → Ⅎ'𝑦∃𝑥𝜑)
Theorem	bj-pm11.53v 37024	Version of pm11.53v 1946 with nonfreeness antecedents. (Contributed by BJ, 7-Oct-2024.)
⊢ ((∀𝑥Ⅎ'𝑦𝜑 ∧ ∀𝑦Ⅎ'𝑥𝜓) → (∀𝑥∀𝑦(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → ∀𝑦𝜓)))
21.19.4.13  Adding ax-13
Theorem	bj-axc10 37025	Alternate proof of axc10 2390. Shorter. One can prove a version with DV (𝑥, 𝑦) without ax-13 2377, by using ax6ev 1971 instead of ax6e 2388. (Contributed by BJ, 31-Mar-2021.) (Proof modification is discouraged.)
⊢ (∀𝑥(𝑥 = 𝑦 → ∀𝑥𝜑) → 𝜑)
Theorem	bj-alequex 37026	A fol lemma. See alequexv 2003 for a version with a disjoint variable condition requiring fewer axioms. Can be used to reduce the proof of spimt 2391 from 133 to 112 bytes. (Contributed by BJ, 6-Oct-2018.)
⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → ∃𝑥𝜑)
Theorem	bj-spimt2 37027	A step in the proof of spimt 2391. (Contributed by BJ, 2-May-2019.)
⊢ (∀𝑥(𝑥 = 𝑦 → (𝜑 → 𝜓)) → ((∃𝑥𝜓 → 𝜓) → (∀𝑥𝜑 → 𝜓)))
Theorem	bj-cbv3ta 37028	Closed form of cbv3 2402. (Contributed by BJ, 2-May-2019.)
⊢ (∀𝑥∀𝑦(𝑥 = 𝑦 → (𝜑 → 𝜓)) → ((∀𝑦(∃𝑥𝜓 → 𝜓) ∧ ∀𝑥(𝜑 → ∀𝑦𝜑)) → (∀𝑥𝜑 → ∀𝑦𝜓)))
Theorem	bj-cbv3tb 37029	Closed form of cbv3 2402. (Contributed by BJ, 2-May-2019.)
⊢ (∀𝑥∀𝑦(𝑥 = 𝑦 → (𝜑 → 𝜓)) → ((∀𝑦Ⅎ𝑥𝜓 ∧ ∀𝑥Ⅎ𝑦𝜑) → (∀𝑥𝜑 → ∀𝑦𝜓)))
Theorem	bj-hbsb3t 37030	A theorem close to a closed form of hbsb3 2492. (Contributed by BJ, 2-May-2019.)
⊢ (∀𝑥(𝜑 → ∀𝑦𝜑) → ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑))
Theorem	bj-hbsb3 37031	Shorter proof of hbsb3 2492. (Contributed by BJ, 2-May-2019.) (Proof modification is discouraged.)
⊢ (𝜑 → ∀𝑦𝜑)    ⇒   ⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑)
Theorem	bj-nfs1t 37032	A theorem close to a closed form of nfs1 2493. (Contributed by BJ, 2-May-2019.)
⊢ (∀𝑥(𝜑 → ∀𝑦𝜑) → Ⅎ𝑥[𝑦 / 𝑥]𝜑)
Theorem	bj-nfs1t2 37033	A theorem close to a closed form of nfs1 2493. (Contributed by BJ, 2-May-2019.)
⊢ (∀𝑥Ⅎ𝑦𝜑 → Ⅎ𝑥[𝑦 / 𝑥]𝜑)
Theorem	bj-nfs1 37034	Shorter proof of nfs1 2493 (three essential steps instead of four). (Contributed by BJ, 2-May-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ Ⅎ𝑥[𝑦 / 𝑥]𝜑
21.19.4.14  Removing dependencies on ax-13 (and ax-11) It is known that ax-13 2377 is logically redundant (see ax13w 2142 and the head comment of the section "Logical redundancy of ax-10--13"). More precisely, one can remove dependency on ax-13 2377 from every theorem in set.mm which is totally unbundled (i.e., has disjoint variable conditions on all setvar variables). Indeed, start with the existing proof, and replace any occurrence of ax-13 2377 with ax13w 2142. This section is an experiment to see in practice if (partially) unbundled versions of existing theorems can be proved more efficiently without ax-13 2377 (and using ax6v 1970 / ax6ev 1971 instead of ax-6 1969 / ax6e 2388, as is currently done). One reason to be optimistic is that the first few utility theorems using ax-13 2377 (roughly 200 of them) are then used mainly with dummy variables, which one can assume distinct from any other, so that the unbundled versions of the utility theorems suffice. In this section, we prove versions of theorems in the main part with dv conditions and not requiring ax-13 2377, labeled bj-xxxv (we follow the proof of xxx but use ax6v 1970 and ax6ev 1971 instead of ax-6 1969 and ax6e 2388, and ax-5 1912 instead of ax13v 2378; shorter proofs may be possible). When no additional dv condition is required, we label it bj-xxx. It is important to keep all the bundled theorems already in set.mm, but one may also add the (partially) unbundled versions which dispense with ax-13 2377, so as to remove dependencies on ax-13 2377 from many existing theorems. UPDATE: it turns out that several theorems of the form bj-xxxv, or minor variations, are already in set.mm with label xxxw. It is also possible to remove dependencies on ax-11 2163, typically by replacing a nonfree hypothesis with a disjoint variable condition (see cbv3v2 2249 and following theorems).
Theorem	bj-axc10v 37035*	Version of axc10 2390 with a disjoint variable condition, which does not require ax-13 2377. (Contributed by BJ, 14-Jun-2019.) (Proof modification is discouraged.)
⊢ (∀𝑥(𝑥 = 𝑦 → ∀𝑥𝜑) → 𝜑)
Theorem	bj-spimtv 37036*	Version of spimt 2391 with a disjoint variable condition, which does not require ax-13 2377. (Contributed by BJ, 14-Jun-2019.) (Proof modification is discouraged.)
⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝑦 → (𝜑 → 𝜓))) → (∀𝑥𝜑 → 𝜓))
Theorem	bj-cbv3hv2 37037*	Version of cbv3h 2409 with two disjoint variable conditions, which does not require ax-11 2163 nor ax-13 2377. (Contributed by BJ, 24-Jun-2019.) (Proof modification is discouraged.)
⊢ (𝜓 → ∀𝑥𝜓)    &   ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))    ⇒   ⊢ (∀𝑥𝜑 → ∀𝑦𝜓)
Theorem	bj-cbv1hv 37038*	Version of cbv1h 2410 with a disjoint variable condition, which does not require ax-13 2377. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ (𝜑 → (𝜓 → ∀𝑦𝜓))    &   ⊢ (𝜑 → (𝜒 → ∀𝑥𝜒))    &   ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 → 𝜒)))    ⇒   ⊢ (∀𝑥∀𝑦𝜑 → (∀𝑥𝜓 → ∀𝑦𝜒))
Theorem	bj-cbv2hv 37039*	Version of cbv2h 2411 with a disjoint variable condition, which does not require ax-13 2377. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ (𝜑 → (𝜓 → ∀𝑦𝜓))    &   ⊢ (𝜑 → (𝜒 → ∀𝑥𝜒))    &   ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (∀𝑥∀𝑦𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒))
Theorem	bj-cbv2v 37040*	Version of cbv2 2408 with a disjoint variable condition, which does not require ax-13 2377. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑦𝜓)    &   ⊢ (𝜑 → Ⅎ𝑥𝜒)    &   ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒))
Theorem	bj-cbvaldv 37041*	Version of cbvald 2412 with a disjoint variable condition, which does not require ax-13 2377. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑦𝜓)    &   ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒))
Theorem	bj-cbvexdv 37042*	Version of cbvexd 2413 with a disjoint variable condition, which does not require ax-13 2377. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑦𝜓)    &   ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑦𝜒))
Theorem	bj-cbval2vv 37043*	Version of cbval2vv 2418 with a disjoint variable condition, which does not require ax-13 2377. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑧∀𝑤𝜓)
Theorem	bj-cbvex2vv 37044*	Version of cbvex2vv 2419 with a disjoint variable condition, which does not require ax-13 2377. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑧∃𝑤𝜓)
Theorem	bj-cbvaldvav 37045*	Version of cbvaldva 2414 with a disjoint variable condition, which does not require ax-13 2377. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒))
Theorem	bj-cbvexdvav 37046*	Version of cbvexdva 2415 with a disjoint variable condition, which does not require ax-13 2377. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑦𝜒))
Theorem	bj-cbvex4vv 37047*	Version of cbvex4v 2420 with a disjoint variable condition, which does not require ax-13 2377. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ ((𝑥 = 𝑣 ∧ 𝑦 = 𝑢) → (𝜑 ↔ 𝜓))    &   ⊢ ((𝑧 = 𝑓 ∧ 𝑤 = 𝑔) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (∃𝑥∃𝑦∃𝑧∃𝑤𝜑 ↔ ∃𝑣∃𝑢∃𝑓∃𝑔𝜒)
Theorem	bj-equsalhv 37048*	Version of equsalh 2425 with a disjoint variable condition, which does not require ax-13 2377. Remark: this is the same as equsalhw 2298. TODO: delete after moving the following paragraph somewhere. Remarks: equsexvw 2007 has been moved to Main; Theorem ax13lem2 2381 has a DV version which is a simple consequence of ax5e 1914; Theorems nfeqf2 2382, dveeq2 2383, nfeqf1 2384, dveeq1 2385, nfeqf 2386, axc9 2387, ax13 2380, have dv versions which are simple consequences of ax-5 1912. (Contributed by BJ, 14-Jun-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜓 → ∀𝑥𝜓)    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜓)
Theorem	bj-axc11nv 37049*	Version of axc11n 2431 with a disjoint variable condition; instance of aevlem 2059. TODO: delete after checking surrounding theorems. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥)
Theorem	bj-aecomsv 37050*	Version of aecoms 2433 with a disjoint variable condition, provable from Tarski's FOL. The corresponding version of naecoms 2434 should not be very useful since ¬ ∀𝑥𝑥 = 𝑦, DV (𝑥, 𝑦) is true when the universe has at least two objects (see dtru 5393). (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → 𝜑)    ⇒   ⊢ (∀𝑦 𝑦 = 𝑥 → 𝜑)
Theorem	bj-axc11v 37051*	Version of axc11 2435 with a disjoint variable condition, which does not require ax-13 2377 nor ax-10 2147. Remark: the following theorems (hbae 2436, nfae 2438, hbnae 2437, nfnae 2439, hbnaes 2440) would need to be totally unbundled to be proved without ax-13 2377, hence would be simple consequences of ax-5 1912 or nfv 1916. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 → ∀𝑦𝜑))
Theorem	bj-drnf2v 37052*	Version of drnf2 2449 with a disjoint variable condition, which does not require ax-10 2147, ax-11 2163, ax-12 2185, ax-13 2377. Instance of nfbidv 1924. Note that the version of axc15 2427 with a disjoint variable condition is actually ax12v2 2187 (up to adding a superfluous antecedent). (Contributed by BJ, 17-Jun-2019.) (Proof modification is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 𝑥 = 𝑦 → (Ⅎ𝑧𝜑 ↔ Ⅎ𝑧𝜓))
Theorem	bj-equs45fv 37053*	Version of equs45f 2464 with a disjoint variable condition, which does not require ax-13 2377. Note that the version of equs5 2465 with a disjoint variable condition is actually sbalex 2250 (up to adding a superfluous antecedent). (Contributed by BJ, 11-Sep-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑))
Theorem	bj-hbs1 37054*	Version of hbsb2 2487 with a disjoint variable condition, which does not require ax-13 2377, and removal of ax-13 2377 from hbs1 2281. (Contributed by BJ, 23-Jun-2019.) (Proof modification is discouraged.)
⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑)
Theorem	bj-nfs1v 37055*	Version of nfsb2 2488 with a disjoint variable condition, which does not require ax-13 2377, and removal of ax-13 2377 from nfs1v 2162. (Contributed by BJ, 24-Jun-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥[𝑦 / 𝑥]𝜑
Theorem	bj-hbsb2av 37056*	Version of hbsb2a 2489 with a disjoint variable condition, which does not require ax-13 2377. (Contributed by BJ, 11-Sep-2019.) (Proof modification is discouraged.)
⊢ ([𝑦 / 𝑥]∀𝑦𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑)
Theorem	bj-hbsb3v 37057*	Version of hbsb3 2492 with a disjoint variable condition, which does not require ax-13 2377. (Remark: the unbundled version of nfs1 2493 is given by bj-nfs1v 37055.) (Contributed by BJ, 11-Sep-2019.) (Proof modification is discouraged.)
⊢ (𝜑 → ∀𝑦𝜑)    ⇒   ⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑)
Theorem	bj-nfsab1 37058*	Remove dependency on ax-13 2377 from nfsab1 2723. UPDATE / TODO: nfsab1 2723 does not use ax-13 2377 either anymore; bj-nfsab1 37058 is shorter than nfsab1 2723 but uses ax-12 2185. (Contributed by BJ, 23-Jun-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥 𝑦 ∈ {𝑥 ∣ 𝜑}
Theorem	bj-dtrucor2v 37059*	Version of dtrucor2 5319 with a disjoint variable condition, which does not require ax-13 2377 (nor ax-4 1811, ax-5 1912, ax-7 2010, ax-12 2185). (Contributed by BJ, 16-Jul-2019.) (Proof modification is discouraged.)
⊢ (𝑥 = 𝑦 → 𝑥 ≠ 𝑦)    ⇒   ⊢ (𝜑 ∧ ¬ 𝜑)
21.19.4.15  Distinct var metavariables The closed formula ∀𝑥∀𝑦𝑥 = 𝑦 approximately means that the var metavariables 𝑥 and 𝑦 represent the same variable vi. In a domain with at most one object, however, this formula is always true, hence the "approximately" in the previous sentence.
Theorem	bj-hbaeb2 37060	Biconditional version of a form of hbae 2436 with commuted quantifiers, not requiring ax-11 2163. (Contributed by BJ, 12-Dec-2019.) (Proof modification is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 ↔ ∀𝑥∀𝑧 𝑥 = 𝑦)
Theorem	bj-hbaeb 37061	Biconditional version of hbae 2436. (Contributed by BJ, 6-Oct-2018.) (Proof modification is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 ↔ ∀𝑧∀𝑥 𝑥 = 𝑦)
Theorem	bj-hbnaeb 37062	Biconditional version of hbnae 2437 (to replace it?). (Contributed by BJ, 6-Oct-2018.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 ↔ ∀𝑧 ¬ ∀𝑥 𝑥 = 𝑦)
Theorem	bj-dvv 37063	A special instance of bj-hbaeb2 37060. A lemma for distinct var metavariables. Note that the right-hand side is a closed formula (a sentence). (Contributed by BJ, 6-Oct-2018.)
⊢ (∀𝑥 𝑥 = 𝑦 ↔ ∀𝑥∀𝑦 𝑥 = 𝑦)
21.19.4.16  Around ~ equsal As a rule of thumb, if a theorem of the form ⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (𝜒 ↔ 𝜃) is in the database, and the "more precise" theorems ⊢ (𝜑 → 𝜓) ⇒ ⊢ (𝜒 → 𝜃) and ⊢ (𝜓 → 𝜑) ⇒ ⊢ (𝜃 → 𝜒) also hold (see bj-bisym 36811), then they should be added to the database. The present case is similar. Similar additions can be done regarding equsex 2423 (and equsalh 2425 and equsexh 2426). Even if only one of these two theorems holds, it should be added to the database.
Theorem	bj-equsal1t 37064	Duplication of wl-equsal1t 37791, with shorter proof. If one imposes a disjoint variable condition on x,y , then one can use alequexv 2003 and reduce axiom dependencies, and similarly for the following theorems. Note: wl-equsalcom 37792 is also interesting. (Contributed by BJ, 6-Oct-2018.)
⊢ (Ⅎ𝑥𝜑 → (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜑))
Theorem	bj-equsal1ti 37065	Inference associated with bj-equsal1t 37064. (Contributed by BJ, 30-Sep-2018.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜑)
Theorem	bj-equsal1 37066	One direction of equsal 2422. (Contributed by BJ, 30-Sep-2018.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))    ⇒   ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → 𝜓)
Theorem	bj-equsal2 37067	One direction of equsal 2422. (Contributed by BJ, 30-Sep-2018.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))    ⇒   ⊢ (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜓))
Theorem	bj-equsal 37068	Shorter proof of equsal 2422. (Contributed by BJ, 30-Sep-2018.) Proof modification is discouraged to avoid using equsal 2422, but "min */exc equsal" is ok. (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜓)
21.19.4.17  Some Principia Mathematica proofs References are made to the second edition (1927, reprinted 1963) of Principia Mathematica, Vol. 1. Theorems are referred to in the form "PM*xx.xx".
Theorem	stdpc5t 37069	Closed form of stdpc5 2216. (Possible to place it before 19.21t 2214 and use it to prove 19.21t 2214). (Contributed by BJ, 15-Sep-2018.) (Proof modification is discouraged.)
⊢ (Ⅎ𝑥𝜑 → (∀𝑥(𝜑 → 𝜓) → (𝜑 → ∀𝑥𝜓)))
Theorem	bj-stdpc5 37070	More direct proof of stdpc5 2216. (Contributed by BJ, 15-Sep-2018.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∀𝑥(𝜑 → 𝜓) → (𝜑 → ∀𝑥𝜓))
Theorem	2stdpc5 37071	A double stdpc5 2216 (one direction of PM*11.3). See also 2stdpc4 2076 and 19.21vv 44726. (Contributed by BJ, 15-Sep-2018.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (∀𝑥∀𝑦(𝜑 → 𝜓) → (𝜑 → ∀𝑥∀𝑦𝜓))
Theorem	bj-19.21t0 37072	Proof of 19.21t 2214 from stdpc5t 37069. (Contributed by BJ, 15-Sep-2018.) (Proof modification is discouraged.)
⊢ (Ⅎ𝑥𝜑 → (∀𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥𝜓)))
Theorem	exlimii 37073	Inference associated with exlimi 2225. Inferring a theorem when it is implied by an antecedent which may be true. (Contributed by BJ, 15-Sep-2018.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝜑 → 𝜓)    &   ⊢ ∃𝑥𝜑    ⇒   ⊢ 𝜓
Theorem	ax11-pm 37074	Proof of ax-11 2163 similar to PM's proof of alcom 2165 (PM*11.2). For a proof closer to PM's proof, see ax11-pm2 37078. Axiom ax-11 2163 is used in the proof only through nfa2 2182. (Contributed by BJ, 15-Sep-2018.) (Proof modification is discouraged.)
⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑)
Theorem	ax6er 37075	Commuted form of ax6e 2388. (Could be placed right after ax6e 2388). (Contributed by BJ, 15-Sep-2018.)
⊢ ∃𝑥 𝑦 = 𝑥
Theorem	exlimiieq1 37076	Inferring a theorem when it is implied by an equality which may be true. (Contributed by BJ, 30-Sep-2018.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝑥 = 𝑦 → 𝜑)    ⇒   ⊢ 𝜑
Theorem	exlimiieq2 37077	Inferring a theorem when it is implied by an equality which may be true. (Contributed by BJ, 15-Sep-2018.) (Revised by BJ, 30-Sep-2018.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝑥 = 𝑦 → 𝜑)    ⇒   ⊢ 𝜑
Theorem	ax11-pm2 37078*	Proof of ax-11 2163 from the standard axioms of predicate calculus, similar to PM's proof of alcom 2165 (PM*11.2). This proof requires that 𝑥 and 𝑦 be distinct. Axiom ax-11 2163 is used in the proof only through nfal 2329, nfsb 2528, sbal 2175, sb8 2522. See also ax11-pm 37074. (Contributed by BJ, 15-Sep-2018.) (Proof modification is discouraged.)
⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑)
21.19.4.18  Alternate definition of substitution
Theorem	bj-sbsb 37079	Biconditional showing two possible (dual) definitions of substitution df-sb 2069 not using dummy variables. (Contributed by BJ, 19-Mar-2021.)
⊢ (((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) ↔ (∀𝑥(𝑥 = 𝑦 → 𝜑) ∨ (𝑥 = 𝑦 ∧ 𝜑)))
Theorem	bj-dfsb2 37080	Alternate (dual) definition of substitution df-sb 2069 not using dummy variables. (Contributed by BJ, 19-Mar-2021.)
⊢ ([𝑦 / 𝑥]𝜑 ↔ (∀𝑥(𝑥 = 𝑦 → 𝜑) ∨ (𝑥 = 𝑦 ∧ 𝜑)))
21.19.4.19  Lemmas for substitution
Theorem	bj-sbf3 37081	Substitution has no effect on a bound variable (existential quantifier case); see sbf2 2279. (Contributed by BJ, 2-May-2019.)
⊢ ([𝑦 / 𝑥]∃𝑥𝜑 ↔ ∃𝑥𝜑)
Theorem	bj-sbf4 37082	Substitution has no effect on a bound variable (nonfreeness case); see sbf2 2279. (Contributed by BJ, 2-May-2019.)
⊢ ([𝑦 / 𝑥]Ⅎ𝑥𝜑 ↔ Ⅎ𝑥𝜑)
21.19.4.20  Existential uniqueness
Theorem	bj-eu3f 37083*	Version of eu3v 2571 where the disjoint variable condition is replaced with a nonfreeness hypothesis. This is a "backup" of a theorem that used to be in the main part with label "eu3" and was deprecated in favor of eu3v 2571. (Contributed by NM, 8-Jul-1994.) (Proof shortened by BJ, 31-May-2019.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦)))
21.19.4.21  First-order logic: miscellaneous Miscellaneous theorems of first-order logic.
Theorem	bj-sblem1 37084*	Lemma for substitution. (Contributed by BJ, 23-Jul-2023.)
⊢ (∀𝑥(𝜑 → (𝜓 → 𝜒)) → (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → 𝜒)))
Theorem	bj-sblem2 37085*	Lemma for substitution. (Contributed by BJ, 23-Jul-2023.)
⊢ (∀𝑥(𝜑 → (𝜒 → 𝜓)) → ((∃𝑥𝜑 → 𝜒) → ∀𝑥(𝜑 → 𝜓)))
Theorem	bj-sblem 37086*	Lemma for substitution. (Contributed by BJ, 23-Jul-2023.)
⊢ (∀𝑥(𝜑 → (𝜓 ↔ 𝜒)) → (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜒)))
Theorem	bj-sbievw1 37087*	Lemma for substitution. (Contributed by BJ, 23-Jul-2023.)
⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) → ([𝑦 / 𝑥]𝜑 → 𝜓))
Theorem	bj-sbievw2 37088*	Lemma for substitution. (Contributed by BJ, 23-Jul-2023.)
⊢ ([𝑦 / 𝑥](𝜓 → 𝜑) → (𝜓 → [𝑦 / 𝑥]𝜑))
Theorem	bj-sbievw 37089*	Lemma for substitution. Closed form of equsalvw 2006 and sbievw 2099. (Contributed by BJ, 23-Jul-2023.)
⊢ ([𝑦 / 𝑥](𝜑 ↔ 𝜓) → ([𝑦 / 𝑥]𝜑 ↔ 𝜓))
Theorem	bj-sbievv 37090	Version of sbie 2507 with a second nonfreeness hypothesis and shorter proof. (Contributed by BJ, 18-Jul-2023.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓)
Theorem	bj-moeub 37091	Uniqueness is equivalent to existence being equivalent to unique existence. (Contributed by BJ, 14-Oct-2022.)
⊢ (∃*𝑥𝜑 ↔ (∃𝑥𝜑 ↔ ∃!𝑥𝜑))
Theorem	bj-sbidmOLD 37092	Obsolete proof of sbidm 2515 temporarily kept here to check it gives no additional insight. (Contributed by NM, 8-Mar-1995.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ([𝑦 / 𝑥][𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)
Theorem	bj-dvelimdv 37093*	Deduction form of dvelim 2456 with disjoint variable conditions. Uncurried (imported) form of bj-dvelimdv1 37094. Typically, 𝑧 is a fresh variable used for the implicit substitution hypothesis that results in 𝜒 (namely, 𝜓 can be thought as 𝜓(𝑥, 𝑦) and 𝜒 as 𝜓(𝑥, 𝑧)). So the theorem says that if x is effectively free in 𝜓(𝑥, 𝑧), then if x and y are not the same variable, then 𝑥 is also effectively free in 𝜓(𝑥, 𝑦), in a context 𝜑. One can weaken the implicit substitution hypothesis by adding the antecedent 𝜑 but this typically does not make the theorem much more useful. Similarly, one could use nonfreeness hypotheses instead of disjoint variable conditions but since this result is typically used when 𝑧 is a dummy variable, this would not be of much benefit. One could also remove DV (𝑥, 𝑧) since in the proof nfv 1916 can be replaced with nfal 2329 followed by nfn 1859. Remark: nfald 2334 uses ax-11 2163; it might be possible to inline and use ax11w 2136 instead, but there is still a use via 19.12 2333 anyway. (Contributed by BJ, 20-Oct-2021.) (Proof modification is discouraged.)
⊢ (𝜑 → Ⅎ𝑥𝜒)    &   ⊢ (𝑧 = 𝑦 → (𝜒 ↔ 𝜓))    ⇒   ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥𝜓)
Theorem	bj-dvelimdv1 37094*	Curried (exported) form of bj-dvelimdv 37093 (of course, one is directly provable from the other, but we keep this proof for illustration purposes). (Contributed by BJ, 20-Oct-2021.) (Proof modification is discouraged.)
⊢ (𝜑 → Ⅎ𝑥𝜒)    &   ⊢ (𝑧 = 𝑦 → (𝜒 ↔ 𝜓))    ⇒   ⊢ (𝜑 → (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝜓))
Theorem	bj-dvelimv 37095*	A version of dvelim 2456 using the "nonfree" idiom. (Contributed by BJ, 20-Oct-2021.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑧 = 𝑦 → (𝜓 ↔ 𝜑))    ⇒   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝜑)
Theorem	bj-nfeel2 37096*	Nonfreeness in a membership statement. (Contributed by BJ, 20-Oct-2021.) (Proof modification is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥 𝑦 ∈ 𝑧)
Theorem	bj-axc14nf 37097	Proof of a version of axc14 2468 using the "nonfree" idiom. (Contributed by BJ, 20-Oct-2021.) (Proof modification is discouraged.)
⊢ (¬ ∀𝑧 𝑧 = 𝑥 → (¬ ∀𝑧 𝑧 = 𝑦 → Ⅎ𝑧 𝑥 ∈ 𝑦))
Theorem	bj-axc14 37098	Alternate proof of axc14 2468 (even when inlining the above results, this gives a shorter proof). (Contributed by BJ, 20-Oct-2021.) (Proof modification is discouraged.)
⊢ (¬ ∀𝑧 𝑧 = 𝑥 → (¬ ∀𝑧 𝑧 = 𝑦 → (𝑥 ∈ 𝑦 → ∀𝑧 𝑥 ∈ 𝑦)))
Theorem	mobidvALT 37099*	Alternate proof of mobidv 2550 directly from its analogues albidv 1922 and exbidv 1923, using deduction style. Note the proof structure, similar to mobi 2548. (Contributed by Mario Carneiro, 7-Oct-2016.) Reduce axiom dependencies and shorten proof. Remove dependency on ax-12 2185 by adapting proof of mobid 2551. (Revised by BJ, 26-Sep-2022.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃*𝑥𝜓 ↔ ∃*𝑥𝜒))
Theorem	sbn1ALT 37100	Alternate proof of sbn1 2113, not using the false constant. (Contributed by BJ, 18-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ([𝑡 / 𝑥] ¬ 𝜑 → ¬ [𝑡 / 𝑥]𝜑)