![]() |
Metamath
Proof Explorer Theorem List (p. 334 of 437) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-28347) |
![]() (28348-29872) |
![]() (29873-43661) |
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.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ Ⅎ𝑥[𝑦 / 𝑥]𝜑 | ||
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.) |
⊢ ∃𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑥) | ||
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.) |
⊢ (∀𝑥 𝑥 = 𝑦 ↔ ∀𝑥∀𝑦 𝑥 = 𝑦) | ||
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.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜓) | ||
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.) |
⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑) | ||
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.) |
⊢ ([𝑦 / 𝑥]𝜑 ↔ (∀𝑥(𝑥 = 𝑦 → 𝜑) ∨ (𝑥 = 𝑦 ∧ 𝜑))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |