Home | Metamath
Proof Explorer Theorem List (p. 342 of 449) | < 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-28687) |
Hilbert Space Explorer
(28688-30210) |
Users' Mathboxes
(30211-44897) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | bj-cbv3ta 34101 | Closed form of cbv3 2409. (Contributed by BJ, 2-May-2019.) |
⊢ (∀𝑥∀𝑦(𝑥 = 𝑦 → (𝜑 → 𝜓)) → ((∀𝑦(∃𝑥𝜓 → 𝜓) ∧ ∀𝑥(𝜑 → ∀𝑦𝜑)) → (∀𝑥𝜑 → ∀𝑦𝜓))) | ||
Theorem | bj-cbv3tb 34102 | Closed form of cbv3 2409. (Contributed by BJ, 2-May-2019.) |
⊢ (∀𝑥∀𝑦(𝑥 = 𝑦 → (𝜑 → 𝜓)) → ((∀𝑦Ⅎ𝑥𝜓 ∧ ∀𝑥Ⅎ𝑦𝜑) → (∀𝑥𝜑 → ∀𝑦𝜓))) | ||
Theorem | bj-hbsb3t 34103 | A theorem close to a closed form of hbsb3 2520. (Contributed by BJ, 2-May-2019.) |
⊢ (∀𝑥(𝜑 → ∀𝑦𝜑) → ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑)) | ||
Theorem | bj-hbsb3 34104 | Shorter proof of hbsb3 2520. (Contributed by BJ, 2-May-2019.) (Proof modification is discouraged.) |
⊢ (𝜑 → ∀𝑦𝜑) ⇒ ⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑) | ||
Theorem | bj-nfs1t 34105 | A theorem close to a closed form of nfs1 2521. (Contributed by BJ, 2-May-2019.) |
⊢ (∀𝑥(𝜑 → ∀𝑦𝜑) → Ⅎ𝑥[𝑦 / 𝑥]𝜑) | ||
Theorem | bj-nfs1t2 34106 | A theorem close to a closed form of nfs1 2521. (Contributed by BJ, 2-May-2019.) |
⊢ (∀𝑥Ⅎ𝑦𝜑 → Ⅎ𝑥[𝑦 / 𝑥]𝜑) | ||
Theorem | bj-nfs1 34107 | Shorter proof of nfs1 2521 (three essential steps instead of four). (Contributed by BJ, 2-May-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ Ⅎ𝑥[𝑦 / 𝑥]𝜑 | ||
It is known that ax-13 2384 is logically redundant (see ax13w 2134 and the head comment of the section "Logical redundancy of ax-10--13"). More precisely, one can remove dependency on ax-13 2384 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 2384 with ax13w 2134. This section is an experiment to see in practice if (partially) unbundled versions of existing theorems can be proved more efficiently without ax-13 2384 (and using ax6v 1965 / ax6ev 1966 instead of ax-6 1964 / ax6e 2395, as is currently done). One reason to be optimistic is that the first few utility theorems using ax-13 2384 (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 2384, labeled bj-xxxv (we follow the proof of xxx but use ax6v 1965 and ax6ev 1966 instead of ax-6 1964 and ax6e 2395, and ax-5 1905 instead of ax13v 2385; 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 2384, so as to remove dependencies on ax-13 2384 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 2154, typically by replacing a nonfree hypothesis with a disjoint variable condition (see cbv3v2 2236 and following theorems). | ||
Theorem | bj-axc10v 34108* | Version of axc10 2397 with a disjoint variable condition, which does not require ax-13 2384. (Contributed by BJ, 14-Jun-2019.) (Proof modification is discouraged.) |
⊢ (∀𝑥(𝑥 = 𝑦 → ∀𝑥𝜑) → 𝜑) | ||
Theorem | bj-spimtv 34109* | Version of spimt 2398 with a disjoint variable condition, which does not require ax-13 2384. (Contributed by BJ, 14-Jun-2019.) (Proof modification is discouraged.) |
⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝑦 → (𝜑 → 𝜓))) → (∀𝑥𝜑 → 𝜓)) | ||
Theorem | bj-cbv3hv2 34110* | Version of cbv3h 2418 with two disjoint variable conditions, which does not require ax-11 2154 nor ax-13 2384. (Contributed by BJ, 24-Jun-2019.) (Proof modification is discouraged.) |
⊢ (𝜓 → ∀𝑥𝜓) & ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) ⇒ ⊢ (∀𝑥𝜑 → ∀𝑦𝜓) | ||
Theorem | bj-cbv1hv 34111* | Version of cbv1h 2419 with a disjoint variable condition, which does not require ax-13 2384. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.) |
⊢ (𝜑 → (𝜓 → ∀𝑦𝜓)) & ⊢ (𝜑 → (𝜒 → ∀𝑥𝜒)) & ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 → 𝜒))) ⇒ ⊢ (∀𝑥∀𝑦𝜑 → (∀𝑥𝜓 → ∀𝑦𝜒)) | ||
Theorem | bj-cbv2hv 34112* | Version of cbv2h 2420 with a disjoint variable condition, which does not require ax-13 2384. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.) |
⊢ (𝜑 → (𝜓 → ∀𝑦𝜓)) & ⊢ (𝜑 → (𝜒 → ∀𝑥𝜒)) & ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))) ⇒ ⊢ (∀𝑥∀𝑦𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒)) | ||
Theorem | bj-cbv2v 34113* | Version of cbv2 2417 with a disjoint variable condition, which does not require ax-13 2384. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑦𝜓) & ⊢ (𝜑 → Ⅎ𝑥𝜒) & ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))) ⇒ ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒)) | ||
Theorem | bj-cbvaldv 34114* | Version of cbvald 2422 with a disjoint variable condition, which does not require ax-13 2384. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑦𝜓) & ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))) ⇒ ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒)) | ||
Theorem | bj-cbvexdv 34115* | Version of cbvexd 2423 with a disjoint variable condition, which does not require ax-13 2384. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑦𝜓) & ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))) ⇒ ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑦𝜒)) | ||
Theorem | bj-cbval2vv 34116* | Version of cbval2vv 2429 with a disjoint variable condition, which does not require ax-13 2384. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.) |
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑧∀𝑤𝜓) | ||
Theorem | bj-cbvex2vv 34117* | Version of cbvex2vv 2430 with a disjoint variable condition, which does not require ax-13 2384. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.) |
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑧∃𝑤𝜓) | ||
Theorem | bj-cbvaldvav 34118* | Version of cbvaldva 2424 with a disjoint variable condition, which does not require ax-13 2384. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.) |
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒)) | ||
Theorem | bj-cbvexdvav 34119* | Version of cbvexdva 2425 with a disjoint variable condition, which does not require ax-13 2384. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.) |
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑦𝜒)) | ||
Theorem | bj-cbvex4vv 34120* | Version of cbvex4v 2431 with a disjoint variable condition, which does not require ax-13 2384. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.) |
⊢ ((𝑥 = 𝑣 ∧ 𝑦 = 𝑢) → (𝜑 ↔ 𝜓)) & ⊢ ((𝑧 = 𝑓 ∧ 𝑤 = 𝑔) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (∃𝑥∃𝑦∃𝑧∃𝑤𝜑 ↔ ∃𝑣∃𝑢∃𝑓∃𝑔𝜒) | ||
Theorem | bj-equsalhv 34121* |
Version of equsalh 2436 with a disjoint variable condition, which
does not
require ax-13 2384. Remark: this is the same as equsalhw 2293. TODO:
delete after moving the following paragraph somewhere.
Remarks: equsexvw 2005 has been moved to Main; the theorem ax13lem2 2388 has a dv version which is a simple consequence of ax5e 1907; the theorems nfeqf2 2389, dveeq2 2390, nfeqf1 2391, dveeq1 2392, nfeqf 2393, axc9 2394, ax13 2387, have dv versions which are simple consequences of ax-5 1905. (Contributed by BJ, 14-Jun-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜓 → ∀𝑥𝜓) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜓) | ||
Theorem | bj-axc11nv 34122* | Version of axc11n 2442 with a disjoint variable condition; instance of aevlem 2054. TODO: delete after checking surrounding theorems. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥) | ||
Theorem | bj-aecomsv 34123* | Version of aecoms 2444 with a disjoint variable condition, provable from Tarski's FOL. The corresponding version of naecoms 2445 should not be very useful since ¬ ∀𝑥𝑥 = 𝑦, DV (𝑥, 𝑦) is true when the universe has at least two objects (see dtru 5262). (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → 𝜑) ⇒ ⊢ (∀𝑦 𝑦 = 𝑥 → 𝜑) | ||
Theorem | bj-axc11v 34124* | Version of axc11 2446 with a disjoint variable condition, which does not require ax-13 2384 nor ax-10 2139. Remark: the following theorems (hbae 2447, nfae 2449, hbnae 2448, nfnae 2450, hbnaes 2451) would need to be totally unbundled to be proved without ax-13 2384, hence would be simple consequences of ax-5 1905 or nfv 1909. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 → ∀𝑦𝜑)) | ||
Theorem | bj-drnf2v 34125* | Version of drnf2 2460 with a disjoint variable condition, which does not require ax-10 2139, ax-11 2154, ax-12 2170, ax-13 2384. Instance of nfbidv 1917. Note that the version of axc15 2438 with a disjoint variable condition is actually ax12v2 2172 (up to adding a superfluous antecedent). (Contributed by BJ, 17-Jun-2019.) (Proof modification is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 𝑥 = 𝑦 → (Ⅎ𝑧𝜑 ↔ Ⅎ𝑧𝜓)) | ||
Theorem | bj-equs45fv 34126* | Version of equs45f 2476 with a disjoint variable condition, which does not require ax-13 2384. Note that the version of equs5 2477 with a disjoint variable condition is actually sb56 2271 (up to adding a superfluous antecedent). (Contributed by BJ, 11-Sep-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑)) | ||
Theorem | bj-hbs1 34127* | Version of hbsb2 2515 with a disjoint variable condition, which does not require ax-13 2384, and removal of ax-13 2384 from hbs1 2268. (Contributed by BJ, 23-Jun-2019.) (Proof modification is discouraged.) |
⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑) | ||
Theorem | bj-nfs1v 34128* | Version of nfsb2 2516 with a disjoint variable condition, which does not require ax-13 2384, and removal of ax-13 2384 from nfs1v 2267. (Contributed by BJ, 24-Jun-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥[𝑦 / 𝑥]𝜑 | ||
Theorem | bj-hbsb2av 34129* | Version of hbsb2a 2517 with a disjoint variable condition, which does not require ax-13 2384. (Contributed by BJ, 11-Sep-2019.) (Proof modification is discouraged.) |
⊢ ([𝑦 / 𝑥]∀𝑦𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑) | ||
Theorem | bj-hbsb3v 34130* | Version of hbsb3 2520 with a disjoint variable condition, which does not require ax-13 2384. (Remark: the unbundled version of nfs1 2521 is given by bj-nfs1v 34128.) (Contributed by BJ, 11-Sep-2019.) (Proof modification is discouraged.) |
⊢ (𝜑 → ∀𝑦𝜑) ⇒ ⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑) | ||
Theorem | bj-nfsab1 34131* | Remove dependency on ax-13 2384 from nfsab1 2806. UPDATE / TODO: nfsab1 2806 does not use ax-13 2384 either anymore; bj-nfsab1 34131 is shorter than nfsab1 2806 but uses ax-12 2170. (Contributed by BJ, 23-Jun-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥 𝑦 ∈ {𝑥 ∣ 𝜑} | ||
Theorem | bj-dtru 34132* |
Remove dependency on ax-13 2384 from dtru 5262. (Contributed by BJ,
31-May-2019.)
TODO: This predates the removal of ax-13 2384 in dtru 5262. But actually, sn-dtru 39102 is better than either, so move it to Main with sn-el 39101 (and determine whether bj-dtru 34132 should be kept as ALT or deleted). (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ¬ ∀𝑥 𝑥 = 𝑦 | ||
Theorem | bj-dtrucor2v 34133* | Version of dtrucor2 5264 with a disjoint variable condition, which does not require ax-13 2384 (nor ax-4 1804, ax-5 1905, ax-7 2009, ax-12 2170). (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 34134 | Biconditional version of a form of hbae 2447 with commuted quantifiers, not requiring ax-11 2154. (Contributed by BJ, 12-Dec-2019.) (Proof modification is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 ↔ ∀𝑥∀𝑧 𝑥 = 𝑦) | ||
Theorem | bj-hbaeb 34135 | Biconditional version of hbae 2447. (Contributed by BJ, 6-Oct-2018.) (Proof modification is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 ↔ ∀𝑧∀𝑥 𝑥 = 𝑦) | ||
Theorem | bj-hbnaeb 34136 | Biconditional version of hbnae 2448 (to replace it?). (Contributed by BJ, 6-Oct-2018.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 ↔ ∀𝑧 ¬ ∀𝑥 𝑥 = 𝑦) | ||
Theorem | bj-dvv 34137 | A special instance of bj-hbaeb2 34134. 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 33917), then they should be added to the database. The present case is similar. Similar additions can be done regarding equsex 2434 (and equsalh 2436 and equsexh 2437). Even if only one of these two theorems holds, it should be added to the database. | ||
Theorem | bj-equsal1t 34138 | Duplication of wl-equsal1t 34773, with shorter proof. If one imposes a disjoint variable condition on x,y , then one can use alequexv 2001 and reduce axiom dependencies, and similarly for the following theorems. Note: wl-equsalcom 34774 is also interesting. (Contributed by BJ, 6-Oct-2018.) |
⊢ (Ⅎ𝑥𝜑 → (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜑)) | ||
Theorem | bj-equsal1ti 34139 | Inference associated with bj-equsal1t 34138. (Contributed by BJ, 30-Sep-2018.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜑) | ||
Theorem | bj-equsal1 34140 | One direction of equsal 2433. (Contributed by BJ, 30-Sep-2018.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) ⇒ ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → 𝜓) | ||
Theorem | bj-equsal2 34141 | One direction of equsal 2433. (Contributed by BJ, 30-Sep-2018.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) ⇒ ⊢ (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜓)) | ||
Theorem | bj-equsal 34142 | Shorter proof of equsal 2433. (Contributed by BJ, 30-Sep-2018.) Proof modification is discouraged to avoid using equsal 2433, 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 34143 | Closed form of stdpc5 2201. (Possible to place it before 19.21t 2199 and use it to prove 19.21t 2199). (Contributed by BJ, 15-Sep-2018.) (Proof modification is discouraged.) |
⊢ (Ⅎ𝑥𝜑 → (∀𝑥(𝜑 → 𝜓) → (𝜑 → ∀𝑥𝜓))) | ||
Theorem | bj-stdpc5 34144 | More direct proof of stdpc5 2201. (Contributed by BJ, 15-Sep-2018.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (∀𝑥(𝜑 → 𝜓) → (𝜑 → ∀𝑥𝜓)) | ||
Theorem | 2stdpc5 34145 | A double stdpc5 2201 (one direction of PM*11.3). See also 2stdpc4 2069 and 19.21vv 40699. (Contributed by BJ, 15-Sep-2018.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (∀𝑥∀𝑦(𝜑 → 𝜓) → (𝜑 → ∀𝑥∀𝑦𝜓)) | ||
Theorem | bj-19.21t0 34146 | Proof of 19.21t 2199 from stdpc5t 34143. (Contributed by BJ, 15-Sep-2018.) (Proof modification is discouraged.) |
⊢ (Ⅎ𝑥𝜑 → (∀𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥𝜓))) | ||
Theorem | exlimii 34147 | Inference associated with exlimi 2210. Inferring a theorem when it is implied by an antecedent which may be true. (Contributed by BJ, 15-Sep-2018.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝜑 → 𝜓) & ⊢ ∃𝑥𝜑 ⇒ ⊢ 𝜓 | ||
Theorem | ax11-pm 34148 | Proof of ax-11 2154 similar to PM's proof of alcom 2156 (PM*11.2). For a proof closer to PM's proof, see ax11-pm2 34152. Axiom ax-11 2154 is used in the proof only through nfa2 2169. (Contributed by BJ, 15-Sep-2018.) (Proof modification is discouraged.) |
⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑) | ||
Theorem | ax6er 34149 | Commuted form of ax6e 2395. (Could be placed right after ax6e 2395). (Contributed by BJ, 15-Sep-2018.) |
⊢ ∃𝑥 𝑦 = 𝑥 | ||
Theorem | exlimiieq1 34150 | Inferring a theorem when it is implied by an equality which may be true. (Contributed by BJ, 30-Sep-2018.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝑥 = 𝑦 → 𝜑) ⇒ ⊢ 𝜑 | ||
Theorem | exlimiieq2 34151 | 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 34152* | Proof of ax-11 2154 from the standard axioms of predicate calculus, similar to PM's proof of alcom 2156 (PM*11.2). This proof requires that 𝑥 and 𝑦 be distinct. Axiom ax-11 2154 is used in the proof only through nfal 2336, nfsb 2559, sbal 2159, sb8 2553. See also ax11-pm 34148. (Contributed by BJ, 15-Sep-2018.) (Proof modification is discouraged.) |
⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑) | ||
Theorem | bj-sbsb 34153 | Biconditional showing two possible (dual) definitions of substitution df-sb 2064 not using dummy variables. (Contributed by BJ, 19-Mar-2021.) |
⊢ (((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) ↔ (∀𝑥(𝑥 = 𝑦 → 𝜑) ∨ (𝑥 = 𝑦 ∧ 𝜑))) | ||
Theorem | bj-dfsb2 34154 | Alternate (dual) definition of substitution df-sb 2064 not using dummy variables. (Contributed by BJ, 19-Mar-2021.) |
⊢ ([𝑦 / 𝑥]𝜑 ↔ (∀𝑥(𝑥 = 𝑦 → 𝜑) ∨ (𝑥 = 𝑦 ∧ 𝜑))) | ||
Theorem | bj-sbf3 34155 | Substitution has no effect on a bound variable (existential quantifier case); see sbf2 2265. (Contributed by BJ, 2-May-2019.) |
⊢ ([𝑦 / 𝑥]∃𝑥𝜑 ↔ ∃𝑥𝜑) | ||
Theorem | bj-sbf4 34156 | Substitution has no effect on a bound variable (nonfreeness case); see sbf2 2265. (Contributed by BJ, 2-May-2019.) |
⊢ ([𝑦 / 𝑥]Ⅎ𝑥𝜑 ↔ Ⅎ𝑥𝜑) | ||
Theorem | bj-sbnf 34157* | Move nonfree predicate in and out of substitution; see sbal 2159 and sbex 2282. (Contributed by BJ, 2-May-2019.) |
⊢ ([𝑧 / 𝑦]Ⅎ𝑥𝜑 ↔ Ⅎ𝑥[𝑧 / 𝑦]𝜑) | ||
Theorem | bj-eu3f 34158* | Version of eu3v 2649 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 2649. (Contributed by NM, 8-Jul-1994.) (Proof shortened by BJ, 31-May-2019.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦))) | ||
Miscellaneous theorems of first-order logic. | ||
Theorem | bj-sblem1 34159* | Lemma for substitution. (Contributed by BJ, 23-Jul-2023.) |
⊢ (∀𝑥(𝜑 → (𝜓 → 𝜒)) → (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → 𝜒))) | ||
Theorem | bj-sblem2 34160* | Lemma for substitution. (Contributed by BJ, 23-Jul-2023.) |
⊢ (∀𝑥(𝜑 → (𝜒 → 𝜓)) → ((∃𝑥𝜑 → 𝜒) → ∀𝑥(𝜑 → 𝜓))) | ||
Theorem | bj-sblem 34161* | Lemma for substitution. (Contributed by BJ, 23-Jul-2023.) |
⊢ (∀𝑥(𝜑 → (𝜓 ↔ 𝜒)) → (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜒))) | ||
Theorem | bj-sbievw1 34162* | Lemma for substitution. (Contributed by BJ, 23-Jul-2023.) |
⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) → ([𝑦 / 𝑥]𝜑 → 𝜓)) | ||
Theorem | bj-sbievw2 34163* | Lemma for substitution. (Contributed by BJ, 23-Jul-2023.) |
⊢ ([𝑦 / 𝑥](𝜓 → 𝜑) → (𝜓 → [𝑦 / 𝑥]𝜑)) | ||
Theorem | bj-sbievw 34164* | Lemma for substitution. Closed form of equsalvw 2004 and sbievw 2097. (Contributed by BJ, 23-Jul-2023.) |
⊢ ([𝑦 / 𝑥](𝜑 ↔ 𝜓) → ([𝑦 / 𝑥]𝜑 ↔ 𝜓)) | ||
Theorem | bj-sbievv 34165 | Version of sbie 2538 with a second nonfreeness hypothesis and shorter proof. (Contributed by BJ, 18-Jul-2023.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ Ⅎ𝑦𝜑 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓) | ||
Theorem | bj-moeub 34166 | Uniqueness is equivalent to existence being equivalent to unique existence. (Contributed by BJ, 14-Oct-2022.) |
⊢ (∃*𝑥𝜑 ↔ (∃𝑥𝜑 ↔ ∃!𝑥𝜑)) | ||
Theorem | bj-sbidmOLD 34167 | Obsolete proof of sbidm 2546 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 34168* |
Deduction form of dvelim 2467 with disjoint variable conditions. Uncurried
(imported) form of bj-dvelimdv1 34169. 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 1909 can be replaced with nfal 2336 followed by nfn 1851. Remark: nfald 2341 uses ax-11 2154; it might be possible to inline and use ax11w 2128 instead, but there is still a use via 19.12 2340 anyway. (Contributed by BJ, 20-Oct-2021.) (Proof modification is discouraged.) |
⊢ (𝜑 → Ⅎ𝑥𝜒) & ⊢ (𝑧 = 𝑦 → (𝜒 ↔ 𝜓)) ⇒ ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥𝜓) | ||
Theorem | bj-dvelimdv1 34169* | Curried (exported) form of bj-dvelimdv 34168 (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 34170* | A version of dvelim 2467 using the "nonfree" idiom. (Contributed by BJ, 20-Oct-2021.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑧 = 𝑦 → (𝜓 ↔ 𝜑)) ⇒ ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝜑) | ||
Theorem | bj-nfeel2 34171* | Nonfreeness in a membership statement. (Contributed by BJ, 20-Oct-2021.) (Proof modification is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥 𝑦 ∈ 𝑧) | ||
Theorem | bj-axc14nf 34172 | Proof of a version of axc14 2480 using the "nonfree" idiom. (Contributed by BJ, 20-Oct-2021.) (Proof modification is discouraged.) |
⊢ (¬ ∀𝑧 𝑧 = 𝑥 → (¬ ∀𝑧 𝑧 = 𝑦 → Ⅎ𝑧 𝑥 ∈ 𝑦)) | ||
Theorem | bj-axc14 34173 | Alternate proof of axc14 2480 (even when inlining the above results, this gives a shorter proof). (Contributed by BJ, 20-Oct-2021.) (Proof modification is discouraged.) |
⊢ (¬ ∀𝑧 𝑧 = 𝑥 → (¬ ∀𝑧 𝑧 = 𝑦 → (𝑥 ∈ 𝑦 → ∀𝑧 𝑥 ∈ 𝑦))) | ||
Theorem | mobidvALT 34174* | Alternate proof of mobidv 2627 directly from its analogues albidv 1915 and exbidv 1916, using deduction style. Note the proof structure, similar to mobi 2624. (Contributed by Mario Carneiro, 7-Oct-2016.) Reduce axiom dependencies and shorten proof. Remove dependency on ax-6 1964, ax-7 2009, ax-12 2170 by adapting proof of mobid 2628. (Revised by BJ, 26-Sep-2022.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃*𝑥𝜓 ↔ ∃*𝑥𝜒)) | ||
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 2791, df-clab 2798, df-cleq 2812, df-clel 2891 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 is set.mm. It states: every formula in the language of FOL + ∈ + class terms, but without class variables, is provably equivalent (over {FOL, ax-ext 2791, df-clab 2798, df-cleq 2812, df-clel 2891 }) 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 following forms: for equality, 𝑥 = {𝑦 ∣ 𝜑}, {𝑥 ∣ 𝜑} = 𝑦, {𝑥 ∣ 𝜑} = {𝑦 ∣ 𝜓}, and for membership, 𝑦 ∈ {𝑥 ∣ 𝜑}, {𝑥 ∣ 𝜑} ∈ 𝑦, {𝑥 ∣ 𝜑} ∈ {𝑦 ∣ 𝜓}. These cases are dealt with by eliminable1 34175 and the following theorems of this section, which are special instances of df-clab 2798, dfcleq 2813 (proved from {FOL, ax-ext 2791, df-cleq 2812 }), and df-clel 2891. 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 34176, eliminable2b 34177 and eliminable3a 34179, 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 1530, 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 2798 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 2798, ax-ext 2791 and df-cleq 2812 are sufficient (over FOL) to eliminate class terms. To prove that { df-clab 2798, df-cleq 2812, df-clel 2891 } provides a definitional extension of {FOL, ax-ext 2791 }, one needs to prove 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 2798, df-cleq 2812, df-clel 2891 }. 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 2791 }. 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 2798, df-cleq 2812, df-clel 2891 }. It involves a careful case study on the structure of the proof tree. | ||
Theorem | eliminable1 34175 | 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 34176* | 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 34177* | 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 34178* | 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 | eliminable3a 34179* | 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 | eliminable3b 34180* | 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.) |
⊢ ({𝑥 ∣ 𝜑} ∈ {𝑦 ∣ 𝜓} ↔ ∃𝑧(𝑧 = {𝑥 ∣ 𝜑} ∧ 𝑧 ∈ {𝑦 ∣ 𝜓})) | ||
A few results about classes can be proved without using ax-ext 2791. One could move all theorems from cab 2797 to df-clel 2891 (except for dfcleq 2813 and cvjust 2814) in a subsection "Classes" before the subsection on the axiom of extensionality, together with the theorems below. In that subsection, the last statement should be df-cleq 2812. Note that without ax-ext 2791, the $a-statements df-clab 2798, df-cleq 2812, and df-clel 2891 are no longer eliminable (see previous section) (but PROBABLY df-clab 2798 is still conservative , while df-cleq 2812 and df-clel 2891 are not). This is not a reason not to study what is provable with them but without ax-ext 2791, in order to gauge their strengths more precisely. Before that subsection, a subsection "The membership predicate" could group the statements with ∈ that are currently in the FOL part (including wcel 2108, wel 2109, ax-8 2110, ax-9 2118). Remark: the weakening of eleq1 2898 / eleq2 2899 to eleq1w 2893 / eleq2w 2894 can also be done with eleq1i 2901, eqeltri 2907, eqeltrri 2908, eleq1a 2906, eleq1d 2895, eqeltrd 2911, eqeltrrd 2912, eqneltrd 2930, eqneltrrd 2931, nelneq 2935. Remark: possibility to remove dependency on ax-10 2139, ax-11 2154, ax-13 2384 from nfcri 2969 and theorems using it if one adds a disjoint variable condition (that theorem is typically used with dummy variables, so the disjoint variable condition addition is not very restrictive), and then shorten nfnfc 2988. | ||
Theorem | bj-denotes 34181* |
This would be the justification theorem for the definition of the unary
predicate "E!" by ⊢ ( E! 𝐴 ↔ ∃𝑥𝑥 = 𝐴) which could be
interpreted as "𝐴 exists" (as a set) or
"𝐴 denotes" (in the
sense of free logic).
A shorter proof using bitri 277 (to add an intermediate proposition ∃𝑧𝑧 = 𝐴 with a fresh 𝑧), cbvexvw 2038, and eqeq1 2823, requires the core axioms and { ax-9 2118, ax-ext 2791, df-cleq 2812 } whereas this proof requires the core axioms and { ax-8 2110, df-clab 2798, df-clel 2891 }. Theorem bj-issetwt 34182 proves that "existing" is equivalent to being a member of a class abstraction. It also requires, with the present proof, { ax-8 2110, df-clab 2798, df-clel 2891 } (whereas with the shorter proof from cbvexvw 2038 and eqeq1 2823 it would require { ax-8 2110, ax-9 2118, ax-ext 2791, df-clab 2798, df-cleq 2812, df-clel 2891 }). That every class is equal to a class abstraction is proved by abid1 2954, which requires { ax-8 2110, ax-9 2118, ax-ext 2791, df-clab 2798, df-cleq 2812, df-clel 2891 }. Note that there is no disjoint variable condition on 𝑥, 𝑦 but the theorem does not depend on ax-13 2384. Actually, the proof depends only on the logical axioms ax-1 6 through ax-7 2009 and sp 2175. The symbol "E!" was chosen to be reminiscent of the analogous predicate in (inclusive or non-inclusive) free logic, which deals with the possibility of nonexistent objects. This analogy should not be taken too far, since here there are no equality axioms for classes: these are derived from ax-ext 2791 and df-cleq 2812 (e.g., eqid 2819 and eqeq1 2823). In particular, one cannot even prove ⊢ ∃𝑥𝑥 = 𝐴 ⇒ ⊢ 𝐴 = 𝐴 without ax-ext 2791 and df-cleq 2812. (Contributed by BJ, 29-Apr-2019.) (Proof modification is discouraged.) |
⊢ (∃𝑥 𝑥 = 𝐴 ↔ ∃𝑦 𝑦 = 𝐴) | ||
Theorem | bj-issetwt 34182* | Closed form of bj-issetw 34183. (Contributed by BJ, 29-Apr-2019.) (Proof modification is discouraged.) |
⊢ (∀𝑥𝜑 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ ∃𝑦 𝑦 = 𝐴)) | ||
Theorem | bj-issetw 34183* | The closest one can get to isset 3505 without using ax-ext 2791. See also vexw 2803. Note that the only disjoint variable condition is between 𝑦 and 𝐴. From there, one can prove isset 3505 using eleq2i 2902 (which requires ax-ext 2791 and df-cleq 2812). (Contributed by BJ, 29-Apr-2019.) (Proof modification is discouraged.) |
⊢ 𝜑 ⇒ ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ ∃𝑦 𝑦 = 𝐴) | ||
Theorem | bj-elissetv 34184* | Version of bj-elisset 34185 with a disjoint variable condition on 𝑥, 𝑉. This proof uses only df-ex 1775, ax-gen 1790, ax-4 1804 and df-clel 2891 on top of propositional calculus. Prefer its use over bj-elisset 34185 when sufficient. (Contributed by BJ, 14-Sep-2019.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴) | ||
Theorem | bj-elisset 34185* | Remove from elisset 3504 dependency on ax-ext 2791 (and on df-cleq 2812 and df-v 3495). This proof uses only df-clab 2798 and df-clel 2891 on top of first-order logic. It only requires ax-1--7 and sp 2175. Use bj-elissetv 34184 instead when sufficient (in particular when 𝑉 is substituted for V). (Contributed by BJ, 29-Apr-2019.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴) | ||
Theorem | bj-issetiv 34186* | Version of bj-isseti 34187 with a disjoint variable condition on 𝑥, 𝑉. This proof uses only df-ex 1775, ax-gen 1790, ax-4 1804 and df-clel 2891 on top of propositional calculus. Prefer its use over bj-isseti 34187 when sufficient (in particular when 𝑉 is substituted for V). (Contributed by BJ, 14-Sep-2019.) (Proof modification is discouraged.) |
⊢ 𝐴 ∈ 𝑉 ⇒ ⊢ ∃𝑥 𝑥 = 𝐴 | ||
Theorem | bj-isseti 34187* | Remove from isseti 3507 dependency on ax-ext 2791 (and on df-cleq 2812 and df-v 3495). This proof uses only df-clab 2798 and df-clel 2891 on top of first-order logic. It only uses ax-12 2170 among the auxiliary logical axioms. The hypothesis uses 𝑉 instead of V for extra generality. This is indeed more general as long as elex 3511 is not available. Use bj-issetiv 34186 instead when sufficient (in particular when 𝑉 is substituted for V). (Contributed by BJ, 13-Jun-2019.) (Proof modification is discouraged.) |
⊢ 𝐴 ∈ 𝑉 ⇒ ⊢ ∃𝑥 𝑥 = 𝐴 | ||
Theorem | bj-ralvw 34188 | A weak version of ralv 3518 not using ax-ext 2791 (nor df-cleq 2812, df-clel 2891, df-v 3495), and only core FOL axioms. See also bj-rexvw 34189. The analogues for reuv 3520 and rmov 3521 are not proved. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.) |
⊢ 𝜓 ⇒ ⊢ (∀𝑥 ∈ {𝑦 ∣ 𝜓}𝜑 ↔ ∀𝑥𝜑) | ||
Theorem | bj-rexvw 34189 | A weak version of rexv 3519 not using ax-ext 2791 (nor df-cleq 2812, df-clel 2891, df-v 3495), and only core FOL axioms. See also bj-ralvw 34188. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.) |
⊢ 𝜓 ⇒ ⊢ (∃𝑥 ∈ {𝑦 ∣ 𝜓}𝜑 ↔ ∃𝑥𝜑) | ||
Theorem | bj-rababw 34190 | A weak version of rabab 3522 not using df-clel 2891 nor df-v 3495 (but requiring ax-ext 2791) nor ax-12 2170. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.) |
⊢ 𝜓 ⇒ ⊢ {𝑥 ∈ {𝑦 ∣ 𝜓} ∣ 𝜑} = {𝑥 ∣ 𝜑} | ||
Theorem | bj-rexcom4bv 34191* | Version of rexcom4b 3523 and bj-rexcom4b 34192 with a disjoint variable condition on 𝑥, 𝑉, hence removing dependency on df-sb 2064 and df-clab 2798 (so that it depends on df-clel 2891 and df-rex 3142 only on top of first-order logic). Prefer its use over bj-rexcom4b 34192 when sufficient (in particular when 𝑉 is substituted for V). Note the 𝑉 in the hypothesis instead of V. (Contributed by BJ, 14-Sep-2019.) (Proof modification is discouraged.) |
⊢ 𝐵 ∈ 𝑉 ⇒ ⊢ (∃𝑥∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵) ↔ ∃𝑦 ∈ 𝐴 𝜑) | ||
Theorem | bj-rexcom4b 34192* | Remove from rexcom4b 3523 dependency on ax-ext 2791 and ax-13 2384 (and on df-or 844, df-cleq 2812, df-nfc 2961, df-v 3495). The hypothesis uses 𝑉 instead of V (see bj-isseti 34187 for the motivation). Use bj-rexcom4bv 34191 instead when sufficient (in particular when 𝑉 is substituted for V). (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.) |
⊢ 𝐵 ∈ 𝑉 ⇒ ⊢ (∃𝑥∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵) ↔ ∃𝑦 ∈ 𝐴 𝜑) | ||
Theorem | bj-ceqsalt0 34193 | The FOL content of ceqsalt 3526. Lemma for bj-ceqsalt 34195 and bj-ceqsaltv 34196. (Contributed by BJ, 26-Sep-2019.) (Proof modification is discouraged.) |
⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝜃 → (𝜑 ↔ 𝜓)) ∧ ∃𝑥𝜃) → (∀𝑥(𝜃 → 𝜑) ↔ 𝜓)) | ||
Theorem | bj-ceqsalt1 34194 | The FOL content of ceqsalt 3526. Lemma for bj-ceqsalt 34195 and bj-ceqsaltv 34196. TODO: consider removing if it does not add anything to bj-ceqsalt0 34193. (Contributed by BJ, 26-Sep-2019.) (Proof modification is discouraged.) |
⊢ (𝜃 → ∃𝑥𝜒) ⇒ ⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝜒 → (𝜑 ↔ 𝜓)) ∧ 𝜃) → (∀𝑥(𝜒 → 𝜑) ↔ 𝜓)) | ||
Theorem | bj-ceqsalt 34195* | Remove from ceqsalt 3526 dependency on ax-ext 2791 (and on df-cleq 2812 and df-v 3495). Note: this is not doable with ceqsralt 3527 (or ceqsralv 3532), which uses eleq1 2898, but the same dependence removal is possible for ceqsalg 3528, ceqsal 3530, ceqsalv 3531, cgsexg 3536, cgsex2g 3537, cgsex4g 3538, ceqsex 3539, ceqsexv 3540, ceqsex2 3542, ceqsex2v 3543, ceqsex3v 3544, ceqsex4v 3545, ceqsex6v 3546, ceqsex8v 3547, gencbvex 3548 (after changing 𝐴 = 𝑦 to 𝑦 = 𝐴), gencbvex2 3549, gencbval 3550, vtoclgft 3552 (it uses Ⅎ, whose justification nfcjust 2960 does not use ax-ext 2791) and several other vtocl* theorems (see for instance bj-vtoclg1f 34227). See also bj-ceqsaltv 34196. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.) |
⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝑉) → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓)) | ||
Theorem | bj-ceqsaltv 34196* | Version of bj-ceqsalt 34195 with a disjoint variable condition on 𝑥, 𝑉, removing dependency on df-sb 2064 and df-clab 2798. Prefer its use over bj-ceqsalt 34195 when sufficient (in particular when 𝑉 is substituted for V). (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.) |
⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝑉) → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓)) | ||
Theorem | bj-ceqsalg0 34197 | The FOL content of ceqsalg 3528. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝜒 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥𝜒 → (∀𝑥(𝜒 → 𝜑) ↔ 𝜓)) | ||
Theorem | bj-ceqsalg 34198* | Remove from ceqsalg 3528 dependency on ax-ext 2791 (and on df-cleq 2812 and df-v 3495). See also bj-ceqsalgv 34200. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓)) | ||
Theorem | bj-ceqsalgALT 34199* | Alternate proof of bj-ceqsalg 34198. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓)) | ||
Theorem | bj-ceqsalgv 34200* | Version of bj-ceqsalg 34198 with a disjoint variable condition on 𝑥, 𝑉, removing dependency on df-sb 2064 and df-clab 2798. Prefer its use over bj-ceqsalg 34198 when sufficient (in particular when 𝑉 is substituted for V). (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |