P. 377 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 37601-37700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	bj-sbidmOLD 37601	Obsolete proof of sbidm 2541 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 37602*	Deduction form of dvelim 2482 with disjoint variable conditions. Uncurried (imported) form of bj-dvelimdv1 37603. 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 1947 can be replaced with nfal 2355 followed by nfn 1890. Remark: nfald 2360 uses ax-11 2194; it might be possible to inline and use ax11w 2167 instead, but there is still a use via 19.12 2359 anyway. (Contributed by BJ, 20-Oct-2021.) (Proof modification is discouraged.)
⊢ (𝜑 → Ⅎ𝑥𝜒)    &   ⊢ (𝑧 = 𝑦 → (𝜒 ↔ 𝜓))    ⇒   ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥𝜓)
Theorem	bj-dvelimdv1 37603*	Curried (exported) form of bj-dvelimdv 37602 (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 37604*	A version of dvelim 2482 using the "nonfree" idiom. (Contributed by BJ, 20-Oct-2021.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑧 = 𝑦 → (𝜓 ↔ 𝜑))    ⇒   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝜑)
Theorem	bj-nfeel2 37605*	Nonfreeness in a membership statement. (Contributed by BJ, 20-Oct-2021.) (Proof modification is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥 𝑦 ∈ 𝑧)
Theorem	bj-axc14nf 37606	Proof of a version of axc14 2494 using the "nonfree" idiom. (Contributed by BJ, 20-Oct-2021.) (Proof modification is discouraged.)
⊢ (¬ ∀𝑧 𝑧 = 𝑥 → (¬ ∀𝑧 𝑧 = 𝑦 → Ⅎ𝑧 𝑥 ∈ 𝑦))
Theorem	bj-axc14 37607	Alternate proof of axc14 2494 (even when inlining the above results, this gives a shorter proof). (Contributed by BJ, 20-Oct-2021.) (Proof modification is discouraged.)
⊢ (¬ ∀𝑧 𝑧 = 𝑥 → (¬ ∀𝑧 𝑧 = 𝑦 → (𝑥 ∈ 𝑦 → ∀𝑧 𝑥 ∈ 𝑦)))
Theorem	mobidvALT 37608*	Alternate proof of mobidv 2576 directly from its analogues albidv 1953 and exbidv 1954, using deduction style. Note the proof structure, similar to mobi 2574. (Contributed by Mario Carneiro, 7-Oct-2016.) Reduce axiom dependencies and shorten proof. Remove dependency on ax-12 2215 by adapting proof of mobid 2577. (Revised by BJ, 26-Sep-2022.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃*𝑥𝜓 ↔ ∃*𝑥𝜒))
Theorem	sbn1ALT 37609	Alternate proof of sbn1 2144, not using the false constant. (Contributed by BJ, 18-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ([𝑡 / 𝑥] ¬ 𝜑 → ¬ [𝑡 / 𝑥]𝜑)
21.19.5  Set theory
21.19.5.1  Eliminability of class terms 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 2734, df-clab 2741, df-cleq 2754, df-clel 2837 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 2734, df-clab 2741, df-cleq 2754, df-clel 2837 }) 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 37617, eliminable-abeqv 37618, eliminable-abeqab 37619, eliminable-velab 37616, eliminable-abelv 37620, eliminable-abelab 37621 respectively, which are all proved from {FOL, ax-ext 2734, df-clab 2741, df-cleq 2754, df-clel 2837 }. (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 2741, dfcleq 2755 (proved from {FOL, ax-ext 2734, df-cleq 2754 }), and dfclel 2838 (proved from {FOL, df-clel 2837 }). 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 37611, eliminable2b 37612 and eliminable3a 37614, 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 1569, 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 2741 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 2741, ax-ext 2734 and df-cleq 2754 are sufficient (over FOL) to eliminate class terms. To prove that { df-clab 2741, df-cleq 2754, df-clel 2837 } provides a definitional extension of {FOL, ax-ext 2734 }, 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 2741, df-cleq 2754, df-clel 2837 }. 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 2734 }. 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 2741, df-cleq 2754, df-clel 2837 }. It involves a careful case study on the structure of the proof tree.
Theorem	eliminable1 37610	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 37611*	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 37612*	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 37613*	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 37614*	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 37615*	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 37616	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 37617*	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 37618*	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 37619*	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 37620*	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 37621*	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.)
⊢ ({𝑥 ∣ 𝜑} ∈ {𝑦 ∣ 𝜓} ↔ ∃𝑧(∀𝑡(𝑡 ∈ 𝑧 ↔ [𝑡 / 𝑥]𝜑) ∧ [𝑧 / 𝑦]𝜓))
21.19.5.2  Classes without the axiom of extensionality A few results about classes can be proved without using ax-ext 2734. One could move all theorems from cab 2740 to df-clel 2837 (except for dfcleq 2755 and cvjust 2756) 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 2754. Note that without ax-ext 2734, the $a-statements df-clab 2741, df-cleq 2754, and df-clel 2837 are no longer eliminable (see previous section) (but PROBABLY df-clab 2741 is still conservative , while df-cleq 2754 and df-clel 2837 are not). This is not a reason not to study what is provable with them but without ax-ext 2734, 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 2145, wel 2146, ax-8 2147, ax-9 2155). Remark: the weakening of eleq1 2850 / eleq2 2851 to eleq1w 2845 / eleq2w 2846 can also be done with eleq1i 2853, eqeltri 2858, eqeltrri 2859, eleq1a 2857, eleq1d 2847, eqeltrd 2862, eqeltrrd 2863, eqneltrd 2882, eqneltrrd 2883, nelneq 2886. Remark: possibility to remove dependency on ax-10 2178, ax-11 2194, ax-13 2403 from nfcri 2916 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 2936.
Theorem	bj-denoteslem 37622*	Duplicate of issettru 2840 and bj-issettruALTV 37624. Lemma for bj-denotesALTV 37623. (Contributed by BJ, 24-Apr-2024.) (Proof modification is discouraged.)
⊢ (∃𝑥 𝑥 = 𝐴 ↔ 𝐴 ∈ {𝑦 ∣ ⊤})
Theorem	bj-denotesALTV 37623*	Moved to main as iseqsetv-clel 2841 and kept for the comments. 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 278 (to add an intermediate proposition ∃𝑧𝑧 = 𝐴 with a fresh 𝑧), cbvexvw 2070, and eqeq1 2766, requires the core axioms and { ax-9 2155, ax-ext 2734, df-cleq 2754 } whereas this proof requires the core axioms and { ax-8 2147, df-clab 2741, df-clel 2837 }. Theorem bj-issetwt 37626 proves that "existing" is equivalent to being a member of a class abstraction. It also requires, with the present proof, { ax-8 2147, df-clab 2741, df-clel 2837 } (whereas with the shorter proof from cbvexvw 2070 and eqeq1 2766 it would require { ax-8 2147, ax-9 2155, ax-ext 2734, df-clab 2741, df-cleq 2754, df-clel 2837 }). That every class is equal to a class abstraction is proved by abid1 2898, which requires { ax-8 2147, ax-9 2155, ax-ext 2734, df-clab 2741, df-cleq 2754, df-clel 2837 }. Note that there is no disjoint variable condition on 𝑥, 𝑦 but the theorem does not depend on ax-13 2403. Actually, the proof depends only on the logical axioms ax-1 6 through ax-7 2041 and sp 2221. 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 2734 and df-cleq 2754 (e.g., eqid 2762 and eqeq1 2766). In particular, one cannot even prove ⊢ ∃𝑥𝑥 = 𝐴 ⇒ ⊢ 𝐴 = 𝐴 without ax-ext 2734 and df-cleq 2754. (Contributed by BJ, 29-Apr-2019.) (Proof modification is discouraged.)
⊢ (∃𝑥 𝑥 = 𝐴 ↔ ∃𝑦 𝑦 = 𝐴)
Theorem	bj-issettruALTV 37624*	Moved to main as issettru 2840 and kept for the comments. Weak version of isset 3467 without ax-ext 2734. (Contributed by BJ, 24-Apr-2024.) (Proof modification is discouraged.)
⊢ (∃𝑥 𝑥 = 𝐴 ↔ 𝐴 ∈ {𝑦 ∣ ⊤})
Theorem	bj-elabtru 37625	This is as close as we can get to proving extensionality for "the" "universal" class without ax-ext 2734. (Contributed by BJ, 24-Apr-2024.) (Proof modification is discouraged.)
⊢ (𝐴 ∈ {𝑥 ∣ ⊤} ↔ 𝐴 ∈ {𝑦 ∣ ⊤})
Theorem	bj-issetwt 37626*	Closed form of bj-issetw 37627. (Contributed by BJ, 29-Apr-2019.) (Proof modification is discouraged.)
⊢ (∀𝑥𝜑 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ ∃𝑦 𝑦 = 𝐴))
Theorem	bj-issetw 37627*	The closest one can get to isset 3467 without using ax-ext 2734. See also vexw 2746. Note that the only disjoint variable condition is between 𝑦 and 𝐴. From there, one can prove isset 3467 using eleq2i 2854 (which requires ax-ext 2734 and df-cleq 2754). (Contributed by BJ, 29-Apr-2019.) (Proof modification is discouraged.)
⊢ 𝜑    ⇒   ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ ∃𝑦 𝑦 = 𝐴)
Theorem	bj-issetiv 37628*	Version of bj-isseti 37629 with a disjoint variable condition on 𝑥, 𝑉. The hypothesis uses 𝑉 instead of V for extra generality. This is indeed more general than isseti 3471 as long as elex 3474 is not available (and the non-dependence of bj-issetiv 37628 on special properties of the universal class V is obvious). Prefer its use over bj-isseti 37629 when sufficient (in particular when 𝑉 is substituted for V). (Contributed by BJ, 14-Sep-2019.) (Proof modification is discouraged.)
⊢ 𝐴 ∈ 𝑉    ⇒   ⊢ ∃𝑥 𝑥 = 𝐴
Theorem	bj-isseti 37629*	Version of isseti 3471 with a class variable 𝑉 in the hypothesis instead of V for extra generality. This is indeed more general than isseti 3471 as long as elex 3474 is not available (and the non-dependence of bj-isseti 37629 on special properties of the universal class V is obvious). Use bj-issetiv 37628 instead when sufficient (in particular when 𝑉 is substituted for V). (Contributed by BJ, 13-Jun-2019.) (Proof modification is discouraged.)
⊢ 𝐴 ∈ 𝑉    ⇒   ⊢ ∃𝑥 𝑥 = 𝐴
Theorem	bj-ralvw 37630	A weak version of ralv 3479 not using ax-ext 2734 (nor df-cleq 2754, df-clel 2837, df-v 3455), and only core FOL axioms. See also bj-rexvw 37631. The analogues for reuv 3481 and rmov 3482 are not proved. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ 𝜓    ⇒   ⊢ (∀𝑥 ∈ {𝑦 ∣ 𝜓}𝜑 ↔ ∀𝑥𝜑)
Theorem	bj-rexvw 37631	A weak version of rexv 3480 not using ax-ext 2734 (nor df-cleq 2754, df-clel 2837, df-v 3455), and only core FOL axioms. See also bj-ralvw 37630. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ 𝜓    ⇒   ⊢ (∃𝑥 ∈ {𝑦 ∣ 𝜓}𝜑 ↔ ∃𝑥𝜑)
Theorem	bj-rababw 37632	A weak version of rabab 3483 not using df-clel 2837 nor df-v 3455 (but requiring ax-ext 2734) nor ax-12 2215. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ 𝜓    ⇒   ⊢ {𝑥 ∈ {𝑦 ∣ 𝜓} ∣ 𝜑} = {𝑥 ∣ 𝜑}
Theorem	bj-rexcom4bv 37633*	Version of rexcom4b 3484 and bj-rexcom4b 37634 with a disjoint variable condition on 𝑥, 𝑉, hence removing dependency on df-sb 2100 and df-clab 2741 (so that it depends on df-clel 2837 and df-rex 3089 only on top of first-order logic). Prefer its use over bj-rexcom4b 37634 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 37634*	Remove from rexcom4b 3484 dependency on ax-ext 2734 and ax-13 2403 (and on df-or 862, df-cleq 2754, df-nfc 2911, df-v 3455). The hypothesis uses 𝑉 instead of V (see bj-isseti 37629 for the motivation). Use bj-rexcom4bv 37633 instead when sufficient (in particular when 𝑉 is substituted for V). (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ 𝐵 ∈ 𝑉    ⇒   ⊢ (∃𝑥∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵) ↔ ∃𝑦 ∈ 𝐴 𝜑)
Theorem	bj-ceqsalt0 37635	The FOL content of ceqsalt 3486. Lemma for bj-ceqsalt 37637 and bj-ceqsaltv 37638. (Contributed by BJ, 26-Sep-2019.) (Proof modification is discouraged.)
⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝜃 → (𝜑 ↔ 𝜓)) ∧ ∃𝑥𝜃) → (∀𝑥(𝜃 → 𝜑) ↔ 𝜓))
Theorem	bj-ceqsalt1 37636	The FOL content of ceqsalt 3486. Lemma for bj-ceqsalt 37637 and bj-ceqsaltv 37638. TODO: consider removing if it does not add anything to bj-ceqsalt0 37635. (Contributed by BJ, 26-Sep-2019.) (Proof modification is discouraged.)
⊢ (𝜃 → ∃𝑥𝜒)    ⇒   ⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝜒 → (𝜑 ↔ 𝜓)) ∧ 𝜃) → (∀𝑥(𝜒 → 𝜑) ↔ 𝜓))
Theorem	bj-ceqsalt 37637*	Remove from ceqsalt 3486 dependency on ax-ext 2734 (and on df-cleq 2754 and df-v 3455). Note: this is not doable with ceqsralt 3487 (or ceqsralv 3493), which uses eleq1 2850, but the same dependence removal is possible for ceqsalg 3488, ceqsal 3490, ceqsalv 3492, cgsexg 3497, cgsex2g 3498, cgsex4g 3499, ceqsex 3500, ceqsexv 3501, ceqsex2 3503, ceqsex2v 3504, ceqsex3v 3505, ceqsex4v 3506, ceqsex6v 3507, ceqsex8v 3508, gencbvex 3509 (after changing 𝐴 = 𝑦 to 𝑦 = 𝐴), gencbvex2 3510, gencbval 3511, vtoclgft 3518 (it uses Ⅎ, whose justification nfcjust 2910 does not use ax-ext 2734) and several other vtocl* theorems (see for instance bj-vtoclg1f 37669). See also bj-ceqsaltv 37638. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝑉) → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
Theorem	bj-ceqsaltv 37638*	Version of bj-ceqsalt 37637 with a disjoint variable condition on 𝑥, 𝑉, removing dependency on df-sb 2100 and df-clab 2741. Prefer its use over bj-ceqsalt 37637 when sufficient (in particular when 𝑉 is substituted for V). (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝑉) → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
Theorem	bj-ceqsalg0 37639	The FOL content of ceqsalg 3488. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝜒 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥𝜒 → (∀𝑥(𝜒 → 𝜑) ↔ 𝜓))
Theorem	bj-ceqsalg 37640*	Remove from ceqsalg 3488 dependency on ax-ext 2734 (and on df-cleq 2754 and df-v 3455). See also bj-ceqsalgv 37642. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
Theorem	bj-ceqsalgALT 37641*	Alternate proof of bj-ceqsalg 37640. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
Theorem	bj-ceqsalgv 37642*	Version of bj-ceqsalg 37640 with a disjoint variable condition on 𝑥, 𝑉, removing dependency on df-sb 2100 and df-clab 2741. Prefer its use over bj-ceqsalg 37640 when sufficient (in particular when 𝑉 is substituted for V). (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
Theorem	bj-ceqsalgvALT 37643*	Alternate proof of bj-ceqsalgv 37642. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
Theorem	bj-ceqsal 37644*	Remove from ceqsal 3490 dependency on ax-ext 2734 (and on df-cleq 2754, df-v 3455, df-clab 2741, df-sb 2100). (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ 𝐴 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓)
Theorem	bj-ceqsalv 37645*	Remove from ceqsalv 3492 dependency on ax-ext 2734 (and on df-cleq 2754, df-v 3455, df-clab 2741, df-sb 2100). (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.)
⊢ 𝐴 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓)
Theorem	bj-spcimdv 37646*	Remove from spcimdv 3550 dependency on ax-9 2155, ax-10 2178, ax-11 2194, ax-13 2403, ax-ext 2734, df-cleq 2754 (and df-nfc 2911, df-v 3455, df-or 862, df-tru 1573, df-nf 1817). For an even more economical version, see bj-spcimdvv 37647. (Contributed by BJ, 30-Nov-2020.) (Proof modification is discouraged.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 → 𝜒))
Theorem	bj-spcimdvv 37647*	Remove from spcimdv 3550 dependency on ax-7 2041, ax-8 2147, ax-10 2178, ax-11 2194, ax-12 2215 ax-13 2403, ax-ext 2734, df-cleq 2754, df-clab 2741 (and df-nfc 2911, df-v 3455, df-or 862, df-tru 1573, df-nf 1817) 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 37646. (Contributed by BJ, 3-Nov-2021.) (Proof modification is discouraged.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 → 𝜒))
21.19.5.3  Characterization among sets versus among classes
Theorem	elelb 37648	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 37649	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 𝐴))
21.19.5.4  The nonfreeness quantifier for classes In this section, we prove the symmetry of the nonfreeness quantifier for classes.
Theorem	bj-nfcsym 37650	The nonfreeness quantifier for classes defines a symmetric binary relation on var metavariables (irreflexivity is proved by nfnid 5344 with additional axioms; see also nfcv 2924). This could be proved from aecom 2458 and nfcvb 5345 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 2768 instead of equcomd 2052; removing dependency on ax-ext 2734 is possible: prove weak versions (i.e. replace classes with setvars) of drnfc1 2943, eleq2d 2848 (using elequ2 2160), nfcvf 2950, dvelimc 2949, dvelimdc 2948, nfcvf2 2951. (Proof modification is discouraged.)
⊢ (Ⅎ𝑥𝑦 ↔ Ⅎ𝑦𝑥)
21.19.5.5  Lemmas for class substitution Some useful theorems for dealing with substitutions: sbbi 2342, sbcbig 3793, sbcel1g 4377, sbcel2 4379, sbcel12 4372, sbceqg 4373, csbvarg 4395.
Theorem	bj-sbeqALT 37651*	Substitution in an equality (use the more general version bj-sbeq 37652 instead, without disjoint variable condition). (Contributed by BJ, 6-Oct-2018.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ ([𝑦 / 𝑥]𝐴 = 𝐵 ↔ ⦋𝑦 / 𝑥⦌𝐴 = ⦋𝑦 / 𝑥⦌𝐵)
Theorem	bj-sbeq 37652	Distribute proper substitution through an equality relation. (See sbceqg 4373). (Contributed by BJ, 6-Oct-2018.)
⊢ ([𝑦 / 𝑥]𝐴 = 𝐵 ↔ ⦋𝑦 / 𝑥⦌𝐴 = ⦋𝑦 / 𝑥⦌𝐵)
Theorem	bj-sbceqgALT 37653	Distribute proper substitution through an equality relation. Alternate proof of sbceqg 4373. (Contributed by BJ, 6-Oct-2018.) Proof modification is discouraged to avoid using sbceqg 4373, but the Metamath program "MM-PA> MINIMIZE_WITH * / EXCEPT sbceqg" command is ok. (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵 = 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶))
Theorem	bj-csbsnlem 37654*	Lemma for bj-csbsn 37655 (in this lemma, 𝑥 cannot occur in 𝐴). (Contributed by BJ, 6-Oct-2018.) (New usage is discouraged.)
⊢ ⦋𝐴 / 𝑥⦌{𝑥} = {𝐴}
Theorem	bj-csbsn 37655	Substitution in a singleton. (Contributed by BJ, 6-Oct-2018.)
⊢ ⦋𝐴 / 𝑥⦌{𝑥} = {𝐴}
Theorem	bj-sbel1 37656*	Version of sbcel1g 4377 when substituting a set. (Note: one could have a corresponding version of sbcel12 4372 when substituting a set, but the point here is that the antecedent of sbcel1g 4377 is not needed when substituting a set.) (Contributed by BJ, 6-Oct-2018.)
⊢ ([𝑦 / 𝑥]𝐴 ∈ 𝐵 ↔ ⦋𝑦 / 𝑥⦌𝐴 ∈ 𝐵)
Theorem	bj-abv 37657	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 37658	Alternate version of bj-abv 37657; shorter but uses ax-8 2147. (Contributed by BJ, 24-Jul-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥𝜑 → {𝑥 ∣ 𝜑} = V)
Theorem	bj-ab0 37659	The class of sets verifying a falsity is the empty set (closed form of abf 4367). (Contributed by BJ, 24-Jul-2019.) (Proof modification is discouraged.)
⊢ (∀𝑥 ¬ 𝜑 → {𝑥 ∣ 𝜑} = ∅)
Theorem	bj-abf 37660	Shorter proof of abf 4367 (which should be kept as abfALT). (Contributed by BJ, 24-Jul-2019.) (Proof modification is discouraged.)
⊢ ¬ 𝜑    ⇒   ⊢ {𝑥 ∣ 𝜑} = ∅
Theorem	bj-csbprc 37661	More direct proof of csbprc 4370 (fewer essential steps). (Contributed by BJ, 24-Jul-2019.) (Proof modification is discouraged.)
⊢ (¬ 𝐴 ∈ V → ⦋𝐴 / 𝑥⦌𝐵 = ∅)
21.19.5.6  Removing some axiom requirements and disjoint variable conditions
Theorem	bj-exlimvmpi 37662*	A Fol lemma (exlimiv 1963 followed by mpi 21). (Contributed by BJ, 2-Jul-2022.) (Proof modification is discouraged.)
⊢ (𝜒 → (𝜑 → 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ (∃𝑥𝜒 → 𝜓)
Theorem	bj-exlimmpi 37663	Lemma for bj-vtoclg1f1 37668 (an instance of this lemma is a version of bj-vtoclg1f1 37668 where 𝑥 and 𝑦 are identified). (Contributed by BJ, 30-Apr-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝜒 → (𝜑 → 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ (∃𝑥𝜒 → 𝜓)
Theorem	bj-exlimmpbi 37664	Lemma for theorems of the vtoclg 3520 family. (Contributed by BJ, 3-Oct-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝜒 → (𝜑 ↔ 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ (∃𝑥𝜒 → 𝜓)
Theorem	bj-exlimmpbir 37665	Lemma for theorems of the vtoclg 3520 family. (Contributed by BJ, 3-Oct-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜒 → (𝜑 ↔ 𝜓))    &   ⊢ 𝜓    ⇒   ⊢ (∃𝑥𝜒 → 𝜑)
Theorem	bj-vtoclf 37666*	Remove dependency on ax-ext 2734, df-clab 2741 and df-cleq 2754 (and df-sb 2100 and df-v 3455) from vtoclf 3528. (Contributed by BJ, 6-Oct-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ 𝐴 ∈ 𝑉    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ 𝜓
Theorem	bj-vtocl 37667*	Remove dependency on ax-ext 2734, df-clab 2741 and df-cleq 2754 (and df-sb 2100 and df-v 3455) from vtocl 3523. (Contributed by BJ, 6-Oct-2019.) (Proof modification is discouraged.)
⊢ 𝐴 ∈ 𝑉    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ 𝜓
Theorem	bj-vtoclg1f1 37668*	The FOL content of vtoclg1f 3533 (hence not using ax-ext 2734, df-cleq 2754, df-nfc 2911, df-v 3455). 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 2734; as a byproduct, this dispenses with ax-11 2194 and ax-13 2403). (Contributed by BJ, 30-Apr-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 → 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ (∃𝑦 𝑦 = 𝐴 → 𝜓)
Theorem	bj-vtoclg1f 37669*	Reprove vtoclg1f 3533 from bj-vtoclg1f1 37668. This removes dependency on ax-ext 2734, df-cleq 2754 and df-v 3455. Use bj-vtoclg1fv 37670 instead when sufficient (in particular when 𝑉 is substituted for V). (Contributed by BJ, 14-Sep-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 → 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝜓)
Theorem	bj-vtoclg1fv 37670*	Version of bj-vtoclg1f 37669 with a disjoint variable condition on 𝑥, 𝑉. This removes dependency on df-sb 2100 and df-clab 2741. Prefer its use over bj-vtoclg1f 37669 when sufficient (in particular when 𝑉 is substituted for V). (Contributed by BJ, 14-Sep-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 → 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝜓)
Theorem	bj-vtoclg 37671*	A version of vtoclg 3520 with an additional disjoint variable condition (which is removable if we allow use of df-clab 2741, see bj-vtoclg1f 37669), which requires fewer axioms (i.e., removes dependency on ax-6 2000, ax-7 2041, ax-9 2155, ax-12 2215, ax-ext 2734, df-clab 2741, df-cleq 2754, df-v 3455). (Contributed by BJ, 2-Jul-2022.) (Proof modification is discouraged.)
⊢ (𝑥 = 𝐴 → (𝜑 → 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝜓)
Theorem	bj-rabeqbid 37672	Version of rabeqbidv 3432 with two disjoint variable conditions removed and the third replaced by a nonfreeness hypothesis. (Contributed by BJ, 27-Apr-2019.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒})
Theorem	bj-seex 37673*	Version of seex 5618 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 37674*	Version of df-nfc 2911 with a disjoint variable condition replaced with a nonfreeness hypothesis. (Contributed by BJ, 2-May-2019.)
⊢ Ⅎ𝑦𝐴    ⇒   ⊢ (Ⅎ𝑥𝐴 ↔ ∀𝑦Ⅎ𝑥 𝑦 ∈ 𝐴)
Theorem	bj-sepg 37675*	Version of sepg 5257 which does not require df-clab 2741, thanks to the use of bj-vtoclg 37671 (and ultimately, to the use of elissetv 2843 instead of elisset 2844). This axiom save is not very important, since this theorem uses df-cleq 2754 and df-clel 2837. This theorem is a remnant of a previous state of set.mm where the axiom saving was larger. (Contributed by BJ, 2-Jul-2022.) (Proof modification is discouraged.)
⊢ (𝐴 ∈ 𝑉 → ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝜑)))
Theorem	bj-inex1gALT 37676	Proof of inex1g 5286 from sepg 5257 to then allow proving inex1 5284 from it. That does not reduce the combined proof size of inex1 5284 and inex1g 5286. (Contributed by BJ, 14-Jul-2026.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∩ 𝐵) ∈ V)
21.19.5.7  Class abstractions A few additional theorems on class abstractions and restricted class abstractions.
Theorem	bj-elabd2ALT 37677*	Alternate proof of elabd2 3627 bypassing elab6g 3626 (and using sbiedvw 2132 instead of the ∀𝑥(𝑥 = 𝑦 → 𝜓) idiom). (Contributed by BJ, 16-Oct-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 = {𝑥 ∣ 𝜓})    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (𝐴 ∈ 𝐵 ↔ 𝜒))
Theorem	bj-unrab 37678*	Generalization of unrab 4264. Equality need not hold. (Contributed by BJ, 21-Apr-2019.)
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∪ {𝑥 ∈ 𝐵 ∣ 𝜓}) ⊆ {𝑥 ∈ (𝐴 ∪ 𝐵) ∣ (𝜑 ∨ 𝜓)}
Theorem	bj-inrab 37679	Generalization of inrab 4265. (Contributed by BJ, 21-Apr-2019.)
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ {𝑥 ∈ 𝐵 ∣ 𝜓}) = {𝑥 ∈ (𝐴 ∩ 𝐵) ∣ (𝜑 ∧ 𝜓)}
Theorem	bj-inrab2 37680	Shorter proof of inrab 4265. (Contributed by BJ, 21-Apr-2019.) (Proof modification is discouraged.)
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ {𝑥 ∈ 𝐴 ∣ 𝜓}) = {𝑥 ∈ 𝐴 ∣ (𝜑 ∧ 𝜓)}
Theorem	bj-inrab3 37681*	Generalization of dfrab3ss 4272. Shortens dfrab3ss 4272. (Contributed by BJ, 21-Apr-2019.) (Revised by OpenAI, 7-Jul-2020.)
⊢ (𝐴 ∩ {𝑥 ∈ 𝐵 ∣ 𝜑}) = ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ 𝐵)
Theorem	bj-rabtr 37682*	Restricted class abstraction with true formula. (Contributed by BJ, 22-Apr-2019.)
⊢ {𝑥 ∈ 𝐴 ∣ ⊤} = 𝐴
Theorem	bj-rabtrALT 37683*	Alternate proof of bj-rabtr 37682. (Contributed by BJ, 22-Apr-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ {𝑥 ∈ 𝐴 ∣ ⊤} = 𝐴
Theorem	bj-rabtrAUTO 37684*	Proof of bj-rabtr 37682 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.)
⊢ {𝑥 ∈ 𝐴 ∣ ⊤} = 𝐴
21.19.5.8  Generalized class abstractions
Syntax	bj-cgab 37685	Syntax for generalized class abstractions.
class {𝐴 ∣ 𝑥 ∣ 𝜑}
Definition	df-bj-gab 37686*	Definition of generalized class abstractions: typically, 𝑥 is a bound variable in 𝐴 and 𝜑 and {𝐴 ∣ 𝑥 ∣ 𝜑} denotes "the class of 𝐴(𝑥)'s such that 𝜑(𝑥)". (Contributed by BJ, 4-Oct-2024.)
⊢ {𝐴 ∣ 𝑥 ∣ 𝜑} = {𝑦 ∣ ∃𝑥(𝐴 = 𝑦 ∧ 𝜑)}
Theorem	bj-gabss 37687	Inclusion of generalized class abstractions. (Contributed by BJ, 4-Oct-2024.)
⊢ (∀𝑥(𝐴 = 𝐵 ∧ (𝜑 → 𝜓)) → {𝐴 ∣ 𝑥 ∣ 𝜑} ⊆ {𝐵 ∣ 𝑥 ∣ 𝜓})
Theorem	bj-gabssd 37688	Inclusion of generalized class abstractions. Deduction form. (Contributed by BJ, 4-Oct-2024.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → {𝐴 ∣ 𝑥 ∣ 𝜓} ⊆ {𝐵 ∣ 𝑥 ∣ 𝜒})
Theorem	bj-gabeqd 37689	Equality of generalized class abstractions. Deduction form. (Contributed by BJ, 4-Oct-2024.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {𝐴 ∣ 𝑥 ∣ 𝜓} = {𝐵 ∣ 𝑥 ∣ 𝜒})
Theorem	bj-gabeqis 37690*	Equality of generalized class abstractions, with implicit substitution. (Contributed by BJ, 4-Oct-2024.)
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ {𝐴 ∣ 𝑥 ∣ 𝜑} = {𝐵 ∣ 𝑦 ∣ 𝜓}
Theorem	bj-elgab 37691	Elements of a generalized class abstraction. (Contributed by BJ, 4-Oct-2024.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → Ⅎ𝑥𝐴)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → (∃𝑥(𝐴 = 𝐵 ∧ 𝜓) ↔ 𝜒))    ⇒   ⊢ (𝜑 → (𝐴 ∈ {𝐵 ∣ 𝑥 ∣ 𝜓} ↔ 𝜒))
Theorem	bj-gabima 37692	Generalized class abstraction as a direct image. TODO: improve the support lemmas elimag 6064 and fvelima 6947 to nonfreeness hypothesis (and for the latter, biconditional). (Contributed by BJ, 4-Oct-2024.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → Ⅎ𝑥𝐹)    &   ⊢ (𝜑 → Fun 𝐹)    &   ⊢ (𝜑 → {𝑥 ∣ 𝜓} ⊆ dom 𝐹)    ⇒   ⊢ (𝜑 → {(𝐹‘𝑥) ∣ 𝑥 ∣ 𝜓} = (𝐹 “ {𝑥 ∣ 𝜓}))
21.19.5.9  Restricted nonfreeness In this subsection, we define restricted nonfreeness (or relative nonfreeness).
Syntax	wrnf 37693	Syntax for restricted nonfreeness.
wff Ⅎ𝑥 ∈ 𝐴𝜑
Definition	df-bj-rnf 37694	Definition of restricted nonfreeness. Informally, the proposition Ⅎ𝑥 ∈ 𝐴𝜑 means that 𝜑(𝑥) does not vary on 𝐴. (Contributed by BJ, 19-Mar-2021.)
⊢ (Ⅎ𝑥 ∈ 𝐴𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜑))
21.19.5.10  Russell's paradox A few results around Russell's paradox. For clarity, we prove separately a FOL statement (now in the main part as ru0 2164) and then two versions (bj-ru1 37695 and bj-ru 37696). Special attention is put on minimizing axiom depencencies.
Theorem	bj-ru1 37695*	A version of Russell's paradox ru 3741 not mentioning the universal class. (see also bj-ru 37696). (Contributed by BJ, 12-Oct-2019.) Remove usage of ax-10 2178, ax-11 2194, ax-12 2215 by using eqabbw 2835 following BTernaryTau's similar revision of ru 3741. (Revised by BJ, 28-Jun-2025.) (Proof modification is discouraged.)
⊢ ¬ ∃𝑦 𝑦 = {𝑥 ∣ ¬ 𝑥 ∈ 𝑥}
Theorem	bj-ru 37696	Remove dependency on ax-13 2403 (and df-v 3455) from Russell's paradox ru 3741 expressed with primitive symbols and with a class variable 𝑉. Note the more economical use of elissetv 2843 instead of isset 3467 to avoid use of df-v 3455. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.)
⊢ ¬ {𝑥 ∣ ¬ 𝑥 ∈ 𝑥} ∈ 𝑉
21.19.5.11  Curry's paradox in set theory
Theorem	currysetlem 37697*	Lemma for currysetlem 37697, where it is used with (𝑥 ∈ 𝑥 → 𝜑) substituted for 𝜓. (Contributed by BJ, 23-Sep-2023.) This proof is intuitionistically valid. (Proof modification is discouraged.)
⊢ ({𝑥 ∣ 𝜓} ∈ 𝑉 → ({𝑥 ∣ 𝜓} ∈ {𝑥 ∣ (𝑥 ∈ 𝑥 → 𝜑)} ↔ ({𝑥 ∣ 𝜓} ∈ {𝑥 ∣ 𝜓} → 𝜑)))
Theorem	curryset 37698*	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 37702. (Contributed by BJ, 23-Sep-2023.) This proof is intuitionistically valid. (Proof modification is discouraged.)
⊢ ¬ {𝑥 ∣ (𝑥 ∈ 𝑥 → 𝜑)} ∈ 𝑉
Theorem	currysetlem1 37699*	Lemma for currysetALT 37702. (Contributed by BJ, 23-Sep-2023.) This proof is intuitionistically valid. (Proof modification is discouraged.)
⊢ 𝑋 = {𝑥 ∣ (𝑥 ∈ 𝑥 → 𝜑)}    ⇒   ⊢ (𝑋 ∈ 𝑉 → (𝑋 ∈ 𝑋 ↔ (𝑋 ∈ 𝑋 → 𝜑)))
Theorem	currysetlem2 37700*	Lemma for currysetALT 37702. (Contributed by BJ, 23-Sep-2023.) This proof is intuitionistically valid. (Proof modification is discouraged.)
⊢ 𝑋 = {𝑥 ∣ (𝑥 ∈ 𝑥 → 𝜑)}    ⇒   ⊢ (𝑋 ∈ 𝑉 → (𝑋 ∈ 𝑋 → 𝜑))