P. 334 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 33301-33400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	bj-hbsb3 33301	Shorter proof of hbsb3 2440. (Contributed by BJ, 2-May-2019.) (Proof modification is discouraged.)
⊢ (𝜑 → ∀𝑦𝜑)    ⇒   ⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑)
Theorem	bj-nfs1t 33302	A theorem close to a closed form of nfs1 2441. (Contributed by BJ, 2-May-2019.)
⊢ (∀𝑥(𝜑 → ∀𝑦𝜑) → Ⅎ𝑥[𝑦 / 𝑥]𝜑)
Theorem	bj-nfs1t2 33303	A theorem close to a closed form of nfs1 2441. (Contributed by BJ, 2-May-2019.)
⊢ (∀𝑥Ⅎ𝑦𝜑 → Ⅎ𝑥[𝑦 / 𝑥]𝜑)
Theorem	bj-nfs1 33304	Shorter proof of nfs1 2441 (three essential steps instead of four). (Contributed by BJ, 2-May-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ Ⅎ𝑥[𝑦 / 𝑥]𝜑
20.14.4.11  Removing dependencies on ax-13 (and ax-11) It is known that ax-13 2334 is logically redundant (see ax13w 2130 and the head comment of the section "Logical redundancy of ax-10--13"). More precisely, one can remove dependency on ax-13 2334 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 2334 with ax13w 2130. This section is an experiment to see in practice if (partially) unbundled versions of existing theorems can be proved more efficiently without ax-13 2334 (and using ax6v 2022 / ax6ev 2023 instead of ax-6 2021 / ax6e 2347, as is currently done). One reason to be optimistic is that the first few utility theorems using ax-13 2334 (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 2334, labeled bj-xxxv (we follow the proof of xxx but use ax6v 2022 and ax6ev 2023 instead of ax-6 2021 and ax6e 2347, and ax-5 1953 instead of ax13v 2335; 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 2334, so as to remove dependencies on ax-13 2334 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 2150, typically by replacing a non-free hypothesis with a disjoint variable condition (see cbv3v2 2240 and following theorems).
Theorem	bj-axc10v 33305*	Version of axc10 2349 with a disjoint variable condition, which does not require ax-13 2334. (Contributed by BJ, 14-Jun-2019.) (Proof modification is discouraged.)
⊢ (∀𝑥(𝑥 = 𝑦 → ∀𝑥𝜑) → 𝜑)
Theorem	bj-spimtv 33306*	Version of spimt 2350 with a disjoint variable condition, which does not require ax-13 2334. (Contributed by BJ, 14-Jun-2019.) (Proof modification is discouraged.)
⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝑦 → (𝜑 → 𝜓))) → (∀𝑥𝜑 → 𝜓))
Theorem	bj-spimedv 33307*	Version of spimed 2353 with a disjoint variable condition, which does not require ax-13 2334. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
⊢ (𝜒 → Ⅎ𝑥𝜑)    &   ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))    ⇒   ⊢ (𝜒 → (𝜑 → ∃𝑥𝜓))
Theorem	bj-spimev 33308*	Version of spime 2354 with a disjoint variable condition, which does not require ax-13 2334. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))    ⇒   ⊢ (𝜑 → ∃𝑥𝜓)
Theorem	bj-spimvv 33309*	Version of spimv 2355 and spimv1 2239 with a disjoint variable condition, which does not require ax-13 2334. UPDATE: this is spimvw 2045 (but different proof). (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))    ⇒   ⊢ (∀𝑥𝜑 → 𝜓)
Theorem	bj-spimevv 33310*	Version of spimev 2357 with a disjoint variable condition, which does not require ax-13 2334. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))    ⇒   ⊢ (𝜑 → ∃𝑥𝜓)
Theorem	bj-spvv 33311*	Version of spv 2358 with a disjoint variable condition, which does not require ax-7 2055, ax-12 2163, ax-13 2334. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥𝜑 → 𝜓)
Theorem	bj-speiv 33312*	Version of spei 2359 with a disjoint variable condition, which does not require ax-13 2334 (neither ax-7 2055 nor ax-12 2163). (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ 𝜓    ⇒   ⊢ ∃𝑥𝜑
Theorem	bj-chvarv 33313*	Version of chvar 2360 with a disjoint variable condition, which does not require ax-13 2334. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ 𝜓
Theorem	bj-chvarvv 33314*	Version of chvarv 2361 with a disjoint variable condition, which does not require ax-13 2334. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ 𝜓
Theorem	bj-cbv3hv2 33315*	Version of cbv3h 2363 with two disjoint variable conditions, which does not require ax-11 2150 nor ax-13 2334. (Contributed by BJ, 24-Jun-2019.) (Proof modification is discouraged.)
⊢ (𝜓 → ∀𝑥𝜓)    &   ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))    ⇒   ⊢ (∀𝑥𝜑 → ∀𝑦𝜓)
Theorem	bj-cbv1v 33316*	Version of cbv1 2364 with a disjoint variable condition, which does not require ax-13 2334. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑦𝜓)    &   ⊢ (𝜑 → Ⅎ𝑥𝜒)    &   ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 → 𝜒)))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 → ∀𝑦𝜒))
Theorem	bj-cbv1hv 33317*	Version of cbv1h 2365 with a disjoint variable condition, which does not require ax-13 2334. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ (𝜑 → (𝜓 → ∀𝑦𝜓))    &   ⊢ (𝜑 → (𝜒 → ∀𝑥𝜒))    &   ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 → 𝜒)))    ⇒   ⊢ (∀𝑥∀𝑦𝜑 → (∀𝑥𝜓 → ∀𝑦𝜒))
Theorem	bj-cbv2hv 33318*	Version of cbv2h 2366 with a disjoint variable condition, which does not require ax-13 2334. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ (𝜑 → (𝜓 → ∀𝑦𝜓))    &   ⊢ (𝜑 → (𝜒 → ∀𝑥𝜒))    &   ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (∀𝑥∀𝑦𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒))
Theorem	bj-cbv2v 33319*	Version of cbv2 2367 with a disjoint variable condition, which does not require ax-13 2334. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑦𝜓)    &   ⊢ (𝜑 → Ⅎ𝑥𝜒)    &   ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒))
Theorem	bj-cbvaldv 33320*	Version of cbvald 2372 with a disjoint variable condition, which does not require ax-13 2334. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑦𝜓)    &   ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒))
Theorem	bj-cbvexdv 33321*	Version of cbvexd 2373 with a disjoint variable condition, which does not require ax-13 2334. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑦𝜓)    &   ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑦𝜒))
Theorem	bj-cbval2v 33322*	Version of cbval2 2374 with a disjoint variable condition, which does not require ax-13 2334. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑧𝜑    &   ⊢ Ⅎ𝑤𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ Ⅎ𝑦𝜓    &   ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑧∀𝑤𝜓)
Theorem	bj-cbvex2v 33323*	Version of cbvex2 2375 with a disjoint variable condition, which does not require ax-13 2334. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑧𝜑    &   ⊢ Ⅎ𝑤𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ Ⅎ𝑦𝜓    &   ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑧∃𝑤𝜓)
Theorem	bj-cbval2vv 33324*	Version of cbval2v 2378 with a disjoint variable condition, which does not require ax-13 2334. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑧∀𝑤𝜓)
Theorem	bj-cbvex2vv 33325*	Version of cbvex2v 2379 with a disjoint variable condition, which does not require ax-13 2334. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑧∃𝑤𝜓)
Theorem	bj-cbvaldvav 33326*	Version of cbvaldva 2376 with a disjoint variable condition, which does not require ax-13 2334. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒))
Theorem	bj-cbvexdvav 33327*	Version of cbvexdva 2377 with a disjoint variable condition, which does not require ax-13 2334. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑦𝜒))
Theorem	bj-cbvex4vv 33328*	Version of cbvex4v 2380 with a disjoint variable condition, which does not require ax-13 2334. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ ((𝑥 = 𝑣 ∧ 𝑦 = 𝑢) → (𝜑 ↔ 𝜓))    &   ⊢ ((𝑧 = 𝑓 ∧ 𝑤 = 𝑔) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (∃𝑥∃𝑦∃𝑧∃𝑤𝜑 ↔ ∃𝑣∃𝑢∃𝑓∃𝑔𝜒)
Theorem	bj-equsalhv 33329*	Version of equsalh 2385 with a disjoint variable condition, which does not require ax-13 2334. Remark: this is the same as equsalhw 2265 (TODO: delete after moving the following paragraph somewhere). Remarks: equsexvw 2052 has been moved to Main; the theorem ax13lem2 2338 has a dv version which is a simple consequence of ax5e 1955; the theorems nfeqf2 2339, dveeq2 2342, nfeqf1 2343, dveeq1 2344, nfeqf 2345, axc9 2346, ax13 2337, have dv versions which are simple consequences of ax-5 1953. (Contributed by BJ, 14-Jun-2019.) (Proof modification is discouraged.)
⊢ (𝜓 → ∀𝑥𝜓)    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜓)
Theorem	bj-axc11nv 33330*	Version of axc11n 2392 with a disjoint variable condition; instance of aevlem 2098 (TODO: delete after checking surrounding theorems). (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥)
Theorem	bj-aecomsv 33331*	Version of aecoms 2394 with a disjoint variable condition, provable from Tarski's FOL. The corresponding version of naecoms 2395 should not be very useful since ¬ ∀𝑥𝑥 = 𝑦, DV(x,y) is true when the universe has at least two objects (see bj-dtru 33373). (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → 𝜑)    ⇒   ⊢ (∀𝑦 𝑦 = 𝑥 → 𝜑)
Theorem	bj-axc11v 33332*	Version of axc11 2396 with a disjoint variable condition, which does not require ax-13 2334 nor ax-10 2135. Remark: the following theorems (hbae 2397, nfae 2398, hbnae 2399, nfnae 2400, hbnaes 2401) would need to be totally unbundled to be proved without ax-13 2334, hence would be simple consequences of ax-5 1953 or nfv 1957. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 → ∀𝑦𝜑))
Theorem	bj-dral1v 33333*	Version of dral1 2405 with a disjoint variable condition, which does not require ax-13 2334. Remark: the corresponding versions for dral2 2404 and drex2 2408 are instances of albidv 1963 and exbidv 1964 respectively. (Contributed by BJ, 17-Jun-2019.) (Proof modification is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 ↔ ∀𝑦𝜓))
Theorem	bj-drex1v 33334*	Version of drex1 2407 with a disjoint variable condition, which does not require ax-13 2334. (Contributed by BJ, 17-Jun-2019.) (Proof modification is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 𝑥 = 𝑦 → (∃𝑥𝜑 ↔ ∃𝑦𝜓))
Theorem	bj-drnf1v 33335*	Version of drnf1 2409 with a disjoint variable condition, which does not require ax-13 2334. (Contributed by BJ, 17-Jun-2019.) (Proof modification is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 𝑥 = 𝑦 → (Ⅎ𝑥𝜑 ↔ Ⅎ𝑦𝜓))
Theorem	bj-drnf2v 33336*	Version of drnf2 2410 with a disjoint variable condition, which does not require ax-10 2135, ax-11 2150, ax-12 2163, ax-13 2334. Instance of nfbidv 1965. Note that the version of axc15 2387 with a disjoint variable condition is actually ax12v2 2165 (up to adding a superfluous antecedent). (Contributed by BJ, 17-Jun-2019.) (Proof modification is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 𝑥 = 𝑦 → (Ⅎ𝑧𝜑 ↔ Ⅎ𝑧𝜓))
Theorem	bj-equs45fv 33337*	Version of equs45f 2425 with a disjoint variable condition, which does not require ax-13 2334. Note that the version of equs5 2426 with a disjoint variable condition is actually sb56 2248 (up to adding a superfluous antecedent). (Contributed by BJ, 11-Sep-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑))
Theorem	bj-2stdpc4v 33338*	Version of 2stdpc4 2429 with a disjoint variable condition, which does not require ax-13 2334. (Contributed by BJ, 24-Jun-2019.) (Proof modification is discouraged.)
⊢ (∀𝑥∀𝑦𝜑 → [𝑧 / 𝑥][𝑤 / 𝑦]𝜑)
Theorem	bj-sb3v 33339*	Version of sb3 2430 with a disjoint variable condition, which does not require ax-13 2334. (Contributed by BJ, 24-Jun-2019.) (Proof modification is discouraged.)
⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → [𝑦 / 𝑥]𝜑)
Theorem	bj-hbs1 33340*	Version of hbsb2 2435 with a disjoint variable condition, which does not require ax-13 2334, and removal of ax-13 2334 from hbs1 2255. (Contributed by BJ, 23-Jun-2019.) (Proof modification is discouraged.)
⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑)
Theorem	bj-nfs1v 33341*	Version of nfsb2 2436 with a disjoint variable condition, which does not require ax-13 2334, and removal of ax-13 2334 from nfs1v 2254. (Contributed by BJ, 24-Jun-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥[𝑦 / 𝑥]𝜑
Theorem	bj-hbsb2av 33342*	Version of hbsb2a 2437 with a disjoint variable condition, which does not require ax-13 2334. (Contributed by BJ, 11-Sep-2019.) (Proof modification is discouraged.)
⊢ ([𝑦 / 𝑥]∀𝑦𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑)
Theorem	bj-hbsb3v 33343*	Version of hbsb3 2440 with a disjoint variable condition, which does not require ax-13 2334. (Remark: the unbundled version of nfs1 2441 is given by bj-nfs1v 33341.) (Contributed by BJ, 11-Sep-2019.) (Proof modification is discouraged.)
⊢ (𝜑 → ∀𝑦𝜑)    ⇒   ⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑)
Theorem	bj-sbfvv 33344*	Version of sbf 2456 with two disjoint variable conditions, which does not require ax-10 2135 nor ax-13 2334. (Contributed by BJ, 1-May-2021.) (Proof modification is discouraged.)
⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜑)
Theorem	bj-sbtv 33345*	Version of sbt 2496 with a disjoint variable condition, which does not require ax-13 2334. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
⊢ 𝜑    ⇒   ⊢ [𝑦 / 𝑥]𝜑
Theorem	bj-axext3 33346*	Remove dependency on ax-13 2334 from axext3 2756. (Contributed by BJ, 12-Jul-2019.) (Proof modification is discouraged.)
⊢ (∀𝑧(𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦) → 𝑥 = 𝑦)
Theorem	bj-axext4 33347*	Remove dependency on ax-13 2334 from axext4 2758. (Contributed by BJ, 6-Oct-2019.) (Proof modification is discouraged.)
⊢ (𝑥 = 𝑦 ↔ ∀𝑧(𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦))
Theorem	bj-hbab1 33348*	Remove dependency on ax-13 2334 from hbab1 2766. (Contributed by BJ, 23-Jun-2019.) (Proof modification is discouraged.)
⊢ (𝑦 ∈ {𝑥 ∣ 𝜑} → ∀𝑥 𝑦 ∈ {𝑥 ∣ 𝜑})
Theorem	bj-nfsab1 33349*	Remove dependency on ax-13 2334 from nfsab1 2767. (Contributed by BJ, 23-Jun-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥 𝑦 ∈ {𝑥 ∣ 𝜑}
Theorem	bj-abeq2 33350*	Remove dependency on ax-13 2334 from abeq2 2892. (Contributed by BJ, 23-Jun-2019.) (Proof modification is discouraged.)
⊢ (𝐴 = {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝜑))
Theorem	bj-abeq1 33351*	Remove dependency on ax-13 2334 from abeq1 2893. Remark: the theorems abeq2i 2895, abeq1i 2896, abeq2d 2894 do not use ax-11 2150 or ax-13 2334. (Contributed by BJ, 23-Jun-2019.) (Proof modification is discouraged.)
⊢ ({𝑥 ∣ 𝜑} = 𝐴 ↔ ∀𝑥(𝜑 ↔ 𝑥 ∈ 𝐴))
Theorem	bj-abbi 33352	Remove dependency on ax-13 2334 from abbi 2902. (Contributed by BJ, 23-Jun-2019.) (Proof modification is discouraged.)
⊢ (∀𝑥(𝜑 ↔ 𝜓) ↔ {𝑥 ∣ 𝜑} = {𝑥 ∣ 𝜓})
Theorem	bj-abbi2i 33353*	Remove dependency on ax-13 2334 from abbi2i 2900. (Contributed by BJ, 23-Jun-2019.) (Proof modification is discouraged.)
⊢ (𝑥 ∈ 𝐴 ↔ 𝜑)    ⇒   ⊢ 𝐴 = {𝑥 ∣ 𝜑}
Theorem	bj-abbii 33354	Remove dependency on ax-13 2334 from abbii 2908. (Contributed by BJ, 23-Jun-2019.) (Proof modification is discouraged.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ {𝑥 ∣ 𝜑} = {𝑥 ∣ 𝜓}
Theorem	bj-abbid 33355	Remove dependency on ax-13 2334 from abbid 2905. (Contributed by BJ, 23-Jun-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {𝑥 ∣ 𝜓} = {𝑥 ∣ 𝜒})
Theorem	bj-abbidv 33356*	Remove dependency on ax-13 2334 from abbidv 2906. (Contributed by BJ, 23-Jun-2019.) (Proof modification is discouraged.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {𝑥 ∣ 𝜓} = {𝑥 ∣ 𝜒})
Theorem	bj-abbi2dv 33357*	Remove dependency on ax-13 2334 from abbi2dv 2897. (Contributed by BJ, 23-Jun-2019.) (Proof modification is discouraged.)
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝜓))    ⇒   ⊢ (𝜑 → 𝐴 = {𝑥 ∣ 𝜓})
Theorem	bj-abbi1dv 33358*	Remove dependency on ax-13 2334 from abbi1dv 2899. (Contributed by BJ, 23-Jun-2019.) (Proof modification is discouraged.)
⊢ (𝜑 → (𝜓 ↔ 𝑥 ∈ 𝐴))    ⇒   ⊢ (𝜑 → {𝑥 ∣ 𝜓} = 𝐴)
Theorem	bj-abid2 33359*	Remove dependency on ax-13 2334 from abid2 2912. (Contributed by BJ, 23-Jun-2019.) (Proof modification is discouraged.)
⊢ {𝑥 ∣ 𝑥 ∈ 𝐴} = 𝐴
Theorem	bj-clabel 33360*	Remove dependency on ax-13 2334 from clabel 2917 (note the absence of disjoint variable conditions among variables in the LHS). (Contributed by BJ, 23-Jun-2019.) (Proof modification is discouraged.)
⊢ ({𝑥 ∣ 𝜑} ∈ 𝐴 ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ ∀𝑥(𝑥 ∈ 𝑦 ↔ 𝜑)))
Theorem	bj-sbab 33361*	Remove dependency on ax-13 2334 from sbab 2918 (note the absence of disjoint variable conditions among variables in the LHS). (Contributed by BJ, 23-Jun-2019.) (Proof modification is discouraged.)
⊢ (𝑥 = 𝑦 → 𝐴 = {𝑧 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝐴})
Theorem	bj-nfab1 33362	Remove dependency on ax-13 2334 from nfab1 2936 (note the absence of disjoint variable conditions). (Contributed by BJ, 6-Oct-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥{𝑥 ∣ 𝜑}
Theorem	bj-vjust 33363	Remove dependency on ax-13 2334 from vjust 3399 (note the absence of disjoint variable conditions). Soundness justification theorem for df-v 3400. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
⊢ {𝑥 ∣ 𝑥 = 𝑥} = {𝑦 ∣ 𝑦 = 𝑦}
Theorem	bj-cdeqab 33364*	Remove dependency on ax-13 2334 from cdeqab 3642. (Contributed by BJ, 6-Oct-2019.) (Proof modification is discouraged.)
⊢ CondEq(𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ CondEq(𝑥 = 𝑦 → {𝑧 ∣ 𝜑} = {𝑧 ∣ 𝜓})
Theorem	bj-axrep1 33365*	Remove dependency on ax-13 2334 from axrep1 5007. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
⊢ ∃𝑥(∃𝑦∀𝑧(𝜑 → 𝑧 = 𝑦) → ∀𝑧(𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ 𝜑)))
Theorem	bj-axrep2 33366*	Remove dependency on ax-13 2334 from axrep2 5009. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
⊢ ∃𝑥(∃𝑦∀𝑧(𝜑 → 𝑧 = 𝑦) → ∀𝑧(𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦𝜑)))
Theorem	bj-axrep3 33367*	Remove dependency on ax-13 2334 from axrep3 5010. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
⊢ ∃𝑥(∃𝑦∀𝑧(𝜑 → 𝑧 = 𝑦) → ∀𝑧(𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑤 ∧ ∀𝑦𝜑)))
Theorem	bj-axrep4 33368*	Remove dependency on ax-13 2334 from axrep4 5011. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑧𝜑    ⇒   ⊢ (∀𝑥∃𝑧∀𝑦(𝜑 → 𝑦 = 𝑧) → ∃𝑧∀𝑦(𝑦 ∈ 𝑧 ↔ ∃𝑥(𝑥 ∈ 𝑤 ∧ 𝜑)))
Theorem	bj-axrep5 33369*	Remove dependency on ax-13 2334 from axrep5 5012. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑧𝜑    ⇒   ⊢ (∀𝑥(𝑥 ∈ 𝑤 → ∃𝑧∀𝑦(𝜑 → 𝑦 = 𝑧)) → ∃𝑧∀𝑦(𝑦 ∈ 𝑧 ↔ ∃𝑥(𝑥 ∈ 𝑤 ∧ 𝜑)))
Theorem	bj-axsep 33370*	Remove dependency on ax-13 2334 from axsep 5016. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
⊢ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))
Theorem	bj-nalset 33371*	Remove dependency on ax-12 2163 and ax-13 2334 (and df-nf 1828) from nalset 5032. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
⊢ ¬ ∃𝑥∀𝑦 𝑦 ∈ 𝑥
Theorem	bj-el 33372*	Remove dependency on ax-13 2334 from el 5081. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
⊢ ∃𝑦 𝑥 ∈ 𝑦
Theorem	bj-dtru 33373*	Remove dependency on ax-13 2334 from dtru 5082. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
⊢ ¬ ∀𝑥 𝑥 = 𝑦
Theorem	bj-axc16b 33374*	Remove dependency on ax-13 2334 from axc16b 5100. (Contributed by BJ, 16-Jul-2019.) (Proof modification is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑥𝜑))
Theorem	bj-eunex 33375	Remove dependency on ax-13 2334 from eunex 5101. (Contributed by BJ, 16-Jul-2019.) (Proof modification is discouraged.)
⊢ (∃!𝑥𝜑 → ∃𝑥 ¬ 𝜑)
Theorem	bj-dtrucor 33376*	Remove dependency on ax-13 2334 from dtrucor 5083. (Contributed by BJ, 16-Jul-2019.) (Proof modification is discouraged.)
⊢ 𝑥 = 𝑦    ⇒   ⊢ 𝑥 ≠ 𝑦
Theorem	bj-dtrucor2v 33377*	Version of dtrucor2 5084 with a disjoint variable condition, which does not require ax-13 2334 (nor ax-4 1853, ax-5 1953, ax-7 2055, ax-12 2163). (Contributed by BJ, 16-Jul-2019.) (Proof modification is discouraged.)
⊢ (𝑥 = 𝑦 → 𝑥 ≠ 𝑦)    ⇒   ⊢ (𝜑 ∧ ¬ 𝜑)
Theorem	bj-dvdemo1 33378*	Remove dependency on ax-13 2334 from dvdemo1 5085 (this removal is noteworthy since dvdemo1 5085 and dvdemo2 5086 illustrate the phenomenon of bundling). (Contributed by BJ, 16-Jul-2019.) (Proof modification is discouraged.)
⊢ ∃𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑥)
Theorem	bj-dvdemo2 33379*	Remove dependency on ax-13 2334 from dvdemo2 5086 (this removal is noteworthy since dvdemo1 5085 and dvdemo2 5086 illustrate the phenomenon of bundling). (Contributed by BJ, 16-Jul-2019.) (Proof modification is discouraged.)
⊢ ∃𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑥)
20.14.4.12  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 33380	Biconditional version of a form of hbae 2397 with commuted quantifiers, not requiring ax-11 2150. (Contributed by BJ, 12-Dec-2019.) (Proof modification is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 ↔ ∀𝑥∀𝑧 𝑥 = 𝑦)
Theorem	bj-hbaeb 33381	Biconditional version of hbae 2397. (Contributed by BJ, 6-Oct-2018.) (Proof modification is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 ↔ ∀𝑧∀𝑥 𝑥 = 𝑦)
Theorem	bj-hbnaeb 33382	Biconditional version of hbnae 2399 (to replace it?). (Contributed by BJ, 6-Oct-2018.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 ↔ ∀𝑧 ¬ ∀𝑥 𝑥 = 𝑦)
Theorem	bj-dvv 33383	A special instance of bj-hbaeb2 33380. 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.14.4.13  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 33154), then they should be added to the database. The present case is similar. Similar additions can be done regarding equsex 2383 (and equsalh 2385 and equsexh 2386). Even if only one of these two theorems holds, it should be added to the database.
Theorem	bj-equsal1t 33384	Duplication of wl-equsal1t 33921, with shorter proof. If one imposes a disjoint variable condition on x,y , then one can use bj-alequexv 33244 and reduce axiom dependencies, and similarly for the following theorems. Note: wl-equsalcom 33922 is also interesting. (Contributed by BJ, 6-Oct-2018.)
⊢ (Ⅎ𝑥𝜑 → (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜑))
Theorem	bj-equsal1ti 33385	Inference associated with bj-equsal1t 33384. (Contributed by BJ, 30-Sep-2018.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜑)
Theorem	bj-equsal1 33386	One direction of equsal 2382. (Contributed by BJ, 30-Sep-2018.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))    ⇒   ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → 𝜓)
Theorem	bj-equsal2 33387	One direction of equsal 2382. (Contributed by BJ, 30-Sep-2018.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))    ⇒   ⊢ (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜓))
Theorem	bj-equsal 33388	Shorter proof of equsal 2382. (Contributed by BJ, 30-Sep-2018.) Proof modification is discouraged to avoid using equsal 2382, but "min */exc equsal" is ok. (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜓)
20.14.4.14  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 33389	Closed form of stdpc5 2193. (Possible to place it before 19.21t 2191 and use it to prove 19.21t 2191). (Contributed by BJ, 15-Sep-2018.) (Proof modification is discouraged.)
⊢ (Ⅎ𝑥𝜑 → (∀𝑥(𝜑 → 𝜓) → (𝜑 → ∀𝑥𝜓)))
Theorem	bj-stdpc5 33390	More direct proof of stdpc5 2193. (Contributed by BJ, 15-Sep-2018.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∀𝑥(𝜑 → 𝜓) → (𝜑 → ∀𝑥𝜓))
Theorem	2stdpc5 33391	A double stdpc5 2193 (one direction of PM*11.3). See also 2stdpc4 2429 and 19.21vv 39535. (Contributed by BJ, 15-Sep-2018.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (∀𝑥∀𝑦(𝜑 → 𝜓) → (𝜑 → ∀𝑥∀𝑦𝜓))
Theorem	bj-19.21t 33392	Proof of 19.21t 2191 from stdpc5t 33389. (Contributed by BJ, 15-Sep-2018.) (Proof modification is discouraged.)
⊢ (Ⅎ𝑥𝜑 → (∀𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥𝜓)))
Theorem	exlimii 33393	Inference associated with exlimi 2203. Inferring a theorem when it is implied by an antecedent which may be true. (Contributed by BJ, 15-Sep-2018.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝜑 → 𝜓)    &   ⊢ ∃𝑥𝜑    ⇒   ⊢ 𝜓
Theorem	ax11-pm 33394	Proof of ax-11 2150 similar to PM's proof of alcom 2152 (PM*11.2). For a proof closer to PM's proof, see ax11-pm2 33398. Axiom ax-11 2150 is used in the proof only through nfa2 2162. (Contributed by BJ, 15-Sep-2018.) (Proof modification is discouraged.)
⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑)
Theorem	ax6er 33395	Commuted form of ax6e 2347. (Could be placed right after ax6e 2347). (Contributed by BJ, 15-Sep-2018.)
⊢ ∃𝑥 𝑦 = 𝑥
Theorem	exlimiieq1 33396	Inferring a theorem when it is implied by an equality which may be true. (Contributed by BJ, 30-Sep-2018.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝑥 = 𝑦 → 𝜑)    ⇒   ⊢ 𝜑
Theorem	exlimiieq2 33397	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 33398*	Proof of ax-11 2150 from the standard axioms of predicate calculus, similar to PM's proof of alcom 2152 (PM*11.2). This proof requires that 𝑥 and 𝑦 be distinct. Axiom ax-11 2150 is used in the proof only through nfal 2299, nfsb 2520, sbal 2542, sb8 2501. See also ax11-pm 33394. (Contributed by BJ, 15-Sep-2018.) (Proof modification is discouraged.)
⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑)
20.14.4.15  Alternate definition of substitution
Theorem	bj-sbsb 33399	Biconditional showing two possible (dual) definitions of substitution df-sb 2012 not using dummy variables. (Contributed by BJ, 19-Mar-2021.)
⊢ (((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) ↔ (∀𝑥(𝑥 = 𝑦 → 𝜑) ∨ (𝑥 = 𝑦 ∧ 𝜑)))
Theorem	bj-dfsb2 33400	Alternate (dual) definition of substitution df-sb 2012 not using dummy variables. (Contributed by BJ, 19-Mar-2021.)
⊢ ([𝑦 / 𝑥]𝜑 ↔ (∀𝑥(𝑥 = 𝑦 → 𝜑) ∨ (𝑥 = 𝑦 ∧ 𝜑)))