Home | Metamath
Proof Explorer Theorem List (p. 343 of 450) | < 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-28697) |
Hilbert Space Explorer
(28698-30220) |
Users' Mathboxes
(30221-44913) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | bj-rexcom4b 34201* | Remove from rexcom4b 3526 dependency on ax-ext 2795 and ax-13 2390 (and on df-or 844, df-cleq 2816, df-nfc 2965, df-v 3498). The hypothesis uses 𝑉 instead of V (see bj-isseti 34196 for the motivation). Use bj-rexcom4bv 34200 instead when sufficient (in particular when 𝑉 is substituted for V). (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.) |
⊢ 𝐵 ∈ 𝑉 ⇒ ⊢ (∃𝑥∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵) ↔ ∃𝑦 ∈ 𝐴 𝜑) | ||
Theorem | bj-ceqsalt0 34202 | The FOL content of ceqsalt 3529. Lemma for bj-ceqsalt 34204 and bj-ceqsaltv 34205. (Contributed by BJ, 26-Sep-2019.) (Proof modification is discouraged.) |
⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝜃 → (𝜑 ↔ 𝜓)) ∧ ∃𝑥𝜃) → (∀𝑥(𝜃 → 𝜑) ↔ 𝜓)) | ||
Theorem | bj-ceqsalt1 34203 | The FOL content of ceqsalt 3529. Lemma for bj-ceqsalt 34204 and bj-ceqsaltv 34205. TODO: consider removing if it does not add anything to bj-ceqsalt0 34202. (Contributed by BJ, 26-Sep-2019.) (Proof modification is discouraged.) |
⊢ (𝜃 → ∃𝑥𝜒) ⇒ ⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝜒 → (𝜑 ↔ 𝜓)) ∧ 𝜃) → (∀𝑥(𝜒 → 𝜑) ↔ 𝜓)) | ||
Theorem | bj-ceqsalt 34204* | Remove from ceqsalt 3529 dependency on ax-ext 2795 (and on df-cleq 2816 and df-v 3498). Note: this is not doable with ceqsralt 3530 (or ceqsralv 3535), which uses eleq1 2902, but the same dependence removal is possible for ceqsalg 3531, ceqsal 3533, ceqsalv 3534, cgsexg 3539, cgsex2g 3540, cgsex4g 3541, ceqsex 3542, ceqsexv 3543, ceqsex2 3545, ceqsex2v 3546, ceqsex3v 3547, ceqsex4v 3548, ceqsex6v 3549, ceqsex8v 3550, gencbvex 3551 (after changing 𝐴 = 𝑦 to 𝑦 = 𝐴), gencbvex2 3552, gencbval 3553, vtoclgft 3555 (it uses Ⅎ, whose justification nfcjust 2964 does not use ax-ext 2795) and several other vtocl* theorems (see for instance bj-vtoclg1f 34236). See also bj-ceqsaltv 34205. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.) |
⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝑉) → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓)) | ||
Theorem | bj-ceqsaltv 34205* | Version of bj-ceqsalt 34204 with a disjoint variable condition on 𝑥, 𝑉, removing dependency on df-sb 2070 and df-clab 2802. Prefer its use over bj-ceqsalt 34204 when sufficient (in particular when 𝑉 is substituted for V). (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.) |
⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝑉) → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓)) | ||
Theorem | bj-ceqsalg0 34206 | The FOL content of ceqsalg 3531. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝜒 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥𝜒 → (∀𝑥(𝜒 → 𝜑) ↔ 𝜓)) | ||
Theorem | bj-ceqsalg 34207* | Remove from ceqsalg 3531 dependency on ax-ext 2795 (and on df-cleq 2816 and df-v 3498). See also bj-ceqsalgv 34209. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓)) | ||
Theorem | bj-ceqsalgALT 34208* | Alternate proof of bj-ceqsalg 34207. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓)) | ||
Theorem | bj-ceqsalgv 34209* | Version of bj-ceqsalg 34207 with a disjoint variable condition on 𝑥, 𝑉, removing dependency on df-sb 2070 and df-clab 2802. Prefer its use over bj-ceqsalg 34207 when sufficient (in particular when 𝑉 is substituted for V). (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓)) | ||
Theorem | bj-ceqsalgvALT 34210* | Alternate proof of bj-ceqsalgv 34209. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓)) | ||
Theorem | bj-ceqsal 34211* | Remove from ceqsal 3533 dependency on ax-ext 2795 (and on df-cleq 2816, df-v 3498, df-clab 2802, df-sb 2070). (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓) | ||
Theorem | bj-ceqsalv 34212* | Remove from ceqsalv 3534 dependency on ax-ext 2795 (and on df-cleq 2816, df-v 3498, df-clab 2802, df-sb 2070). (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.) |
⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓) | ||
Theorem | bj-spcimdv 34213* | Remove from spcimdv 3594 dependency on ax-9 2124, ax-10 2145, ax-11 2161, ax-13 2390, ax-ext 2795, df-cleq 2816 (and df-nfc 2965, df-v 3498, df-or 844, df-tru 1540, df-nf 1785). For an even more economical version, see bj-spcimdvv 34214. (Contributed by BJ, 30-Nov-2020.) (Proof modification is discouraged.) |
⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥𝜓 → 𝜒)) | ||
Theorem | bj-spcimdvv 34214* | Remove from spcimdv 3594 dependency on ax-7 2015, ax-8 2116, ax-10 2145, ax-11 2161, ax-12 2177 ax-13 2390, ax-ext 2795, df-cleq 2816, df-clab 2802 (and df-nfc 2965, df-v 3498, df-or 844, df-tru 1540, df-nf 1785) at the price of adding a disjoint variable condition on 𝑥, 𝐵 (but in usages, 𝑥 is typically a dummy, hence fresh, variable). For the version without this disjoint variable condition, see bj-spcimdv 34213. (Contributed by BJ, 3-Nov-2021.) (Proof modification is discouraged.) |
⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥𝜓 → 𝜒)) | ||
Theorem | elelb 34215 | Equivalence between two common ways to characterize elements of a class 𝐵: the LHS says that sets are elements of 𝐵 if and only if they satisfy 𝜑 while the RHS says that classes are elements of 𝐵 if and only if they are sets and satisfy 𝜑. Therefore, the LHS is a characterization among sets while the RHS is a characterization among classes. Note that the LHS is often formulated using a class variable instead of the universe V while this is not possible for the RHS (apart from using 𝐵 itself, which would not be very useful). (Contributed by BJ, 26-Feb-2023.) |
⊢ ((𝐴 ∈ V → (𝐴 ∈ 𝐵 ↔ 𝜑)) ↔ (𝐴 ∈ 𝐵 ↔ (𝐴 ∈ V ∧ 𝜑))) | ||
Theorem | bj-pwvrelb 34216 | Characterization of the elements of the powerclass of the cartesian square of the universal class: they are exactly the sets which are binary relations. (Contributed by BJ, 16-Dec-2023.) |
⊢ (𝐴 ∈ 𝒫 (V × V) ↔ (𝐴 ∈ V ∧ Rel 𝐴)) | ||
In this section, we prove the symmetry of the nonfreeness quantifier for classes. | ||
Theorem | bj-nfcsym 34217 | The nonfreeness quantifier for classes defines a symmetric binary relation on var metavariables (irreflexivity is proved by nfnid 5278 with additional axioms; see also nfcv 2979). This could be proved from aecom 2449 and nfcvb 5279 but the latter requires a domain with at least two objects (hence uses extra axioms). (Contributed by BJ, 30-Sep-2018.) Proof modification is discouraged to avoid use of eqcomd 2829 instead of equcomd 2026; removing dependency on ax-ext 2795 is possible: prove weak versions (i.e. replace classes with setvars) of drnfc1 2999, eleq2d 2900 (using elequ2 2129), nfcvf 3009, dvelimc 3008, dvelimdc 3007, nfcvf2 3010. (Proof modification is discouraged.) |
⊢ (Ⅎ𝑥𝑦 ↔ Ⅎ𝑦𝑥) | ||
Note: now that the proposals have been adopted as df-cleq 2816 and df-clel 2895, and that ax9ALT 2819 is in the main section, we only keep bj-ax9 34218 here as a weaker version of ax9ALT 2819 proved without ax-8 2116. | ||
Theorem | bj-ax9 34218* | Proof of ax-9 2124 from Tarski's FOL=, sp 2182, dfcleq 2817 and ax-ext 2795 (with two extra disjoint variable conditions on 𝑥, 𝑧 and 𝑦, 𝑧). See ax9ALT 2819 for a more general version, proved using also ax-8 2116. (Contributed by BJ, 24-Jun-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦)) | ||
Some useful theorems for dealing with substitutions: sbbi 2317, sbcbig 3825, sbcel1g 4367, sbcel2 4369, sbcel12 4362, sbceqg 4363, csbvarg 4385. | ||
Theorem | bj-sbeqALT 34219* | Substitution in an equality (use the more general version bj-sbeq 34220 instead, without disjoint variable condition). (Contributed by BJ, 6-Oct-2018.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ([𝑦 / 𝑥]𝐴 = 𝐵 ↔ ⦋𝑦 / 𝑥⦌𝐴 = ⦋𝑦 / 𝑥⦌𝐵) | ||
Theorem | bj-sbeq 34220 | Distribute proper substitution through an equality relation. (See sbceqg 4363). (Contributed by BJ, 6-Oct-2018.) |
⊢ ([𝑦 / 𝑥]𝐴 = 𝐵 ↔ ⦋𝑦 / 𝑥⦌𝐴 = ⦋𝑦 / 𝑥⦌𝐵) | ||
Theorem | bj-sbceqgALT 34221 | Distribute proper substitution through an equality relation. Alternate proof of sbceqg 4363. (Contributed by BJ, 6-Oct-2018.) Proof modification is discouraged to avoid using sbceqg 4363, but the Metamath program "MM-PA> MINIMIZE_WITH * / EXCEPT sbceqg" command is ok. (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵 = 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶)) | ||
Theorem | bj-csbsnlem 34222* | Lemma for bj-csbsn 34223 (in this lemma, 𝑥 cannot occur in 𝐴). (Contributed by BJ, 6-Oct-2018.) (New usage is discouraged.) |
⊢ ⦋𝐴 / 𝑥⦌{𝑥} = {𝐴} | ||
Theorem | bj-csbsn 34223 | Substitution in a singleton. (Contributed by BJ, 6-Oct-2018.) |
⊢ ⦋𝐴 / 𝑥⦌{𝑥} = {𝐴} | ||
Theorem | bj-sbel1 34224* | Version of sbcel1g 4367 when substituting a set. (Note: one could have a corresponding version of sbcel12 4362 when substituting a set, but the point here is that the antecedent of sbcel1g 4367 is not needed when substituting a set.) (Contributed by BJ, 6-Oct-2018.) |
⊢ ([𝑦 / 𝑥]𝐴 ∈ 𝐵 ↔ ⦋𝑦 / 𝑥⦌𝐴 ∈ 𝐵) | ||
Theorem | bj-abv 34225 | The class of sets verifying a tautology is the universal class. (Contributed by BJ, 24-Jul-2019.) (Proof modification is discouraged.) |
⊢ (∀𝑥𝜑 → {𝑥 ∣ 𝜑} = V) | ||
Theorem | bj-ab0 34226 | The class of sets verifying a falsity is the empty set (closed form of abf 4358). (Contributed by BJ, 24-Jul-2019.) (Proof modification is discouraged.) |
⊢ (∀𝑥 ¬ 𝜑 → {𝑥 ∣ 𝜑} = ∅) | ||
Theorem | bj-abf 34227 | Shorter proof of abf 4358 (which should be kept as abfALT). (Contributed by BJ, 24-Jul-2019.) (Proof modification is discouraged.) |
⊢ ¬ 𝜑 ⇒ ⊢ {𝑥 ∣ 𝜑} = ∅ | ||
Theorem | bj-csbprc 34228 | More direct proof of csbprc 4360 (fewer essential steps). (Contributed by BJ, 24-Jul-2019.) (Proof modification is discouraged.) |
⊢ (¬ 𝐴 ∈ V → ⦋𝐴 / 𝑥⦌𝐵 = ∅) | ||
Theorem | bj-exlimvmpi 34229* | A Fol lemma (exlimiv 1931 followed by mpi 20). (Contributed by BJ, 2-Jul-2022.) (Proof modification is discouraged.) |
⊢ (𝜒 → (𝜑 → 𝜓)) & ⊢ 𝜑 ⇒ ⊢ (∃𝑥𝜒 → 𝜓) | ||
Theorem | bj-exlimmpi 34230 | Lemma for bj-vtoclg1f1 34235 (an instance of this lemma is a version of bj-vtoclg1f1 34235 where 𝑥 and 𝑦 are identified). (Contributed by BJ, 30-Apr-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝜒 → (𝜑 → 𝜓)) & ⊢ 𝜑 ⇒ ⊢ (∃𝑥𝜒 → 𝜓) | ||
Theorem | bj-exlimmpbi 34231 | Lemma for theorems of the vtoclg 3569 family. (Contributed by BJ, 3-Oct-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝜒 → (𝜑 ↔ 𝜓)) & ⊢ 𝜑 ⇒ ⊢ (∃𝑥𝜒 → 𝜓) | ||
Theorem | bj-exlimmpbir 34232 | Lemma for theorems of the vtoclg 3569 family. (Contributed by BJ, 3-Oct-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜒 → (𝜑 ↔ 𝜓)) & ⊢ 𝜓 ⇒ ⊢ (∃𝑥𝜒 → 𝜑) | ||
Theorem | bj-vtoclf 34233* | Remove dependency on ax-ext 2795, df-clab 2802 and df-cleq 2816 (and df-sb 2070 and df-v 3498) from vtoclf 3560. (Contributed by BJ, 6-Oct-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ 𝐴 ∈ 𝑉 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ 𝜑 ⇒ ⊢ 𝜓 | ||
Theorem | bj-vtocl 34234* | Remove dependency on ax-ext 2795, df-clab 2802 and df-cleq 2816 (and df-sb 2070 and df-v 3498) from vtocl 3561. (Contributed by BJ, 6-Oct-2019.) (Proof modification is discouraged.) |
⊢ 𝐴 ∈ 𝑉 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ 𝜑 ⇒ ⊢ 𝜓 | ||
Theorem | bj-vtoclg1f1 34235* | The FOL content of vtoclg1f 3568 (hence not using ax-ext 2795, df-cleq 2816, df-nfc 2965, df-v 3498). Note the weakened "major" hypothesis and the disjoint variable condition between 𝑥 and 𝐴 (needed since the nonfreeness quantifier for classes is not available without ax-ext 2795; as a byproduct, this dispenses with ax-11 2161 and ax-13 2390). (Contributed by BJ, 30-Apr-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝐴 → (𝜑 → 𝜓)) & ⊢ 𝜑 ⇒ ⊢ (∃𝑦 𝑦 = 𝐴 → 𝜓) | ||
Theorem | bj-vtoclg1f 34236* | Reprove vtoclg1f 3568 from bj-vtoclg1f1 34235. This removes dependency on ax-ext 2795, df-cleq 2816 and df-v 3498. Use bj-vtoclg1fv 34237 instead when sufficient (in particular when 𝑉 is substituted for V). (Contributed by BJ, 14-Sep-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝐴 → (𝜑 → 𝜓)) & ⊢ 𝜑 ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝜓) | ||
Theorem | bj-vtoclg1fv 34237* | Version of bj-vtoclg1f 34236 with a disjoint variable condition on 𝑥, 𝑉. This removes dependency on df-sb 2070 and df-clab 2802. Prefer its use over bj-vtoclg1f 34236 when sufficient (in particular when 𝑉 is substituted for V). (Contributed by BJ, 14-Sep-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝐴 → (𝜑 → 𝜓)) & ⊢ 𝜑 ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝜓) | ||
Theorem | bj-vtoclg 34238* | A version of vtoclg 3569 with an additional disjoint variable condition (which is removable if we allow use of df-clab 2802, see bj-vtoclg1f 34236), which requires fewer axioms (i.e., removes dependency on ax-6 1970, ax-7 2015, ax-9 2124, ax-12 2177, ax-ext 2795, df-clab 2802, df-cleq 2816, df-v 3498). (Contributed by BJ, 2-Jul-2022.) (Proof modification is discouraged.) |
⊢ (𝑥 = 𝐴 → (𝜑 → 𝜓)) & ⊢ 𝜑 ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝜓) | ||
Theorem | bj-rabbida2 34239 | Version of rabbidva2 3478 with disjoint variable condition replaced by nonfreeness hypothesis. (Contributed by BJ, 27-Apr-2019.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐵 ∧ 𝜒))) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒}) | ||
Theorem | bj-rabeqd 34240 | Deduction form of rabeq 3485. Note that contrary to rabeq 3485 it has no disjoint variable condition. (Contributed by BJ, 27-Apr-2019.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜓}) | ||
Theorem | bj-rabeqbid 34241 | Version of rabeqbidv 3487 with two disjoint variable conditions removed and the third replaced by a nonfreeness hypothesis. (Contributed by BJ, 27-Apr-2019.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒}) | ||
Theorem | bj-rabeqbida 34242 | Version of rabeqbidva 3488 with two disjoint variable conditions removed and the third replaced by a nonfreeness hypothesis. (Contributed by BJ, 27-Apr-2019.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒}) | ||
Theorem | bj-seex 34243* | Version of seex 5520 with a disjoint variable condition replaced by a nonfreeness hypothesis (for the sake of illustration). (Contributed by BJ, 27-Apr-2019.) |
⊢ Ⅎ𝑥𝐵 ⇒ ⊢ ((𝑅 Se 𝐴 ∧ 𝐵 ∈ 𝐴) → {𝑥 ∈ 𝐴 ∣ 𝑥𝑅𝐵} ∈ V) | ||
Theorem | bj-nfcf 34244* | Version of df-nfc 2965 with a disjoint variable condition replaced with a nonfreeness hypothesis. (Contributed by BJ, 2-May-2019.) |
⊢ Ⅎ𝑦𝐴 ⇒ ⊢ (Ⅎ𝑥𝐴 ↔ ∀𝑦Ⅎ𝑥 𝑦 ∈ 𝐴) | ||
Theorem | bj-zfauscl 34245* |
General version of zfauscl 5207.
Remark: the comment in zfauscl 5207 is misleading: the essential use of ax-ext 2795 is the one via eleq2 2903 and not the one via vtocl 3561, since the latter can be proved without ax-ext 2795 (see bj-vtoclg 34238). (Contributed by BJ, 2-Jul-2022.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ 𝑉 → ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝜑))) | ||
A few additional theorems on class abstractions and restricted class abstractions. | ||
Theorem | bj-unrab 34246* | Generalization of unrab 4276. Equality need not hold. (Contributed by BJ, 21-Apr-2019.) |
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∪ {𝑥 ∈ 𝐵 ∣ 𝜓}) ⊆ {𝑥 ∈ (𝐴 ∪ 𝐵) ∣ (𝜑 ∨ 𝜓)} | ||
Theorem | bj-inrab 34247 | Generalization of inrab 4277. (Contributed by BJ, 21-Apr-2019.) |
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ {𝑥 ∈ 𝐵 ∣ 𝜓}) = {𝑥 ∈ (𝐴 ∩ 𝐵) ∣ (𝜑 ∧ 𝜓)} | ||
Theorem | bj-inrab2 34248 | Shorter proof of inrab 4277. (Contributed by BJ, 21-Apr-2019.) (Proof modification is discouraged.) |
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ {𝑥 ∈ 𝐴 ∣ 𝜓}) = {𝑥 ∈ 𝐴 ∣ (𝜑 ∧ 𝜓)} | ||
Theorem | bj-inrab3 34249* | Generalization of dfrab3ss 4283, which it may shorten. (Contributed by BJ, 21-Apr-2019.) (Revised by OpenAI, 7-Jul-2020.) |
⊢ (𝐴 ∩ {𝑥 ∈ 𝐵 ∣ 𝜑}) = ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ 𝐵) | ||
Theorem | bj-rabtr 34250* | Restricted class abstraction with true formula. (Contributed by BJ, 22-Apr-2019.) |
⊢ {𝑥 ∈ 𝐴 ∣ ⊤} = 𝐴 | ||
Theorem | bj-rabtrALT 34251* | Alternate proof of bj-rabtr 34250. (Contributed by BJ, 22-Apr-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ {𝑥 ∈ 𝐴 ∣ ⊤} = 𝐴 | ||
Theorem | bj-rabtrAUTO 34252* | Proof of bj-rabtr 34250 found automatically by the Metamath program "MM-PA> IMPROVE ALL / DEPTH 3 / 3" command followed by "MM-PA> MINIMIZE_WITH *". (Contributed by BJ, 22-Apr-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ {𝑥 ∈ 𝐴 ∣ ⊤} = 𝐴 | ||
In this subsection, we define restricted nonfreeness (or relative nonfreeness). | ||
Syntax | wrnf 34253 | Syntax for restricted nonfreeness. |
wff Ⅎ𝑥 ∈ 𝐴𝜑 | ||
Definition | df-bj-rnf 34254 | Definition of restricted nonfreeness. Informally, the proposition Ⅎ𝑥 ∈ 𝐴𝜑 means that 𝜑(𝑥) does not vary on 𝐴. (Contributed by BJ, 19-Mar-2021.) |
⊢ (Ⅎ𝑥 ∈ 𝐴𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜑)) | ||
A few results around Russell's paradox. For clarity, we prove separately its FOL part (bj-ru0 34255) and then two versions (bj-ru1 34256 and bj-ru 34257). Special attention is put on minimizing axiom depencencies. | ||
Theorem | bj-ru0 34255* | The FOL part of Russell's paradox ru 3773 (see also bj-ru1 34256, bj-ru 34257). Use of elequ1 2121, bj-elequ12 34014 (instead of eleq1 2902, eleq12d 2909 as in ru 3773) permits to remove dependency on ax-10 2145, ax-11 2161, ax-12 2177, ax-ext 2795, df-sb 2070, df-clab 2802, df-cleq 2816, df-clel 2895. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.) |
⊢ ¬ ∀𝑥(𝑥 ∈ 𝑦 ↔ ¬ 𝑥 ∈ 𝑥) | ||
Theorem | bj-ru1 34256* | A version of Russell's paradox ru 3773 (see also bj-ru 34257). (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.) |
⊢ ¬ ∃𝑦 𝑦 = {𝑥 ∣ ¬ 𝑥 ∈ 𝑥} | ||
Theorem | bj-ru 34257 | Remove dependency on ax-13 2390 (and df-v 3498) from Russell's paradox ru 3773 expressed with primitive symbols and with a class variable 𝑉. Note the more economical use of bj-elissetv 34193 instead of isset 3508 to avoid use of df-v 3498. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.) |
⊢ ¬ {𝑥 ∣ ¬ 𝑥 ∈ 𝑥} ∈ 𝑉 | ||
Theorem | currysetlem 34258* | Lemma for currysetlem 34258, where it is used with (𝑥 ∈ 𝑥 → 𝜑) substituted for 𝜓. (Contributed by BJ, 23-Sep-2023.) This proof is intuitionistically valid. (Proof modification is discouraged.) |
⊢ ({𝑥 ∣ 𝜓} ∈ 𝑉 → ({𝑥 ∣ 𝜓} ∈ {𝑥 ∣ (𝑥 ∈ 𝑥 → 𝜑)} ↔ ({𝑥 ∣ 𝜓} ∈ {𝑥 ∣ 𝜓} → 𝜑))) | ||
Theorem | curryset 34259* | Curry's paradox in set theory. This can be seen as a generalization of Russell's paradox, which corresponds to the case where 𝜑 is ⊥. See alternate exposal of basically the same proof currysetALT 34263. (Contributed by BJ, 23-Sep-2023.) This proof is intuitionistically valid. (Proof modification is discouraged.) |
⊢ ¬ {𝑥 ∣ (𝑥 ∈ 𝑥 → 𝜑)} ∈ 𝑉 | ||
Theorem | currysetlem1 34260* | Lemma for currysetALT 34263. (Contributed by BJ, 23-Sep-2023.) This proof is intuitionistically valid. (Proof modification is discouraged.) |
⊢ 𝑋 = {𝑥 ∣ (𝑥 ∈ 𝑥 → 𝜑)} ⇒ ⊢ (𝑋 ∈ 𝑉 → (𝑋 ∈ 𝑋 ↔ (𝑋 ∈ 𝑋 → 𝜑))) | ||
Theorem | currysetlem2 34261* | Lemma for currysetALT 34263. (Contributed by BJ, 23-Sep-2023.) This proof is intuitionistically valid. (Proof modification is discouraged.) |
⊢ 𝑋 = {𝑥 ∣ (𝑥 ∈ 𝑥 → 𝜑)} ⇒ ⊢ (𝑋 ∈ 𝑉 → (𝑋 ∈ 𝑋 → 𝜑)) | ||
Theorem | currysetlem3 34262* | Lemma for currysetALT 34263. (Contributed by BJ, 23-Sep-2023.) This proof is intuitionistically valid. (Proof modification is discouraged.) |
⊢ 𝑋 = {𝑥 ∣ (𝑥 ∈ 𝑥 → 𝜑)} ⇒ ⊢ ¬ 𝑋 ∈ 𝑉 | ||
Theorem | currysetALT 34263* | Alternate proof of curryset 34259, or more precisely alternate exposal of the same proof. (Contributed by BJ, 23-Sep-2023.) This proof is intuitionistically valid. (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ¬ {𝑥 ∣ (𝑥 ∈ 𝑥 → 𝜑)} ∈ 𝑉 | ||
A few utility theorems on disjointness of classes. | ||
Theorem | bj-n0i 34264* | Inference associated with n0 4312. Shortens 2ndcdisj 22066 (2888>2878), notzfaus 5264 (264>253). (Contributed by BJ, 22-Apr-2019.) |
⊢ 𝐴 ≠ ∅ ⇒ ⊢ ∃𝑥 𝑥 ∈ 𝐴 | ||
Theorem | bj-disjcsn 34265 | A class is disjoint from its singleton. A consequence of regularity. Shorter proof than bnj521 32009 and does not depend on df-ne 3019. (Contributed by BJ, 4-Apr-2019.) |
⊢ (𝐴 ∩ {𝐴}) = ∅ | ||
Theorem | bj-disjsn01 34266 | Disjointness of the singletons containing 0 and 1. This is a consequence of bj-disjcsn 34265 but the present proof does not use regularity. (Contributed by BJ, 4-Apr-2019.) (Proof modification is discouraged.) |
⊢ ({∅} ∩ {1o}) = ∅ | ||
Theorem | bj-0nel1 34267 | The empty set does not belong to {1o}. (Contributed by BJ, 6-Apr-2019.) |
⊢ ∅ ∉ {1o} | ||
Theorem | bj-1nel0 34268 | 1o does not belong to {∅}. (Contributed by BJ, 6-Apr-2019.) |
⊢ 1o ∉ {∅} | ||
A few utility theorems on direct products. | ||
Theorem | bj-xpimasn 34269 | The image of a singleton, general case. [Change and relabel xpimasn 6044 accordingly, maybe to xpima2sn.] (Contributed by BJ, 6-Apr-2019.) |
⊢ ((𝐴 × 𝐵) “ {𝑋}) = if(𝑋 ∈ 𝐴, 𝐵, ∅) | ||
Theorem | bj-xpima1sn 34270 | The image of a singleton by a direct product, empty case. [Change and relabel xpimasn 6044 accordingly, maybe to xpima2sn.] (Contributed by BJ, 6-Apr-2019.) |
⊢ (¬ 𝑋 ∈ 𝐴 → ((𝐴 × 𝐵) “ {𝑋}) = ∅) | ||
Theorem | bj-xpima1snALT 34271 | Alternate proof of bj-xpima1sn 34270. (Contributed by BJ, 6-Apr-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ 𝑋 ∈ 𝐴 → ((𝐴 × 𝐵) “ {𝑋}) = ∅) | ||
Theorem | bj-xpima2sn 34272 | The image of a singleton by a direct product, nonempty case. [To replace xpimasn 6044] (Contributed by BJ, 6-Apr-2019.) (Proof modification is discouraged.) |
⊢ (𝑋 ∈ 𝐴 → ((𝐴 × 𝐵) “ {𝑋}) = 𝐵) | ||
Theorem | bj-xpnzex 34273 | If the first factor of a product is nonempty, and the product is a set, then the second factor is a set. UPDATE: this is actually the curried (exported) form of xpexcnv 7627 (up to commutation in the product). (Contributed by BJ, 6-Oct-2018.) (Proof modification is discouraged.) |
⊢ (𝐴 ≠ ∅ → ((𝐴 × 𝐵) ∈ 𝑉 → 𝐵 ∈ V)) | ||
Theorem | bj-xpexg2 34274 | Curried (exported) form of xpexg 7475. (Contributed by BJ, 2-Apr-2019.) |
⊢ (𝐴 ∈ 𝑉 → (𝐵 ∈ 𝑊 → (𝐴 × 𝐵) ∈ V)) | ||
Theorem | bj-xpnzexb 34275 | If the first factor of a product is a nonempty set, then the product is a set if and only if the second factor is a set. (Contributed by BJ, 2-Apr-2019.) |
⊢ (𝐴 ∈ (𝑉 ∖ {∅}) → (𝐵 ∈ V ↔ (𝐴 × 𝐵) ∈ V)) | ||
Theorem | bj-cleq 34276* | Substitution property for certain classes. (Contributed by BJ, 2-Apr-2019.) |
⊢ (𝐴 = 𝐵 → {𝑥 ∣ {𝑥} ∈ (𝐴 “ 𝐶)} = {𝑥 ∣ {𝑥} ∈ (𝐵 “ 𝐶)}) | ||
This subsection introduces the "singletonization" and the "tagging" of a class. The singletonization of a class is the class of singletons of elements of that class. It is useful since all nonsingletons are disjoint from it, so one can easily adjoin to it disjoint elements, which is what the tagging does: it adjoins the empty set. This can be used for instance to define the one-point compactification of a topological space. It will be used in the next section to define tuples which work for proper classes. | ||
Theorem | bj-snsetex 34277* | The class of sets "whose singletons" belong to a set is a set. Nice application of ax-rep 5192. (Contributed by BJ, 6-Oct-2018.) |
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V) | ||
Theorem | bj-clex 34278* | Sethood of certain classes. (Contributed by BJ, 2-Apr-2019.) |
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∣ {𝑥} ∈ (𝐴 “ 𝐵)} ∈ V) | ||
Syntax | bj-csngl 34279 | Syntax for singletonization. (Contributed by BJ, 6-Oct-2018.) |
class sngl 𝐴 | ||
Definition | df-bj-sngl 34280* | Definition of "singletonization". The class sngl 𝐴 is isomorphic to 𝐴 and since it contains only singletons, it can be easily be adjoined disjoint elements, which can be useful in various constructions. (Contributed by BJ, 6-Oct-2018.) |
⊢ sngl 𝐴 = {𝑥 ∣ ∃𝑦 ∈ 𝐴 𝑥 = {𝑦}} | ||
Theorem | bj-sngleq 34281 | Substitution property for sngl. (Contributed by BJ, 6-Oct-2018.) |
⊢ (𝐴 = 𝐵 → sngl 𝐴 = sngl 𝐵) | ||
Theorem | bj-elsngl 34282* | Characterization of the elements of the singletonization of a class. (Contributed by BJ, 6-Oct-2018.) |
⊢ (𝐴 ∈ sngl 𝐵 ↔ ∃𝑥 ∈ 𝐵 𝐴 = {𝑥}) | ||
Theorem | bj-snglc 34283 | Characterization of the elements of 𝐴 in terms of elements of its singletonization. (Contributed by BJ, 6-Oct-2018.) |
⊢ (𝐴 ∈ 𝐵 ↔ {𝐴} ∈ sngl 𝐵) | ||
Theorem | bj-snglss 34284 | The singletonization of a class is included in its powerclass. (Contributed by BJ, 6-Oct-2018.) |
⊢ sngl 𝐴 ⊆ 𝒫 𝐴 | ||
Theorem | bj-0nelsngl 34285 | The empty set is not a member of a singletonization (neither is any nonsingleton, in particular any von Neuman ordinal except possibly df-1o 8104). (Contributed by BJ, 6-Oct-2018.) |
⊢ ∅ ∉ sngl 𝐴 | ||
Theorem | bj-snglinv 34286* | Inverse of singletonization. (Contributed by BJ, 6-Oct-2018.) |
⊢ 𝐴 = {𝑥 ∣ {𝑥} ∈ sngl 𝐴} | ||
Theorem | bj-snglex 34287 | A class is a set if and only if its singletonization is a set. (Contributed by BJ, 6-Oct-2018.) |
⊢ (𝐴 ∈ V ↔ sngl 𝐴 ∈ V) | ||
Syntax | bj-ctag 34288 | Syntax for the tagged copy of a class. (Contributed by BJ, 6-Oct-2018.) |
class tag 𝐴 | ||
Definition | df-bj-tag 34289 | Definition of the tagged copy of a class, that is, the adjunction to (an isomorph of) 𝐴 of a disjoint element (here, the empty set). Remark: this could be used for the one-point compactification of a topological space. (Contributed by BJ, 6-Oct-2018.) |
⊢ tag 𝐴 = (sngl 𝐴 ∪ {∅}) | ||
Theorem | bj-tageq 34290 | Substitution property for tag. (Contributed by BJ, 6-Oct-2018.) |
⊢ (𝐴 = 𝐵 → tag 𝐴 = tag 𝐵) | ||
Theorem | bj-eltag 34291* | Characterization of the elements of the tagging of a class. (Contributed by BJ, 6-Oct-2018.) |
⊢ (𝐴 ∈ tag 𝐵 ↔ (∃𝑥 ∈ 𝐵 𝐴 = {𝑥} ∨ 𝐴 = ∅)) | ||
Theorem | bj-0eltag 34292 | The empty set belongs to the tagging of a class. (Contributed by BJ, 6-Apr-2019.) |
⊢ ∅ ∈ tag 𝐴 | ||
Theorem | bj-tagn0 34293 | The tagging of a class is nonempty. (Contributed by BJ, 6-Apr-2019.) |
⊢ tag 𝐴 ≠ ∅ | ||
Theorem | bj-tagss 34294 | The tagging of a class is included in its powerclass. (Contributed by BJ, 6-Oct-2018.) |
⊢ tag 𝐴 ⊆ 𝒫 𝐴 | ||
Theorem | bj-snglsstag 34295 | The singletonization is included in the tagging. (Contributed by BJ, 6-Oct-2018.) |
⊢ sngl 𝐴 ⊆ tag 𝐴 | ||
Theorem | bj-sngltagi 34296 | The singletonization is included in the tagging. (Contributed by BJ, 6-Oct-2018.) |
⊢ (𝐴 ∈ sngl 𝐵 → 𝐴 ∈ tag 𝐵) | ||
Theorem | bj-sngltag 34297 | The singletonization and the tagging of a set contain the same singletons. (Contributed by BJ, 6-Oct-2018.) |
⊢ (𝐴 ∈ 𝑉 → ({𝐴} ∈ sngl 𝐵 ↔ {𝐴} ∈ tag 𝐵)) | ||
Theorem | bj-tagci 34298 | Characterization of the elements of 𝐵 in terms of elements of its tagged version. (Contributed by BJ, 6-Oct-2018.) |
⊢ (𝐴 ∈ 𝐵 → {𝐴} ∈ tag 𝐵) | ||
Theorem | bj-tagcg 34299 | Characterization of the elements of 𝐵 in terms of elements of its tagged version. (Contributed by BJ, 6-Oct-2018.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ {𝐴} ∈ tag 𝐵)) | ||
Theorem | bj-taginv 34300* | Inverse of tagging. (Contributed by BJ, 6-Oct-2018.) |
⊢ 𝐴 = {𝑥 ∣ {𝑥} ∈ tag 𝐴} |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |