Home | Metamath
Proof Explorer Theorem List (p. 320 of 424) | < 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: | Metamath Proof Explorer
(1-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | bj-nfs1t 31901 | A theorem close to a closed form of nfs1 2353. (Contributed by BJ, 2-May-2019.) |
⊢ (∀𝑥(𝜑 → ∀𝑦𝜑) → Ⅎ𝑥[𝑦 / 𝑥]𝜑) | ||
Theorem | bj-nfs1t2 31902 | A theorem close to a closed form of nfs1 2353. (Contributed by BJ, 2-May-2019.) |
⊢ (∀𝑥Ⅎ𝑦𝜑 → Ⅎ𝑥[𝑦 / 𝑥]𝜑) | ||
Theorem | bj-nfs1 31903 | Shorter proof of nfs1 2353 (three essential steps instead of four). (Contributed by BJ, 2-May-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ Ⅎ𝑥[𝑦 / 𝑥]𝜑 | ||
It is known that ax-13 2234 is logically redundant (see ax13w 2000 and the head comment of the section "Logical redundancy of ax-10--13"). More precisely, one can remove dependency on ax-13 2234 from every theorem in set.mm which is totally unbundled (i.e., has dv conditions on all setvar variables). Indeed, start with the existing proof, and replace any occurrence of ax-13 2234 with ax13w 2000. This section is an experiment to see in practice if (partially) unbundled versions of existing theorems can be proved more efficiently without ax-13 2234 (and using ax6v 1876 / ax6ev 1877 instead of ax-6 1875 / ax6e 2238, as is currently done). One reason to be optimistic is that the first few utility theorems using ax-13 2234 (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 2234, labeled bj-xxxv (we follow the proof of xxx but use ax6v 1876 and ax6ev 1877 instead of ax-6 1875 and ax6e 2238, and ax-5 1827 instead of ax13v 2235; 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 2234, so as to remove dependencies on ax-13 2234 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 2021, typically by replacing a non-free hypothesis with a dv condition (see bj-cbv3v2 31914 and following theorems). | ||
Theorem | bj-axc10v 31904* | Version of axc10 2240 with a dv condition, which does not require ax-13 2234. (Contributed by BJ, 14-Jun-2019.) (Proof modification is discouraged.) |
⊢ (∀𝑥(𝑥 = 𝑦 → ∀𝑥𝜑) → 𝜑) | ||
Theorem | bj-spimtv 31905* | Version of spimt 2241 with a dv condition, which does not require ax-13 2234. (Contributed by BJ, 14-Jun-2019.) (Proof modification is discouraged.) |
⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝑦 → (𝜑 → 𝜓))) → (∀𝑥𝜑 → 𝜓)) | ||
Theorem | bj-spimedv 31906* | Version of spimed 2243 with a dv condition, which does not require ax-13 2234. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.) |
⊢ (𝜒 → Ⅎ𝑥𝜑) & ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) ⇒ ⊢ (𝜒 → (𝜑 → ∃𝑥𝜓)) | ||
Theorem | bj-spimev 31907* | Version of spime 2244 with a dv condition, which does not require ax-13 2234. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) ⇒ ⊢ (𝜑 → ∃𝑥𝜓) | ||
Theorem | bj-spimvv 31908* | Version of spimv 2245 and spimv1 2101 with a dv condition, which does not require ax-13 2234. UPDATE: this is spimvw 1914. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) ⇒ ⊢ (∀𝑥𝜑 → 𝜓) | ||
Theorem | bj-spimevv 31909* | Version of spimev 2247 with a dv condition, which does not require ax-13 2234. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) ⇒ ⊢ (𝜑 → ∃𝑥𝜓) | ||
Theorem | bj-spvv 31910* | Version of spv 2248 with a dv condition, which does not require ax-13 2234. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥𝜑 → 𝜓) | ||
Theorem | bj-speiv 31911* | Version of spei 2249 with a dv condition, which does not require ax-13 2234 (neither ax-7 1922 nor ax-12 2034). (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ 𝜓 ⇒ ⊢ ∃𝑥𝜑 | ||
Theorem | bj-chvarv 31912* | Version of chvar 2250 with a dv condition, which does not require ax-13 2234. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ 𝜑 ⇒ ⊢ 𝜓 | ||
Theorem | bj-chvarvv 31913* | Version of chvarv 2251 with a dv condition, which does not require ax-13 2234. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ 𝜑 ⇒ ⊢ 𝜓 | ||
Theorem | bj-cbv3v2 31914* | Version of cbv3 2253 with two dv conditions, which does not require ax-11 2021 nor ax-13 2234. (Contributed by BJ, 24-Jun-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) ⇒ ⊢ (∀𝑥𝜑 → ∀𝑦𝜓) | ||
Theorem | bj-cbv3hv2 31915* | Version of cbv3h 2254 with two dv conditions, which does not require ax-11 2021 nor ax-13 2234. (Contributed by BJ, 24-Jun-2019.) (Proof modification is discouraged.) |
⊢ (𝜓 → ∀𝑥𝜓) & ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) ⇒ ⊢ (∀𝑥𝜑 → ∀𝑦𝜓) | ||
Theorem | bj-cbv1v 31916* | Version of cbv1 2255 with a dv condition, which does not require ax-13 2234. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑦𝜓) & ⊢ (𝜑 → Ⅎ𝑥𝜒) & ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 → 𝜒))) ⇒ ⊢ (𝜑 → (∀𝑥𝜓 → ∀𝑦𝜒)) | ||
Theorem | bj-cbv1hv 31917* | Version of cbv1h 2256 with a dv condition, which does not require ax-13 2234. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.) |
⊢ (𝜑 → (𝜓 → ∀𝑦𝜓)) & ⊢ (𝜑 → (𝜒 → ∀𝑥𝜒)) & ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 → 𝜒))) ⇒ ⊢ (∀𝑥∀𝑦𝜑 → (∀𝑥𝜓 → ∀𝑦𝜒)) | ||
Theorem | bj-cbv2hv 31918* | Version of cbv2h 2257 with a dv condition, which does not require ax-13 2234. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.) |
⊢ (𝜑 → (𝜓 → ∀𝑦𝜓)) & ⊢ (𝜑 → (𝜒 → ∀𝑥𝜒)) & ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))) ⇒ ⊢ (∀𝑥∀𝑦𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒)) | ||
Theorem | bj-cbv2v 31919* | Version of cbv2 2258 with a dv condition, which does not require ax-13 2234. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑦𝜓) & ⊢ (𝜑 → Ⅎ𝑥𝜒) & ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))) ⇒ ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒)) | ||
Theorem | bj-cbvalvv 31920* | Version of cbvalv 2261 with a dv condition, which does not require ax-13 2234. UPDATE: this is cbvalvw 1956 (which is proved with fewer axioms). (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓) | ||
Theorem | bj-cbvexvv 31921* | Version of cbvexv 2263 with a dv condition, which does not require ax-13 2234. UPDATE: this is cbvexvw 1957 (which is proved with fewer axioms). (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓) | ||
Theorem | bj-cbvaldv 31922* | Version of cbvald 2265 with a dv condition, which does not require ax-13 2234. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑦𝜓) & ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))) ⇒ ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒)) | ||
Theorem | bj-cbvexdv 31923* | Version of cbvexd 2266 with a dv condition, which does not require ax-13 2234. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑦𝜓) & ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))) ⇒ ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑦𝜒)) | ||
Theorem | bj-cbval2v 31924* | Version of cbval2 2267 with a dv condition, which does not require ax-13 2234. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑧𝜑 & ⊢ Ⅎ𝑤𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ Ⅎ𝑦𝜓 & ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑧∀𝑤𝜓) | ||
Theorem | bj-cbvex2v 31925* | Version of cbvex2 2268 with a dv condition, which does not require ax-13 2234. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑧𝜑 & ⊢ Ⅎ𝑤𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ Ⅎ𝑦𝜓 & ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑧∃𝑤𝜓) | ||
Theorem | bj-cbval2vv 31926* | Version of cbval2v 2273 with a dv condition, which does not require ax-13 2234. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.) |
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑧∀𝑤𝜓) | ||
Theorem | bj-cbvex2vv 31927* | Version of cbvex2v 2275 with a dv condition, which does not require ax-13 2234. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.) |
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑧∃𝑤𝜓) | ||
Theorem | bj-cbvaldvav 31928* | Version of cbvaldva 2269 with a dv condition, which does not require ax-13 2234. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.) |
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒)) | ||
Theorem | bj-cbvexdvav 31929* | Version of cbvexdva 2271 with a dv condition, which does not require ax-13 2234. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.) |
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑦𝜒)) | ||
Theorem | bj-cbvex4vv 31930* | Version of cbvex4v 2277 with a dv condition, which does not require ax-13 2234. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.) |
⊢ ((𝑥 = 𝑣 ∧ 𝑦 = 𝑢) → (𝜑 ↔ 𝜓)) & ⊢ ((𝑧 = 𝑓 ∧ 𝑤 = 𝑔) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (∃𝑥∃𝑦∃𝑧∃𝑤𝜑 ↔ ∃𝑣∃𝑢∃𝑓∃𝑔𝜒) | ||
Theorem | bj-equsalv 31931* | Version of equsal 2279 with a dv condition, which does not require ax-13 2234. See equsalvw 1918 for a version with two dv conditions requiring fewer axioms. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜓) | ||
Theorem | bj-equsalhv 31932* |
Version of equsalh 2280 with a dv condition, which does not require
ax-13 2234. Remark: this is the same as equsalhw 2109.
Remarks: equsexvw 1919 has been moved to Main; the theorem ax13lem2 2284 has a dv version which is a simple consequence of ax5e 1829; the theorems nfeqf2 2285, dveeq2 2286, nfeqf1 2287, dveeq1 2288, nfeqf 2289, axc9 2290, ax13 2237, have dv versions which are simple consequences of ax-5 1827. (Contributed by BJ, 14-Jun-2019.) (Proof modification is discouraged.) |
⊢ (𝜓 → ∀𝑥𝜓) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜓) | ||
Theorem | bj-axc11nv 31933* | Version of axc11n 2295 with a dv condition; instance of aevlem 1968. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥) | ||
Theorem | bj-aecomsv 31934* | Version of aecoms 2300 with a dv condition, provable from Tarski's FOL. The corresponding version of naecoms 2301 should not be very useful since ¬ ∀𝑥𝑥 = 𝑦, DV(x, y) is true when the universe has at least two objects (see bj-dtru 31985). (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → 𝜑) ⇒ ⊢ (∀𝑦 𝑦 = 𝑥 → 𝜑) | ||
Theorem | bj-axc11v 31935* | Version of axc11 2302 with a dv condition, which does not require ax-13 2234 nor ax-10 2006. Remark: the following theorems (hbae 2303, nfae 2304, hbnae 2305, nfnae 2306, hbnaes 2307) would need to be totally unbundled to be proved without ax-13 2234, hence would be simple consequences of ax-5 1827 or nfv 1830. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 → ∀𝑦𝜑)) | ||
Theorem | bj-dral1v 31936* | Version of dral1 2313 with a dv condition, which does not require ax-13 2234. Remark: the corresponding versions for dral2 2312 and drex2 2316 are instances of albidv 1836 and exbidv 1837 respectively. (Contributed by BJ, 17-Jun-2019.) (Proof modification is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 ↔ ∀𝑦𝜓)) | ||
Theorem | bj-drex1v 31937* | Version of drex1 2315 with a dv condition, which does not require ax-13 2234. (Contributed by BJ, 17-Jun-2019.) (Proof modification is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 𝑥 = 𝑦 → (∃𝑥𝜑 ↔ ∃𝑦𝜓)) | ||
Theorem | bj-drnf1v 31938* | Version of drnf1 2317 with a dv condition, which does not require ax-13 2234. (Contributed by BJ, 17-Jun-2019.) (Proof modification is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 𝑥 = 𝑦 → (Ⅎ𝑥𝜑 ↔ Ⅎ𝑦𝜓)) | ||
Theorem | bj-drnf2v 31939* | Version of drnf2 2318 with a dv condition, which does not require ax-13 2234. Could be labeled "nfbidv". Note that the version of axc15 2291 with a dv condition is actually ax12v2 2036 (up to adding a superfluous antecedent). (Contributed by BJ, 17-Jun-2019.) (Proof modification is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 𝑥 = 𝑦 → (Ⅎ𝑧𝜑 ↔ Ⅎ𝑧𝜓)) | ||
Theorem | bj-equs45fv 31940* | Version of equs45f 2338 with a dv condition, which does not require ax-13 2234. Note that the version of equs5 2339 with a dv condition is actually sb56 2136 (up to adding a superfluous antecedent). (Contributed by BJ, 11-Sep-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑)) | ||
Theorem | bj-sb2v 31941* | Version of sb2 2340 with a dv condition, which does not require ax-13 2234. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.) |
⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → [𝑦 / 𝑥]𝜑) | ||
Theorem | bj-stdpc4v 31942* | Version of stdpc4 2341 with a dv condition, which does not require ax-13 2234. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.) |
⊢ (∀𝑥𝜑 → [𝑦 / 𝑥]𝜑) | ||
Theorem | bj-2stdpc4v 31943* | Version of 2stdpc4 2342 with a dv condition, which does not require ax-13 2234. (Contributed by BJ, 24-Jun-2019.) (Proof modification is discouraged.) |
⊢ (∀𝑥∀𝑦𝜑 → [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) | ||
Theorem | bj-sb3v 31944* | Version of sb3 2343 with a dv condition, which does not require ax-13 2234. This allows to remove ax-13 2234 from sb5 2418 (see bj-sb5 31956). (Contributed by BJ, 24-Jun-2019.) (Proof modification is discouraged.) |
⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → [𝑦 / 𝑥]𝜑) | ||
Theorem | bj-sb4v 31945* | Version of sb4 2344 with a dv condition, which does not require ax-13 2234. (Contributed by BJ, 23-Jun-2019.) Together with bj-sb2v 31941, this allosw to remove ax-13 2234 from sb6 2417 (see bj-sb6 31955). Note that this subsumes the version of sb4b 2346 with a dv condition. (Proof modification is discouraged.) |
⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)) | ||
Theorem | bj-hbs1 31946* | Version of hbsb2 2347 with a dv condition, which does not require ax-13 2234, and removal of ax-13 2234 from hbs1 2424. (Contributed by BJ, 23-Jun-2019.) (Proof modification is discouraged.) |
⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑) | ||
Theorem | bj-nfs1v 31947* | Version of nfsb2 2348 with a dv condition, which does not require ax-13 2234, and removal of ax-13 2234 from nfs1v 2425. (Contributed by BJ, 24-Jun-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥[𝑦 / 𝑥]𝜑 | ||
Theorem | bj-hbsb2av 31948* | Version of hbsb2a 2349 with a dv condition, which does not require ax-13 2234. (Contributed by BJ, 11-Sep-2019.) (Proof modification is discouraged.) |
⊢ ([𝑦 / 𝑥]∀𝑦𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑) | ||
Theorem | bj-hbsb3v 31949* | Version of hbsb3 2352 with a dv condition, which does not require ax-13 2234. (Remark: the unbundled version of nfs1 2353 is given by bj-nfs1v 31947.) (Contributed by BJ, 11-Sep-2019.) (Proof modification is discouraged.) |
⊢ (𝜑 → ∀𝑦𝜑) ⇒ ⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑) | ||
Theorem | bj-equsb1v 31950* | Version of equsb1 2356 with a dv condition, which does not require ax-13 2234. (Contributed by BJ, 11-Sep-2019.) (Proof modification is discouraged.) |
⊢ [𝑦 / 𝑥]𝑥 = 𝑦 | ||
Theorem | bj-sbftv 31951* | Version of sbft 2367 with a dv condition, which does not require ax-13 2234. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.) |
⊢ (Ⅎ𝑥𝜑 → ([𝑦 / 𝑥]𝜑 ↔ 𝜑)) | ||
Theorem | bj-sbfv 31952* | Version of sbf 2368 with a dv condition, which does not require ax-13 2234. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜑) | ||
Theorem | bj-sbfvv 31953* | Version of sbf 2368 with two dv conditions, which does not require ax-10 2006 nor ax-13 2234. (Contributed by BJ, 1-May-2021.) (Proof modification is discouraged.) |
⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜑) | ||
Theorem | bj-sbtv 31954* | Version of sbt 2407 with a dv condition, which does not require ax-13 2234. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.) |
⊢ 𝜑 ⇒ ⊢ [𝑦 / 𝑥]𝜑 | ||
Theorem | bj-sb6 31955* | Remove dependency on ax-13 2234 from sb6 2417. (Contributed by BJ, 11-Sep-2019.) (Proof modification is discouraged.) |
⊢ ([𝑦 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑)) | ||
Theorem | bj-sb5 31956* | Remove dependency on ax-13 2234 from sb5 2418. (Contributed by BJ, 11-Sep-2019.) (Proof modification is discouraged.) |
⊢ ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) | ||
Theorem | bj-axext3 31957* | Remove dependency on ax-13 2234 from axext3 2592. (Contributed by BJ, 12-Jul-2019.) (Proof modification is discouraged.) |
⊢ (∀𝑧(𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦) → 𝑥 = 𝑦) | ||
Theorem | bj-axext4 31958* | Remove dependency on ax-13 2234 from axext4 2594. (Contributed by BJ, 6-Oct-2019.) (Proof modification is discouraged.) |
⊢ (𝑥 = 𝑦 ↔ ∀𝑧(𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦)) | ||
Theorem | bj-hbab1 31959* | Remove dependency on ax-13 2234 from hbab1 2599. (Contributed by BJ, 23-Jun-2019.) (Proof modification is discouraged.) |
⊢ (𝑦 ∈ {𝑥 ∣ 𝜑} → ∀𝑥 𝑦 ∈ {𝑥 ∣ 𝜑}) | ||
Theorem | bj-nfsab1 31960* | Remove dependency on ax-13 2234 from nfsab1 2600. (Contributed by BJ, 23-Jun-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥 𝑦 ∈ {𝑥 ∣ 𝜑} | ||
Theorem | bj-abeq2 31961* | Remove dependency on ax-13 2234 from abeq2 2719. (Contributed by BJ, 23-Jun-2019.) (Proof modification is discouraged.) |
⊢ (𝐴 = {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝜑)) | ||
Theorem | bj-abeq1 31962* | Remove dependency on ax-13 2234 from abeq1 2720. Remark: the theorems abeq2i 2722, abeq1i 2723, abeq2d 2721 do not use ax-11 2021 or ax-13 2234. (Contributed by BJ, 23-Jun-2019.) (Proof modification is discouraged.) |
⊢ ({𝑥 ∣ 𝜑} = 𝐴 ↔ ∀𝑥(𝜑 ↔ 𝑥 ∈ 𝐴)) | ||
Theorem | bj-abbi 31963 | Remove dependency on ax-13 2234 from abbi 2724. (Contributed by BJ, 23-Jun-2019.) (Proof modification is discouraged.) |
⊢ (∀𝑥(𝜑 ↔ 𝜓) ↔ {𝑥 ∣ 𝜑} = {𝑥 ∣ 𝜓}) | ||
Theorem | bj-abbi2i 31964* | Remove dependency on ax-13 2234 from abbi2i 2725. (Contributed by BJ, 23-Jun-2019.) (Proof modification is discouraged.) |
⊢ (𝑥 ∈ 𝐴 ↔ 𝜑) ⇒ ⊢ 𝐴 = {𝑥 ∣ 𝜑} | ||
Theorem | bj-abbii 31965 | Remove dependency on ax-13 2234 from abbii 2726. (Contributed by BJ, 23-Jun-2019.) (Proof modification is discouraged.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ {𝑥 ∣ 𝜑} = {𝑥 ∣ 𝜓} | ||
Theorem | bj-abbid 31966 | Remove dependency on ax-13 2234 from abbid 2727. (Contributed by BJ, 23-Jun-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {𝑥 ∣ 𝜓} = {𝑥 ∣ 𝜒}) | ||
Theorem | bj-abbidv 31967* | Remove dependency on ax-13 2234 from abbidv 2728. (Contributed by BJ, 23-Jun-2019.) (Proof modification is discouraged.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {𝑥 ∣ 𝜓} = {𝑥 ∣ 𝜒}) | ||
Theorem | bj-abbi2dv 31968* | Remove dependency on ax-13 2234 from abbi2dv 2729. (Contributed by BJ, 23-Jun-2019.) (Proof modification is discouraged.) |
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝜓)) ⇒ ⊢ (𝜑 → 𝐴 = {𝑥 ∣ 𝜓}) | ||
Theorem | bj-abbi1dv 31969* | Remove dependency on ax-13 2234 from abbi1dv 2730. (Contributed by BJ, 23-Jun-2019.) (Proof modification is discouraged.) |
⊢ (𝜑 → (𝜓 ↔ 𝑥 ∈ 𝐴)) ⇒ ⊢ (𝜑 → {𝑥 ∣ 𝜓} = 𝐴) | ||
Theorem | bj-abid2 31970* | Remove dependency on ax-13 2234 from abid2 2732. (Contributed by BJ, 23-Jun-2019.) (Proof modification is discouraged.) |
⊢ {𝑥 ∣ 𝑥 ∈ 𝐴} = 𝐴 | ||
Theorem | bj-clabel 31971* | Remove dependency on ax-13 2234 from clabel 2736 (note the absence of DV conditions among variables in the LHS). (Contributed by BJ, 23-Jun-2019.) (Proof modification is discouraged.) |
⊢ ({𝑥 ∣ 𝜑} ∈ 𝐴 ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ ∀𝑥(𝑥 ∈ 𝑦 ↔ 𝜑))) | ||
Theorem | bj-sbab 31972* | Remove dependency on ax-13 2234 from sbab 2737 (note the absence of DV conditions among variables in the LHS). (Contributed by BJ, 23-Jun-2019.) (Proof modification is discouraged.) |
⊢ (𝑥 = 𝑦 → 𝐴 = {𝑧 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝐴}) | ||
Theorem | bj-nfab1 31973 | Remove dependency on ax-13 2234 from nfab1 2753 (note the absence of DV conditions). (Contributed by BJ, 6-Oct-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥{𝑥 ∣ 𝜑} | ||
Theorem | bj-vjust 31974 | Remove dependency on ax-13 2234 from vjust 3174 (note the absence of DV conditions). Soundness justification theorem for df-v 3175. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.) |
⊢ {𝑥 ∣ 𝑥 = 𝑥} = {𝑦 ∣ 𝑦 = 𝑦} | ||
Theorem | bj-cdeqab 31975* | Remove dependency on ax-13 2234 from cdeqab 3392. (Contributed by BJ, 6-Oct-2019.) (Proof modification is discouraged.) |
⊢ CondEq(𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ CondEq(𝑥 = 𝑦 → {𝑧 ∣ 𝜑} = {𝑧 ∣ 𝜓}) | ||
Theorem | bj-axrep1 31976* | Remove dependency on ax-13 2234 from axrep1 4700. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.) |
⊢ ∃𝑥(∃𝑦∀𝑧(𝜑 → 𝑧 = 𝑦) → ∀𝑧(𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ 𝜑))) | ||
Theorem | bj-axrep2 31977* | Remove dependency on ax-13 2234 from axrep2 4701. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.) |
⊢ ∃𝑥(∃𝑦∀𝑧(𝜑 → 𝑧 = 𝑦) → ∀𝑧(𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦𝜑))) | ||
Theorem | bj-axrep3 31978* | Remove dependency on ax-13 2234 from axrep3 4702. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.) |
⊢ ∃𝑥(∃𝑦∀𝑧(𝜑 → 𝑧 = 𝑦) → ∀𝑧(𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑤 ∧ ∀𝑦𝜑))) | ||
Theorem | bj-axrep4 31979* | Remove dependency on ax-13 2234 from axrep4 4703. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑧𝜑 ⇒ ⊢ (∀𝑥∃𝑧∀𝑦(𝜑 → 𝑦 = 𝑧) → ∃𝑧∀𝑦(𝑦 ∈ 𝑧 ↔ ∃𝑥(𝑥 ∈ 𝑤 ∧ 𝜑))) | ||
Theorem | bj-axrep5 31980* | Remove dependency on ax-13 2234 from axrep5 4704. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑧𝜑 ⇒ ⊢ (∀𝑥(𝑥 ∈ 𝑤 → ∃𝑧∀𝑦(𝜑 → 𝑦 = 𝑧)) → ∃𝑧∀𝑦(𝑦 ∈ 𝑧 ↔ ∃𝑥(𝑥 ∈ 𝑤 ∧ 𝜑))) | ||
Theorem | bj-axsep 31981* | Remove dependency on ax-13 2234 from axsep 4708. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.) |
⊢ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑)) | ||
Theorem | bj-nalset 31982* | Remove dependency on ax-13 2234 from nalset 4723. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.) |
⊢ ¬ ∃𝑥∀𝑦 𝑦 ∈ 𝑥 | ||
Theorem | bj-zfpow 31983* | Remove dependency on ax-13 2234 from zfpow 4770. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.) |
⊢ ∃𝑥∀𝑦(∀𝑥(𝑥 ∈ 𝑦 → 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥) | ||
Theorem | bj-el 31984* | Remove dependency on ax-13 2234 from el 4773. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.) |
⊢ ∃𝑦 𝑥 ∈ 𝑦 | ||
Theorem | bj-dtru 31985* | Remove dependency on ax-13 2234 from dtru 4783. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.) |
⊢ ¬ ∀𝑥 𝑥 = 𝑦 | ||
Theorem | bj-axc16b 31986* | Remove dependency on ax-13 2234 from axc16b 4784. (Contributed by BJ, 16-Jul-2019.) (Proof modification is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑥𝜑)) | ||
Theorem | bj-eunex 31987 | Remove dependency on ax-13 2234 from eunex 4785. (Contributed by BJ, 16-Jul-2019.) (Proof modification is discouraged.) |
⊢ (∃!𝑥𝜑 → ∃𝑥 ¬ 𝜑) | ||
Theorem | bj-dtrucor 31988* | Remove dependency on ax-13 2234 from dtrucor 4827. (Contributed by BJ, 16-Jul-2019.) (Proof modification is discouraged.) |
⊢ 𝑥 = 𝑦 ⇒ ⊢ 𝑥 ≠ 𝑦 | ||
Theorem | bj-dtrucor2v 31989* | Version of dtrucor2 4828 with a dv condition, which does not require ax-13 2234 (nor ax-4 1728, ax-5 1827, ax-7 1922, ax-12 2034). (Contributed by BJ, 16-Jul-2019.) (Proof modification is discouraged.) |
⊢ (𝑥 = 𝑦 → 𝑥 ≠ 𝑦) ⇒ ⊢ (𝜑 ∧ ¬ 𝜑) | ||
Theorem | bj-dvdemo1 31990* | Remove dependency on ax-13 2234 from dvdemo1 4829 (this removal is noteworthy since dvdemo1 4829 and dvdemo2 4830 illustrate the phenomenon of bundling). (Contributed by BJ, 16-Jul-2019.) (Proof modification is discouraged.) |
⊢ ∃𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑥) | ||
Theorem | bj-dvdemo2 31991* | Remove dependency on ax-13 2234 from dvdemo2 4830 (this removal is noteworthy since dvdemo1 4829 and dvdemo2 4830 illustrate the phenomenon of bundling). (Contributed by BJ, 16-Jul-2019.) (Proof modification is discouraged.) |
⊢ ∃𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑥) | ||
Typically, these are biconditional versions of theorems in the main part which are formulated as implications. They could be added after said implication, or sometimes replace it (by "inlining" it). This could also be done for hba1 2137, hbe1 2008, hbn1 2007, modal-5 2019. | ||
Theorem | bj-sb3b 31992 | Simplified definition of substitution when variables are distinct. This is to sb3 2343 what sb4b 2346 is to sb4 2344. Actually, one may keep only bj-sb3b 31992 and sb4b 2346 in the database, renaming them sb3 and sb4. (Contributed by BJ, 6-Oct-2018.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) | ||
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 31993 | Biconditional version of a form of hbae 2303 with commuted quantifiers, not requiring ax-11 2021. (Contributed by BJ, 12-Dec-2019.) (Proof modification is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 ↔ ∀𝑥∀𝑧 𝑥 = 𝑦) | ||
Theorem | bj-hbaeb 31994 | Biconditional version of hbae 2303. (Contributed by BJ, 6-Oct-2018.) (Proof modification is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 ↔ ∀𝑧∀𝑥 𝑥 = 𝑦) | ||
Theorem | bj-hbnaeb 31995 | Biconditional version of hbnae 2305 (to replace it?). (Contributed by BJ, 6-Oct-2018.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 ↔ ∀𝑧 ¬ ∀𝑥 𝑥 = 𝑦) | ||
Theorem | bj-dvv 31996 | A special instance of bj-hbaeb2 31993. 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 31748), then they should be added to the database. The present case is similar. Similar additions can be done regarding equsex 2281 (and equsalh 2280 and equsexh 2283). Even if only one of these two theorems holds, it should be added to the database. | ||
Theorem | bj-equsal1t 31997 | Duplication of wl-equsal1t 32506, with shorter proof. Note: wl-equsalcom 32507 is also interesting. (Contributed by BJ, 6-Oct-2018.) |
⊢ (Ⅎ𝑥𝜑 → (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜑)) | ||
Theorem | bj-equsal1ti 31998 | Inference associated with bj-equsal1t 31997. (Contributed by BJ, 30-Sep-2018.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜑) | ||
Theorem | bj-equsal1 31999 | One direction of equsal 2279. (Contributed by BJ, 30-Sep-2018.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) ⇒ ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → 𝜓) | ||
Theorem | bj-equsal2 32000 | One direction of equsal 2279. (Contributed by BJ, 30-Sep-2018.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) ⇒ ⊢ (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜓)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |