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-28695) |
Hilbert Space Explorer
(28696-30218) |
Users' Mathboxes
(30219-44955) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | bj-rexcom4bv 34201* | Version of rexcom4b 3524 and bj-rexcom4b 34202 with a disjoint variable condition on 𝑥, 𝑉, hence removing dependency on df-sb 2070 and df-clab 2800 (so that it depends on df-clel 2893 and df-rex 3144 only on top of first-order logic). Prefer its use over bj-rexcom4b 34202 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 34202* | Remove from rexcom4b 3524 dependency on ax-ext 2793 and ax-13 2390 (and on df-or 844, df-cleq 2814, df-nfc 2963, df-v 3496). The hypothesis uses 𝑉 instead of V (see bj-isseti 34197 for the motivation). Use bj-rexcom4bv 34201 instead when sufficient (in particular when 𝑉 is substituted for V). (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.) |
⊢ 𝐵 ∈ 𝑉 ⇒ ⊢ (∃𝑥∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵) ↔ ∃𝑦 ∈ 𝐴 𝜑) | ||
Theorem | bj-ceqsalt0 34203 | The FOL content of ceqsalt 3527. Lemma for bj-ceqsalt 34205 and bj-ceqsaltv 34206. (Contributed by BJ, 26-Sep-2019.) (Proof modification is discouraged.) |
⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝜃 → (𝜑 ↔ 𝜓)) ∧ ∃𝑥𝜃) → (∀𝑥(𝜃 → 𝜑) ↔ 𝜓)) | ||
Theorem | bj-ceqsalt1 34204 | The FOL content of ceqsalt 3527. Lemma for bj-ceqsalt 34205 and bj-ceqsaltv 34206. TODO: consider removing if it does not add anything to bj-ceqsalt0 34203. (Contributed by BJ, 26-Sep-2019.) (Proof modification is discouraged.) |
⊢ (𝜃 → ∃𝑥𝜒) ⇒ ⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝜒 → (𝜑 ↔ 𝜓)) ∧ 𝜃) → (∀𝑥(𝜒 → 𝜑) ↔ 𝜓)) | ||
Theorem | bj-ceqsalt 34205* | Remove from ceqsalt 3527 dependency on ax-ext 2793 (and on df-cleq 2814 and df-v 3496). Note: this is not doable with ceqsralt 3528 (or ceqsralv 3533), which uses eleq1 2900, but the same dependence removal is possible for ceqsalg 3529, ceqsal 3531, ceqsalv 3532, cgsexg 3537, cgsex2g 3538, cgsex4g 3539, ceqsex 3540, ceqsexv 3541, ceqsex2 3543, ceqsex2v 3544, ceqsex3v 3545, ceqsex4v 3546, ceqsex6v 3547, ceqsex8v 3548, gencbvex 3549 (after changing 𝐴 = 𝑦 to 𝑦 = 𝐴), gencbvex2 3550, gencbval 3551, vtoclgft 3553 (it uses Ⅎ, whose justification nfcjust 2962 does not use ax-ext 2793) and several other vtocl* theorems (see for instance bj-vtoclg1f 34237). See also bj-ceqsaltv 34206. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.) |
⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝑉) → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓)) | ||
Theorem | bj-ceqsaltv 34206* | Version of bj-ceqsalt 34205 with a disjoint variable condition on 𝑥, 𝑉, removing dependency on df-sb 2070 and df-clab 2800. Prefer its use over bj-ceqsalt 34205 when sufficient (in particular when 𝑉 is substituted for V). (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.) |
⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝑉) → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓)) | ||
Theorem | bj-ceqsalg0 34207 | The FOL content of ceqsalg 3529. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝜒 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥𝜒 → (∀𝑥(𝜒 → 𝜑) ↔ 𝜓)) | ||
Theorem | bj-ceqsalg 34208* | Remove from ceqsalg 3529 dependency on ax-ext 2793 (and on df-cleq 2814 and df-v 3496). See also bj-ceqsalgv 34210. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓)) | ||
Theorem | bj-ceqsalgALT 34209* | Alternate proof of bj-ceqsalg 34208. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓)) | ||
Theorem | bj-ceqsalgv 34210* | Version of bj-ceqsalg 34208 with a disjoint variable condition on 𝑥, 𝑉, removing dependency on df-sb 2070 and df-clab 2800. Prefer its use over bj-ceqsalg 34208 when sufficient (in particular when 𝑉 is substituted for V). (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓)) | ||
Theorem | bj-ceqsalgvALT 34211* | Alternate proof of bj-ceqsalgv 34210. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓)) | ||
Theorem | bj-ceqsal 34212* | Remove from ceqsal 3531 dependency on ax-ext 2793 (and on df-cleq 2814, df-v 3496, df-clab 2800, df-sb 2070). (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓) | ||
Theorem | bj-ceqsalv 34213* | Remove from ceqsalv 3532 dependency on ax-ext 2793 (and on df-cleq 2814, df-v 3496, df-clab 2800, df-sb 2070). (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.) |
⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓) | ||
Theorem | bj-spcimdv 34214* | Remove from spcimdv 3592 dependency on ax-9 2124, ax-10 2145, ax-11 2161, ax-13 2390, ax-ext 2793, df-cleq 2814 (and df-nfc 2963, df-v 3496, df-or 844, df-tru 1540, df-nf 1785). For an even more economical version, see bj-spcimdvv 34215. (Contributed by BJ, 30-Nov-2020.) (Proof modification is discouraged.) |
⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥𝜓 → 𝜒)) | ||
Theorem | bj-spcimdvv 34215* | Remove from spcimdv 3592 dependency on ax-7 2015, ax-8 2116, ax-10 2145, ax-11 2161, ax-12 2177 ax-13 2390, ax-ext 2793, df-cleq 2814, df-clab 2800 (and df-nfc 2963, df-v 3496, 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 34214. (Contributed by BJ, 3-Nov-2021.) (Proof modification is discouraged.) |
⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥𝜓 → 𝜒)) | ||
Theorem | elelb 34216 | 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 34217 | 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 34218 | The nonfreeness quantifier for classes defines a symmetric binary relation on var metavariables (irreflexivity is proved by nfnid 5276 with additional axioms; see also nfcv 2977). This could be proved from aecom 2449 and nfcvb 5277 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 2827 instead of equcomd 2026; removing dependency on ax-ext 2793 is possible: prove weak versions (i.e. replace classes with setvars) of drnfc1 2997, eleq2d 2898 (using elequ2 2129), nfcvf 3007, dvelimc 3006, dvelimdc 3005, nfcvf2 3008. (Proof modification is discouraged.) |
⊢ (Ⅎ𝑥𝑦 ↔ Ⅎ𝑦𝑥) | ||
Note: now that the proposals have been adopted as df-cleq 2814 and df-clel 2893, and that ax9ALT 2817 is in the main section, we only keep bj-ax9 34219 here as a weaker version of ax9ALT 2817 proved without ax-8 2116. | ||
Theorem | bj-ax9 34219* | Proof of ax-9 2124 from Tarski's FOL=, sp 2182, dfcleq 2815 and ax-ext 2793 (with two extra disjoint variable conditions on 𝑥, 𝑧 and 𝑦, 𝑧). See ax9ALT 2817 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 3823, sbcel1g 4365, sbcel2 4367, sbcel12 4360, sbceqg 4361, csbvarg 4383. | ||
Theorem | bj-sbeqALT 34220* | Substitution in an equality (use the more general version bj-sbeq 34221 instead, without disjoint variable condition). (Contributed by BJ, 6-Oct-2018.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ([𝑦 / 𝑥]𝐴 = 𝐵 ↔ ⦋𝑦 / 𝑥⦌𝐴 = ⦋𝑦 / 𝑥⦌𝐵) | ||
Theorem | bj-sbeq 34221 | Distribute proper substitution through an equality relation. (See sbceqg 4361). (Contributed by BJ, 6-Oct-2018.) |
⊢ ([𝑦 / 𝑥]𝐴 = 𝐵 ↔ ⦋𝑦 / 𝑥⦌𝐴 = ⦋𝑦 / 𝑥⦌𝐵) | ||
Theorem | bj-sbceqgALT 34222 | Distribute proper substitution through an equality relation. Alternate proof of sbceqg 4361. (Contributed by BJ, 6-Oct-2018.) Proof modification is discouraged to avoid using sbceqg 4361, but the Metamath program "MM-PA> MINIMIZE_WITH * / EXCEPT sbceqg" command is ok. (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵 = 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶)) | ||
Theorem | bj-csbsnlem 34223* | Lemma for bj-csbsn 34224 (in this lemma, 𝑥 cannot occur in 𝐴). (Contributed by BJ, 6-Oct-2018.) (New usage is discouraged.) |
⊢ ⦋𝐴 / 𝑥⦌{𝑥} = {𝐴} | ||
Theorem | bj-csbsn 34224 | Substitution in a singleton. (Contributed by BJ, 6-Oct-2018.) |
⊢ ⦋𝐴 / 𝑥⦌{𝑥} = {𝐴} | ||
Theorem | bj-sbel1 34225* | Version of sbcel1g 4365 when substituting a set. (Note: one could have a corresponding version of sbcel12 4360 when substituting a set, but the point here is that the antecedent of sbcel1g 4365 is not needed when substituting a set.) (Contributed by BJ, 6-Oct-2018.) |
⊢ ([𝑦 / 𝑥]𝐴 ∈ 𝐵 ↔ ⦋𝑦 / 𝑥⦌𝐴 ∈ 𝐵) | ||
Theorem | bj-abv 34226 | 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 34227 | The class of sets verifying a falsity is the empty set (closed form of abf 4356). (Contributed by BJ, 24-Jul-2019.) (Proof modification is discouraged.) |
⊢ (∀𝑥 ¬ 𝜑 → {𝑥 ∣ 𝜑} = ∅) | ||
Theorem | bj-abf 34228 | Shorter proof of abf 4356 (which should be kept as abfALT). (Contributed by BJ, 24-Jul-2019.) (Proof modification is discouraged.) |
⊢ ¬ 𝜑 ⇒ ⊢ {𝑥 ∣ 𝜑} = ∅ | ||
Theorem | bj-csbprc 34229 | More direct proof of csbprc 4358 (fewer essential steps). (Contributed by BJ, 24-Jul-2019.) (Proof modification is discouraged.) |
⊢ (¬ 𝐴 ∈ V → ⦋𝐴 / 𝑥⦌𝐵 = ∅) | ||
Theorem | bj-exlimvmpi 34230* | A Fol lemma (exlimiv 1931 followed by mpi 20). (Contributed by BJ, 2-Jul-2022.) (Proof modification is discouraged.) |
⊢ (𝜒 → (𝜑 → 𝜓)) & ⊢ 𝜑 ⇒ ⊢ (∃𝑥𝜒 → 𝜓) | ||
Theorem | bj-exlimmpi 34231 | Lemma for bj-vtoclg1f1 34236 (an instance of this lemma is a version of bj-vtoclg1f1 34236 where 𝑥 and 𝑦 are identified). (Contributed by BJ, 30-Apr-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝜒 → (𝜑 → 𝜓)) & ⊢ 𝜑 ⇒ ⊢ (∃𝑥𝜒 → 𝜓) | ||
Theorem | bj-exlimmpbi 34232 | Lemma for theorems of the vtoclg 3567 family. (Contributed by BJ, 3-Oct-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝜒 → (𝜑 ↔ 𝜓)) & ⊢ 𝜑 ⇒ ⊢ (∃𝑥𝜒 → 𝜓) | ||
Theorem | bj-exlimmpbir 34233 | Lemma for theorems of the vtoclg 3567 family. (Contributed by BJ, 3-Oct-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜒 → (𝜑 ↔ 𝜓)) & ⊢ 𝜓 ⇒ ⊢ (∃𝑥𝜒 → 𝜑) | ||
Theorem | bj-vtoclf 34234* | Remove dependency on ax-ext 2793, df-clab 2800 and df-cleq 2814 (and df-sb 2070 and df-v 3496) from vtoclf 3558. (Contributed by BJ, 6-Oct-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ 𝐴 ∈ 𝑉 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ 𝜑 ⇒ ⊢ 𝜓 | ||
Theorem | bj-vtocl 34235* | Remove dependency on ax-ext 2793, df-clab 2800 and df-cleq 2814 (and df-sb 2070 and df-v 3496) from vtocl 3559. (Contributed by BJ, 6-Oct-2019.) (Proof modification is discouraged.) |
⊢ 𝐴 ∈ 𝑉 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ 𝜑 ⇒ ⊢ 𝜓 | ||
Theorem | bj-vtoclg1f1 34236* | The FOL content of vtoclg1f 3566 (hence not using ax-ext 2793, df-cleq 2814, df-nfc 2963, df-v 3496). 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 2793; 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 34237* | Reprove vtoclg1f 3566 from bj-vtoclg1f1 34236. This removes dependency on ax-ext 2793, df-cleq 2814 and df-v 3496. Use bj-vtoclg1fv 34238 instead when sufficient (in particular when 𝑉 is substituted for V). (Contributed by BJ, 14-Sep-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝐴 → (𝜑 → 𝜓)) & ⊢ 𝜑 ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝜓) | ||
Theorem | bj-vtoclg1fv 34238* | Version of bj-vtoclg1f 34237 with a disjoint variable condition on 𝑥, 𝑉. This removes dependency on df-sb 2070 and df-clab 2800. Prefer its use over bj-vtoclg1f 34237 when sufficient (in particular when 𝑉 is substituted for V). (Contributed by BJ, 14-Sep-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝐴 → (𝜑 → 𝜓)) & ⊢ 𝜑 ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝜓) | ||
Theorem | bj-vtoclg 34239* | A version of vtoclg 3567 with an additional disjoint variable condition (which is removable if we allow use of df-clab 2800, see bj-vtoclg1f 34237), which requires fewer axioms (i.e., removes dependency on ax-6 1970, ax-7 2015, ax-9 2124, ax-12 2177, ax-ext 2793, df-clab 2800, df-cleq 2814, df-v 3496). (Contributed by BJ, 2-Jul-2022.) (Proof modification is discouraged.) |
⊢ (𝑥 = 𝐴 → (𝜑 → 𝜓)) & ⊢ 𝜑 ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝜓) | ||
Theorem | bj-rabbida2 34240 | Version of rabbidva2 3476 with disjoint variable condition replaced by nonfreeness hypothesis. (Contributed by BJ, 27-Apr-2019.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐵 ∧ 𝜒))) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒}) | ||
Theorem | bj-rabeqd 34241 | Deduction form of rabeq 3483. Note that contrary to rabeq 3483 it has no disjoint variable condition. (Contributed by BJ, 27-Apr-2019.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜓}) | ||
Theorem | bj-rabeqbid 34242 | Version of rabeqbidv 3485 with two disjoint variable conditions removed and the third replaced by a nonfreeness hypothesis. (Contributed by BJ, 27-Apr-2019.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒}) | ||
Theorem | bj-rabeqbida 34243 | Version of rabeqbidva 3486 with two disjoint variable conditions removed and the third replaced by a nonfreeness hypothesis. (Contributed by BJ, 27-Apr-2019.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒}) | ||
Theorem | bj-seex 34244* | Version of seex 5518 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 34245* | Version of df-nfc 2963 with a disjoint variable condition replaced with a nonfreeness hypothesis. (Contributed by BJ, 2-May-2019.) |
⊢ Ⅎ𝑦𝐴 ⇒ ⊢ (Ⅎ𝑥𝐴 ↔ ∀𝑦Ⅎ𝑥 𝑦 ∈ 𝐴) | ||
Theorem | bj-zfauscl 34246* |
General version of zfauscl 5205.
Remark: the comment in zfauscl 5205 is misleading: the essential use of ax-ext 2793 is the one via eleq2 2901 and not the one via vtocl 3559, since the latter can be proved without ax-ext 2793 (see bj-vtoclg 34239). (Contributed by BJ, 2-Jul-2022.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ 𝑉 → ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝜑))) | ||
A few additional theorems on class abstractions and restricted class abstractions. | ||
Theorem | bj-unrab 34247* | Generalization of unrab 4274. Equality need not hold. (Contributed by BJ, 21-Apr-2019.) |
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∪ {𝑥 ∈ 𝐵 ∣ 𝜓}) ⊆ {𝑥 ∈ (𝐴 ∪ 𝐵) ∣ (𝜑 ∨ 𝜓)} | ||
Theorem | bj-inrab 34248 | Generalization of inrab 4275. (Contributed by BJ, 21-Apr-2019.) |
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ {𝑥 ∈ 𝐵 ∣ 𝜓}) = {𝑥 ∈ (𝐴 ∩ 𝐵) ∣ (𝜑 ∧ 𝜓)} | ||
Theorem | bj-inrab2 34249 | Shorter proof of inrab 4275. (Contributed by BJ, 21-Apr-2019.) (Proof modification is discouraged.) |
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ {𝑥 ∈ 𝐴 ∣ 𝜓}) = {𝑥 ∈ 𝐴 ∣ (𝜑 ∧ 𝜓)} | ||
Theorem | bj-inrab3 34250* | Generalization of dfrab3ss 4281, which it may shorten. (Contributed by BJ, 21-Apr-2019.) (Revised by OpenAI, 7-Jul-2020.) |
⊢ (𝐴 ∩ {𝑥 ∈ 𝐵 ∣ 𝜑}) = ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ 𝐵) | ||
Theorem | bj-rabtr 34251* | Restricted class abstraction with true formula. (Contributed by BJ, 22-Apr-2019.) |
⊢ {𝑥 ∈ 𝐴 ∣ ⊤} = 𝐴 | ||
Theorem | bj-rabtrALT 34252* | Alternate proof of bj-rabtr 34251. (Contributed by BJ, 22-Apr-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ {𝑥 ∈ 𝐴 ∣ ⊤} = 𝐴 | ||
Theorem | bj-rabtrAUTO 34253* | Proof of bj-rabtr 34251 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 34254 | Syntax for restricted nonfreeness. |
wff Ⅎ𝑥 ∈ 𝐴𝜑 | ||
Definition | df-bj-rnf 34255 | 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 34256) and then two versions (bj-ru1 34257 and bj-ru 34258). Special attention is put on minimizing axiom depencencies. | ||
Theorem | bj-ru0 34256* | The FOL part of Russell's paradox ru 3771 (see also bj-ru1 34257, bj-ru 34258). Use of elequ1 2121, bj-elequ12 34012 (instead of eleq1 2900, eleq12d 2907 as in ru 3771) permits to remove dependency on ax-10 2145, ax-11 2161, ax-12 2177, ax-ext 2793, df-sb 2070, df-clab 2800, df-cleq 2814, df-clel 2893. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.) |
⊢ ¬ ∀𝑥(𝑥 ∈ 𝑦 ↔ ¬ 𝑥 ∈ 𝑥) | ||
Theorem | bj-ru1 34257* | A version of Russell's paradox ru 3771 (see also bj-ru 34258). (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.) |
⊢ ¬ ∃𝑦 𝑦 = {𝑥 ∣ ¬ 𝑥 ∈ 𝑥} | ||
Theorem | bj-ru 34258 | Remove dependency on ax-13 2390 (and df-v 3496) from Russell's paradox ru 3771 expressed with primitive symbols and with a class variable 𝑉. Note the more economical use of bj-elissetv 34194 instead of isset 3506 to avoid use of df-v 3496. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.) |
⊢ ¬ {𝑥 ∣ ¬ 𝑥 ∈ 𝑥} ∈ 𝑉 | ||
Theorem | currysetlem 34259* | Lemma for currysetlem 34259, where it is used with (𝑥 ∈ 𝑥 → 𝜑) substituted for 𝜓. (Contributed by BJ, 23-Sep-2023.) This proof is intuitionistically valid. (Proof modification is discouraged.) |
⊢ ({𝑥 ∣ 𝜓} ∈ 𝑉 → ({𝑥 ∣ 𝜓} ∈ {𝑥 ∣ (𝑥 ∈ 𝑥 → 𝜑)} ↔ ({𝑥 ∣ 𝜓} ∈ {𝑥 ∣ 𝜓} → 𝜑))) | ||
Theorem | curryset 34260* | 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 34264. (Contributed by BJ, 23-Sep-2023.) This proof is intuitionistically valid. (Proof modification is discouraged.) |
⊢ ¬ {𝑥 ∣ (𝑥 ∈ 𝑥 → 𝜑)} ∈ 𝑉 | ||
Theorem | currysetlem1 34261* | Lemma for currysetALT 34264. (Contributed by BJ, 23-Sep-2023.) This proof is intuitionistically valid. (Proof modification is discouraged.) |
⊢ 𝑋 = {𝑥 ∣ (𝑥 ∈ 𝑥 → 𝜑)} ⇒ ⊢ (𝑋 ∈ 𝑉 → (𝑋 ∈ 𝑋 ↔ (𝑋 ∈ 𝑋 → 𝜑))) | ||
Theorem | currysetlem2 34262* | Lemma for currysetALT 34264. (Contributed by BJ, 23-Sep-2023.) This proof is intuitionistically valid. (Proof modification is discouraged.) |
⊢ 𝑋 = {𝑥 ∣ (𝑥 ∈ 𝑥 → 𝜑)} ⇒ ⊢ (𝑋 ∈ 𝑉 → (𝑋 ∈ 𝑋 → 𝜑)) | ||
Theorem | currysetlem3 34263* | Lemma for currysetALT 34264. (Contributed by BJ, 23-Sep-2023.) This proof is intuitionistically valid. (Proof modification is discouraged.) |
⊢ 𝑋 = {𝑥 ∣ (𝑥 ∈ 𝑥 → 𝜑)} ⇒ ⊢ ¬ 𝑋 ∈ 𝑉 | ||
Theorem | currysetALT 34264* | Alternate proof of curryset 34260, 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 34265* | Inference associated with n0 4310. Shortens 2ndcdisj 22064 (2888>2878), notzfaus 5262 (264>253). (Contributed by BJ, 22-Apr-2019.) |
⊢ 𝐴 ≠ ∅ ⇒ ⊢ ∃𝑥 𝑥 ∈ 𝐴 | ||
Theorem | bj-disjcsn 34266 | A class is disjoint from its singleton. A consequence of regularity. Shorter proof than bnj521 32007 and does not depend on df-ne 3017. (Contributed by BJ, 4-Apr-2019.) |
⊢ (𝐴 ∩ {𝐴}) = ∅ | ||
Theorem | bj-disjsn01 34267 | Disjointness of the singletons containing 0 and 1. This is a consequence of bj-disjcsn 34266 but the present proof does not use regularity. (Contributed by BJ, 4-Apr-2019.) (Proof modification is discouraged.) |
⊢ ({∅} ∩ {1o}) = ∅ | ||
Theorem | bj-0nel1 34268 | The empty set does not belong to {1o}. (Contributed by BJ, 6-Apr-2019.) |
⊢ ∅ ∉ {1o} | ||
Theorem | bj-1nel0 34269 | 1o does not belong to {∅}. (Contributed by BJ, 6-Apr-2019.) |
⊢ 1o ∉ {∅} | ||
A few utility theorems on direct products. | ||
Theorem | bj-xpimasn 34270 | The image of a singleton, general case. [Change and relabel xpimasn 6042 accordingly, maybe to xpima2sn.] (Contributed by BJ, 6-Apr-2019.) |
⊢ ((𝐴 × 𝐵) “ {𝑋}) = if(𝑋 ∈ 𝐴, 𝐵, ∅) | ||
Theorem | bj-xpima1sn 34271 | The image of a singleton by a direct product, empty case. [Change and relabel xpimasn 6042 accordingly, maybe to xpima2sn.] (Contributed by BJ, 6-Apr-2019.) |
⊢ (¬ 𝑋 ∈ 𝐴 → ((𝐴 × 𝐵) “ {𝑋}) = ∅) | ||
Theorem | bj-xpima1snALT 34272 | Alternate proof of bj-xpima1sn 34271. (Contributed by BJ, 6-Apr-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ 𝑋 ∈ 𝐴 → ((𝐴 × 𝐵) “ {𝑋}) = ∅) | ||
Theorem | bj-xpima2sn 34273 | The image of a singleton by a direct product, nonempty case. [To replace xpimasn 6042] (Contributed by BJ, 6-Apr-2019.) (Proof modification is discouraged.) |
⊢ (𝑋 ∈ 𝐴 → ((𝐴 × 𝐵) “ {𝑋}) = 𝐵) | ||
Theorem | bj-xpnzex 34274 | 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 7625 (up to commutation in the product). (Contributed by BJ, 6-Oct-2018.) (Proof modification is discouraged.) |
⊢ (𝐴 ≠ ∅ → ((𝐴 × 𝐵) ∈ 𝑉 → 𝐵 ∈ V)) | ||
Theorem | bj-xpexg2 34275 | Curried (exported) form of xpexg 7473. (Contributed by BJ, 2-Apr-2019.) |
⊢ (𝐴 ∈ 𝑉 → (𝐵 ∈ 𝑊 → (𝐴 × 𝐵) ∈ V)) | ||
Theorem | bj-xpnzexb 34276 | 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 34277* | 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 34278* | The class of sets "whose singletons" belong to a set is a set. Nice application of ax-rep 5190. (Contributed by BJ, 6-Oct-2018.) |
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V) | ||
Theorem | bj-clex 34279* | Sethood of certain classes. (Contributed by BJ, 2-Apr-2019.) |
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∣ {𝑥} ∈ (𝐴 “ 𝐵)} ∈ V) | ||
Syntax | bj-csngl 34280 | Syntax for singletonization. (Contributed by BJ, 6-Oct-2018.) |
class sngl 𝐴 | ||
Definition | df-bj-sngl 34281* | 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 34282 | Substitution property for sngl. (Contributed by BJ, 6-Oct-2018.) |
⊢ (𝐴 = 𝐵 → sngl 𝐴 = sngl 𝐵) | ||
Theorem | bj-elsngl 34283* | Characterization of the elements of the singletonization of a class. (Contributed by BJ, 6-Oct-2018.) |
⊢ (𝐴 ∈ sngl 𝐵 ↔ ∃𝑥 ∈ 𝐵 𝐴 = {𝑥}) | ||
Theorem | bj-snglc 34284 | Characterization of the elements of 𝐴 in terms of elements of its singletonization. (Contributed by BJ, 6-Oct-2018.) |
⊢ (𝐴 ∈ 𝐵 ↔ {𝐴} ∈ sngl 𝐵) | ||
Theorem | bj-snglss 34285 | The singletonization of a class is included in its powerclass. (Contributed by BJ, 6-Oct-2018.) |
⊢ sngl 𝐴 ⊆ 𝒫 𝐴 | ||
Theorem | bj-0nelsngl 34286 | The empty set is not a member of a singletonization (neither is any nonsingleton, in particular any von Neuman ordinal except possibly df-1o 8102). (Contributed by BJ, 6-Oct-2018.) |
⊢ ∅ ∉ sngl 𝐴 | ||
Theorem | bj-snglinv 34287* | Inverse of singletonization. (Contributed by BJ, 6-Oct-2018.) |
⊢ 𝐴 = {𝑥 ∣ {𝑥} ∈ sngl 𝐴} | ||
Theorem | bj-snglex 34288 | 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 34289 | Syntax for the tagged copy of a class. (Contributed by BJ, 6-Oct-2018.) |
class tag 𝐴 | ||
Definition | df-bj-tag 34290 | 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 34291 | Substitution property for tag. (Contributed by BJ, 6-Oct-2018.) |
⊢ (𝐴 = 𝐵 → tag 𝐴 = tag 𝐵) | ||
Theorem | bj-eltag 34292* | Characterization of the elements of the tagging of a class. (Contributed by BJ, 6-Oct-2018.) |
⊢ (𝐴 ∈ tag 𝐵 ↔ (∃𝑥 ∈ 𝐵 𝐴 = {𝑥} ∨ 𝐴 = ∅)) | ||
Theorem | bj-0eltag 34293 | The empty set belongs to the tagging of a class. (Contributed by BJ, 6-Apr-2019.) |
⊢ ∅ ∈ tag 𝐴 | ||
Theorem | bj-tagn0 34294 | The tagging of a class is nonempty. (Contributed by BJ, 6-Apr-2019.) |
⊢ tag 𝐴 ≠ ∅ | ||
Theorem | bj-tagss 34295 | The tagging of a class is included in its powerclass. (Contributed by BJ, 6-Oct-2018.) |
⊢ tag 𝐴 ⊆ 𝒫 𝐴 | ||
Theorem | bj-snglsstag 34296 | The singletonization is included in the tagging. (Contributed by BJ, 6-Oct-2018.) |
⊢ sngl 𝐴 ⊆ tag 𝐴 | ||
Theorem | bj-sngltagi 34297 | The singletonization is included in the tagging. (Contributed by BJ, 6-Oct-2018.) |
⊢ (𝐴 ∈ sngl 𝐵 → 𝐴 ∈ tag 𝐵) | ||
Theorem | bj-sngltag 34298 | The singletonization and the tagging of a set contain the same singletons. (Contributed by BJ, 6-Oct-2018.) |
⊢ (𝐴 ∈ 𝑉 → ({𝐴} ∈ sngl 𝐵 ↔ {𝐴} ∈ tag 𝐵)) | ||
Theorem | bj-tagci 34299 | Characterization of the elements of 𝐵 in terms of elements of its tagged version. (Contributed by BJ, 6-Oct-2018.) |
⊢ (𝐴 ∈ 𝐵 → {𝐴} ∈ tag 𝐵) | ||
Theorem | bj-tagcg 34300 | Characterization of the elements of 𝐵 in terms of elements of its tagged version. (Contributed by BJ, 6-Oct-2018.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ {𝐴} ∈ tag 𝐵)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |