P. 374 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 37301-37400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	eliminable-abeqab 37301*	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 37302*	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 37303*	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 2728. One could move all theorems from cab 2734 to df-clel 2831 (except for dfcleq 2749 and cvjust 2750) 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 2748. Note that without ax-ext 2728, the $a-statements df-clab 2735, df-cleq 2748, and df-clel 2831 are no longer eliminable (see previous section) (but PROBABLY df-clab 2735 is still conservative , while df-cleq 2748 and df-clel 2831 are not). This is not a reason not to study what is provable with them but without ax-ext 2728, 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 2136, wel 2137, ax-8 2138, ax-9 2146). Remark: the weakening of eleq1 2844 / eleq2 2845 to eleq1w 2839 / eleq2w 2840 can also be done with eleq1i 2847, eqeltri 2852, eqeltrri 2853, eleq1a 2851, eleq1d 2841, eqeltrd 2856, eqeltrrd 2857, eqneltrd 2876, eqneltrrd 2877, nelneq 2880. Remark: possibility to remove dependency on ax-10 2169, ax-11 2185, ax-13 2397 from nfcri 2910 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 2930.
Theorem	bj-denoteslem 37304*	Duplicate of issettru 2834 and bj-issettruALTV 37306. Lemma for bj-denotesALTV 37305. (Contributed by BJ, 24-Apr-2024.) (Proof modification is discouraged.)
⊢ (∃𝑥 𝑥 = 𝐴 ↔ 𝐴 ∈ {𝑦 ∣ ⊤})
Theorem	bj-denotesALTV 37305*	Moved to main as iseqsetv-clel 2835 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 277 (to add an intermediate proposition ∃𝑧𝑧 = 𝐴 with a fresh 𝑧), cbvexvw 2051, and eqeq1 2760, requires the core axioms and { ax-9 2146, ax-ext 2728, df-cleq 2748 } whereas this proof requires the core axioms and { ax-8 2138, df-clab 2735, df-clel 2831 }. Theorem bj-issetwt 37308 proves that "existing" is equivalent to being a member of a class abstraction. It also requires, with the present proof, { ax-8 2138, df-clab 2735, df-clel 2831 } (whereas with the shorter proof from cbvexvw 2051 and eqeq1 2760 it would require { ax-8 2138, ax-9 2146, ax-ext 2728, df-clab 2735, df-cleq 2748, df-clel 2831 }). That every class is equal to a class abstraction is proved by abid1 2892, which requires { ax-8 2138, ax-9 2146, ax-ext 2728, df-clab 2735, df-cleq 2748, df-clel 2831 }. Note that there is no disjoint variable condition on 𝑥, 𝑦 but the theorem does not depend on ax-13 2397. Actually, the proof depends only on the logical axioms ax-1 6 through ax-7 2022 and sp 2212. 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 2728 and df-cleq 2748 (e.g., eqid 2756 and eqeq1 2760). In particular, one cannot even prove ⊢ ∃𝑥𝑥 = 𝐴 ⇒ ⊢ 𝐴 = 𝐴 without ax-ext 2728 and df-cleq 2748. (Contributed by BJ, 29-Apr-2019.) (Proof modification is discouraged.)
⊢ (∃𝑥 𝑥 = 𝐴 ↔ ∃𝑦 𝑦 = 𝐴)
Theorem	bj-issettruALTV 37306*	Moved to main as issettru 2834 and kept for the comments. Weak version of isset 3462 without ax-ext 2728. (Contributed by BJ, 24-Apr-2024.) (Proof modification is discouraged.)
⊢ (∃𝑥 𝑥 = 𝐴 ↔ 𝐴 ∈ {𝑦 ∣ ⊤})
Theorem	bj-elabtru 37307	This is as close as we can get to proving extensionality for "the" "universal" class without ax-ext 2728. (Contributed by BJ, 24-Apr-2024.) (Proof modification is discouraged.)
⊢ (𝐴 ∈ {𝑥 ∣ ⊤} ↔ 𝐴 ∈ {𝑦 ∣ ⊤})
Theorem	bj-issetwt 37308*	Closed form of bj-issetw 37309. (Contributed by BJ, 29-Apr-2019.) (Proof modification is discouraged.)
⊢ (∀𝑥𝜑 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ ∃𝑦 𝑦 = 𝐴))
Theorem	bj-issetw 37309*	The closest one can get to isset 3462 without using ax-ext 2728. See also vexw 2740. Note that the only disjoint variable condition is between 𝑦 and 𝐴. From there, one can prove isset 3462 using eleq2i 2848 (which requires ax-ext 2728 and df-cleq 2748). (Contributed by BJ, 29-Apr-2019.) (Proof modification is discouraged.)
⊢ 𝜑    ⇒   ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ ∃𝑦 𝑦 = 𝐴)
Theorem	bj-issetiv 37310*	Version of bj-isseti 37311 with a disjoint variable condition on 𝑥, 𝑉. The hypothesis uses 𝑉 instead of V for extra generality. This is indeed more general than isseti 3466 as long as elex 3469 is not available (and the non-dependence of bj-issetiv 37310 on special properties of the universal class V is obvious). Prefer its use over bj-isseti 37311 when sufficient (in particular when 𝑉 is substituted for V). (Contributed by BJ, 14-Sep-2019.) (Proof modification is discouraged.)
⊢ 𝐴 ∈ 𝑉    ⇒   ⊢ ∃𝑥 𝑥 = 𝐴
Theorem	bj-isseti 37311*	Version of isseti 3466 with a class variable 𝑉 in the hypothesis instead of V for extra generality. This is indeed more general than isseti 3466 as long as elex 3469 is not available (and the non-dependence of bj-isseti 37311 on special properties of the universal class V is obvious). Use bj-issetiv 37310 instead when sufficient (in particular when 𝑉 is substituted for V). (Contributed by BJ, 13-Jun-2019.) (Proof modification is discouraged.)
⊢ 𝐴 ∈ 𝑉    ⇒   ⊢ ∃𝑥 𝑥 = 𝐴
Theorem	bj-ralvw 37312	A weak version of ralv 3474 not using ax-ext 2728 (nor df-cleq 2748, df-clel 2831, df-v 3450), and only core FOL axioms. See also bj-rexvw 37313. The analogues for reuv 3476 and rmov 3477 are not proved. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ 𝜓    ⇒   ⊢ (∀𝑥 ∈ {𝑦 ∣ 𝜓}𝜑 ↔ ∀𝑥𝜑)
Theorem	bj-rexvw 37313	A weak version of rexv 3475 not using ax-ext 2728 (nor df-cleq 2748, df-clel 2831, df-v 3450), and only core FOL axioms. See also bj-ralvw 37312. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ 𝜓    ⇒   ⊢ (∃𝑥 ∈ {𝑦 ∣ 𝜓}𝜑 ↔ ∃𝑥𝜑)
Theorem	bj-rababw 37314	A weak version of rabab 3478 not using df-clel 2831 nor df-v 3450 (but requiring ax-ext 2728) nor ax-12 2206. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ 𝜓    ⇒   ⊢ {𝑥 ∈ {𝑦 ∣ 𝜓} ∣ 𝜑} = {𝑥 ∣ 𝜑}
Theorem	bj-rexcom4bv 37315*	Version of rexcom4b 3479 and bj-rexcom4b 37316 with a disjoint variable condition on 𝑥, 𝑉, hence removing dependency on df-sb 2085 and df-clab 2735 (so that it depends on df-clel 2831 and df-rex 3081 only on top of first-order logic). Prefer its use over bj-rexcom4b 37316 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 37316*	Remove from rexcom4b 3479 dependency on ax-ext 2728 and ax-13 2397 (and on df-or 857, df-cleq 2748, df-nfc 2905, df-v 3450). The hypothesis uses 𝑉 instead of V (see bj-isseti 37311 for the motivation). Use bj-rexcom4bv 37315 instead when sufficient (in particular when 𝑉 is substituted for V). (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ 𝐵 ∈ 𝑉    ⇒   ⊢ (∃𝑥∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵) ↔ ∃𝑦 ∈ 𝐴 𝜑)
Theorem	bj-ceqsalt0 37317	The FOL content of ceqsalt 3481. Lemma for bj-ceqsalt 37319 and bj-ceqsaltv 37320. (Contributed by BJ, 26-Sep-2019.) (Proof modification is discouraged.)
⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝜃 → (𝜑 ↔ 𝜓)) ∧ ∃𝑥𝜃) → (∀𝑥(𝜃 → 𝜑) ↔ 𝜓))
Theorem	bj-ceqsalt1 37318	The FOL content of ceqsalt 3481. Lemma for bj-ceqsalt 37319 and bj-ceqsaltv 37320. TODO: consider removing if it does not add anything to bj-ceqsalt0 37317. (Contributed by BJ, 26-Sep-2019.) (Proof modification is discouraged.)
⊢ (𝜃 → ∃𝑥𝜒)    ⇒   ⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝜒 → (𝜑 ↔ 𝜓)) ∧ 𝜃) → (∀𝑥(𝜒 → 𝜑) ↔ 𝜓))
Theorem	bj-ceqsalt 37319*	Remove from ceqsalt 3481 dependency on ax-ext 2728 (and on df-cleq 2748 and df-v 3450). Note: this is not doable with ceqsralt 3482 (or ceqsralv 3488), which uses eleq1 2844, but the same dependence removal is possible for ceqsalg 3483, ceqsal 3485, ceqsalv 3487, cgsexg 3492, cgsex2g 3493, cgsex4g 3494, ceqsex 3495, ceqsexv 3496, ceqsex2 3498, ceqsex2v 3499, ceqsex3v 3500, ceqsex4v 3501, ceqsex6v 3502, ceqsex8v 3503, gencbvex 3504 (after changing 𝐴 = 𝑦 to 𝑦 = 𝐴), gencbvex2 3505, gencbval 3506, vtoclgft 3514 (it uses Ⅎ, whose justification nfcjust 2904 does not use ax-ext 2728) and several other vtocl* theorems (see for instance bj-vtoclg1f 37351). See also bj-ceqsaltv 37320. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝑉) → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
Theorem	bj-ceqsaltv 37320*	Version of bj-ceqsalt 37319 with a disjoint variable condition on 𝑥, 𝑉, removing dependency on df-sb 2085 and df-clab 2735. Prefer its use over bj-ceqsalt 37319 when sufficient (in particular when 𝑉 is substituted for V). (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝑉) → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
Theorem	bj-ceqsalg0 37321	The FOL content of ceqsalg 3483. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝜒 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥𝜒 → (∀𝑥(𝜒 → 𝜑) ↔ 𝜓))
Theorem	bj-ceqsalg 37322*	Remove from ceqsalg 3483 dependency on ax-ext 2728 (and on df-cleq 2748 and df-v 3450). See also bj-ceqsalgv 37324. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
Theorem	bj-ceqsalgALT 37323*	Alternate proof of bj-ceqsalg 37322. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
Theorem	bj-ceqsalgv 37324*	Version of bj-ceqsalg 37322 with a disjoint variable condition on 𝑥, 𝑉, removing dependency on df-sb 2085 and df-clab 2735. Prefer its use over bj-ceqsalg 37322 when sufficient (in particular when 𝑉 is substituted for V). (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
Theorem	bj-ceqsalgvALT 37325*	Alternate proof of bj-ceqsalgv 37324. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
Theorem	bj-ceqsal 37326*	Remove from ceqsal 3485 dependency on ax-ext 2728 (and on df-cleq 2748, df-v 3450, df-clab 2735, df-sb 2085). (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ 𝐴 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓)
Theorem	bj-ceqsalv 37327*	Remove from ceqsalv 3487 dependency on ax-ext 2728 (and on df-cleq 2748, df-v 3450, df-clab 2735, df-sb 2085). (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.)
⊢ 𝐴 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓)
Theorem	bj-spcimdv 37328*	Remove from spcimdv 3547 dependency on ax-9 2146, ax-10 2169, ax-11 2185, ax-13 2397, ax-ext 2728, df-cleq 2748 (and df-nfc 2905, df-v 3450, df-or 857, df-tru 1557, df-nf 1798). For an even more economical version, see bj-spcimdvv 37329. (Contributed by BJ, 30-Nov-2020.) (Proof modification is discouraged.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 → 𝜒))
Theorem	bj-spcimdvv 37329*	Remove from spcimdv 3547 dependency on ax-7 2022, ax-8 2138, ax-10 2169, ax-11 2185, ax-12 2206 ax-13 2397, ax-ext 2728, df-cleq 2748, df-clab 2735 (and df-nfc 2905, df-v 3450, df-or 857, df-tru 1557, df-nf 1798) 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 37328. (Contributed by BJ, 3-Nov-2021.) (Proof modification is discouraged.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 → 𝜒))
21.19.5.3  Characterization among sets versus among classes
Theorem	elelb 37330	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 37331	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 37332	The nonfreeness quantifier for classes defines a symmetric binary relation on var metavariables (irreflexivity is proved by nfnid 5326 with additional axioms; see also nfcv 2918). This could be proved from aecom 2452 and nfcvb 5327 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 2762 instead of equcomd 2033; removing dependency on ax-ext 2728 is possible: prove weak versions (i.e. replace classes with setvars) of drnfc1 2937, eleq2d 2842 (using elequ2 2151), nfcvf 2944, dvelimc 2943, dvelimdc 2942, nfcvf2 2945. (Proof modification is discouraged.)
⊢ (Ⅎ𝑥𝑦 ↔ Ⅎ𝑦𝑥)
21.19.5.5  Lemmas for class substitution Some useful theorems for dealing with substitutions: sbbi 2335, sbcbig 3790, sbcel1g 4364, sbcel2 4366, sbcel12 4359, sbceqg 4360, csbvarg 4382.
Theorem	bj-sbeqALT 37333*	Substitution in an equality (use the more general version bj-sbeq 37334 instead, without disjoint variable condition). (Contributed by BJ, 6-Oct-2018.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ ([𝑦 / 𝑥]𝐴 = 𝐵 ↔ ⦋𝑦 / 𝑥⦌𝐴 = ⦋𝑦 / 𝑥⦌𝐵)
Theorem	bj-sbeq 37334	Distribute proper substitution through an equality relation. (See sbceqg 4360). (Contributed by BJ, 6-Oct-2018.)
⊢ ([𝑦 / 𝑥]𝐴 = 𝐵 ↔ ⦋𝑦 / 𝑥⦌𝐴 = ⦋𝑦 / 𝑥⦌𝐵)
Theorem	bj-sbceqgALT 37335	Distribute proper substitution through an equality relation. Alternate proof of sbceqg 4360. (Contributed by BJ, 6-Oct-2018.) Proof modification is discouraged to avoid using sbceqg 4360, but the Metamath program "MM-PA> MINIMIZE_WITH * / EXCEPT sbceqg" command is ok. (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵 = 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶))
Theorem	bj-csbsnlem 37336*	Lemma for bj-csbsn 37337 (in this lemma, 𝑥 cannot occur in 𝐴). (Contributed by BJ, 6-Oct-2018.) (New usage is discouraged.)
⊢ ⦋𝐴 / 𝑥⦌{𝑥} = {𝐴}
Theorem	bj-csbsn 37337	Substitution in a singleton. (Contributed by BJ, 6-Oct-2018.)
⊢ ⦋𝐴 / 𝑥⦌{𝑥} = {𝐴}
Theorem	bj-sbel1 37338*	Version of sbcel1g 4364 when substituting a set. (Note: one could have a corresponding version of sbcel12 4359 when substituting a set, but the point here is that the antecedent of sbcel1g 4364 is not needed when substituting a set.) (Contributed by BJ, 6-Oct-2018.)
⊢ ([𝑦 / 𝑥]𝐴 ∈ 𝐵 ↔ ⦋𝑦 / 𝑥⦌𝐴 ∈ 𝐵)
Theorem	bj-abv 37339	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 37340	Alternate version of bj-abv 37339; shorter but uses ax-8 2138. (Contributed by BJ, 24-Jul-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥𝜑 → {𝑥 ∣ 𝜑} = V)
Theorem	bj-ab0 37341	The class of sets verifying a falsity is the empty set (closed form of abf 4354). (Contributed by BJ, 24-Jul-2019.) (Proof modification is discouraged.)
⊢ (∀𝑥 ¬ 𝜑 → {𝑥 ∣ 𝜑} = ∅)
Theorem	bj-abf 37342	Shorter proof of abf 4354 (which should be kept as abfALT). (Contributed by BJ, 24-Jul-2019.) (Proof modification is discouraged.)
⊢ ¬ 𝜑    ⇒   ⊢ {𝑥 ∣ 𝜑} = ∅
Theorem	bj-csbprc 37343	More direct proof of csbprc 4357 (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 37344*	A Fol lemma (exlimiv 1944 followed by mpi 20). (Contributed by BJ, 2-Jul-2022.) (Proof modification is discouraged.)
⊢ (𝜒 → (𝜑 → 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ (∃𝑥𝜒 → 𝜓)
Theorem	bj-exlimmpi 37345	Lemma for bj-vtoclg1f1 37350 (an instance of this lemma is a version of bj-vtoclg1f1 37350 where 𝑥 and 𝑦 are identified). (Contributed by BJ, 30-Apr-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝜒 → (𝜑 → 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ (∃𝑥𝜒 → 𝜓)
Theorem	bj-exlimmpbi 37346	Lemma for theorems of the vtoclg 3516 family. (Contributed by BJ, 3-Oct-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝜒 → (𝜑 ↔ 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ (∃𝑥𝜒 → 𝜓)
Theorem	bj-exlimmpbir 37347	Lemma for theorems of the vtoclg 3516 family. (Contributed by BJ, 3-Oct-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜒 → (𝜑 ↔ 𝜓))    &   ⊢ 𝜓    ⇒   ⊢ (∃𝑥𝜒 → 𝜑)
Theorem	bj-vtoclf 37348*	Remove dependency on ax-ext 2728, df-clab 2735 and df-cleq 2748 (and df-sb 2085 and df-v 3450) from vtoclf 3525. (Contributed by BJ, 6-Oct-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ 𝐴 ∈ 𝑉    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ 𝜓
Theorem	bj-vtocl 37349*	Remove dependency on ax-ext 2728, df-clab 2735 and df-cleq 2748 (and df-sb 2085 and df-v 3450) from vtocl 3519. (Contributed by BJ, 6-Oct-2019.) (Proof modification is discouraged.)
⊢ 𝐴 ∈ 𝑉    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ 𝜓
Theorem	bj-vtoclg1f1 37350*	The FOL content of vtoclg1f 3530 (hence not using ax-ext 2728, df-cleq 2748, df-nfc 2905, df-v 3450). 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 2728; as a byproduct, this dispenses with ax-11 2185 and ax-13 2397). (Contributed by BJ, 30-Apr-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 → 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ (∃𝑦 𝑦 = 𝐴 → 𝜓)
Theorem	bj-vtoclg1f 37351*	Reprove vtoclg1f 3530 from bj-vtoclg1f1 37350. This removes dependency on ax-ext 2728, df-cleq 2748 and df-v 3450. Use bj-vtoclg1fv 37352 instead when sufficient (in particular when 𝑉 is substituted for V). (Contributed by BJ, 14-Sep-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 → 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝜓)
Theorem	bj-vtoclg1fv 37352*	Version of bj-vtoclg1f 37351 with a disjoint variable condition on 𝑥, 𝑉. This removes dependency on df-sb 2085 and df-clab 2735. Prefer its use over bj-vtoclg1f 37351 when sufficient (in particular when 𝑉 is substituted for V). (Contributed by BJ, 14-Sep-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 → 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝜓)
Theorem	bj-vtoclg 37353*	A version of vtoclg 3516 with an additional disjoint variable condition (which is removable if we allow use of df-clab 2735, see bj-vtoclg1f 37351), which requires fewer axioms (i.e., removes dependency on ax-6 1981, ax-7 2022, ax-9 2146, ax-12 2206, ax-ext 2728, df-clab 2735, df-cleq 2748, df-v 3450). (Contributed by BJ, 2-Jul-2022.) (Proof modification is discouraged.)
⊢ (𝑥 = 𝐴 → (𝜑 → 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝜓)
Theorem	bj-rabeqbid 37354	Version of rabeqbidv 3426 with two disjoint variable conditions removed and the third replaced by a nonfreeness hypothesis. (Contributed by BJ, 27-Apr-2019.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒})
Theorem	bj-seex 37355*	Version of seex 5599 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 37356*	Version of df-nfc 2905 with a disjoint variable condition replaced with a nonfreeness hypothesis. (Contributed by BJ, 2-May-2019.)
⊢ Ⅎ𝑦𝐴    ⇒   ⊢ (Ⅎ𝑥𝐴 ↔ ∀𝑦Ⅎ𝑥 𝑦 ∈ 𝐴)
Theorem	bj-zfauscl 37357*	General version of zfauscl 5242. Remark: the comment in zfauscl 5242 is misleading: the essential use of ax-ext 2728 is the one via eleq2 2845 and not the one via vtocl 3519, since the latter can be proved without ax-ext 2728 (see bj-vtoclg 37353). (Contributed by BJ, 2-Jul-2022.) (Proof modification is discouraged.)
⊢ (𝐴 ∈ 𝑉 → ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝜑)))
21.19.5.7  Class abstractions A few additional theorems on class abstractions and restricted class abstractions.
Theorem	bj-elabd2ALT 37358*	Alternate proof of elabd2 3624 bypassing elab6g 3623 (and using sbiedvw 2123 instead of the ∀𝑥(𝑥 = 𝑦 → 𝜓) idiom). (Contributed by BJ, 16-Oct-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 = {𝑥 ∣ 𝜓})    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (𝐴 ∈ 𝐵 ↔ 𝜒))
Theorem	bj-unrab 37359*	Generalization of unrab 4262. Equality need not hold. (Contributed by BJ, 21-Apr-2019.)
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∪ {𝑥 ∈ 𝐵 ∣ 𝜓}) ⊆ {𝑥 ∈ (𝐴 ∪ 𝐵) ∣ (𝜑 ∨ 𝜓)}
Theorem	bj-inrab 37360	Generalization of inrab 4263. (Contributed by BJ, 21-Apr-2019.)
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ {𝑥 ∈ 𝐵 ∣ 𝜓}) = {𝑥 ∈ (𝐴 ∩ 𝐵) ∣ (𝜑 ∧ 𝜓)}
Theorem	bj-inrab2 37361	Shorter proof of inrab 4263. (Contributed by BJ, 21-Apr-2019.) (Proof modification is discouraged.)
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ {𝑥 ∈ 𝐴 ∣ 𝜓}) = {𝑥 ∈ 𝐴 ∣ (𝜑 ∧ 𝜓)}
Theorem	bj-inrab3 37362*	Generalization of dfrab3ss 4270. Shortens dfrab3ss 4270. (Contributed by BJ, 21-Apr-2019.) (Revised by OpenAI, 7-Jul-2020.)
⊢ (𝐴 ∩ {𝑥 ∈ 𝐵 ∣ 𝜑}) = ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ 𝐵)
Theorem	bj-rabtr 37363*	Restricted class abstraction with true formula. (Contributed by BJ, 22-Apr-2019.)
⊢ {𝑥 ∈ 𝐴 ∣ ⊤} = 𝐴
Theorem	bj-rabtrALT 37364*	Alternate proof of bj-rabtr 37363. (Contributed by BJ, 22-Apr-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ {𝑥 ∈ 𝐴 ∣ ⊤} = 𝐴
Theorem	bj-rabtrAUTO 37365*	Proof of bj-rabtr 37363 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 37366	Syntax for generalized class abstractions.
class {𝐴 ∣ 𝑥 ∣ 𝜑}
Definition	df-bj-gab 37367*	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 37368	Inclusion of generalized class abstractions. (Contributed by BJ, 4-Oct-2024.)
⊢ (∀𝑥(𝐴 = 𝐵 ∧ (𝜑 → 𝜓)) → {𝐴 ∣ 𝑥 ∣ 𝜑} ⊆ {𝐵 ∣ 𝑥 ∣ 𝜓})
Theorem	bj-gabssd 37369	Inclusion of generalized class abstractions. Deduction form. (Contributed by BJ, 4-Oct-2024.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → {𝐴 ∣ 𝑥 ∣ 𝜓} ⊆ {𝐵 ∣ 𝑥 ∣ 𝜒})
Theorem	bj-gabeqd 37370	Equality of generalized class abstractions. Deduction form. (Contributed by BJ, 4-Oct-2024.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {𝐴 ∣ 𝑥 ∣ 𝜓} = {𝐵 ∣ 𝑥 ∣ 𝜒})
Theorem	bj-gabeqis 37371*	Equality of generalized class abstractions, with implicit substitution. (Contributed by BJ, 4-Oct-2024.)
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ {𝐴 ∣ 𝑥 ∣ 𝜑} = {𝐵 ∣ 𝑦 ∣ 𝜓}
Theorem	bj-elgab 37372	Elements of a generalized class abstraction. (Contributed by BJ, 4-Oct-2024.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → Ⅎ𝑥𝐴)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → (∃𝑥(𝐴 = 𝐵 ∧ 𝜓) ↔ 𝜒))    ⇒   ⊢ (𝜑 → (𝐴 ∈ {𝐵 ∣ 𝑥 ∣ 𝜓} ↔ 𝜒))
Theorem	bj-gabima 37373	Generalized class abstraction as a direct image. TODO: improve the support lemmas elimag 6043 and fvelima 6921 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 37374	Syntax for restricted nonfreeness.
wff Ⅎ𝑥 ∈ 𝐴𝜑
Definition	df-bj-rnf 37375	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 2155) and then two versions (bj-ru1 37376 and bj-ru 37377). Special attention is put on minimizing axiom depencencies.
Theorem	bj-ru1 37376*	A version of Russell's paradox ru 3737 not mentioning the universal class. (see also bj-ru 37377). (Contributed by BJ, 12-Oct-2019.) Remove usage of ax-10 2169, ax-11 2185, ax-12 2206 by using eqabbw 2829 following BTernaryTau's similar revision of ru 3737. (Revised by BJ, 28-Jun-2025.) (Proof modification is discouraged.)
⊢ ¬ ∃𝑦 𝑦 = {𝑥 ∣ ¬ 𝑥 ∈ 𝑥}
Theorem	bj-ru 37377	Remove dependency on ax-13 2397 (and df-v 3450) from Russell's paradox ru 3737 expressed with primitive symbols and with a class variable 𝑉. Note the more economical use of elissetv 2837 instead of isset 3462 to avoid use of df-v 3450. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.)
⊢ ¬ {𝑥 ∣ ¬ 𝑥 ∈ 𝑥} ∈ 𝑉
21.19.5.11  Curry's paradox in set theory
Theorem	currysetlem 37378*	Lemma for currysetlem 37378, where it is used with (𝑥 ∈ 𝑥 → 𝜑) substituted for 𝜓. (Contributed by BJ, 23-Sep-2023.) This proof is intuitionistically valid. (Proof modification is discouraged.)
⊢ ({𝑥 ∣ 𝜓} ∈ 𝑉 → ({𝑥 ∣ 𝜓} ∈ {𝑥 ∣ (𝑥 ∈ 𝑥 → 𝜑)} ↔ ({𝑥 ∣ 𝜓} ∈ {𝑥 ∣ 𝜓} → 𝜑)))
Theorem	curryset 37379*	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 37383. (Contributed by BJ, 23-Sep-2023.) This proof is intuitionistically valid. (Proof modification is discouraged.)
⊢ ¬ {𝑥 ∣ (𝑥 ∈ 𝑥 → 𝜑)} ∈ 𝑉
Theorem	currysetlem1 37380*	Lemma for currysetALT 37383. (Contributed by BJ, 23-Sep-2023.) This proof is intuitionistically valid. (Proof modification is discouraged.)
⊢ 𝑋 = {𝑥 ∣ (𝑥 ∈ 𝑥 → 𝜑)}    ⇒   ⊢ (𝑋 ∈ 𝑉 → (𝑋 ∈ 𝑋 ↔ (𝑋 ∈ 𝑋 → 𝜑)))
Theorem	currysetlem2 37381*	Lemma for currysetALT 37383. (Contributed by BJ, 23-Sep-2023.) This proof is intuitionistically valid. (Proof modification is discouraged.)
⊢ 𝑋 = {𝑥 ∣ (𝑥 ∈ 𝑥 → 𝜑)}    ⇒   ⊢ (𝑋 ∈ 𝑉 → (𝑋 ∈ 𝑋 → 𝜑))
Theorem	currysetlem3 37382*	Lemma for currysetALT 37383. (Contributed by BJ, 23-Sep-2023.) This proof is intuitionistically valid. (Proof modification is discouraged.)
⊢ 𝑋 = {𝑥 ∣ (𝑥 ∈ 𝑥 → 𝜑)}    ⇒   ⊢ ¬ 𝑋 ∈ 𝑉
Theorem	currysetALT 37383*	Alternate proof of curryset 37379, 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.19.5.12  Some disjointness results A few utility theorems on disjointness of classes.
Theorem	bj-n0i 37384*	Inference associated with n0 4300. Shortens 2ndcdisj 23489 (2888>2878), notzfaus 5314 (264>253). (Contributed by BJ, 22-Apr-2019.)
⊢ 𝐴 ≠ ∅    ⇒   ⊢ ∃𝑥 𝑥 ∈ 𝐴
Theorem	bj-disjsn01 37385	Disjointness of the singletons containing 0 and 1. This is a consequence of disjcsn 9548 but the present proof does not use regularity. (Contributed by BJ, 4-Apr-2019.) (Proof modification is discouraged.)
⊢ ({∅} ∩ {1o}) = ∅
Theorem	bj-0nel1 37386	The empty set does not belong to {1o}. (Contributed by BJ, 6-Apr-2019.)
⊢ ∅ ∉ {1o}
Theorem	bj-1nel0 37387	1o does not belong to {∅}. (Contributed by BJ, 6-Apr-2019.)
⊢ 1o ∉ {∅}
21.19.5.13  Complements on direct products A few utility theorems on direct products.
Theorem	bj-xpimasn 37388	The image of a singleton, general case. [Change and relabel xpimasn 6160 accordingly, maybe to xpima2sn.] (Contributed by BJ, 6-Apr-2019.)
⊢ ((𝐴 × 𝐵) “ {𝑋}) = if(𝑋 ∈ 𝐴, 𝐵, ∅)
Theorem	bj-xpima1sn 37389	The image of a singleton by a direct product, empty case. [Change and relabel xpimasn 6160 accordingly, maybe to xpima2sn.] (Contributed by BJ, 6-Apr-2019.)
⊢ (¬ 𝑋 ∈ 𝐴 → ((𝐴 × 𝐵) “ {𝑋}) = ∅)
Theorem	bj-xpima1snALT 37390	Alternate proof of bj-xpima1sn 37389. (Contributed by BJ, 6-Apr-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ 𝑋 ∈ 𝐴 → ((𝐴 × 𝐵) “ {𝑋}) = ∅)
Theorem	bj-xpima2sn 37391	The image of a singleton by a direct product, nonempty case. [To replace xpimasn 6160.] (Contributed by BJ, 6-Apr-2019.) (Proof modification is discouraged.)
⊢ (𝑋 ∈ 𝐴 → ((𝐴 × 𝐵) “ {𝑋}) = 𝐵)
Theorem	bj-xpnzex 37392	If the first factor of a product is nonempty, and the product is a set, then the second factor is a set. UPDATE: this is actually the curried (exported) form of xpexcnv 7890 (up to commutation in the product). (Contributed by BJ, 6-Oct-2018.) (Proof modification is discouraged.)
⊢ (𝐴 ≠ ∅ → ((𝐴 × 𝐵) ∈ 𝑉 → 𝐵 ∈ V))
Theorem	bj-xpexg2 37393	Curried (exported) form of xpexg 7722. (Contributed by BJ, 2-Apr-2019.)
⊢ (𝐴 ∈ 𝑉 → (𝐵 ∈ 𝑊 → (𝐴 × 𝐵) ∈ V))
Theorem	bj-xpnzexb 37394	If the first factor of a product is a nonempty set, then the product is a set if and only if the second factor is a set. (Contributed by BJ, 2-Apr-2019.)
⊢ (𝐴 ∈ (𝑉 ∖ {∅}) → (𝐵 ∈ V ↔ (𝐴 × 𝐵) ∈ V))
Theorem	bj-cleq 37395*	Substitution property for certain classes. (Contributed by BJ, 2-Apr-2019.)
⊢ (𝐴 = 𝐵 → {𝑥 ∣ {𝑥} ∈ (𝐴 “ 𝐶)} = {𝑥 ∣ {𝑥} ∈ (𝐵 “ 𝐶)})
21.19.5.14  "Singletonization" and tagging This subsection introduces the "singletonization" and the "tagging" of a class. The singletonization of a class is the class of singletons of elements of that class. It is useful since all nonsingletons are disjoint from it, so one can easily adjoin to it disjoint elements, which is what the tagging does: it adjoins the empty set. This can be used for instance to define the one-point compactification of a topological space. It will be used in the next section to define tuples which work for proper classes.
Theorem	bj-snsetex 37396*	The class of sets "whose singletons" belong to a set is a set. Nice application of ax-rep 5221. (Contributed by BJ, 6-Oct-2018.)
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V)
Theorem	bj-clexab 37397*	Sethood of certain classes. (Contributed by BJ, 2-Apr-2019.)
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∣ {𝑥} ∈ (𝐴 “ 𝐵)} ∈ V)
Syntax	bj-csngl 37398	Syntax for singletonization. (Contributed by BJ, 6-Oct-2018.)
class sngl 𝐴
Definition	df-bj-sngl 37399*	Definition of "singletonization". The class sngl 𝐴 is isomorphic to 𝐴 and since it contains only singletons, it can be easily be adjoined disjoint elements, which can be useful in various constructions. (Contributed by BJ, 6-Oct-2018.)
⊢ sngl 𝐴 = {𝑥 ∣ ∃𝑦 ∈ 𝐴 𝑥 = {𝑦}}
Theorem	bj-sngleq 37400	Substitution property for sngl. (Contributed by BJ, 6-Oct-2018.)
⊢ (𝐴 = 𝐵 → sngl 𝐴 = sngl 𝐵)