![]() |
Metamath
Proof Explorer Theorem List (p. 354 of 473) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-29860) |
![]() (29861-31383) |
![]() (31384-47242) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ax11-pm2 35301* | 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 2316, nfsb 2525, sbal 2159, sb8 2519. See also ax11-pm 35297. (Contributed by BJ, 15-Sep-2018.) (Proof modification is discouraged.) |
⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑) | ||
Theorem | bj-sbsb 35302 | Biconditional showing two possible (dual) definitions of substitution df-sb 2068 not using dummy variables. (Contributed by BJ, 19-Mar-2021.) |
⊢ (((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) ↔ (∀𝑥(𝑥 = 𝑦 → 𝜑) ∨ (𝑥 = 𝑦 ∧ 𝜑))) | ||
Theorem | bj-dfsb2 35303 | Alternate (dual) definition of substitution df-sb 2068 not using dummy variables. (Contributed by BJ, 19-Mar-2021.) |
⊢ ([𝑦 / 𝑥]𝜑 ↔ (∀𝑥(𝑥 = 𝑦 → 𝜑) ∨ (𝑥 = 𝑦 ∧ 𝜑))) | ||
Theorem | bj-sbf3 35304 | Substitution has no effect on a bound variable (existential quantifier case); see sbf2 2263. (Contributed by BJ, 2-May-2019.) |
⊢ ([𝑦 / 𝑥]∃𝑥𝜑 ↔ ∃𝑥𝜑) | ||
Theorem | bj-sbf4 35305 | Substitution has no effect on a bound variable (nonfreeness case); see sbf2 2263. (Contributed by BJ, 2-May-2019.) |
⊢ ([𝑦 / 𝑥]Ⅎ𝑥𝜑 ↔ Ⅎ𝑥𝜑) | ||
Theorem | bj-sbnf 35306* | Move nonfree predicate in and out of substitution; see sbal 2159 and sbex 2277. (Contributed by BJ, 2-May-2019.) |
⊢ ([𝑧 / 𝑦]Ⅎ𝑥𝜑 ↔ Ⅎ𝑥[𝑧 / 𝑦]𝜑) | ||
Theorem | bj-eu3f 35307* | Version of eu3v 2568 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 2568. (Contributed by NM, 8-Jul-1994.) (Proof shortened by BJ, 31-May-2019.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦))) | ||
Miscellaneous theorems of first-order logic. | ||
Theorem | bj-sblem1 35308* | Lemma for substitution. (Contributed by BJ, 23-Jul-2023.) |
⊢ (∀𝑥(𝜑 → (𝜓 → 𝜒)) → (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → 𝜒))) | ||
Theorem | bj-sblem2 35309* | Lemma for substitution. (Contributed by BJ, 23-Jul-2023.) |
⊢ (∀𝑥(𝜑 → (𝜒 → 𝜓)) → ((∃𝑥𝜑 → 𝜒) → ∀𝑥(𝜑 → 𝜓))) | ||
Theorem | bj-sblem 35310* | Lemma for substitution. (Contributed by BJ, 23-Jul-2023.) |
⊢ (∀𝑥(𝜑 → (𝜓 ↔ 𝜒)) → (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜒))) | ||
Theorem | bj-sbievw1 35311* | Lemma for substitution. (Contributed by BJ, 23-Jul-2023.) |
⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) → ([𝑦 / 𝑥]𝜑 → 𝜓)) | ||
Theorem | bj-sbievw2 35312* | Lemma for substitution. (Contributed by BJ, 23-Jul-2023.) |
⊢ ([𝑦 / 𝑥](𝜓 → 𝜑) → (𝜓 → [𝑦 / 𝑥]𝜑)) | ||
Theorem | bj-sbievw 35313* | Lemma for substitution. Closed form of equsalvw 2007 and sbievw 2095. (Contributed by BJ, 23-Jul-2023.) |
⊢ ([𝑦 / 𝑥](𝜑 ↔ 𝜓) → ([𝑦 / 𝑥]𝜑 ↔ 𝜓)) | ||
Theorem | bj-sbievv 35314 | Version of sbie 2504 with a second nonfreeness hypothesis and shorter proof. (Contributed by BJ, 18-Jul-2023.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ Ⅎ𝑦𝜑 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓) | ||
Theorem | bj-moeub 35315 | Uniqueness is equivalent to existence being equivalent to unique existence. (Contributed by BJ, 14-Oct-2022.) |
⊢ (∃*𝑥𝜑 ↔ (∃𝑥𝜑 ↔ ∃!𝑥𝜑)) | ||
Theorem | bj-sbidmOLD 35316 | Obsolete proof of sbidm 2512 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 35317* |
Deduction form of dvelim 2449 with disjoint variable conditions. Uncurried
(imported) form of bj-dvelimdv1 35318. 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 1917 can be replaced with nfal 2316 followed by nfn 1860. Remark: nfald 2321 uses ax-11 2154; it might be possible to inline and use ax11w 2126 instead, but there is still a use via 19.12 2320 anyway. (Contributed by BJ, 20-Oct-2021.) (Proof modification is discouraged.) |
⊢ (𝜑 → Ⅎ𝑥𝜒) & ⊢ (𝑧 = 𝑦 → (𝜒 ↔ 𝜓)) ⇒ ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥𝜓) | ||
Theorem | bj-dvelimdv1 35318* | Curried (exported) form of bj-dvelimdv 35317 (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 35319* | A version of dvelim 2449 using the "nonfree" idiom. (Contributed by BJ, 20-Oct-2021.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑧 = 𝑦 → (𝜓 ↔ 𝜑)) ⇒ ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝜑) | ||
Theorem | bj-nfeel2 35320* | Nonfreeness in a membership statement. (Contributed by BJ, 20-Oct-2021.) (Proof modification is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥 𝑦 ∈ 𝑧) | ||
Theorem | bj-axc14nf 35321 | Proof of a version of axc14 2461 using the "nonfree" idiom. (Contributed by BJ, 20-Oct-2021.) (Proof modification is discouraged.) |
⊢ (¬ ∀𝑧 𝑧 = 𝑥 → (¬ ∀𝑧 𝑧 = 𝑦 → Ⅎ𝑧 𝑥 ∈ 𝑦)) | ||
Theorem | bj-axc14 35322 | Alternate proof of axc14 2461 (even when inlining the above results, this gives a shorter proof). (Contributed by BJ, 20-Oct-2021.) (Proof modification is discouraged.) |
⊢ (¬ ∀𝑧 𝑧 = 𝑥 → (¬ ∀𝑧 𝑧 = 𝑦 → (𝑥 ∈ 𝑦 → ∀𝑧 𝑥 ∈ 𝑦))) | ||
Theorem | mobidvALT 35323* | Alternate proof of mobidv 2547 directly from its analogues albidv 1923 and exbidv 1924, using deduction style. Note the proof structure, similar to mobi 2545. (Contributed by Mario Carneiro, 7-Oct-2016.) Reduce axiom dependencies and shorten proof. Remove dependency on ax-6 1971, ax-7 2011, ax-12 2171 by adapting proof of mobid 2548. (Revised by BJ, 26-Sep-2022.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃*𝑥𝜓 ↔ ∃*𝑥𝜒)) | ||
Theorem | sbn1ALT 35324 | Alternate proof of sbn1 2105, not using the false constant. (Contributed by BJ, 18-Sep-2024.) (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 2707, df-clab 2714, df-cleq 2728, df-clel 2814 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 in set.mm. It states: every formula in the language of FOL + ∈ + class terms, but without class variables, is provably equivalent (over {FOL, ax-ext 2707, df-clab 2714, df-cleq 2728, df-clel 2814 }) 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 six following forms: for equality, 𝑥 = {𝑦 ∣ 𝜑}, {𝑥 ∣ 𝜑} = 𝑦, {𝑥 ∣ 𝜑} = {𝑦 ∣ 𝜓}, and for membership, 𝑦 ∈ {𝑥 ∣ 𝜑}, {𝑥 ∣ 𝜑} ∈ 𝑦, {𝑥 ∣ 𝜑} ∈ {𝑦 ∣ 𝜓}. These cases are dealt with by eliminable-veqab 35332, eliminable-abeqv 35333, eliminable-abeqab 35334, eliminable-velab 35331, eliminable-abelv 35335, eliminable-abelab 35336 respectively, which are all proved from {FOL, ax-ext 2707, df-clab 2714, df-cleq 2728, df-clel 2814 }. (Details on the proof of the above six theorems. To understand how they were systematically proved, look at the theorems "eliminablei" below, which are special instances of df-clab 2714, dfcleq 2729 (proved from {FOL, ax-ext 2707, df-cleq 2728 }), and dfclel 2815 (proved from {FOL, df-clel 2814 }). 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 35326, eliminable2b 35327 and eliminable3a 35329, 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 1540, 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 2714 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 2714, ax-ext 2707 and df-cleq 2728 are sufficient (over FOL) to eliminate class terms. To prove that { df-clab 2714, df-cleq 2728, df-clel 2814 } provides a definitional extension of {FOL, ax-ext 2707 }, one needs to prove both 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 2714, df-cleq 2728, df-clel 2814 }. 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 2707 }. 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 2714, df-cleq 2728, df-clel 2814 }. It involves a careful case study on the structure of the proof tree. | ||
Theorem | eliminable1 35325 | 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 35326* | 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 35327* | 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 35328* | 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 35329* | 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 35330* | 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 | eliminable-velab 35331 | A theorem used to prove the base case of the Eliminability Theorem (see section comment): variable belongs to abstraction. (Contributed by BJ, 30-Apr-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ [𝑦 / 𝑥]𝜑) | ||
Theorem | eliminable-veqab 35332* | A theorem used to prove the base case of the Eliminability Theorem (see section comment): variable equals abstraction. (Contributed by BJ, 30-Apr-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 = {𝑦 ∣ 𝜑} ↔ ∀𝑧(𝑧 ∈ 𝑥 ↔ [𝑧 / 𝑦]𝜑)) | ||
Theorem | eliminable-abeqv 35333* | A theorem used to prove the base case of the Eliminability Theorem (see section comment): abstraction equals variable. (Contributed by BJ, 30-Apr-2024.) Beware not to use symmetry of class equality. (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ({𝑥 ∣ 𝜑} = 𝑦 ↔ ∀𝑧([𝑧 / 𝑥]𝜑 ↔ 𝑧 ∈ 𝑦)) | ||
Theorem | eliminable-abeqab 35334* | A theorem used to prove the base case of the Eliminability Theorem (see section comment): abstraction equals abstraction. (Contributed by BJ, 30-Apr-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ({𝑥 ∣ 𝜑} = {𝑦 ∣ 𝜓} ↔ ∀𝑧([𝑧 / 𝑥]𝜑 ↔ [𝑧 / 𝑦]𝜓)) | ||
Theorem | eliminable-abelv 35335* | A theorem used to prove the base case of the Eliminability Theorem (see section comment): abstraction belongs to variable. (Contributed by BJ, 30-Apr-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ({𝑥 ∣ 𝜑} ∈ 𝑦 ↔ ∃𝑧(∀𝑡(𝑡 ∈ 𝑧 ↔ [𝑡 / 𝑥]𝜑) ∧ 𝑧 ∈ 𝑦)) | ||
Theorem | eliminable-abelab 35336* | A theorem used to prove the base case of the Eliminability Theorem (see section comment): abstraction belongs to abstraction. (Contributed by BJ, 30-Apr-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ({𝑥 ∣ 𝜑} ∈ {𝑦 ∣ 𝜓} ↔ ∃𝑧(∀𝑡(𝑡 ∈ 𝑧 ↔ [𝑡 / 𝑥]𝜑) ∧ [𝑧 / 𝑦]𝜓)) | ||
A few results about classes can be proved without using ax-ext 2707. One could move all theorems from cab 2713 to df-clel 2814 (except for dfcleq 2729 and cvjust 2730) 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 2728. Note that without ax-ext 2707, the $a-statements df-clab 2714, df-cleq 2728, and df-clel 2814 are no longer eliminable (see previous section) (but PROBABLY df-clab 2714 is still conservative , while df-cleq 2728 and df-clel 2814 are not). This is not a reason not to study what is provable with them but without ax-ext 2707, 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 2106, wel 2107, ax-8 2108, ax-9 2116). Remark: the weakening of eleq1 2825 / eleq2 2826 to eleq1w 2820 / eleq2w 2821 can also be done with eleq1i 2828, eqeltri 2834, eqeltrri 2835, eleq1a 2833, eleq1d 2822, eqeltrd 2838, eqeltrrd 2839, eqneltrd 2857, eqneltrrd 2858, nelneq 2861. Remark: possibility to remove dependency on ax-10 2137, ax-11 2154, ax-13 2370 from nfcri 2894 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 2919. | ||
Theorem | bj-denoteslem 35337* | Lemma for bj-denotes 35338. (Contributed by BJ, 24-Apr-2024.) (Proof modification is discouraged.) |
⊢ (∃𝑥 𝑥 = 𝐴 ↔ 𝐴 ∈ {𝑦 ∣ ⊤}) | ||
Theorem | bj-denotes 35338* |
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 274 (to add an intermediate proposition ∃𝑧𝑧 = 𝐴 with a fresh 𝑧), cbvexvw 2040, and eqeq1 2740, requires the core axioms and { ax-9 2116, ax-ext 2707, df-cleq 2728 } whereas this proof requires the core axioms and { ax-8 2108, df-clab 2714, df-clel 2814 }. Theorem bj-issetwt 35341 proves that "existing" is equivalent to being a member of a class abstraction. It also requires, with the present proof, { ax-8 2108, df-clab 2714, df-clel 2814 } (whereas with the shorter proof from cbvexvw 2040 and eqeq1 2740 it would require { ax-8 2108, ax-9 2116, ax-ext 2707, df-clab 2714, df-cleq 2728, df-clel 2814 }). That every class is equal to a class abstraction is proved by abid1 2874, which requires { ax-8 2108, ax-9 2116, ax-ext 2707, df-clab 2714, df-cleq 2728, df-clel 2814 }. Note that there is no disjoint variable condition on 𝑥, 𝑦 but the theorem does not depend on ax-13 2370. Actually, the proof depends only on the logical axioms ax-1 6 through ax-7 2011 and sp 2176. 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 2707 and df-cleq 2728 (e.g., eqid 2736 and eqeq1 2740). In particular, one cannot even prove ⊢ ∃𝑥𝑥 = 𝐴 ⇒ ⊢ 𝐴 = 𝐴 without ax-ext 2707 and df-cleq 2728. (Contributed by BJ, 29-Apr-2019.) (Proof modification is discouraged.) |
⊢ (∃𝑥 𝑥 = 𝐴 ↔ ∃𝑦 𝑦 = 𝐴) | ||
Theorem | bj-issettru 35339* | Weak version of isset 3458 without ax-ext 2707. (Contributed by BJ, 24-Apr-2024.) (Proof modification is discouraged.) |
⊢ (∃𝑥 𝑥 = 𝐴 ↔ 𝐴 ∈ {𝑦 ∣ ⊤}) | ||
Theorem | bj-elabtru 35340 | This is as close as we can get to proving extensionality for "the" "universal" class without ax-ext 2707. (Contributed by BJ, 24-Apr-2024.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ {𝑥 ∣ ⊤} ↔ 𝐴 ∈ {𝑦 ∣ ⊤}) | ||
Theorem | bj-issetwt 35341* | Closed form of bj-issetw 35342. (Contributed by BJ, 29-Apr-2019.) (Proof modification is discouraged.) |
⊢ (∀𝑥𝜑 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ ∃𝑦 𝑦 = 𝐴)) | ||
Theorem | bj-issetw 35342* | The closest one can get to isset 3458 without using ax-ext 2707. See also vexw 2719. Note that the only disjoint variable condition is between 𝑦 and 𝐴. From there, one can prove isset 3458 using eleq2i 2829 (which requires ax-ext 2707 and df-cleq 2728). (Contributed by BJ, 29-Apr-2019.) (Proof modification is discouraged.) |
⊢ 𝜑 ⇒ ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ ∃𝑦 𝑦 = 𝐴) | ||
Theorem | bj-elissetALT 35343* | Alternate proof of elisset 2819. This is essentially the same proof as seen by inlining bj-denotes 35338 and bj-denoteslem 35337. Use elissetv 2818 instead when sufficient (in particular when 𝑉 is substituted for V). (Contributed by BJ, 29-Apr-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴) | ||
Theorem | bj-issetiv 35344* | Version of bj-isseti 35345 with a disjoint variable condition on 𝑥, 𝑉. The hypothesis uses 𝑉 instead of V for extra generality. This is indeed more general than isseti 3460 as long as elex 3463 is not available (and the non-dependence of bj-issetiv 35344 on special properties of the universal class V is obvious). Prefer its use over bj-isseti 35345 when sufficient (in particular when 𝑉 is substituted for V). (Contributed by BJ, 14-Sep-2019.) (Proof modification is discouraged.) |
⊢ 𝐴 ∈ 𝑉 ⇒ ⊢ ∃𝑥 𝑥 = 𝐴 | ||
Theorem | bj-isseti 35345* | Version of isseti 3460 with a class variable 𝑉 in the hypothesis instead of V for extra generality. This is indeed more general than isseti 3460 as long as elex 3463 is not available (and the non-dependence of bj-isseti 35345 on special properties of the universal class V is obvious). Use bj-issetiv 35344 instead when sufficient (in particular when 𝑉 is substituted for V). (Contributed by BJ, 13-Jun-2019.) (Proof modification is discouraged.) |
⊢ 𝐴 ∈ 𝑉 ⇒ ⊢ ∃𝑥 𝑥 = 𝐴 | ||
Theorem | bj-ralvw 35346 | A weak version of ralv 3469 not using ax-ext 2707 (nor df-cleq 2728, df-clel 2814, df-v 3447), and only core FOL axioms. See also bj-rexvw 35347. The analogues for reuv 3471 and rmov 3472 are not proved. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.) |
⊢ 𝜓 ⇒ ⊢ (∀𝑥 ∈ {𝑦 ∣ 𝜓}𝜑 ↔ ∀𝑥𝜑) | ||
Theorem | bj-rexvw 35347 | A weak version of rexv 3470 not using ax-ext 2707 (nor df-cleq 2728, df-clel 2814, df-v 3447), and only core FOL axioms. See also bj-ralvw 35346. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.) |
⊢ 𝜓 ⇒ ⊢ (∃𝑥 ∈ {𝑦 ∣ 𝜓}𝜑 ↔ ∃𝑥𝜑) | ||
Theorem | bj-rababw 35348 | A weak version of rabab 3473 not using df-clel 2814 nor df-v 3447 (but requiring ax-ext 2707) nor ax-12 2171. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.) |
⊢ 𝜓 ⇒ ⊢ {𝑥 ∈ {𝑦 ∣ 𝜓} ∣ 𝜑} = {𝑥 ∣ 𝜑} | ||
Theorem | bj-rexcom4bv 35349* | Version of rexcom4b 3474 and bj-rexcom4b 35350 with a disjoint variable condition on 𝑥, 𝑉, hence removing dependency on df-sb 2068 and df-clab 2714 (so that it depends on df-clel 2814 and df-rex 3074 only on top of first-order logic). Prefer its use over bj-rexcom4b 35350 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 35350* | Remove from rexcom4b 3474 dependency on ax-ext 2707 and ax-13 2370 (and on df-or 846, df-cleq 2728, df-nfc 2889, df-v 3447). The hypothesis uses 𝑉 instead of V (see bj-isseti 35345 for the motivation). Use bj-rexcom4bv 35349 instead when sufficient (in particular when 𝑉 is substituted for V). (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.) |
⊢ 𝐵 ∈ 𝑉 ⇒ ⊢ (∃𝑥∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵) ↔ ∃𝑦 ∈ 𝐴 𝜑) | ||
Theorem | bj-ceqsalt0 35351 | The FOL content of ceqsalt 3475. Lemma for bj-ceqsalt 35353 and bj-ceqsaltv 35354. (Contributed by BJ, 26-Sep-2019.) (Proof modification is discouraged.) |
⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝜃 → (𝜑 ↔ 𝜓)) ∧ ∃𝑥𝜃) → (∀𝑥(𝜃 → 𝜑) ↔ 𝜓)) | ||
Theorem | bj-ceqsalt1 35352 | The FOL content of ceqsalt 3475. Lemma for bj-ceqsalt 35353 and bj-ceqsaltv 35354. TODO: consider removing if it does not add anything to bj-ceqsalt0 35351. (Contributed by BJ, 26-Sep-2019.) (Proof modification is discouraged.) |
⊢ (𝜃 → ∃𝑥𝜒) ⇒ ⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝜒 → (𝜑 ↔ 𝜓)) ∧ 𝜃) → (∀𝑥(𝜒 → 𝜑) ↔ 𝜓)) | ||
Theorem | bj-ceqsalt 35353* | Remove from ceqsalt 3475 dependency on ax-ext 2707 (and on df-cleq 2728 and df-v 3447). Note: this is not doable with ceqsralt 3476 (or ceqsralv 3483), which uses eleq1 2825, but the same dependence removal is possible for ceqsalg 3477, ceqsal 3479, ceqsalv 3481, cgsexg 3488, cgsex2g 3489, cgsex4g 3490, ceqsex 3492, ceqsexv 3494, ceqsex2 3498, ceqsex2v 3499, ceqsex3v 3500, ceqsex4v 3501, ceqsex6v 3502, ceqsex8v 3503, gencbvex 3504 (after changing 𝐴 = 𝑦 to 𝑦 = 𝐴), gencbvex2 3505, gencbval 3506, vtoclgft 3509 (it uses Ⅎ, whose justification nfcjust 2888 does not use ax-ext 2707) and several other vtocl* theorems (see for instance bj-vtoclg1f 35385). See also bj-ceqsaltv 35354. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.) |
⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝑉) → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓)) | ||
Theorem | bj-ceqsaltv 35354* | Version of bj-ceqsalt 35353 with a disjoint variable condition on 𝑥, 𝑉, removing dependency on df-sb 2068 and df-clab 2714. Prefer its use over bj-ceqsalt 35353 when sufficient (in particular when 𝑉 is substituted for V). (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.) |
⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝑉) → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓)) | ||
Theorem | bj-ceqsalg0 35355 | The FOL content of ceqsalg 3477. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝜒 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥𝜒 → (∀𝑥(𝜒 → 𝜑) ↔ 𝜓)) | ||
Theorem | bj-ceqsalg 35356* | Remove from ceqsalg 3477 dependency on ax-ext 2707 (and on df-cleq 2728 and df-v 3447). See also bj-ceqsalgv 35358. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓)) | ||
Theorem | bj-ceqsalgALT 35357* | Alternate proof of bj-ceqsalg 35356. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓)) | ||
Theorem | bj-ceqsalgv 35358* | Version of bj-ceqsalg 35356 with a disjoint variable condition on 𝑥, 𝑉, removing dependency on df-sb 2068 and df-clab 2714. Prefer its use over bj-ceqsalg 35356 when sufficient (in particular when 𝑉 is substituted for V). (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓)) | ||
Theorem | bj-ceqsalgvALT 35359* | Alternate proof of bj-ceqsalgv 35358. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓)) | ||
Theorem | bj-ceqsal 35360* | Remove from ceqsal 3479 dependency on ax-ext 2707 (and on df-cleq 2728, df-v 3447, df-clab 2714, df-sb 2068). (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓) | ||
Theorem | bj-ceqsalv 35361* | Remove from ceqsalv 3481 dependency on ax-ext 2707 (and on df-cleq 2728, df-v 3447, df-clab 2714, df-sb 2068). (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.) |
⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓) | ||
Theorem | bj-spcimdv 35362* | Remove from spcimdv 3552 dependency on ax-9 2116, ax-10 2137, ax-11 2154, ax-13 2370, ax-ext 2707, df-cleq 2728 (and df-nfc 2889, df-v 3447, df-or 846, df-tru 1544, df-nf 1786). For an even more economical version, see bj-spcimdvv 35363. (Contributed by BJ, 30-Nov-2020.) (Proof modification is discouraged.) |
⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥𝜓 → 𝜒)) | ||
Theorem | bj-spcimdvv 35363* | Remove from spcimdv 3552 dependency on ax-7 2011, ax-8 2108, ax-10 2137, ax-11 2154, ax-12 2171 ax-13 2370, ax-ext 2707, df-cleq 2728, df-clab 2714 (and df-nfc 2889, df-v 3447, df-or 846, df-tru 1544, df-nf 1786) 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 35362. (Contributed by BJ, 3-Nov-2021.) (Proof modification is discouraged.) |
⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥𝜓 → 𝜒)) | ||
Theorem | elelb 35364 | 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 35365 | 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 35366 | The nonfreeness quantifier for classes defines a symmetric binary relation on var metavariables (irreflexivity is proved by nfnid 5330 with additional axioms; see also nfcv 2907). This could be proved from aecom 2425 and nfcvb 5331 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 2742 instead of equcomd 2022; removing dependency on ax-ext 2707 is possible: prove weak versions (i.e. replace classes with setvars) of drnfc1 2926, eleq2d 2823 (using elequ2 2121), nfcvf 2936, dvelimc 2935, dvelimdc 2934, nfcvf2 2937. (Proof modification is discouraged.) |
⊢ (Ⅎ𝑥𝑦 ↔ Ⅎ𝑦𝑥) | ||
Some useful theorems for dealing with substitutions: sbbi 2304, sbcbig 3793, sbcel1g 4373, sbcel2 4375, sbcel12 4368, sbceqg 4369, csbvarg 4391. | ||
Theorem | bj-sbeqALT 35367* | Substitution in an equality (use the more general version bj-sbeq 35368 instead, without disjoint variable condition). (Contributed by BJ, 6-Oct-2018.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ([𝑦 / 𝑥]𝐴 = 𝐵 ↔ ⦋𝑦 / 𝑥⦌𝐴 = ⦋𝑦 / 𝑥⦌𝐵) | ||
Theorem | bj-sbeq 35368 | Distribute proper substitution through an equality relation. (See sbceqg 4369). (Contributed by BJ, 6-Oct-2018.) |
⊢ ([𝑦 / 𝑥]𝐴 = 𝐵 ↔ ⦋𝑦 / 𝑥⦌𝐴 = ⦋𝑦 / 𝑥⦌𝐵) | ||
Theorem | bj-sbceqgALT 35369 | Distribute proper substitution through an equality relation. Alternate proof of sbceqg 4369. (Contributed by BJ, 6-Oct-2018.) Proof modification is discouraged to avoid using sbceqg 4369, but the Metamath program "MM-PA> MINIMIZE_WITH * / EXCEPT sbceqg" command is ok. (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵 = 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶)) | ||
Theorem | bj-csbsnlem 35370* | Lemma for bj-csbsn 35371 (in this lemma, 𝑥 cannot occur in 𝐴). (Contributed by BJ, 6-Oct-2018.) (New usage is discouraged.) |
⊢ ⦋𝐴 / 𝑥⦌{𝑥} = {𝐴} | ||
Theorem | bj-csbsn 35371 | Substitution in a singleton. (Contributed by BJ, 6-Oct-2018.) |
⊢ ⦋𝐴 / 𝑥⦌{𝑥} = {𝐴} | ||
Theorem | bj-sbel1 35372* | Version of sbcel1g 4373 when substituting a set. (Note: one could have a corresponding version of sbcel12 4368 when substituting a set, but the point here is that the antecedent of sbcel1g 4373 is not needed when substituting a set.) (Contributed by BJ, 6-Oct-2018.) |
⊢ ([𝑦 / 𝑥]𝐴 ∈ 𝐵 ↔ ⦋𝑦 / 𝑥⦌𝐴 ∈ 𝐵) | ||
Theorem | bj-abv 35373 | The class of sets verifying a tautology is the universal class. (Contributed by BJ, 24-Jul-2019.) (Proof modification is discouraged.) |
⊢ (∀𝑥𝜑 → {𝑥 ∣ 𝜑} = V) | ||
Theorem | bj-abvALT 35374 | Alternate version of bj-abv 35373; shorter but uses ax-8 2108. (Contributed by BJ, 24-Jul-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥𝜑 → {𝑥 ∣ 𝜑} = V) | ||
Theorem | bj-ab0 35375 | The class of sets verifying a falsity is the empty set (closed form of abf 4362). (Contributed by BJ, 24-Jul-2019.) (Proof modification is discouraged.) |
⊢ (∀𝑥 ¬ 𝜑 → {𝑥 ∣ 𝜑} = ∅) | ||
Theorem | bj-abf 35376 | Shorter proof of abf 4362 (which should be kept as abfALT). (Contributed by BJ, 24-Jul-2019.) (Proof modification is discouraged.) |
⊢ ¬ 𝜑 ⇒ ⊢ {𝑥 ∣ 𝜑} = ∅ | ||
Theorem | bj-csbprc 35377 | More direct proof of csbprc 4366 (fewer essential steps). (Contributed by BJ, 24-Jul-2019.) (Proof modification is discouraged.) |
⊢ (¬ 𝐴 ∈ V → ⦋𝐴 / 𝑥⦌𝐵 = ∅) | ||
Theorem | bj-exlimvmpi 35378* | A Fol lemma (exlimiv 1933 followed by mpi 20). (Contributed by BJ, 2-Jul-2022.) (Proof modification is discouraged.) |
⊢ (𝜒 → (𝜑 → 𝜓)) & ⊢ 𝜑 ⇒ ⊢ (∃𝑥𝜒 → 𝜓) | ||
Theorem | bj-exlimmpi 35379 | Lemma for bj-vtoclg1f1 35384 (an instance of this lemma is a version of bj-vtoclg1f1 35384 where 𝑥 and 𝑦 are identified). (Contributed by BJ, 30-Apr-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝜒 → (𝜑 → 𝜓)) & ⊢ 𝜑 ⇒ ⊢ (∃𝑥𝜒 → 𝜓) | ||
Theorem | bj-exlimmpbi 35380 | Lemma for theorems of the vtoclg 3525 family. (Contributed by BJ, 3-Oct-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝜒 → (𝜑 ↔ 𝜓)) & ⊢ 𝜑 ⇒ ⊢ (∃𝑥𝜒 → 𝜓) | ||
Theorem | bj-exlimmpbir 35381 | Lemma for theorems of the vtoclg 3525 family. (Contributed by BJ, 3-Oct-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜒 → (𝜑 ↔ 𝜓)) & ⊢ 𝜓 ⇒ ⊢ (∃𝑥𝜒 → 𝜑) | ||
Theorem | bj-vtoclf 35382* | Remove dependency on ax-ext 2707, df-clab 2714 and df-cleq 2728 (and df-sb 2068 and df-v 3447) from vtoclf 3516. (Contributed by BJ, 6-Oct-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ 𝐴 ∈ 𝑉 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ 𝜑 ⇒ ⊢ 𝜓 | ||
Theorem | bj-vtocl 35383* | Remove dependency on ax-ext 2707, df-clab 2714 and df-cleq 2728 (and df-sb 2068 and df-v 3447) from vtocl 3518. (Contributed by BJ, 6-Oct-2019.) (Proof modification is discouraged.) |
⊢ 𝐴 ∈ 𝑉 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ 𝜑 ⇒ ⊢ 𝜓 | ||
Theorem | bj-vtoclg1f1 35384* | The FOL content of vtoclg1f 3524 (hence not using ax-ext 2707, df-cleq 2728, df-nfc 2889, df-v 3447). 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 2707; as a byproduct, this dispenses with ax-11 2154 and ax-13 2370). (Contributed by BJ, 30-Apr-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝐴 → (𝜑 → 𝜓)) & ⊢ 𝜑 ⇒ ⊢ (∃𝑦 𝑦 = 𝐴 → 𝜓) | ||
Theorem | bj-vtoclg1f 35385* | Reprove vtoclg1f 3524 from bj-vtoclg1f1 35384. This removes dependency on ax-ext 2707, df-cleq 2728 and df-v 3447. Use bj-vtoclg1fv 35386 instead when sufficient (in particular when 𝑉 is substituted for V). (Contributed by BJ, 14-Sep-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝐴 → (𝜑 → 𝜓)) & ⊢ 𝜑 ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝜓) | ||
Theorem | bj-vtoclg1fv 35386* | Version of bj-vtoclg1f 35385 with a disjoint variable condition on 𝑥, 𝑉. This removes dependency on df-sb 2068 and df-clab 2714. Prefer its use over bj-vtoclg1f 35385 when sufficient (in particular when 𝑉 is substituted for V). (Contributed by BJ, 14-Sep-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝐴 → (𝜑 → 𝜓)) & ⊢ 𝜑 ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝜓) | ||
Theorem | bj-vtoclg 35387* | A version of vtoclg 3525 with an additional disjoint variable condition (which is removable if we allow use of df-clab 2714, see bj-vtoclg1f 35385), which requires fewer axioms (i.e., removes dependency on ax-6 1971, ax-7 2011, ax-9 2116, ax-12 2171, ax-ext 2707, df-clab 2714, df-cleq 2728, df-v 3447). (Contributed by BJ, 2-Jul-2022.) (Proof modification is discouraged.) |
⊢ (𝑥 = 𝐴 → (𝜑 → 𝜓)) & ⊢ 𝜑 ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝜓) | ||
Theorem | bj-rabbida2 35388 | Version of rabbidva2 3409 with disjoint variable condition replaced by nonfreeness hypothesis. (Contributed by BJ, 27-Apr-2019.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐵 ∧ 𝜒))) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒}) | ||
Theorem | bj-rabeqd 35389 | Deduction form of rabeq 3421. Note that contrary to rabeq 3421 it has no disjoint variable condition. (Contributed by BJ, 27-Apr-2019.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜓}) | ||
Theorem | bj-rabeqbid 35390 | Version of rabeqbidv 3424 with two disjoint variable conditions removed and the third replaced by a nonfreeness hypothesis. (Contributed by BJ, 27-Apr-2019.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒}) | ||
Theorem | bj-rabeqbida 35391 | Version of rabeqbidva 3423 with two disjoint variable conditions removed and the third replaced by a nonfreeness hypothesis. (Contributed by BJ, 27-Apr-2019.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒}) | ||
Theorem | bj-seex 35392* | Version of seex 5595 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 35393* | Version of df-nfc 2889 with a disjoint variable condition replaced with a nonfreeness hypothesis. (Contributed by BJ, 2-May-2019.) |
⊢ Ⅎ𝑦𝐴 ⇒ ⊢ (Ⅎ𝑥𝐴 ↔ ∀𝑦Ⅎ𝑥 𝑦 ∈ 𝐴) | ||
Theorem | bj-zfauscl 35394* |
General version of zfauscl 5258.
Remark: the comment in zfauscl 5258 is misleading: the essential use of ax-ext 2707 is the one via eleq2 2826 and not the one via vtocl 3518, since the latter can be proved without ax-ext 2707 (see bj-vtoclg 35387). (Contributed by BJ, 2-Jul-2022.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ 𝑉 → ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝜑))) | ||
A few additional theorems on class abstractions and restricted class abstractions. | ||
Theorem | bj-elabd2ALT 35395* | Alternate proof of elabd2 3622 bypassing elab6g 3621 (and using sbiedvw 2096 instead of the ∀𝑥(𝑥 = 𝑦 → 𝜓) idiom). (Contributed by BJ, 16-Oct-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 = {𝑥 ∣ 𝜓}) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (𝐴 ∈ 𝐵 ↔ 𝜒)) | ||
Theorem | bj-unrab 35396* | Generalization of unrab 4265. Equality need not hold. (Contributed by BJ, 21-Apr-2019.) |
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∪ {𝑥 ∈ 𝐵 ∣ 𝜓}) ⊆ {𝑥 ∈ (𝐴 ∪ 𝐵) ∣ (𝜑 ∨ 𝜓)} | ||
Theorem | bj-inrab 35397 | Generalization of inrab 4266. (Contributed by BJ, 21-Apr-2019.) |
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ {𝑥 ∈ 𝐵 ∣ 𝜓}) = {𝑥 ∈ (𝐴 ∩ 𝐵) ∣ (𝜑 ∧ 𝜓)} | ||
Theorem | bj-inrab2 35398 | Shorter proof of inrab 4266. (Contributed by BJ, 21-Apr-2019.) (Proof modification is discouraged.) |
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ {𝑥 ∈ 𝐴 ∣ 𝜓}) = {𝑥 ∈ 𝐴 ∣ (𝜑 ∧ 𝜓)} | ||
Theorem | bj-inrab3 35399* | Generalization of dfrab3ss 4272, which it may shorten. (Contributed by BJ, 21-Apr-2019.) (Revised by OpenAI, 7-Jul-2020.) |
⊢ (𝐴 ∩ {𝑥 ∈ 𝐵 ∣ 𝜑}) = ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ 𝐵) | ||
Theorem | bj-rabtr 35400* | Restricted class abstraction with true formula. (Contributed by BJ, 22-Apr-2019.) |
⊢ {𝑥 ∈ 𝐴 ∣ ⊤} = 𝐴 |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |