P. 343 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 34201-34300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	bj-dfnnf3 34201	Alternate definition of nonfreeness when sp 2180 is available. (Contributed by BJ, 28-Jul-2023.) The proof should not rely on df-nf 1786. (Proof modification is discouraged.)
⊢ (Ⅎ'𝑥𝜑 ↔ (∃𝑥𝜑 → ∀𝑥𝜑))
Theorem	bj-nfnnfTEMP 34202	New nonfreeness is equivalent to old nonfreeness on core FOL axioms plus sp 2180. (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-nnfa1 34203	See nfa1 2152. (Contributed by BJ, 12-Aug-2023.) (Proof modification is discouraged.)
⊢ Ⅎ'𝑥∀𝑥𝜑
Theorem	bj-nnfe1 34204	See nfe1 2151. (Contributed by BJ, 12-Aug-2023.) (Proof modification is discouraged.)
⊢ Ⅎ'𝑥∃𝑥𝜑
Theorem	bj-19.12 34205	See 19.12 2335. Could be labeled "exalimalex" for "'there exists for all' implies 'for all there exists'". This proof is from excom 2166 and modal (B) on top of modalK logic. (Contributed by BJ, 12-Aug-2023.) The proof should not rely on df-nf 1786 or df-bj-nnf 34171, directly or indirectly. (Proof modification is discouraged.)
⊢ (∃𝑥∀𝑦𝜑 → ∀𝑦∃𝑥𝜑)
Theorem	bj-nnflemaa 34206	One of four lemmas for nonfreeness: antecedent and consequent both expressed using universal quantifier. Note: this is bj-hbalt 34128. (Contributed by BJ, 12-Aug-2023.) (Proof modification is discouraged.)
⊢ (∀𝑥(𝜑 → ∀𝑦𝜑) → (∀𝑥𝜑 → ∀𝑦∀𝑥𝜑))
Theorem	bj-nnflemee 34207	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 34208	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 34209	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 34210	See nfal 2331 and bj-nfalt 34158. (Contributed by BJ, 12-Aug-2023.) (Proof modification is discouraged.)
⊢ (∀𝑥Ⅎ'𝑦𝜑 → Ⅎ'𝑦∀𝑥𝜑)
Theorem	bj-nnfext 34211	See nfex 2332 and bj-nfext 34159. (Contributed by BJ, 12-Aug-2023.) (Proof modification is discouraged.)
⊢ (∀𝑥Ⅎ'𝑦𝜑 → Ⅎ'𝑦∃𝑥𝜑)
Theorem	bj-stdpc5t 34212	Alias of bj-nnf-alrim 34199 for labeling consistency (a standard predicate calculus axiom). Closed form of stdpc5 2206 proved from modalK (obsoleting stdpc5v 1939). (Contributed by BJ, 2-Dec-2023.) Use bj-nnf-alrim 34199 instead. (New usaged is discouraged.)
⊢ (Ⅎ'𝑥𝜑 → (∀𝑥(𝜑 → 𝜓) → (𝜑 → ∀𝑥𝜓)))
Theorem	bj-19.21t 34213	Statement 19.21t 2204 proved from modalK (obsoleting 19.21v 1940). (Contributed by BJ, 2-Dec-2023.)
⊢ (Ⅎ'𝑥𝜑 → (∀𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥𝜓)))
Theorem	bj-19.23t 34214	Statement 19.23t 2208 proved from modalK (obsoleting 19.23v 1943). (Contributed by BJ, 2-Dec-2023.)
⊢ (Ⅎ'𝑥𝜓 → (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜓)))
Theorem	bj-19.36im 34215	One direction of 19.36 2230 from the same axioms as 19.36imv 1946. (Contributed by BJ, 2-Dec-2023.)
⊢ (Ⅎ'𝑥𝜓 → (∃𝑥(𝜑 → 𝜓) → (∀𝑥𝜑 → 𝜓)))
Theorem	bj-19.37im 34216	One direction of 19.37 2232 from the same axioms as 19.37imv 1948. (Contributed by BJ, 2-Dec-2023.)
⊢ (Ⅎ'𝑥𝜑 → (∃𝑥(𝜑 → 𝜓) → (𝜑 → ∃𝑥𝜓)))
Theorem	bj-19.42t 34217	Closed form of 19.42 2236 from the same axioms as 19.42v 1954. (Contributed by BJ, 2-Dec-2023.)
⊢ (Ⅎ'𝑥𝜑 → (∃𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥𝜓)))
Theorem	bj-19.41t 34218	Closed form of 19.41 2235 from the same axioms as 19.41v 1950. The same is doable with 19.27 2227, 19.28 2228, 19.31 2234, 19.32 2233, 19.44 2237, 19.45 2238. (Contributed by BJ, 2-Dec-2023.)
⊢ (Ⅎ'𝑥𝜓 → (∃𝑥(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ 𝜓)))
Theorem	bj-sbft 34219	Version of sbft 2267 using Ⅎ', proved from core axioms. (Contributed by BJ, 19-Nov-2023.)
⊢ (Ⅎ'𝑥𝜑 → ([𝑡 / 𝑥]𝜑 ↔ 𝜑))
20.15.4.11  Adding ax-13
Theorem	bj-axc10 34220	Alternate (shorter) proof of axc10 2392. One can prove a version with DV (𝑥, 𝑦) without ax-13 2379, by using ax6ev 1972 instead of ax6e 2390. (Contributed by BJ, 31-Mar-2021.) (Proof modification is discouraged.)
⊢ (∀𝑥(𝑥 = 𝑦 → ∀𝑥𝜑) → 𝜑)
Theorem	bj-alequex 34221	A fol lemma. See alequexv 2007 for a version with a disjoint variable condition requiring fewer axioms. Can be used to reduce the proof of spimt 2393 from 133 to 112 bytes. (Contributed by BJ, 6-Oct-2018.)
⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → ∃𝑥𝜑)
Theorem	bj-spimt2 34222	A step in the proof of spimt 2393. (Contributed by BJ, 2-May-2019.)
⊢ (∀𝑥(𝑥 = 𝑦 → (𝜑 → 𝜓)) → ((∃𝑥𝜓 → 𝜓) → (∀𝑥𝜑 → 𝜓)))
Theorem	bj-cbv3ta 34223	Closed form of cbv3 2404. (Contributed by BJ, 2-May-2019.)
⊢ (∀𝑥∀𝑦(𝑥 = 𝑦 → (𝜑 → 𝜓)) → ((∀𝑦(∃𝑥𝜓 → 𝜓) ∧ ∀𝑥(𝜑 → ∀𝑦𝜑)) → (∀𝑥𝜑 → ∀𝑦𝜓)))
Theorem	bj-cbv3tb 34224	Closed form of cbv3 2404. (Contributed by BJ, 2-May-2019.)
⊢ (∀𝑥∀𝑦(𝑥 = 𝑦 → (𝜑 → 𝜓)) → ((∀𝑦Ⅎ𝑥𝜓 ∧ ∀𝑥Ⅎ𝑦𝜑) → (∀𝑥𝜑 → ∀𝑦𝜓)))
Theorem	bj-hbsb3t 34225	A theorem close to a closed form of hbsb3 2505. (Contributed by BJ, 2-May-2019.)
⊢ (∀𝑥(𝜑 → ∀𝑦𝜑) → ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑))
Theorem	bj-hbsb3 34226	Shorter proof of hbsb3 2505. (Contributed by BJ, 2-May-2019.) (Proof modification is discouraged.)
⊢ (𝜑 → ∀𝑦𝜑)    ⇒   ⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑)
Theorem	bj-nfs1t 34227	A theorem close to a closed form of nfs1 2506. (Contributed by BJ, 2-May-2019.)
⊢ (∀𝑥(𝜑 → ∀𝑦𝜑) → Ⅎ𝑥[𝑦 / 𝑥]𝜑)
Theorem	bj-nfs1t2 34228	A theorem close to a closed form of nfs1 2506. (Contributed by BJ, 2-May-2019.)
⊢ (∀𝑥Ⅎ𝑦𝜑 → Ⅎ𝑥[𝑦 / 𝑥]𝜑)
Theorem	bj-nfs1 34229	Shorter proof of nfs1 2506 (three essential steps instead of four). (Contributed by BJ, 2-May-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ Ⅎ𝑥[𝑦 / 𝑥]𝜑
20.15.4.12  Removing dependencies on ax-13 (and ax-11) It is known that ax-13 2379 is logically redundant (see ax13w 2137 and the head comment of the section "Logical redundancy of ax-10--13"). More precisely, one can remove dependency on ax-13 2379 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 2379 with ax13w 2137. This section is an experiment to see in practice if (partially) unbundled versions of existing theorems can be proved more efficiently without ax-13 2379 (and using ax6v 1971 / ax6ev 1972 instead of ax-6 1970 / ax6e 2390, as is currently done). One reason to be optimistic is that the first few utility theorems using ax-13 2379 (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 2379, labeled bj-xxxv (we follow the proof of xxx but use ax6v 1971 and ax6ev 1972 instead of ax-6 1970 and ax6e 2390, and ax-5 1911 instead of ax13v 2380; 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 dipense with ax-13 2379, so as to remove dependencies on ax-13 2379 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 2158, typically by replacing a nonfree hypothesis with a disjoint variable condition (see cbv3v2 2241 and following theorems).
Theorem	bj-axc10v 34230*	Version of axc10 2392 with a disjoint variable condition, which does not require ax-13 2379. (Contributed by BJ, 14-Jun-2019.) (Proof modification is discouraged.)
⊢ (∀𝑥(𝑥 = 𝑦 → ∀𝑥𝜑) → 𝜑)
Theorem	bj-spimtv 34231*	Version of spimt 2393 with a disjoint variable condition, which does not require ax-13 2379. (Contributed by BJ, 14-Jun-2019.) (Proof modification is discouraged.)
⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝑦 → (𝜑 → 𝜓))) → (∀𝑥𝜑 → 𝜓))
Theorem	bj-cbv3hv2 34232*	Version of cbv3h 2413 with two disjoint variable conditions, which does not require ax-11 2158 nor ax-13 2379. (Contributed by BJ, 24-Jun-2019.) (Proof modification is discouraged.)
⊢ (𝜓 → ∀𝑥𝜓)    &   ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))    ⇒   ⊢ (∀𝑥𝜑 → ∀𝑦𝜓)
Theorem	bj-cbv1hv 34233*	Version of cbv1h 2414 with a disjoint variable condition, which does not require ax-13 2379. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ (𝜑 → (𝜓 → ∀𝑦𝜓))    &   ⊢ (𝜑 → (𝜒 → ∀𝑥𝜒))    &   ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 → 𝜒)))    ⇒   ⊢ (∀𝑥∀𝑦𝜑 → (∀𝑥𝜓 → ∀𝑦𝜒))
Theorem	bj-cbv2hv 34234*	Version of cbv2h 2415 with a disjoint variable condition, which does not require ax-13 2379. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ (𝜑 → (𝜓 → ∀𝑦𝜓))    &   ⊢ (𝜑 → (𝜒 → ∀𝑥𝜒))    &   ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (∀𝑥∀𝑦𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒))
Theorem	bj-cbv2v 34235*	Version of cbv2 2412 with a disjoint variable condition, which does not require ax-13 2379. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑦𝜓)    &   ⊢ (𝜑 → Ⅎ𝑥𝜒)    &   ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒))
Theorem	bj-cbvaldv 34236*	Version of cbvald 2417 with a disjoint variable condition, which does not require ax-13 2379. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑦𝜓)    &   ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒))
Theorem	bj-cbvexdv 34237*	Version of cbvexd 2418 with a disjoint variable condition, which does not require ax-13 2379. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑦𝜓)    &   ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑦𝜒))
Theorem	bj-cbval2vv 34238*	Version of cbval2vv 2424 with a disjoint variable condition, which does not require ax-13 2379. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑧∀𝑤𝜓)
Theorem	bj-cbvex2vv 34239*	Version of cbvex2vv 2425 with a disjoint variable condition, which does not require ax-13 2379. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑧∃𝑤𝜓)
Theorem	bj-cbvaldvav 34240*	Version of cbvaldva 2419 with a disjoint variable condition, which does not require ax-13 2379. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒))
Theorem	bj-cbvexdvav 34241*	Version of cbvexdva 2420 with a disjoint variable condition, which does not require ax-13 2379. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑦𝜒))
Theorem	bj-cbvex4vv 34242*	Version of cbvex4v 2426 with a disjoint variable condition, which does not require ax-13 2379. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ ((𝑥 = 𝑣 ∧ 𝑦 = 𝑢) → (𝜑 ↔ 𝜓))    &   ⊢ ((𝑧 = 𝑓 ∧ 𝑤 = 𝑔) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (∃𝑥∃𝑦∃𝑧∃𝑤𝜑 ↔ ∃𝑣∃𝑢∃𝑓∃𝑔𝜒)
Theorem	bj-equsalhv 34243*	Version of equsalh 2431 with a disjoint variable condition, which does not require ax-13 2379. Remark: this is the same as equsalhw 2295. TODO: delete after moving the following paragraph somewhere. Remarks: equsexvw 2011 has been moved to Main; the theorem ax13lem2 2383 has a dv version which is a simple consequence of ax5e 1913; the theorems nfeqf2 2384, dveeq2 2385, nfeqf1 2386, dveeq1 2387, nfeqf 2388, axc9 2389, ax13 2382, have dv versions which are simple consequences of ax-5 1911. (Contributed by BJ, 14-Jun-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜓 → ∀𝑥𝜓)    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜓)
Theorem	bj-axc11nv 34244*	Version of axc11n 2437 with a disjoint variable condition; instance of aevlem 2060. TODO: delete after checking surrounding theorems. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥)
Theorem	bj-aecomsv 34245*	Version of aecoms 2439 with a disjoint variable condition, provable from Tarski's FOL. The corresponding version of naecoms 2440 should not be very useful since ¬ ∀𝑥𝑥 = 𝑦, DV (𝑥, 𝑦) is true when the universe has at least two objects (see dtru 5236). (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → 𝜑)    ⇒   ⊢ (∀𝑦 𝑦 = 𝑥 → 𝜑)
Theorem	bj-axc11v 34246*	Version of axc11 2441 with a disjoint variable condition, which does not require ax-13 2379 nor ax-10 2142. Remark: the following theorems (hbae 2442, nfae 2444, hbnae 2443, nfnae 2445, hbnaes 2446) would need to be totally unbundled to be proved without ax-13 2379, hence would be simple consequences of ax-5 1911 or nfv 1915. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 → ∀𝑦𝜑))
Theorem	bj-drnf2v 34247*	Version of drnf2 2455 with a disjoint variable condition, which does not require ax-10 2142, ax-11 2158, ax-12 2175, ax-13 2379. Instance of nfbidv 1923. Note that the version of axc15 2433 with a disjoint variable condition is actually ax12v2 2177 (up to adding a superfluous antecedent). (Contributed by BJ, 17-Jun-2019.) (Proof modification is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 𝑥 = 𝑦 → (Ⅎ𝑧𝜑 ↔ Ⅎ𝑧𝜓))
Theorem	bj-equs45fv 34248*	Version of equs45f 2471 with a disjoint variable condition, which does not require ax-13 2379. Note that the version of equs5 2472 with a disjoint variable condition is actually sb56 2274 (up to adding a superfluous antecedent). (Contributed by BJ, 11-Sep-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑))
Theorem	bj-hbs1 34249*	Version of hbsb2 2500 with a disjoint variable condition, which does not require ax-13 2379, and removal of ax-13 2379 from hbs1 2271. (Contributed by BJ, 23-Jun-2019.) (Proof modification is discouraged.)
⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑)
Theorem	bj-nfs1v 34250*	Version of nfsb2 2501 with a disjoint variable condition, which does not require ax-13 2379, and removal of ax-13 2379 from nfs1v 2157. (Contributed by BJ, 24-Jun-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥[𝑦 / 𝑥]𝜑
Theorem	bj-hbsb2av 34251*	Version of hbsb2a 2502 with a disjoint variable condition, which does not require ax-13 2379. (Contributed by BJ, 11-Sep-2019.) (Proof modification is discouraged.)
⊢ ([𝑦 / 𝑥]∀𝑦𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑)
Theorem	bj-hbsb3v 34252*	Version of hbsb3 2505 with a disjoint variable condition, which does not require ax-13 2379. (Remark: the unbundled version of nfs1 2506 is given by bj-nfs1v 34250.) (Contributed by BJ, 11-Sep-2019.) (Proof modification is discouraged.)
⊢ (𝜑 → ∀𝑦𝜑)    ⇒   ⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑)
Theorem	bj-nfsab1 34253*	Remove dependency on ax-13 2379 from nfsab1 2785. UPDATE / TODO: nfsab1 2785 does not use ax-13 2379 either anymore; bj-nfsab1 34253 is shorter than nfsab1 2785 but uses ax-12 2175. (Contributed by BJ, 23-Jun-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥 𝑦 ∈ {𝑥 ∣ 𝜑}
Theorem	bj-dtru 34254*	Remove dependency on ax-13 2379 from dtru 5236. (Contributed by BJ, 31-May-2019.) TODO: This predates the removal of ax-13 2379 in dtru 5236. But actually, sn-dtru 39403 is better than either, so move it to Main with sn-el 39402 (and determine whether bj-dtru 34254 should be kept as ALT or deleted). (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ¬ ∀𝑥 𝑥 = 𝑦
Theorem	bj-dtrucor2v 34255*	Version of dtrucor2 5238 with a disjoint variable condition, which does not require ax-13 2379 (nor ax-4 1811, ax-5 1911, ax-7 2015, ax-12 2175). (Contributed by BJ, 16-Jul-2019.) (Proof modification is discouraged.)
⊢ (𝑥 = 𝑦 → 𝑥 ≠ 𝑦)    ⇒   ⊢ (𝜑 ∧ ¬ 𝜑)
20.15.4.13  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 34256	Biconditional version of a form of hbae 2442 with commuted quantifiers, not requiring ax-11 2158. (Contributed by BJ, 12-Dec-2019.) (Proof modification is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 ↔ ∀𝑥∀𝑧 𝑥 = 𝑦)
Theorem	bj-hbaeb 34257	Biconditional version of hbae 2442. (Contributed by BJ, 6-Oct-2018.) (Proof modification is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 ↔ ∀𝑧∀𝑥 𝑥 = 𝑦)
Theorem	bj-hbnaeb 34258	Biconditional version of hbnae 2443 (to replace it?). (Contributed by BJ, 6-Oct-2018.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 ↔ ∀𝑧 ¬ ∀𝑥 𝑥 = 𝑦)
Theorem	bj-dvv 34259	A special instance of bj-hbaeb2 34256. A lemma for distinct var metavariables. Note that the right-hand side is a closed formula (a sentence). (Contributed by BJ, 6-Oct-2018.)
⊢ (∀𝑥 𝑥 = 𝑦 ↔ ∀𝑥∀𝑦 𝑥 = 𝑦)
20.15.4.14  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 34037), then they should be added to the database. The present case is similar. Similar additions can be done regarding equsex 2429 (and equsalh 2431 and equsexh 2432). Even if only one of these two theorems holds, it should be added to the database.
Theorem	bj-equsal1t 34260	Duplication of wl-equsal1t 34946, with shorter proof. If one imposes a disjoint variable condition on x,y , then one can use alequexv 2007 and reduce axiom dependencies, and similarly for the following theorems. Note: wl-equsalcom 34947 is also interesting. (Contributed by BJ, 6-Oct-2018.)
⊢ (Ⅎ𝑥𝜑 → (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜑))
Theorem	bj-equsal1ti 34261	Inference associated with bj-equsal1t 34260. (Contributed by BJ, 30-Sep-2018.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜑)
Theorem	bj-equsal1 34262	One direction of equsal 2428. (Contributed by BJ, 30-Sep-2018.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))    ⇒   ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → 𝜓)
Theorem	bj-equsal2 34263	One direction of equsal 2428. (Contributed by BJ, 30-Sep-2018.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))    ⇒   ⊢ (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜓))
Theorem	bj-equsal 34264	Shorter proof of equsal 2428. (Contributed by BJ, 30-Sep-2018.) Proof modification is discouraged to avoid using equsal 2428, but "min */exc equsal" is ok. (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜓)
20.15.4.15  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 34265	Closed form of stdpc5 2206. (Possible to place it before 19.21t 2204 and use it to prove 19.21t 2204). (Contributed by BJ, 15-Sep-2018.) (Proof modification is discouraged.)
⊢ (Ⅎ𝑥𝜑 → (∀𝑥(𝜑 → 𝜓) → (𝜑 → ∀𝑥𝜓)))
Theorem	bj-stdpc5 34266	More direct proof of stdpc5 2206. (Contributed by BJ, 15-Sep-2018.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∀𝑥(𝜑 → 𝜓) → (𝜑 → ∀𝑥𝜓))
Theorem	2stdpc5 34267	A double stdpc5 2206 (one direction of PM*11.3). See also 2stdpc4 2075 and 19.21vv 41080. (Contributed by BJ, 15-Sep-2018.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (∀𝑥∀𝑦(𝜑 → 𝜓) → (𝜑 → ∀𝑥∀𝑦𝜓))
Theorem	bj-19.21t0 34268	Proof of 19.21t 2204 from stdpc5t 34265. (Contributed by BJ, 15-Sep-2018.) (Proof modification is discouraged.)
⊢ (Ⅎ𝑥𝜑 → (∀𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥𝜓)))
Theorem	exlimii 34269	Inference associated with exlimi 2215. Inferring a theorem when it is implied by an antecedent which may be true. (Contributed by BJ, 15-Sep-2018.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝜑 → 𝜓)    &   ⊢ ∃𝑥𝜑    ⇒   ⊢ 𝜓
Theorem	ax11-pm 34270	Proof of ax-11 2158 similar to PM's proof of alcom 2160 (PM*11.2). For a proof closer to PM's proof, see ax11-pm2 34274. Axiom ax-11 2158 is used in the proof only through nfa2 2174. (Contributed by BJ, 15-Sep-2018.) (Proof modification is discouraged.)
⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑)
Theorem	ax6er 34271	Commuted form of ax6e 2390. (Could be placed right after ax6e 2390). (Contributed by BJ, 15-Sep-2018.)
⊢ ∃𝑥 𝑦 = 𝑥
Theorem	exlimiieq1 34272	Inferring a theorem when it is implied by an equality which may be true. (Contributed by BJ, 30-Sep-2018.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝑥 = 𝑦 → 𝜑)    ⇒   ⊢ 𝜑
Theorem	exlimiieq2 34273	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 34274*	Proof of ax-11 2158 from the standard axioms of predicate calculus, similar to PM's proof of alcom 2160 (PM*11.2). This proof requires that 𝑥 and 𝑦 be distinct. Axiom ax-11 2158 is used in the proof only through nfal 2331, nfsb 2542, sbal 2163, sb8 2536. See also ax11-pm 34270. (Contributed by BJ, 15-Sep-2018.) (Proof modification is discouraged.)
⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑)
20.15.4.16  Alternate definition of substitution
Theorem	bj-sbsb 34275	Biconditional showing two possible (dual) definitions of substitution df-sb 2070 not using dummy variables. (Contributed by BJ, 19-Mar-2021.)
⊢ (((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) ↔ (∀𝑥(𝑥 = 𝑦 → 𝜑) ∨ (𝑥 = 𝑦 ∧ 𝜑)))
Theorem	bj-dfsb2 34276	Alternate (dual) definition of substitution df-sb 2070 not using dummy variables. (Contributed by BJ, 19-Mar-2021.)
⊢ ([𝑦 / 𝑥]𝜑 ↔ (∀𝑥(𝑥 = 𝑦 → 𝜑) ∨ (𝑥 = 𝑦 ∧ 𝜑)))
20.15.4.17  Lemmas for substitution
Theorem	bj-sbf3 34277	Substitution has no effect on a bound variable (existential quantifier case); see sbf2 2269. (Contributed by BJ, 2-May-2019.)
⊢ ([𝑦 / 𝑥]∃𝑥𝜑 ↔ ∃𝑥𝜑)
Theorem	bj-sbf4 34278	Substitution has no effect on a bound variable (nonfreeness case); see sbf2 2269. (Contributed by BJ, 2-May-2019.)
⊢ ([𝑦 / 𝑥]Ⅎ𝑥𝜑 ↔ Ⅎ𝑥𝜑)
Theorem	bj-sbnf 34279*	Move nonfree predicate in and out of substitution; see sbal 2163 and sbex 2284. (Contributed by BJ, 2-May-2019.)
⊢ ([𝑧 / 𝑦]Ⅎ𝑥𝜑 ↔ Ⅎ𝑥[𝑧 / 𝑦]𝜑)
20.15.4.18  Existential uniqueness
Theorem	bj-eu3f 34280*	Version of eu3v 2630 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 2630. (Contributed by NM, 8-Jul-1994.) (Proof shortened by BJ, 31-May-2019.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦)))
20.15.4.19  First-order logic: miscellaneous Miscellaneous theorems of first-order logic.
Theorem	bj-sblem1 34281*	Lemma for substitution. (Contributed by BJ, 23-Jul-2023.)
⊢ (∀𝑥(𝜑 → (𝜓 → 𝜒)) → (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → 𝜒)))
Theorem	bj-sblem2 34282*	Lemma for substitution. (Contributed by BJ, 23-Jul-2023.)
⊢ (∀𝑥(𝜑 → (𝜒 → 𝜓)) → ((∃𝑥𝜑 → 𝜒) → ∀𝑥(𝜑 → 𝜓)))
Theorem	bj-sblem 34283*	Lemma for substitution. (Contributed by BJ, 23-Jul-2023.)
⊢ (∀𝑥(𝜑 → (𝜓 ↔ 𝜒)) → (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜒)))
Theorem	bj-sbievw1 34284*	Lemma for substitution. (Contributed by BJ, 23-Jul-2023.)
⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) → ([𝑦 / 𝑥]𝜑 → 𝜓))
Theorem	bj-sbievw2 34285*	Lemma for substitution. (Contributed by BJ, 23-Jul-2023.)
⊢ ([𝑦 / 𝑥](𝜓 → 𝜑) → (𝜓 → [𝑦 / 𝑥]𝜑))
Theorem	bj-sbievw 34286*	Lemma for substitution. Closed form of equsalvw 2010 and sbievw 2100. (Contributed by BJ, 23-Jul-2023.)
⊢ ([𝑦 / 𝑥](𝜑 ↔ 𝜓) → ([𝑦 / 𝑥]𝜑 ↔ 𝜓))
Theorem	bj-sbievv 34287	Version of sbie 2521 with a second nonfreeness hypothesis and shorter proof. (Contributed by BJ, 18-Jul-2023.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓)
Theorem	bj-moeub 34288	Uniqueness is equivalent to existence being equivalent to unique existence. (Contributed by BJ, 14-Oct-2022.)
⊢ (∃*𝑥𝜑 ↔ (∃𝑥𝜑 ↔ ∃!𝑥𝜑))
Theorem	bj-sbidmOLD 34289	Obsolete proof of sbidm 2529 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 34290*	Deduction form of dvelim 2462 with disjoint variable conditions. Uncurried (imported) form of bj-dvelimdv1 34291. 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 1915 can be replaced with nfal 2331 followed by nfn 1858. Remark: nfald 2336 uses ax-11 2158; it might be possible to inline and use ax11w 2131 instead, but there is still a use via 19.12 2335 anyway. (Contributed by BJ, 20-Oct-2021.) (Proof modification is discouraged.)
⊢ (𝜑 → Ⅎ𝑥𝜒)    &   ⊢ (𝑧 = 𝑦 → (𝜒 ↔ 𝜓))    ⇒   ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥𝜓)
Theorem	bj-dvelimdv1 34291*	Curried (exported) form of bj-dvelimdv 34290 (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 34292*	A version of dvelim 2462 using the "nonfree" idiom. (Contributed by BJ, 20-Oct-2021.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑧 = 𝑦 → (𝜓 ↔ 𝜑))    ⇒   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝜑)
Theorem	bj-nfeel2 34293*	Nonfreeness in a membership statement. (Contributed by BJ, 20-Oct-2021.) (Proof modification is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥 𝑦 ∈ 𝑧)
Theorem	bj-axc14nf 34294	Proof of a version of axc14 2475 using the "nonfree" idiom. (Contributed by BJ, 20-Oct-2021.) (Proof modification is discouraged.)
⊢ (¬ ∀𝑧 𝑧 = 𝑥 → (¬ ∀𝑧 𝑧 = 𝑦 → Ⅎ𝑧 𝑥 ∈ 𝑦))
Theorem	bj-axc14 34295	Alternate proof of axc14 2475 (even when inlining the above results, this gives a shorter proof). (Contributed by BJ, 20-Oct-2021.) (Proof modification is discouraged.)
⊢ (¬ ∀𝑧 𝑧 = 𝑥 → (¬ ∀𝑧 𝑧 = 𝑦 → (𝑥 ∈ 𝑦 → ∀𝑧 𝑥 ∈ 𝑦)))
Theorem	mobidvALT 34296*	Alternate proof of mobidv 2608 directly from its analogues albidv 1921 and exbidv 1922, using deduction style. Note the proof structure, similar to mobi 2605. (Contributed by Mario Carneiro, 7-Oct-2016.) Reduce axiom dependencies and shorten proof. Remove dependency on ax-6 1970, ax-7 2015, ax-12 2175 by adapting proof of mobid 2609. (Revised by BJ, 26-Sep-2022.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃*𝑥𝜓 ↔ ∃*𝑥𝜒))
20.15.5  Set theory
20.15.5.1  Eliminability of class terms In this section, we give a sketch of the proof of the Eliminability Theorem for class terms in an extensional set theory where quantification occurs only over set variables. Eliminability of class variables using the $a-statements ax-ext 2770, df-clab 2777, df-cleq 2791, df-clel 2870 is an easy result, proved for instance in Appendix X of Azriel Levy, Basic Set Theory, Dover Publications, 2002. Note that viewed from the set.mm axiomatization, it is a metatheorem not formalizable in set.mm. It states: every formula in the language of FOL + ∈ + class terms, but without class variables, is provably equivalent (over {FOL, ax-ext 2770, df-clab 2777, df-cleq 2791, df-clel 2870 }) to a formula in the language of FOL + ∈ (that is, without class terms). The proof goes by induction on the complexity of the formula (see op. cit. for details). The base case is that of atomic formulas. The atomic formulas containing class terms are of one of the six following forms: for equality, 𝑥 = {𝑦 ∣ 𝜑}, {𝑥 ∣ 𝜑} = 𝑦, {𝑥 ∣ 𝜑} = {𝑦 ∣ 𝜓}, and for membership, 𝑦 ∈ {𝑥 ∣ 𝜑}, {𝑥 ∣ 𝜑} ∈ 𝑦, {𝑥 ∣ 𝜑} ∈ {𝑦 ∣ 𝜓}. These cases are dealt with by eliminable-veqab 34304, eliminable-abeqv 34305, eliminable-abeqab 34306, eliminable-velab 34303, eliminable-abelv 34307, eliminable-abelab 34308 respectively, which are all proved from {FOL, ax-ext 2770, df-clab 2777, df-cleq 2791, df-clel 2870 }. (Details on the proof of the above six theorems. To understand how they were systematically proved, look at the theorems "eliminablei" below, which are special instances of df-clab 2777, dfcleq 2792 (proved from {FOL, ax-ext 2770, df-cleq 2791 }), and dfclel 2871 (proved from {FOL, df-clel 2870 }). Indeed, denote by (i) the formula proved by "eliminablei". One sees that the RHS of (1) has no class terms, the RHS's of (2x) have only class terms of the form dealt with by (1), and the RHS's of (3x) have only class terms of the forms dealt with by (1) and (2a). Note that in order to prove eliminable2a 34298, eliminable2b 34299 and eliminable3a 34301, we need to substitute a class variable for a setvar variable. This is possible because setvars are class terms: this is the content of the syntactic theorem cv 1537, which is used in these proofs (this does not appear in the html pages but it is in the set.mm file and you can check it using the Metamath program).) The induction step relies on the fact that any formula is a FOL-combination of atomic formulas, so if one found equivalents for all atomic formulas constituting the formula, then the same FOL-combination of these equivalents will be equivalent to the original formula. Note that one has a slightly more precise result: if the original formula has only class terms appearing in atomic formulas of the form 𝑦 ∈ {𝑥 ∣ 𝜑}, then df-clab 2777 is sufficient (over FOL) to eliminate class terms, and if the original formula has only class terms appearing in atomic formulas of the form 𝑦 ∈ {𝑥 ∣ 𝜑} and equalities, then df-clab 2777, ax-ext 2770 and df-cleq 2791 are sufficient (over FOL) to eliminate class terms. To prove that { df-clab 2777, df-cleq 2791, df-clel 2870 } provides a definitional extension of {FOL, ax-ext 2770 }, one needs to prove both the above Eliminability Theorem, which compares the expressive powers of the languages with and without class terms, and the Conservativity Theorem, which compares the deductive powers when one adds { df-clab 2777, df-cleq 2791, df-clel 2870 }. It states that a formula without class terms is provable in one axiom system if and only if it is provable in the other, and that this remains true when one adds further definitions to {FOL, ax-ext 2770 }. It is also proved in op. cit. The proof is more difficult, since one has to construct for each proof of a statement without class terms, an associated proof not using { df-clab 2777, df-cleq 2791, df-clel 2870 }. It involves a careful case study on the structure of the proof tree.
Theorem	eliminable1 34297	A theorem used to prove the base case of the Eliminability Theorem (see section comment). (Contributed by BJ, 19-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ [𝑦 / 𝑥]𝜑)
Theorem	eliminable2a 34298*	A theorem used to prove the base case of the Eliminability Theorem (see section comment). (Contributed by BJ, 19-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 = {𝑦 ∣ 𝜑} ↔ ∀𝑧(𝑧 ∈ 𝑥 ↔ 𝑧 ∈ {𝑦 ∣ 𝜑}))
Theorem	eliminable2b 34299*	A theorem used to prove the base case of the Eliminability Theorem (see section comment). (Contributed by BJ, 19-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ({𝑥 ∣ 𝜑} = 𝑦 ↔ ∀𝑧(𝑧 ∈ {𝑥 ∣ 𝜑} ↔ 𝑧 ∈ 𝑦))
Theorem	eliminable2c 34300*	A theorem used to prove the base case of the Eliminability Theorem (see section comment). (Contributed by BJ, 19-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ({𝑥 ∣ 𝜑} = {𝑦 ∣ 𝜓} ↔ ∀𝑧(𝑧 ∈ {𝑥 ∣ 𝜑} ↔ 𝑧 ∈ {𝑦 ∣ 𝜓}))