P. 344 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 34301-34400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	eliminable3a 34301*	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 34302*	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 34303	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 34304*	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 34305*	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 34306*	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 34307*	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 34308*	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.)
⊢ ({𝑥 ∣ 𝜑} ∈ {𝑦 ∣ 𝜓} ↔ ∃𝑧(∀𝑡(𝑡 ∈ 𝑧 ↔ [𝑡 / 𝑥]𝜑) ∧ [𝑧 / 𝑦]𝜓))
20.15.5.2  Classes without the axiom of extensionality A few results about classes can be proved without using ax-ext 2770. One could move all theorems from cab 2776 to df-clel 2870 (except for dfcleq 2792 and cvjust 2793) 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 2791. Note that without ax-ext 2770, the $a-statements df-clab 2777, df-cleq 2791, and df-clel 2870 are no longer eliminable (see previous section) (but PROBABLY df-clab 2777 is still conservative , while df-cleq 2791 and df-clel 2870 are not). This is not a reason not to study what is provable with them but without ax-ext 2770, 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 2111, wel 2112, ax-8 2113, ax-9 2121). Remark: the weakening of eleq1 2877 / eleq2 2878 to eleq1w 2872 / eleq2w 2873 can also be done with eleq1i 2880, eqeltri 2886, eqeltrri 2887, eleq1a 2885, eleq1d 2874, eqeltrd 2890, eqeltrrd 2891, eqneltrd 2909, eqneltrrd 2910, nelneq 2914. Remark: possibility to remove dependency on ax-10 2142, ax-11 2158, ax-13 2379 from nfcri 2943 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 2967.
Theorem	bj-denoteslem 34309*	Lemma for bj-denotes 34310. (Contributed by BJ, 24-Apr-2024.)
⊢ (∃𝑥 𝑥 = 𝐴 ↔ 𝐴 ∈ {𝑦 ∣ ⊤})
Theorem	bj-denotes 34310*	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 2044, and eqeq1 2802, requires the core axioms and { ax-9 2121, ax-ext 2770, df-cleq 2791 } whereas this proof requires the core axioms and { ax-8 2113, df-clab 2777, df-clel 2870 }. Theorem bj-issetwt 34313 proves that "existing" is equivalent to being a member of a class abstraction. It also requires, with the present proof, { ax-8 2113, df-clab 2777, df-clel 2870 } (whereas with the shorter proof from cbvexvw 2044 and eqeq1 2802 it would require { ax-8 2113, ax-9 2121, ax-ext 2770, df-clab 2777, df-cleq 2791, df-clel 2870 }). That every class is equal to a class abstraction is proved by abid1 2931, which requires { ax-8 2113, ax-9 2121, ax-ext 2770, df-clab 2777, df-cleq 2791, df-clel 2870 }. Note that there is no disjoint variable condition on 𝑥, 𝑦 but the theorem does not depend on ax-13 2379. Actually, the proof depends only on the logical axioms ax-1 6 through ax-7 2015 and sp 2180. 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 2770 and df-cleq 2791 (e.g., eqid 2798 and eqeq1 2802). In particular, one cannot even prove ⊢ ∃𝑥𝑥 = 𝐴 ⇒ ⊢ 𝐴 = 𝐴 without ax-ext 2770 and df-cleq 2791. (Contributed by BJ, 29-Apr-2019.) (Proof modification is discouraged.)
⊢ (∃𝑥 𝑥 = 𝐴 ↔ ∃𝑦 𝑦 = 𝐴)
Theorem	bj-issettru 34311*	Weak version of isset 3453 without ax-ext 2770. (Contributed by BJ, 24-Apr-2024.)
⊢ (∃𝑥 𝑥 = 𝐴 ↔ 𝐴 ∈ {𝑦 ∣ ⊤})
Theorem	bj-elabtru 34312	This is as close as we can get to proving extensionality for "the" "universal" class without ax-ext 2770. (Contributed by BJ, 24-Apr-2024.)
⊢ (𝐴 ∈ {𝑥 ∣ ⊤} ↔ 𝐴 ∈ {𝑦 ∣ ⊤})
Theorem	bj-issetwt 34313*	Closed form of bj-issetw 34314. (Contributed by BJ, 29-Apr-2019.) (Proof modification is discouraged.)
⊢ (∀𝑥𝜑 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ ∃𝑦 𝑦 = 𝐴))
Theorem	bj-issetw 34314*	The closest one can get to isset 3453 without using ax-ext 2770. See also vexw 2782. Note that the only disjoint variable condition is between 𝑦 and 𝐴. From there, one can prove isset 3453 using eleq2i 2881 (which requires ax-ext 2770 and df-cleq 2791). (Contributed by BJ, 29-Apr-2019.) (Proof modification is discouraged.)
⊢ 𝜑    ⇒   ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ ∃𝑦 𝑦 = 𝐴)
Theorem	bj-elissetv 34315*	Version of bj-elisset 34316 with a disjoint variable condition on 𝑥, 𝑉. This proof uses only df-ex 1782, ax-gen 1797, ax-4 1811 and df-clel 2870 on top of propositional calculus. Prefer its use over bj-elisset 34316 when sufficient. (Contributed by BJ, 14-Sep-2019.) (Proof modification is discouraged.)
⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴)
Theorem	bj-elisset 34316*	Remove from elisset 3452 dependency on ax-ext 2770 (and on df-cleq 2791 and df-v 3443). This proof uses only df-clab 2777 and df-clel 2870 on top of first-order logic. It only requires ax-1--7 and sp 2180. Use bj-elissetv 34315 instead when sufficient (in particular when 𝑉 is substituted for V). (Contributed by BJ, 29-Apr-2019.) (Proof modification is discouraged.)
⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴)
Theorem	bj-issetiv 34317*	Version of bj-isseti 34318 with a disjoint variable condition on 𝑥, 𝑉. This proof uses only df-ex 1782, ax-gen 1797, ax-4 1811 and df-clel 2870 on top of propositional calculus. Prefer its use over bj-isseti 34318 when sufficient (in particular when 𝑉 is substituted for V). (Contributed by BJ, 14-Sep-2019.) (Proof modification is discouraged.)
⊢ 𝐴 ∈ 𝑉    ⇒   ⊢ ∃𝑥 𝑥 = 𝐴
Theorem	bj-isseti 34318*	Remove from isseti 3455 dependency on ax-ext 2770 (and on df-cleq 2791 and df-v 3443). This proof uses only df-clab 2777 and df-clel 2870 on top of first-order logic. It only uses ax-12 2175 among the auxiliary logical axioms. The hypothesis uses 𝑉 instead of V for extra generality. This is indeed more general as long as elex 3459 is not available. Use bj-issetiv 34317 instead when sufficient (in particular when 𝑉 is substituted for V). (Contributed by BJ, 13-Jun-2019.) (Proof modification is discouraged.)
⊢ 𝐴 ∈ 𝑉    ⇒   ⊢ ∃𝑥 𝑥 = 𝐴
Theorem	bj-ralvw 34319	A weak version of ralv 3466 not using ax-ext 2770 (nor df-cleq 2791, df-clel 2870, df-v 3443), and only core FOL axioms. See also bj-rexvw 34320. The analogues for reuv 3468 and rmov 3469 are not proved. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ 𝜓    ⇒   ⊢ (∀𝑥 ∈ {𝑦 ∣ 𝜓}𝜑 ↔ ∀𝑥𝜑)
Theorem	bj-rexvw 34320	A weak version of rexv 3467 not using ax-ext 2770 (nor df-cleq 2791, df-clel 2870, df-v 3443), and only core FOL axioms. See also bj-ralvw 34319. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ 𝜓    ⇒   ⊢ (∃𝑥 ∈ {𝑦 ∣ 𝜓}𝜑 ↔ ∃𝑥𝜑)
Theorem	bj-rababw 34321	A weak version of rabab 3470 not using df-clel 2870 nor df-v 3443 (but requiring ax-ext 2770) nor ax-12 2175. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ 𝜓    ⇒   ⊢ {𝑥 ∈ {𝑦 ∣ 𝜓} ∣ 𝜑} = {𝑥 ∣ 𝜑}
Theorem	bj-rexcom4bv 34322*	Version of rexcom4b 3471 and bj-rexcom4b 34323 with a disjoint variable condition on 𝑥, 𝑉, hence removing dependency on df-sb 2070 and df-clab 2777 (so that it depends on df-clel 2870 and df-rex 3112 only on top of first-order logic). Prefer its use over bj-rexcom4b 34323 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 34323*	Remove from rexcom4b 3471 dependency on ax-ext 2770 and ax-13 2379 (and on df-or 845, df-cleq 2791, df-nfc 2938, df-v 3443). The hypothesis uses 𝑉 instead of V (see bj-isseti 34318 for the motivation). Use bj-rexcom4bv 34322 instead when sufficient (in particular when 𝑉 is substituted for V). (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ 𝐵 ∈ 𝑉    ⇒   ⊢ (∃𝑥∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵) ↔ ∃𝑦 ∈ 𝐴 𝜑)
Theorem	bj-ceqsalt0 34324	The FOL content of ceqsalt 3474. Lemma for bj-ceqsalt 34326 and bj-ceqsaltv 34327. (Contributed by BJ, 26-Sep-2019.) (Proof modification is discouraged.)
⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝜃 → (𝜑 ↔ 𝜓)) ∧ ∃𝑥𝜃) → (∀𝑥(𝜃 → 𝜑) ↔ 𝜓))
Theorem	bj-ceqsalt1 34325	The FOL content of ceqsalt 3474. Lemma for bj-ceqsalt 34326 and bj-ceqsaltv 34327. TODO: consider removing if it does not add anything to bj-ceqsalt0 34324. (Contributed by BJ, 26-Sep-2019.) (Proof modification is discouraged.)
⊢ (𝜃 → ∃𝑥𝜒)    ⇒   ⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝜒 → (𝜑 ↔ 𝜓)) ∧ 𝜃) → (∀𝑥(𝜒 → 𝜑) ↔ 𝜓))
Theorem	bj-ceqsalt 34326*	Remove from ceqsalt 3474 dependency on ax-ext 2770 (and on df-cleq 2791 and df-v 3443). Note: this is not doable with ceqsralt 3475 (or ceqsralv 3480), which uses eleq1 2877, but the same dependence removal is possible for ceqsalg 3476, ceqsal 3478, ceqsalv 3479, cgsexg 3484, cgsex2g 3485, cgsex4g 3486, ceqsex 3488, ceqsexv 3489, ceqsex2 3491, ceqsex2v 3492, ceqsex3v 3493, ceqsex4v 3494, ceqsex6v 3495, ceqsex8v 3496, gencbvex 3497 (after changing 𝐴 = 𝑦 to 𝑦 = 𝐴), gencbvex2 3498, gencbval 3499, vtoclgft 3501 (it uses Ⅎ, whose justification nfcjust 2937 does not use ax-ext 2770) and several other vtocl* theorems (see for instance bj-vtoclg1f 34358). See also bj-ceqsaltv 34327. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝑉) → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
Theorem	bj-ceqsaltv 34327*	Version of bj-ceqsalt 34326 with a disjoint variable condition on 𝑥, 𝑉, removing dependency on df-sb 2070 and df-clab 2777. Prefer its use over bj-ceqsalt 34326 when sufficient (in particular when 𝑉 is substituted for V). (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝑉) → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
Theorem	bj-ceqsalg0 34328	The FOL content of ceqsalg 3476. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝜒 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥𝜒 → (∀𝑥(𝜒 → 𝜑) ↔ 𝜓))
Theorem	bj-ceqsalg 34329*	Remove from ceqsalg 3476 dependency on ax-ext 2770 (and on df-cleq 2791 and df-v 3443). See also bj-ceqsalgv 34331. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
Theorem	bj-ceqsalgALT 34330*	Alternate proof of bj-ceqsalg 34329. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
Theorem	bj-ceqsalgv 34331*	Version of bj-ceqsalg 34329 with a disjoint variable condition on 𝑥, 𝑉, removing dependency on df-sb 2070 and df-clab 2777. Prefer its use over bj-ceqsalg 34329 when sufficient (in particular when 𝑉 is substituted for V). (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
Theorem	bj-ceqsalgvALT 34332*	Alternate proof of bj-ceqsalgv 34331. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
Theorem	bj-ceqsal 34333*	Remove from ceqsal 3478 dependency on ax-ext 2770 (and on df-cleq 2791, df-v 3443, df-clab 2777, df-sb 2070). (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ 𝐴 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓)
Theorem	bj-ceqsalv 34334*	Remove from ceqsalv 3479 dependency on ax-ext 2770 (and on df-cleq 2791, df-v 3443, df-clab 2777, df-sb 2070). (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.)
⊢ 𝐴 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓)
Theorem	bj-spcimdv 34335*	Remove from spcimdv 3540 dependency on ax-9 2121, ax-10 2142, ax-11 2158, ax-13 2379, ax-ext 2770, df-cleq 2791 (and df-nfc 2938, df-v 3443, df-or 845, df-tru 1541, df-nf 1786). For an even more economical version, see bj-spcimdvv 34336. (Contributed by BJ, 30-Nov-2020.) (Proof modification is discouraged.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 → 𝜒))
Theorem	bj-spcimdvv 34336*	Remove from spcimdv 3540 dependency on ax-7 2015, ax-8 2113, ax-10 2142, ax-11 2158, ax-12 2175 ax-13 2379, ax-ext 2770, df-cleq 2791, df-clab 2777 (and df-nfc 2938, df-v 3443, df-or 845, df-tru 1541, 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 34335. (Contributed by BJ, 3-Nov-2021.) (Proof modification is discouraged.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 → 𝜒))
20.15.5.3  Characterization among sets versus among classes
Theorem	elelb 34337	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 34338	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 𝐴))
20.15.5.4  The nonfreeness quantifier for classes In this section, we prove the symmetry of the nonfreeness quantifier for classes.
Theorem	bj-nfcsym 34339	The nonfreeness quantifier for classes defines a symmetric binary relation on var metavariables (irreflexivity is proved by nfnid 5241 with additional axioms; see also nfcv 2955). This could be proved from aecom 2438 and nfcvb 5242 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 2804 instead of equcomd 2026; removing dependency on ax-ext 2770 is possible: prove weak versions (i.e. replace classes with setvars) of drnfc1 2974, eleq2d 2875 (using elequ2 2126), nfcvf 2981, dvelimc 2980, dvelimdc 2979, nfcvf2 2982. (Proof modification is discouraged.)
⊢ (Ⅎ𝑥𝑦 ↔ Ⅎ𝑦𝑥)
20.15.5.5  Proposal for the definitions of class membership and class equality Note: now that the proposals have been adopted as df-cleq 2791 and df-clel 2870, and that ax9ALT 2794 is in the main section, we only keep bj-ax9 34340 here as a weaker version of ax9ALT 2794 proved without ax-8 2113.
Theorem	bj-ax9 34340*	Proof of ax-9 2121 from Tarski's FOL=, sp 2180, dfcleq 2792 and ax-ext 2770 (with two extra disjoint variable conditions on 𝑥, 𝑧 and 𝑦, 𝑧). See ax9ALT 2794 for a more general version, proved using also ax-8 2113. (Contributed by BJ, 24-Jun-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦))
20.15.5.6  Lemmas for class substitution Some useful theorems for dealing with substitutions: sbbi 2313, sbcbig 3770, sbcel1g 4321, sbcel2 4323, sbcel12 4316, sbceqg 4317, csbvarg 4339.
Theorem	bj-sbeqALT 34341*	Substitution in an equality (use the more general version bj-sbeq 34342 instead, without disjoint variable condition). (Contributed by BJ, 6-Oct-2018.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ ([𝑦 / 𝑥]𝐴 = 𝐵 ↔ ⦋𝑦 / 𝑥⦌𝐴 = ⦋𝑦 / 𝑥⦌𝐵)
Theorem	bj-sbeq 34342	Distribute proper substitution through an equality relation. (See sbceqg 4317). (Contributed by BJ, 6-Oct-2018.)
⊢ ([𝑦 / 𝑥]𝐴 = 𝐵 ↔ ⦋𝑦 / 𝑥⦌𝐴 = ⦋𝑦 / 𝑥⦌𝐵)
Theorem	bj-sbceqgALT 34343	Distribute proper substitution through an equality relation. Alternate proof of sbceqg 4317. (Contributed by BJ, 6-Oct-2018.) Proof modification is discouraged to avoid using sbceqg 4317, but the Metamath program "MM-PA> MINIMIZE_WITH * / EXCEPT sbceqg" command is ok. (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵 = 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶))
Theorem	bj-csbsnlem 34344*	Lemma for bj-csbsn 34345 (in this lemma, 𝑥 cannot occur in 𝐴). (Contributed by BJ, 6-Oct-2018.) (New usage is discouraged.)
⊢ ⦋𝐴 / 𝑥⦌{𝑥} = {𝐴}
Theorem	bj-csbsn 34345	Substitution in a singleton. (Contributed by BJ, 6-Oct-2018.)
⊢ ⦋𝐴 / 𝑥⦌{𝑥} = {𝐴}
Theorem	bj-sbel1 34346*	Version of sbcel1g 4321 when substituting a set. (Note: one could have a corresponding version of sbcel12 4316 when substituting a set, but the point here is that the antecedent of sbcel1g 4321 is not needed when substituting a set.) (Contributed by BJ, 6-Oct-2018.)
⊢ ([𝑦 / 𝑥]𝐴 ∈ 𝐵 ↔ ⦋𝑦 / 𝑥⦌𝐴 ∈ 𝐵)
Theorem	bj-abv 34347	The class of sets verifying a tautology is the universal class. (Contributed by BJ, 24-Jul-2019.) (Proof modification is discouraged.)
⊢ (∀𝑥𝜑 → {𝑥 ∣ 𝜑} = V)
Theorem	bj-ab0 34348	The class of sets verifying a falsity is the empty set (closed form of abf 4310). (Contributed by BJ, 24-Jul-2019.) (Proof modification is discouraged.)
⊢ (∀𝑥 ¬ 𝜑 → {𝑥 ∣ 𝜑} = ∅)
Theorem	bj-abf 34349	Shorter proof of abf 4310 (which should be kept as abfALT). (Contributed by BJ, 24-Jul-2019.) (Proof modification is discouraged.)
⊢ ¬ 𝜑    ⇒   ⊢ {𝑥 ∣ 𝜑} = ∅
Theorem	bj-csbprc 34350	More direct proof of csbprc 4313 (fewer essential steps). (Contributed by BJ, 24-Jul-2019.) (Proof modification is discouraged.)
⊢ (¬ 𝐴 ∈ V → ⦋𝐴 / 𝑥⦌𝐵 = ∅)
20.15.5.7  Removing some axiom requirements and disjoint variable conditions
Theorem	bj-exlimvmpi 34351*	A Fol lemma (exlimiv 1931 followed by mpi 20). (Contributed by BJ, 2-Jul-2022.) (Proof modification is discouraged.)
⊢ (𝜒 → (𝜑 → 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ (∃𝑥𝜒 → 𝜓)
Theorem	bj-exlimmpi 34352	Lemma for bj-vtoclg1f1 34357 (an instance of this lemma is a version of bj-vtoclg1f1 34357 where 𝑥 and 𝑦 are identified). (Contributed by BJ, 30-Apr-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝜒 → (𝜑 → 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ (∃𝑥𝜒 → 𝜓)
Theorem	bj-exlimmpbi 34353	Lemma for theorems of the vtoclg 3515 family. (Contributed by BJ, 3-Oct-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝜒 → (𝜑 ↔ 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ (∃𝑥𝜒 → 𝜓)
Theorem	bj-exlimmpbir 34354	Lemma for theorems of the vtoclg 3515 family. (Contributed by BJ, 3-Oct-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜒 → (𝜑 ↔ 𝜓))    &   ⊢ 𝜓    ⇒   ⊢ (∃𝑥𝜒 → 𝜑)
Theorem	bj-vtoclf 34355*	Remove dependency on ax-ext 2770, df-clab 2777 and df-cleq 2791 (and df-sb 2070 and df-v 3443) from vtoclf 3506. (Contributed by BJ, 6-Oct-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ 𝐴 ∈ 𝑉    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ 𝜓
Theorem	bj-vtocl 34356*	Remove dependency on ax-ext 2770, df-clab 2777 and df-cleq 2791 (and df-sb 2070 and df-v 3443) from vtocl 3507. (Contributed by BJ, 6-Oct-2019.) (Proof modification is discouraged.)
⊢ 𝐴 ∈ 𝑉    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ 𝜓
Theorem	bj-vtoclg1f1 34357*	The FOL content of vtoclg1f 3514 (hence not using ax-ext 2770, df-cleq 2791, df-nfc 2938, df-v 3443). 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 2770; as a byproduct, this dispenses with ax-11 2158 and ax-13 2379). (Contributed by BJ, 30-Apr-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 → 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ (∃𝑦 𝑦 = 𝐴 → 𝜓)
Theorem	bj-vtoclg1f 34358*	Reprove vtoclg1f 3514 from bj-vtoclg1f1 34357. This removes dependency on ax-ext 2770, df-cleq 2791 and df-v 3443. Use bj-vtoclg1fv 34359 instead when sufficient (in particular when 𝑉 is substituted for V). (Contributed by BJ, 14-Sep-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 → 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝜓)
Theorem	bj-vtoclg1fv 34359*	Version of bj-vtoclg1f 34358 with a disjoint variable condition on 𝑥, 𝑉. This removes dependency on df-sb 2070 and df-clab 2777. Prefer its use over bj-vtoclg1f 34358 when sufficient (in particular when 𝑉 is substituted for V). (Contributed by BJ, 14-Sep-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 → 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝜓)
Theorem	bj-vtoclg 34360*	A version of vtoclg 3515 with an additional disjoint variable condition (which is removable if we allow use of df-clab 2777, see bj-vtoclg1f 34358), which requires fewer axioms (i.e., removes dependency on ax-6 1970, ax-7 2015, ax-9 2121, ax-12 2175, ax-ext 2770, df-clab 2777, df-cleq 2791, df-v 3443). (Contributed by BJ, 2-Jul-2022.) (Proof modification is discouraged.)
⊢ (𝑥 = 𝐴 → (𝜑 → 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝜓)
Theorem	bj-rabbida2 34361	Version of rabbidva2 3423 with disjoint variable condition replaced by nonfreeness hypothesis. (Contributed by BJ, 27-Apr-2019.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐵 ∧ 𝜒)))    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒})
Theorem	bj-rabeqd 34362	Deduction form of rabeq 3431. Note that contrary to rabeq 3431 it has no disjoint variable condition. (Contributed by BJ, 27-Apr-2019.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜓})
Theorem	bj-rabeqbid 34363	Version of rabeqbidv 3433 with two disjoint variable conditions removed and the third replaced by a nonfreeness hypothesis. (Contributed by BJ, 27-Apr-2019.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒})
Theorem	bj-rabeqbida 34364	Version of rabeqbidva 3434 with two disjoint variable conditions removed and the third replaced by a nonfreeness hypothesis. (Contributed by BJ, 27-Apr-2019.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒})
Theorem	bj-seex 34365*	Version of seex 5482 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 34366*	Version of df-nfc 2938 with a disjoint variable condition replaced with a nonfreeness hypothesis. (Contributed by BJ, 2-May-2019.)
⊢ Ⅎ𝑦𝐴    ⇒   ⊢ (Ⅎ𝑥𝐴 ↔ ∀𝑦Ⅎ𝑥 𝑦 ∈ 𝐴)
Theorem	bj-zfauscl 34367*	General version of zfauscl 5169. Remark: the comment in zfauscl 5169 is misleading: the essential use of ax-ext 2770 is the one via eleq2 2878 and not the one via vtocl 3507, since the latter can be proved without ax-ext 2770 (see bj-vtoclg 34360). (Contributed by BJ, 2-Jul-2022.) (Proof modification is discouraged.)
⊢ (𝐴 ∈ 𝑉 → ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝜑)))
20.15.5.8  Class abstractions A few additional theorems on class abstractions and restricted class abstractions.
Theorem	bj-unrab 34368*	Generalization of unrab 4226. Equality need not hold. (Contributed by BJ, 21-Apr-2019.)
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∪ {𝑥 ∈ 𝐵 ∣ 𝜓}) ⊆ {𝑥 ∈ (𝐴 ∪ 𝐵) ∣ (𝜑 ∨ 𝜓)}
Theorem	bj-inrab 34369	Generalization of inrab 4227. (Contributed by BJ, 21-Apr-2019.)
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ {𝑥 ∈ 𝐵 ∣ 𝜓}) = {𝑥 ∈ (𝐴 ∩ 𝐵) ∣ (𝜑 ∧ 𝜓)}
Theorem	bj-inrab2 34370	Shorter proof of inrab 4227. (Contributed by BJ, 21-Apr-2019.) (Proof modification is discouraged.)
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ {𝑥 ∈ 𝐴 ∣ 𝜓}) = {𝑥 ∈ 𝐴 ∣ (𝜑 ∧ 𝜓)}
Theorem	bj-inrab3 34371*	Generalization of dfrab3ss 4233, which it may shorten. (Contributed by BJ, 21-Apr-2019.) (Revised by OpenAI, 7-Jul-2020.)
⊢ (𝐴 ∩ {𝑥 ∈ 𝐵 ∣ 𝜑}) = ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ 𝐵)
Theorem	bj-rabtr 34372*	Restricted class abstraction with true formula. (Contributed by BJ, 22-Apr-2019.)
⊢ {𝑥 ∈ 𝐴 ∣ ⊤} = 𝐴
Theorem	bj-rabtrALT 34373*	Alternate proof of bj-rabtr 34372. (Contributed by BJ, 22-Apr-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ {𝑥 ∈ 𝐴 ∣ ⊤} = 𝐴
Theorem	bj-rabtrAUTO 34374*	Proof of bj-rabtr 34372 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.)
⊢ {𝑥 ∈ 𝐴 ∣ ⊤} = 𝐴
20.15.5.9  Restricted nonfreeness In this subsection, we define restricted nonfreeness (or relative nonfreeness).
Syntax	wrnf 34375	Syntax for restricted nonfreeness.
wff Ⅎ𝑥 ∈ 𝐴𝜑
Definition	df-bj-rnf 34376	Definition of restricted nonfreeness. Informally, the proposition Ⅎ𝑥 ∈ 𝐴𝜑 means that 𝜑(𝑥) does not vary on 𝐴. (Contributed by BJ, 19-Mar-2021.)
⊢ (Ⅎ𝑥 ∈ 𝐴𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜑))
20.15.5.10  Russell's paradox A few results around Russell's paradox. For clarity, we prove separately its FOL part (bj-ru0 34377) and then two versions (bj-ru1 34378 and bj-ru 34379). Special attention is put on minimizing axiom depencencies.
Theorem	bj-ru0 34377*	The FOL part of Russell's paradox ru 3719 (see also bj-ru1 34378, bj-ru 34379). Use of elequ1 2118, bj-elequ12 34125 (instead of eleq1 2877, eleq12d 2884 as in ru 3719) permits to remove dependency on ax-10 2142, ax-11 2158, ax-12 2175, ax-ext 2770, df-sb 2070, df-clab 2777, df-cleq 2791, df-clel 2870. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.)
⊢ ¬ ∀𝑥(𝑥 ∈ 𝑦 ↔ ¬ 𝑥 ∈ 𝑥)
Theorem	bj-ru1 34378*	A version of Russell's paradox ru 3719 (see also bj-ru 34379). (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.)
⊢ ¬ ∃𝑦 𝑦 = {𝑥 ∣ ¬ 𝑥 ∈ 𝑥}
Theorem	bj-ru 34379	Remove dependency on ax-13 2379 (and df-v 3443) from Russell's paradox ru 3719 expressed with primitive symbols and with a class variable 𝑉. Note the more economical use of bj-elissetv 34315 instead of isset 3453 to avoid use of df-v 3443. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.)
⊢ ¬ {𝑥 ∣ ¬ 𝑥 ∈ 𝑥} ∈ 𝑉
20.15.5.11  Curry's paradox in set theory
Theorem	currysetlem 34380*	Lemma for currysetlem 34380, where it is used with (𝑥 ∈ 𝑥 → 𝜑) substituted for 𝜓. (Contributed by BJ, 23-Sep-2023.) This proof is intuitionistically valid. (Proof modification is discouraged.)
⊢ ({𝑥 ∣ 𝜓} ∈ 𝑉 → ({𝑥 ∣ 𝜓} ∈ {𝑥 ∣ (𝑥 ∈ 𝑥 → 𝜑)} ↔ ({𝑥 ∣ 𝜓} ∈ {𝑥 ∣ 𝜓} → 𝜑)))
Theorem	curryset 34381*	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 34385. (Contributed by BJ, 23-Sep-2023.) This proof is intuitionistically valid. (Proof modification is discouraged.)
⊢ ¬ {𝑥 ∣ (𝑥 ∈ 𝑥 → 𝜑)} ∈ 𝑉
Theorem	currysetlem1 34382*	Lemma for currysetALT 34385. (Contributed by BJ, 23-Sep-2023.) This proof is intuitionistically valid. (Proof modification is discouraged.)
⊢ 𝑋 = {𝑥 ∣ (𝑥 ∈ 𝑥 → 𝜑)}    ⇒   ⊢ (𝑋 ∈ 𝑉 → (𝑋 ∈ 𝑋 ↔ (𝑋 ∈ 𝑋 → 𝜑)))
Theorem	currysetlem2 34383*	Lemma for currysetALT 34385. (Contributed by BJ, 23-Sep-2023.) This proof is intuitionistically valid. (Proof modification is discouraged.)
⊢ 𝑋 = {𝑥 ∣ (𝑥 ∈ 𝑥 → 𝜑)}    ⇒   ⊢ (𝑋 ∈ 𝑉 → (𝑋 ∈ 𝑋 → 𝜑))
Theorem	currysetlem3 34384*	Lemma for currysetALT 34385. (Contributed by BJ, 23-Sep-2023.) This proof is intuitionistically valid. (Proof modification is discouraged.)
⊢ 𝑋 = {𝑥 ∣ (𝑥 ∈ 𝑥 → 𝜑)}    ⇒   ⊢ ¬ 𝑋 ∈ 𝑉
Theorem	currysetALT 34385*	Alternate proof of curryset 34381, 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.)
⊢ ¬ {𝑥 ∣ (𝑥 ∈ 𝑥 → 𝜑)} ∈ 𝑉
20.15.5.12  Some disjointness results A few utility theorems on disjointness of classes.
Theorem	bj-n0i 34386*	Inference associated with n0 4260. Shortens 2ndcdisj 22061 (2888>2878), notzfaus 5227 (264>253). (Contributed by BJ, 22-Apr-2019.)
⊢ 𝐴 ≠ ∅    ⇒   ⊢ ∃𝑥 𝑥 ∈ 𝐴
Theorem	bj-disjcsn 34387	A class is disjoint from its singleton. A consequence of regularity. Shorter proof than bnj521 32117 and does not depend on df-ne 2988. (Contributed by BJ, 4-Apr-2019.)
⊢ (𝐴 ∩ {𝐴}) = ∅
Theorem	bj-disjsn01 34388	Disjointness of the singletons containing 0 and 1. This is a consequence of bj-disjcsn 34387 but the present proof does not use regularity. (Contributed by BJ, 4-Apr-2019.) (Proof modification is discouraged.)
⊢ ({∅} ∩ {1o}) = ∅
Theorem	bj-0nel1 34389	The empty set does not belong to {1o}. (Contributed by BJ, 6-Apr-2019.)
⊢ ∅ ∉ {1o}
Theorem	bj-1nel0 34390	1o does not belong to {∅}. (Contributed by BJ, 6-Apr-2019.)
⊢ 1o ∉ {∅}
20.15.5.13  Complements on direct products A few utility theorems on direct products.
Theorem	bj-xpimasn 34391	The image of a singleton, general case. [Change and relabel xpimasn 6009 accordingly, maybe to xpima2sn.] (Contributed by BJ, 6-Apr-2019.)
⊢ ((𝐴 × 𝐵) “ {𝑋}) = if(𝑋 ∈ 𝐴, 𝐵, ∅)
Theorem	bj-xpima1sn 34392	The image of a singleton by a direct product, empty case. [Change and relabel xpimasn 6009 accordingly, maybe to xpima2sn.] (Contributed by BJ, 6-Apr-2019.)
⊢ (¬ 𝑋 ∈ 𝐴 → ((𝐴 × 𝐵) “ {𝑋}) = ∅)
Theorem	bj-xpima1snALT 34393	Alternate proof of bj-xpima1sn 34392. (Contributed by BJ, 6-Apr-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ 𝑋 ∈ 𝐴 → ((𝐴 × 𝐵) “ {𝑋}) = ∅)
Theorem	bj-xpima2sn 34394	The image of a singleton by a direct product, nonempty case. [To replace xpimasn 6009.] (Contributed by BJ, 6-Apr-2019.) (Proof modification is discouraged.)
⊢ (𝑋 ∈ 𝐴 → ((𝐴 × 𝐵) “ {𝑋}) = 𝐵)
Theorem	bj-xpnzex 34395	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 7607 (up to commutation in the product). (Contributed by BJ, 6-Oct-2018.) (Proof modification is discouraged.)
⊢ (𝐴 ≠ ∅ → ((𝐴 × 𝐵) ∈ 𝑉 → 𝐵 ∈ V))
Theorem	bj-xpexg2 34396	Curried (exported) form of xpexg 7453. (Contributed by BJ, 2-Apr-2019.)
⊢ (𝐴 ∈ 𝑉 → (𝐵 ∈ 𝑊 → (𝐴 × 𝐵) ∈ V))
Theorem	bj-xpnzexb 34397	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 34398*	Substitution property for certain classes. (Contributed by BJ, 2-Apr-2019.)
⊢ (𝐴 = 𝐵 → {𝑥 ∣ {𝑥} ∈ (𝐴 “ 𝐶)} = {𝑥 ∣ {𝑥} ∈ (𝐵 “ 𝐶)})
20.15.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 34399*	The class of sets "whose singletons" belong to a set is a set. Nice application of ax-rep 5154. (Contributed by BJ, 6-Oct-2018.)
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V)
Theorem	bj-clex 34400*	Sethood of certain classes. (Contributed by BJ, 2-Apr-2019.)
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∣ {𝑥} ∈ (𝐴 “ 𝐵)} ∈ V)