P. 355 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 35401-35500   *Has distinct variable group(s)

Type	Label	Description
Statement
21.15.5  Set theory
21.15.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 2702, df-clab 2709, df-cleq 2723, df-clel 2809 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 2702, df-clab 2709, df-cleq 2723, df-clel 2809 }) 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 35408, eliminable-abeqv 35409, eliminable-abeqab 35410, eliminable-velab 35407, eliminable-abelv 35411, eliminable-abelab 35412 respectively, which are all proved from {FOL, ax-ext 2702, df-clab 2709, df-cleq 2723, df-clel 2809 }. (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 2709, dfcleq 2724 (proved from {FOL, ax-ext 2702, df-cleq 2723 }), and dfclel 2810 (proved from {FOL, df-clel 2809 }). 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 35402, eliminable2b 35403 and eliminable3a 35405, 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 2709 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 2709, ax-ext 2702 and df-cleq 2723 are sufficient (over FOL) to eliminate class terms. To prove that { df-clab 2709, df-cleq 2723, df-clel 2809 } provides a definitional extension of {FOL, ax-ext 2702 }, 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 2709, df-cleq 2723, df-clel 2809 }. 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 2702 }. 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 2709, df-cleq 2723, df-clel 2809 }. It involves a careful case study on the structure of the proof tree.
Theorem	eliminable1 35401	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 35402*	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 35403*	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 35404*	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 35405*	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 35406*	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 35407	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 35408*	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 35409*	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 35410*	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 35411*	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 35412*	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.15.5.2  Classes without the axiom of extensionality A few results about classes can be proved without using ax-ext 2702. One could move all theorems from cab 2708 to df-clel 2809 (except for dfcleq 2724 and cvjust 2725) 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 2723. Note that without ax-ext 2702, the $a-statements df-clab 2709, df-cleq 2723, and df-clel 2809 are no longer eliminable (see previous section) (but PROBABLY df-clab 2709 is still conservative , while df-cleq 2723 and df-clel 2809 are not). This is not a reason not to study what is provable with them but without ax-ext 2702, 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 2820 / eleq2 2821 to eleq1w 2815 / eleq2w 2816 can also be done with eleq1i 2823, eqeltri 2828, eqeltrri 2829, eleq1a 2827, eleq1d 2817, eqeltrd 2832, eqeltrrd 2833, eqneltrd 2852, eqneltrrd 2853, nelneq 2856. Remark: possibility to remove dependency on ax-10 2137, ax-11 2154, ax-13 2370 from nfcri 2889 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 2914.
Theorem	bj-denoteslem 35413*	Lemma for bj-denotes 35414. (Contributed by BJ, 24-Apr-2024.) (Proof modification is discouraged.)
⊢ (∃𝑥 𝑥 = 𝐴 ↔ 𝐴 ∈ {𝑦 ∣ ⊤})
Theorem	bj-denotes 35414*	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 2735, requires the core axioms and { ax-9 2116, ax-ext 2702, df-cleq 2723 } whereas this proof requires the core axioms and { ax-8 2108, df-clab 2709, df-clel 2809 }. Theorem bj-issetwt 35417 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 2709, df-clel 2809 } (whereas with the shorter proof from cbvexvw 2040 and eqeq1 2735 it would require { ax-8 2108, ax-9 2116, ax-ext 2702, df-clab 2709, df-cleq 2723, df-clel 2809 }). That every class is equal to a class abstraction is proved by abid1 2869, which requires { ax-8 2108, ax-9 2116, ax-ext 2702, df-clab 2709, df-cleq 2723, df-clel 2809 }. 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 2702 and df-cleq 2723 (e.g., eqid 2731 and eqeq1 2735). In particular, one cannot even prove ⊢ ∃𝑥𝑥 = 𝐴 ⇒ ⊢ 𝐴 = 𝐴 without ax-ext 2702 and df-cleq 2723. (Contributed by BJ, 29-Apr-2019.) (Proof modification is discouraged.)
⊢ (∃𝑥 𝑥 = 𝐴 ↔ ∃𝑦 𝑦 = 𝐴)
Theorem	bj-issettru 35415*	Weak version of isset 3459 without ax-ext 2702. (Contributed by BJ, 24-Apr-2024.) (Proof modification is discouraged.)
⊢ (∃𝑥 𝑥 = 𝐴 ↔ 𝐴 ∈ {𝑦 ∣ ⊤})
Theorem	bj-elabtru 35416	This is as close as we can get to proving extensionality for "the" "universal" class without ax-ext 2702. (Contributed by BJ, 24-Apr-2024.) (Proof modification is discouraged.)
⊢ (𝐴 ∈ {𝑥 ∣ ⊤} ↔ 𝐴 ∈ {𝑦 ∣ ⊤})
Theorem	bj-issetwt 35417*	Closed form of bj-issetw 35418. (Contributed by BJ, 29-Apr-2019.) (Proof modification is discouraged.)
⊢ (∀𝑥𝜑 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ ∃𝑦 𝑦 = 𝐴))
Theorem	bj-issetw 35418*	The closest one can get to isset 3459 without using ax-ext 2702. See also vexw 2714. Note that the only disjoint variable condition is between 𝑦 and 𝐴. From there, one can prove isset 3459 using eleq2i 2824 (which requires ax-ext 2702 and df-cleq 2723). (Contributed by BJ, 29-Apr-2019.) (Proof modification is discouraged.)
⊢ 𝜑    ⇒   ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ ∃𝑦 𝑦 = 𝐴)
Theorem	bj-elissetALT 35419*	Alternate proof of elisset 2814. This is essentially the same proof as seen by inlining bj-denotes 35414 and bj-denoteslem 35413. Use elissetv 2813 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 35420*	Version of bj-isseti 35421 with a disjoint variable condition on 𝑥, 𝑉. The hypothesis uses 𝑉 instead of V for extra generality. This is indeed more general than isseti 3461 as long as elex 3464 is not available (and the non-dependence of bj-issetiv 35420 on special properties of the universal class V is obvious). Prefer its use over bj-isseti 35421 when sufficient (in particular when 𝑉 is substituted for V). (Contributed by BJ, 14-Sep-2019.) (Proof modification is discouraged.)
⊢ 𝐴 ∈ 𝑉    ⇒   ⊢ ∃𝑥 𝑥 = 𝐴
Theorem	bj-isseti 35421*	Version of isseti 3461 with a class variable 𝑉 in the hypothesis instead of V for extra generality. This is indeed more general than isseti 3461 as long as elex 3464 is not available (and the non-dependence of bj-isseti 35421 on special properties of the universal class V is obvious). Use bj-issetiv 35420 instead when sufficient (in particular when 𝑉 is substituted for V). (Contributed by BJ, 13-Jun-2019.) (Proof modification is discouraged.)
⊢ 𝐴 ∈ 𝑉    ⇒   ⊢ ∃𝑥 𝑥 = 𝐴
Theorem	bj-ralvw 35422	A weak version of ralv 3470 not using ax-ext 2702 (nor df-cleq 2723, df-clel 2809, df-v 3448), and only core FOL axioms. See also bj-rexvw 35423. The analogues for reuv 3472 and rmov 3473 are not proved. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ 𝜓    ⇒   ⊢ (∀𝑥 ∈ {𝑦 ∣ 𝜓}𝜑 ↔ ∀𝑥𝜑)
Theorem	bj-rexvw 35423	A weak version of rexv 3471 not using ax-ext 2702 (nor df-cleq 2723, df-clel 2809, df-v 3448), and only core FOL axioms. See also bj-ralvw 35422. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ 𝜓    ⇒   ⊢ (∃𝑥 ∈ {𝑦 ∣ 𝜓}𝜑 ↔ ∃𝑥𝜑)
Theorem	bj-rababw 35424	A weak version of rabab 3474 not using df-clel 2809 nor df-v 3448 (but requiring ax-ext 2702) nor ax-12 2171. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ 𝜓    ⇒   ⊢ {𝑥 ∈ {𝑦 ∣ 𝜓} ∣ 𝜑} = {𝑥 ∣ 𝜑}
Theorem	bj-rexcom4bv 35425*	Version of rexcom4b 3475 and bj-rexcom4b 35426 with a disjoint variable condition on 𝑥, 𝑉, hence removing dependency on df-sb 2068 and df-clab 2709 (so that it depends on df-clel 2809 and df-rex 3070 only on top of first-order logic). Prefer its use over bj-rexcom4b 35426 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 35426*	Remove from rexcom4b 3475 dependency on ax-ext 2702 and ax-13 2370 (and on df-or 846, df-cleq 2723, df-nfc 2884, df-v 3448). The hypothesis uses 𝑉 instead of V (see bj-isseti 35421 for the motivation). Use bj-rexcom4bv 35425 instead when sufficient (in particular when 𝑉 is substituted for V). (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ 𝐵 ∈ 𝑉    ⇒   ⊢ (∃𝑥∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵) ↔ ∃𝑦 ∈ 𝐴 𝜑)
Theorem	bj-ceqsalt0 35427	The FOL content of ceqsalt 3476. Lemma for bj-ceqsalt 35429 and bj-ceqsaltv 35430. (Contributed by BJ, 26-Sep-2019.) (Proof modification is discouraged.)
⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝜃 → (𝜑 ↔ 𝜓)) ∧ ∃𝑥𝜃) → (∀𝑥(𝜃 → 𝜑) ↔ 𝜓))
Theorem	bj-ceqsalt1 35428	The FOL content of ceqsalt 3476. Lemma for bj-ceqsalt 35429 and bj-ceqsaltv 35430. TODO: consider removing if it does not add anything to bj-ceqsalt0 35427. (Contributed by BJ, 26-Sep-2019.) (Proof modification is discouraged.)
⊢ (𝜃 → ∃𝑥𝜒)    ⇒   ⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝜒 → (𝜑 ↔ 𝜓)) ∧ 𝜃) → (∀𝑥(𝜒 → 𝜑) ↔ 𝜓))
Theorem	bj-ceqsalt 35429*	Remove from ceqsalt 3476 dependency on ax-ext 2702 (and on df-cleq 2723 and df-v 3448). Note: this is not doable with ceqsralt 3477 (or ceqsralv 3484), which uses eleq1 2820, but the same dependence removal is possible for ceqsalg 3478, ceqsal 3480, ceqsalv 3482, cgsexg 3489, cgsex2g 3490, cgsex4g 3491, ceqsex 3493, ceqsexv 3495, ceqsex2 3499, ceqsex2v 3500, ceqsex3v 3501, ceqsex4v 3502, ceqsex6v 3503, ceqsex8v 3504, gencbvex 3505 (after changing 𝐴 = 𝑦 to 𝑦 = 𝐴), gencbvex2 3506, gencbval 3507, vtoclgft 3510 (it uses Ⅎ, whose justification nfcjust 2883 does not use ax-ext 2702) and several other vtocl* theorems (see for instance bj-vtoclg1f 35461). See also bj-ceqsaltv 35430. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝑉) → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
Theorem	bj-ceqsaltv 35430*	Version of bj-ceqsalt 35429 with a disjoint variable condition on 𝑥, 𝑉, removing dependency on df-sb 2068 and df-clab 2709. Prefer its use over bj-ceqsalt 35429 when sufficient (in particular when 𝑉 is substituted for V). (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝑉) → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
Theorem	bj-ceqsalg0 35431	The FOL content of ceqsalg 3478. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝜒 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥𝜒 → (∀𝑥(𝜒 → 𝜑) ↔ 𝜓))
Theorem	bj-ceqsalg 35432*	Remove from ceqsalg 3478 dependency on ax-ext 2702 (and on df-cleq 2723 and df-v 3448). See also bj-ceqsalgv 35434. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
Theorem	bj-ceqsalgALT 35433*	Alternate proof of bj-ceqsalg 35432. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
Theorem	bj-ceqsalgv 35434*	Version of bj-ceqsalg 35432 with a disjoint variable condition on 𝑥, 𝑉, removing dependency on df-sb 2068 and df-clab 2709. Prefer its use over bj-ceqsalg 35432 when sufficient (in particular when 𝑉 is substituted for V). (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
Theorem	bj-ceqsalgvALT 35435*	Alternate proof of bj-ceqsalgv 35434. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
Theorem	bj-ceqsal 35436*	Remove from ceqsal 3480 dependency on ax-ext 2702 (and on df-cleq 2723, df-v 3448, df-clab 2709, df-sb 2068). (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ 𝐴 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓)
Theorem	bj-ceqsalv 35437*	Remove from ceqsalv 3482 dependency on ax-ext 2702 (and on df-cleq 2723, df-v 3448, df-clab 2709, df-sb 2068). (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.)
⊢ 𝐴 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓)
Theorem	bj-spcimdv 35438*	Remove from spcimdv 3553 dependency on ax-9 2116, ax-10 2137, ax-11 2154, ax-13 2370, ax-ext 2702, df-cleq 2723 (and df-nfc 2884, df-v 3448, df-or 846, df-tru 1544, df-nf 1786). For an even more economical version, see bj-spcimdvv 35439. (Contributed by BJ, 30-Nov-2020.) (Proof modification is discouraged.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 → 𝜒))
Theorem	bj-spcimdvv 35439*	Remove from spcimdv 3553 dependency on ax-7 2011, ax-8 2108, ax-10 2137, ax-11 2154, ax-12 2171 ax-13 2370, ax-ext 2702, df-cleq 2723, df-clab 2709 (and df-nfc 2884, df-v 3448, 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 35438. (Contributed by BJ, 3-Nov-2021.) (Proof modification is discouraged.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 → 𝜒))
21.15.5.3  Characterization among sets versus among classes
Theorem	elelb 35440	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 35441	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.15.5.4  The nonfreeness quantifier for classes In this section, we prove the symmetry of the nonfreeness quantifier for classes.
Theorem	bj-nfcsym 35442	The nonfreeness quantifier for classes defines a symmetric binary relation on var metavariables (irreflexivity is proved by nfnid 5335 with additional axioms; see also nfcv 2902). This could be proved from aecom 2425 and nfcvb 5336 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 2737 instead of equcomd 2022; removing dependency on ax-ext 2702 is possible: prove weak versions (i.e. replace classes with setvars) of drnfc1 2921, eleq2d 2818 (using elequ2 2121), nfcvf 2931, dvelimc 2930, dvelimdc 2929, nfcvf2 2932. (Proof modification is discouraged.)
⊢ (Ⅎ𝑥𝑦 ↔ Ⅎ𝑦𝑥)
21.15.5.5  Lemmas for class substitution Some useful theorems for dealing with substitutions: sbbi 2304, sbcbig 3796, sbcel1g 4378, sbcel2 4380, sbcel12 4373, sbceqg 4374, csbvarg 4396.
Theorem	bj-sbeqALT 35443*	Substitution in an equality (use the more general version bj-sbeq 35444 instead, without disjoint variable condition). (Contributed by BJ, 6-Oct-2018.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ ([𝑦 / 𝑥]𝐴 = 𝐵 ↔ ⦋𝑦 / 𝑥⦌𝐴 = ⦋𝑦 / 𝑥⦌𝐵)
Theorem	bj-sbeq 35444	Distribute proper substitution through an equality relation. (See sbceqg 4374). (Contributed by BJ, 6-Oct-2018.)
⊢ ([𝑦 / 𝑥]𝐴 = 𝐵 ↔ ⦋𝑦 / 𝑥⦌𝐴 = ⦋𝑦 / 𝑥⦌𝐵)
Theorem	bj-sbceqgALT 35445	Distribute proper substitution through an equality relation. Alternate proof of sbceqg 4374. (Contributed by BJ, 6-Oct-2018.) Proof modification is discouraged to avoid using sbceqg 4374, but the Metamath program "MM-PA> MINIMIZE_WITH * / EXCEPT sbceqg" command is ok. (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵 = 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶))
Theorem	bj-csbsnlem 35446*	Lemma for bj-csbsn 35447 (in this lemma, 𝑥 cannot occur in 𝐴). (Contributed by BJ, 6-Oct-2018.) (New usage is discouraged.)
⊢ ⦋𝐴 / 𝑥⦌{𝑥} = {𝐴}
Theorem	bj-csbsn 35447	Substitution in a singleton. (Contributed by BJ, 6-Oct-2018.)
⊢ ⦋𝐴 / 𝑥⦌{𝑥} = {𝐴}
Theorem	bj-sbel1 35448*	Version of sbcel1g 4378 when substituting a set. (Note: one could have a corresponding version of sbcel12 4373 when substituting a set, but the point here is that the antecedent of sbcel1g 4378 is not needed when substituting a set.) (Contributed by BJ, 6-Oct-2018.)
⊢ ([𝑦 / 𝑥]𝐴 ∈ 𝐵 ↔ ⦋𝑦 / 𝑥⦌𝐴 ∈ 𝐵)
Theorem	bj-abv 35449	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 35450	Alternate version of bj-abv 35449; shorter but uses ax-8 2108. (Contributed by BJ, 24-Jul-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥𝜑 → {𝑥 ∣ 𝜑} = V)
Theorem	bj-ab0 35451	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 35452	Shorter proof of abf 4367 (which should be kept as abfALT). (Contributed by BJ, 24-Jul-2019.) (Proof modification is discouraged.)
⊢ ¬ 𝜑    ⇒   ⊢ {𝑥 ∣ 𝜑} = ∅
Theorem	bj-csbprc 35453	More direct proof of csbprc 4371 (fewer essential steps). (Contributed by BJ, 24-Jul-2019.) (Proof modification is discouraged.)
⊢ (¬ 𝐴 ∈ V → ⦋𝐴 / 𝑥⦌𝐵 = ∅)
21.15.5.6  Removing some axiom requirements and disjoint variable conditions
Theorem	bj-exlimvmpi 35454*	A Fol lemma (exlimiv 1933 followed by mpi 20). (Contributed by BJ, 2-Jul-2022.) (Proof modification is discouraged.)
⊢ (𝜒 → (𝜑 → 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ (∃𝑥𝜒 → 𝜓)
Theorem	bj-exlimmpi 35455	Lemma for bj-vtoclg1f1 35460 (an instance of this lemma is a version of bj-vtoclg1f1 35460 where 𝑥 and 𝑦 are identified). (Contributed by BJ, 30-Apr-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝜒 → (𝜑 → 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ (∃𝑥𝜒 → 𝜓)
Theorem	bj-exlimmpbi 35456	Lemma for theorems of the vtoclg 3526 family. (Contributed by BJ, 3-Oct-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝜒 → (𝜑 ↔ 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ (∃𝑥𝜒 → 𝜓)
Theorem	bj-exlimmpbir 35457	Lemma for theorems of the vtoclg 3526 family. (Contributed by BJ, 3-Oct-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜒 → (𝜑 ↔ 𝜓))    &   ⊢ 𝜓    ⇒   ⊢ (∃𝑥𝜒 → 𝜑)
Theorem	bj-vtoclf 35458*	Remove dependency on ax-ext 2702, df-clab 2709 and df-cleq 2723 (and df-sb 2068 and df-v 3448) from vtoclf 3517. (Contributed by BJ, 6-Oct-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ 𝐴 ∈ 𝑉    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ 𝜓
Theorem	bj-vtocl 35459*	Remove dependency on ax-ext 2702, df-clab 2709 and df-cleq 2723 (and df-sb 2068 and df-v 3448) from vtocl 3519. (Contributed by BJ, 6-Oct-2019.) (Proof modification is discouraged.)
⊢ 𝐴 ∈ 𝑉    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ 𝜓
Theorem	bj-vtoclg1f1 35460*	The FOL content of vtoclg1f 3525 (hence not using ax-ext 2702, df-cleq 2723, df-nfc 2884, df-v 3448). 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 2702; 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 35461*	Reprove vtoclg1f 3525 from bj-vtoclg1f1 35460. This removes dependency on ax-ext 2702, df-cleq 2723 and df-v 3448. Use bj-vtoclg1fv 35462 instead when sufficient (in particular when 𝑉 is substituted for V). (Contributed by BJ, 14-Sep-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 → 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝜓)
Theorem	bj-vtoclg1fv 35462*	Version of bj-vtoclg1f 35461 with a disjoint variable condition on 𝑥, 𝑉. This removes dependency on df-sb 2068 and df-clab 2709. Prefer its use over bj-vtoclg1f 35461 when sufficient (in particular when 𝑉 is substituted for V). (Contributed by BJ, 14-Sep-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 → 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝜓)
Theorem	bj-vtoclg 35463*	A version of vtoclg 3526 with an additional disjoint variable condition (which is removable if we allow use of df-clab 2709, see bj-vtoclg1f 35461), which requires fewer axioms (i.e., removes dependency on ax-6 1971, ax-7 2011, ax-9 2116, ax-12 2171, ax-ext 2702, df-clab 2709, df-cleq 2723, df-v 3448). (Contributed by BJ, 2-Jul-2022.) (Proof modification is discouraged.)
⊢ (𝑥 = 𝐴 → (𝜑 → 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝜓)
Theorem	bj-rabeqbid 35464	Version of rabeqbidv 3422 with two disjoint variable conditions removed and the third replaced by a nonfreeness hypothesis. (Contributed by BJ, 27-Apr-2019.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒})
Theorem	bj-seex 35465*	Version of seex 5600 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 35466*	Version of df-nfc 2884 with a disjoint variable condition replaced with a nonfreeness hypothesis. (Contributed by BJ, 2-May-2019.)
⊢ Ⅎ𝑦𝐴    ⇒   ⊢ (Ⅎ𝑥𝐴 ↔ ∀𝑦Ⅎ𝑥 𝑦 ∈ 𝐴)
Theorem	bj-zfauscl 35467*	General version of zfauscl 5263. Remark: the comment in zfauscl 5263 is misleading: the essential use of ax-ext 2702 is the one via eleq2 2821 and not the one via vtocl 3519, since the latter can be proved without ax-ext 2702 (see bj-vtoclg 35463). (Contributed by BJ, 2-Jul-2022.) (Proof modification is discouraged.)
⊢ (𝐴 ∈ 𝑉 → ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝜑)))
21.15.5.7  Class abstractions A few additional theorems on class abstractions and restricted class abstractions.
Theorem	bj-elabd2ALT 35468*	Alternate proof of elabd2 3625 bypassing elab6g 3624 (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 35469*	Generalization of unrab 4270. Equality need not hold. (Contributed by BJ, 21-Apr-2019.)
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∪ {𝑥 ∈ 𝐵 ∣ 𝜓}) ⊆ {𝑥 ∈ (𝐴 ∪ 𝐵) ∣ (𝜑 ∨ 𝜓)}
Theorem	bj-inrab 35470	Generalization of inrab 4271. (Contributed by BJ, 21-Apr-2019.)
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ {𝑥 ∈ 𝐵 ∣ 𝜓}) = {𝑥 ∈ (𝐴 ∩ 𝐵) ∣ (𝜑 ∧ 𝜓)}
Theorem	bj-inrab2 35471	Shorter proof of inrab 4271. (Contributed by BJ, 21-Apr-2019.) (Proof modification is discouraged.)
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ {𝑥 ∈ 𝐴 ∣ 𝜓}) = {𝑥 ∈ 𝐴 ∣ (𝜑 ∧ 𝜓)}
Theorem	bj-inrab3 35472*	Generalization of dfrab3ss 4277, which it may shorten. (Contributed by BJ, 21-Apr-2019.) (Revised by OpenAI, 7-Jul-2020.)
⊢ (𝐴 ∩ {𝑥 ∈ 𝐵 ∣ 𝜑}) = ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ 𝐵)
Theorem	bj-rabtr 35473*	Restricted class abstraction with true formula. (Contributed by BJ, 22-Apr-2019.)
⊢ {𝑥 ∈ 𝐴 ∣ ⊤} = 𝐴
Theorem	bj-rabtrALT 35474*	Alternate proof of bj-rabtr 35473. (Contributed by BJ, 22-Apr-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ {𝑥 ∈ 𝐴 ∣ ⊤} = 𝐴
Theorem	bj-rabtrAUTO 35475*	Proof of bj-rabtr 35473 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.15.5.8  Generalized class abstractions
Syntax	bj-cgab 35476	Syntax for generalized class abstractions.
class {𝐴 ∣ 𝑥 ∣ 𝜑}
Definition	df-bj-gab 35477*	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 35478	Inclusion of generalized class abstractions. (Contributed by BJ, 4-Oct-2024.)
⊢ (∀𝑥(𝐴 = 𝐵 ∧ (𝜑 → 𝜓)) → {𝐴 ∣ 𝑥 ∣ 𝜑} ⊆ {𝐵 ∣ 𝑥 ∣ 𝜓})
Theorem	bj-gabssd 35479	Inclusion of generalized class abstractions. Deduction form. (Contributed by BJ, 4-Oct-2024.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → {𝐴 ∣ 𝑥 ∣ 𝜓} ⊆ {𝐵 ∣ 𝑥 ∣ 𝜒})
Theorem	bj-gabeqd 35480	Equality of generalized class abstractions. Deduction form. (Contributed by BJ, 4-Oct-2024.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {𝐴 ∣ 𝑥 ∣ 𝜓} = {𝐵 ∣ 𝑥 ∣ 𝜒})
Theorem	bj-gabeqis 35481*	Equality of generalized class abstractions, with implicit substitution. (Contributed by BJ, 4-Oct-2024.)
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ {𝐴 ∣ 𝑥 ∣ 𝜑} = {𝐵 ∣ 𝑦 ∣ 𝜓}
Theorem	bj-elgab 35482	Elements of a generalized class abstraction. (Contributed by BJ, 4-Oct-2024.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → Ⅎ𝑥𝐴)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → (∃𝑥(𝐴 = 𝐵 ∧ 𝜓) ↔ 𝜒))    ⇒   ⊢ (𝜑 → (𝐴 ∈ {𝐵 ∣ 𝑥 ∣ 𝜓} ↔ 𝜒))
Theorem	bj-gabima 35483	Generalized class abstraction as a direct image. TODO: improve the support lemmas elimag 6022 and fvelima 6913 to nonfreeness hypothesis (and for the latter, biconditional). (Contributed by BJ, 4-Oct-2024.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → Ⅎ𝑥𝐹)    &   ⊢ (𝜑 → Fun 𝐹)    &   ⊢ (𝜑 → {𝑥 ∣ 𝜓} ⊆ dom 𝐹)    ⇒   ⊢ (𝜑 → {(𝐹‘𝑥) ∣ 𝑥 ∣ 𝜓} = (𝐹 “ {𝑥 ∣ 𝜓}))
21.15.5.9  Restricted nonfreeness In this subsection, we define restricted nonfreeness (or relative nonfreeness).
Syntax	wrnf 35484	Syntax for restricted nonfreeness.
wff Ⅎ𝑥 ∈ 𝐴𝜑
Definition	df-bj-rnf 35485	Definition of restricted nonfreeness. Informally, the proposition Ⅎ𝑥 ∈ 𝐴𝜑 means that 𝜑(𝑥) does not vary on 𝐴. (Contributed by BJ, 19-Mar-2021.)
⊢ (Ⅎ𝑥 ∈ 𝐴𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜑))
21.15.5.10  Russell's paradox A few results around Russell's paradox. For clarity, we prove separately its FOL part (bj-ru0 35486) and then two versions (bj-ru1 35487 and bj-ru 35488). Special attention is put on minimizing axiom depencencies.
Theorem	bj-ru0 35486*	The FOL part of Russell's paradox ru 3741 (see also bj-ru1 35487, bj-ru 35488). Use of elequ1 2113, bj-elequ12 35219 (instead of eleq1 2820, eleq12d 2826 as in ru 3741) permits to remove dependency on ax-10 2137, ax-11 2154, ax-12 2171, ax-ext 2702, df-sb 2068, df-clab 2709, df-cleq 2723, df-clel 2809. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.)
⊢ ¬ ∀𝑥(𝑥 ∈ 𝑦 ↔ ¬ 𝑥 ∈ 𝑥)
Theorem	bj-ru1 35487*	A version of Russell's paradox ru 3741 (see also bj-ru 35488). (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.)
⊢ ¬ ∃𝑦 𝑦 = {𝑥 ∣ ¬ 𝑥 ∈ 𝑥}
Theorem	bj-ru 35488	Remove dependency on ax-13 2370 (and df-v 3448) from Russell's paradox ru 3741 expressed with primitive symbols and with a class variable 𝑉. Note the more economical use of elissetv 2813 instead of isset 3459 to avoid use of df-v 3448. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.)
⊢ ¬ {𝑥 ∣ ¬ 𝑥 ∈ 𝑥} ∈ 𝑉
21.15.5.11  Curry's paradox in set theory
Theorem	currysetlem 35489*	Lemma for currysetlem 35489, where it is used with (𝑥 ∈ 𝑥 → 𝜑) substituted for 𝜓. (Contributed by BJ, 23-Sep-2023.) This proof is intuitionistically valid. (Proof modification is discouraged.)
⊢ ({𝑥 ∣ 𝜓} ∈ 𝑉 → ({𝑥 ∣ 𝜓} ∈ {𝑥 ∣ (𝑥 ∈ 𝑥 → 𝜑)} ↔ ({𝑥 ∣ 𝜓} ∈ {𝑥 ∣ 𝜓} → 𝜑)))
Theorem	curryset 35490*	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 35494. (Contributed by BJ, 23-Sep-2023.) This proof is intuitionistically valid. (Proof modification is discouraged.)
⊢ ¬ {𝑥 ∣ (𝑥 ∈ 𝑥 → 𝜑)} ∈ 𝑉
Theorem	currysetlem1 35491*	Lemma for currysetALT 35494. (Contributed by BJ, 23-Sep-2023.) This proof is intuitionistically valid. (Proof modification is discouraged.)
⊢ 𝑋 = {𝑥 ∣ (𝑥 ∈ 𝑥 → 𝜑)}    ⇒   ⊢ (𝑋 ∈ 𝑉 → (𝑋 ∈ 𝑋 ↔ (𝑋 ∈ 𝑋 → 𝜑)))
Theorem	currysetlem2 35492*	Lemma for currysetALT 35494. (Contributed by BJ, 23-Sep-2023.) This proof is intuitionistically valid. (Proof modification is discouraged.)
⊢ 𝑋 = {𝑥 ∣ (𝑥 ∈ 𝑥 → 𝜑)}    ⇒   ⊢ (𝑋 ∈ 𝑉 → (𝑋 ∈ 𝑋 → 𝜑))
Theorem	currysetlem3 35493*	Lemma for currysetALT 35494. (Contributed by BJ, 23-Sep-2023.) This proof is intuitionistically valid. (Proof modification is discouraged.)
⊢ 𝑋 = {𝑥 ∣ (𝑥 ∈ 𝑥 → 𝜑)}    ⇒   ⊢ ¬ 𝑋 ∈ 𝑉
Theorem	currysetALT 35494*	Alternate proof of curryset 35490, 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.)
⊢ ¬ {𝑥 ∣ (𝑥 ∈ 𝑥 → 𝜑)} ∈ 𝑉
21.15.5.12  Some disjointness results A few utility theorems on disjointness of classes.
Theorem	bj-n0i 35495*	Inference associated with n0 4311. Shortens 2ndcdisj 22844 (2888>2878), notzfaus 5323 (264>253). (Contributed by BJ, 22-Apr-2019.)
⊢ 𝐴 ≠ ∅    ⇒   ⊢ ∃𝑥 𝑥 ∈ 𝐴
Theorem	bj-disjsn01 35496	Disjointness of the singletons containing 0 and 1. This is a consequence of disjcsn 9549 but the present proof does not use regularity. (Contributed by BJ, 4-Apr-2019.) (Proof modification is discouraged.)
⊢ ({∅} ∩ {1o}) = ∅
Theorem	bj-0nel1 35497	The empty set does not belong to {1o}. (Contributed by BJ, 6-Apr-2019.)
⊢ ∅ ∉ {1o}
Theorem	bj-1nel0 35498	1o does not belong to {∅}. (Contributed by BJ, 6-Apr-2019.)
⊢ 1o ∉ {∅}
21.15.5.13  Complements on direct products A few utility theorems on direct products.
Theorem	bj-xpimasn 35499	The image of a singleton, general case. [Change and relabel xpimasn 6142 accordingly, maybe to xpima2sn.] (Contributed by BJ, 6-Apr-2019.)
⊢ ((𝐴 × 𝐵) “ {𝑋}) = if(𝑋 ∈ 𝐴, 𝐵, ∅)
Theorem	bj-xpima1sn 35500	The image of a singleton by a direct product, empty case. [Change and relabel xpimasn 6142 accordingly, maybe to xpima2sn.] (Contributed by BJ, 6-Apr-2019.)
⊢ (¬ 𝑋 ∈ 𝐴 → ((𝐴 × 𝐵) “ {𝑋}) = ∅)