P. 366 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 36501-36600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	bj-ceqsalgvALT 36501*	Alternate proof of bj-ceqsalgv 36500. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
Theorem	bj-ceqsal 36502*	Remove from ceqsal 3498 dependency on ax-ext 2696 (and on df-cleq 2717, df-v 3463, df-clab 2703, df-sb 2060). (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ 𝐴 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓)
Theorem	bj-ceqsalv 36503*	Remove from ceqsalv 3500 dependency on ax-ext 2696 (and on df-cleq 2717, df-v 3463, df-clab 2703, df-sb 2060). (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.)
⊢ 𝐴 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓)
Theorem	bj-spcimdv 36504*	Remove from spcimdv 3577 dependency on ax-9 2108, ax-10 2129, ax-11 2146, ax-13 2365, ax-ext 2696, df-cleq 2717 (and df-nfc 2877, df-v 3463, df-or 846, df-tru 1536, df-nf 1778). For an even more economical version, see bj-spcimdvv 36505. (Contributed by BJ, 30-Nov-2020.) (Proof modification is discouraged.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 → 𝜒))
Theorem	bj-spcimdvv 36505*	Remove from spcimdv 3577 dependency on ax-7 2003, ax-8 2100, ax-10 2129, ax-11 2146, ax-12 2166 ax-13 2365, ax-ext 2696, df-cleq 2717, df-clab 2703 (and df-nfc 2877, df-v 3463, df-or 846, df-tru 1536, df-nf 1778) 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 36504. (Contributed by BJ, 3-Nov-2021.) (Proof modification is discouraged.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 → 𝜒))
21.17.5.3  Characterization among sets versus among classes
Theorem	elelb 36506	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 36507	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.17.5.4  The nonfreeness quantifier for classes In this section, we prove the symmetry of the nonfreeness quantifier for classes.
Theorem	bj-nfcsym 36508	The nonfreeness quantifier for classes defines a symmetric binary relation on var metavariables (irreflexivity is proved by nfnid 5375 with additional axioms; see also nfcv 2891). This could be proved from aecom 2420 and nfcvb 5376 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 2731 instead of equcomd 2014; removing dependency on ax-ext 2696 is possible: prove weak versions (i.e. replace classes with setvars) of drnfc1 2911, eleq2d 2811 (using elequ2 2113), nfcvf 2921, dvelimc 2920, dvelimdc 2919, nfcvf2 2922. (Proof modification is discouraged.)
⊢ (Ⅎ𝑥𝑦 ↔ Ⅎ𝑦𝑥)
21.17.5.5  Lemmas for class substitution Some useful theorems for dealing with substitutions: sbbi 2297, sbcbig 3828, sbcel1g 4415, sbcel2 4417, sbcel12 4410, sbceqg 4411, csbvarg 4433.
Theorem	bj-sbeqALT 36509*	Substitution in an equality (use the more general version bj-sbeq 36510 instead, without disjoint variable condition). (Contributed by BJ, 6-Oct-2018.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ ([𝑦 / 𝑥]𝐴 = 𝐵 ↔ ⦋𝑦 / 𝑥⦌𝐴 = ⦋𝑦 / 𝑥⦌𝐵)
Theorem	bj-sbeq 36510	Distribute proper substitution through an equality relation. (See sbceqg 4411). (Contributed by BJ, 6-Oct-2018.)
⊢ ([𝑦 / 𝑥]𝐴 = 𝐵 ↔ ⦋𝑦 / 𝑥⦌𝐴 = ⦋𝑦 / 𝑥⦌𝐵)
Theorem	bj-sbceqgALT 36511	Distribute proper substitution through an equality relation. Alternate proof of sbceqg 4411. (Contributed by BJ, 6-Oct-2018.) Proof modification is discouraged to avoid using sbceqg 4411, but the Metamath program "MM-PA> MINIMIZE_WITH * / EXCEPT sbceqg" command is ok. (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵 = 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶))
Theorem	bj-csbsnlem 36512*	Lemma for bj-csbsn 36513 (in this lemma, 𝑥 cannot occur in 𝐴). (Contributed by BJ, 6-Oct-2018.) (New usage is discouraged.)
⊢ ⦋𝐴 / 𝑥⦌{𝑥} = {𝐴}
Theorem	bj-csbsn 36513	Substitution in a singleton. (Contributed by BJ, 6-Oct-2018.)
⊢ ⦋𝐴 / 𝑥⦌{𝑥} = {𝐴}
Theorem	bj-sbel1 36514*	Version of sbcel1g 4415 when substituting a set. (Note: one could have a corresponding version of sbcel12 4410 when substituting a set, but the point here is that the antecedent of sbcel1g 4415 is not needed when substituting a set.) (Contributed by BJ, 6-Oct-2018.)
⊢ ([𝑦 / 𝑥]𝐴 ∈ 𝐵 ↔ ⦋𝑦 / 𝑥⦌𝐴 ∈ 𝐵)
Theorem	bj-abv 36515	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 36516	Alternate version of bj-abv 36515; shorter but uses ax-8 2100. (Contributed by BJ, 24-Jul-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥𝜑 → {𝑥 ∣ 𝜑} = V)
Theorem	bj-ab0 36517	The class of sets verifying a falsity is the empty set (closed form of abf 4404). (Contributed by BJ, 24-Jul-2019.) (Proof modification is discouraged.)
⊢ (∀𝑥 ¬ 𝜑 → {𝑥 ∣ 𝜑} = ∅)
Theorem	bj-abf 36518	Shorter proof of abf 4404 (which should be kept as abfALT). (Contributed by BJ, 24-Jul-2019.) (Proof modification is discouraged.)
⊢ ¬ 𝜑    ⇒   ⊢ {𝑥 ∣ 𝜑} = ∅
Theorem	bj-csbprc 36519	More direct proof of csbprc 4408 (fewer essential steps). (Contributed by BJ, 24-Jul-2019.) (Proof modification is discouraged.)
⊢ (¬ 𝐴 ∈ V → ⦋𝐴 / 𝑥⦌𝐵 = ∅)
21.17.5.6  Removing some axiom requirements and disjoint variable conditions
Theorem	bj-exlimvmpi 36520*	A Fol lemma (exlimiv 1925 followed by mpi 20). (Contributed by BJ, 2-Jul-2022.) (Proof modification is discouraged.)
⊢ (𝜒 → (𝜑 → 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ (∃𝑥𝜒 → 𝜓)
Theorem	bj-exlimmpi 36521	Lemma for bj-vtoclg1f1 36526 (an instance of this lemma is a version of bj-vtoclg1f1 36526 where 𝑥 and 𝑦 are identified). (Contributed by BJ, 30-Apr-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝜒 → (𝜑 → 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ (∃𝑥𝜒 → 𝜓)
Theorem	bj-exlimmpbi 36522	Lemma for theorems of the vtoclg 3532 family. (Contributed by BJ, 3-Oct-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝜒 → (𝜑 ↔ 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ (∃𝑥𝜒 → 𝜓)
Theorem	bj-exlimmpbir 36523	Lemma for theorems of the vtoclg 3532 family. (Contributed by BJ, 3-Oct-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜒 → (𝜑 ↔ 𝜓))    &   ⊢ 𝜓    ⇒   ⊢ (∃𝑥𝜒 → 𝜑)
Theorem	bj-vtoclf 36524*	Remove dependency on ax-ext 2696, df-clab 2703 and df-cleq 2717 (and df-sb 2060 and df-v 3463) from vtoclf 3542. (Contributed by BJ, 6-Oct-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ 𝐴 ∈ 𝑉    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ 𝜓
Theorem	bj-vtocl 36525*	Remove dependency on ax-ext 2696, df-clab 2703 and df-cleq 2717 (and df-sb 2060 and df-v 3463) from vtocl 3536. (Contributed by BJ, 6-Oct-2019.) (Proof modification is discouraged.)
⊢ 𝐴 ∈ 𝑉    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ 𝜓
Theorem	bj-vtoclg1f1 36526*	The FOL content of vtoclg1f 3549 (hence not using ax-ext 2696, df-cleq 2717, df-nfc 2877, df-v 3463). 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 2696; as a byproduct, this dispenses with ax-11 2146 and ax-13 2365). (Contributed by BJ, 30-Apr-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 → 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ (∃𝑦 𝑦 = 𝐴 → 𝜓)
Theorem	bj-vtoclg1f 36527*	Reprove vtoclg1f 3549 from bj-vtoclg1f1 36526. This removes dependency on ax-ext 2696, df-cleq 2717 and df-v 3463. Use bj-vtoclg1fv 36528 instead when sufficient (in particular when 𝑉 is substituted for V). (Contributed by BJ, 14-Sep-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 → 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝜓)
Theorem	bj-vtoclg1fv 36528*	Version of bj-vtoclg1f 36527 with a disjoint variable condition on 𝑥, 𝑉. This removes dependency on df-sb 2060 and df-clab 2703. Prefer its use over bj-vtoclg1f 36527 when sufficient (in particular when 𝑉 is substituted for V). (Contributed by BJ, 14-Sep-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 → 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝜓)
Theorem	bj-vtoclg 36529*	A version of vtoclg 3532 with an additional disjoint variable condition (which is removable if we allow use of df-clab 2703, see bj-vtoclg1f 36527), which requires fewer axioms (i.e., removes dependency on ax-6 1963, ax-7 2003, ax-9 2108, ax-12 2166, ax-ext 2696, df-clab 2703, df-cleq 2717, df-v 3463). (Contributed by BJ, 2-Jul-2022.) (Proof modification is discouraged.)
⊢ (𝑥 = 𝐴 → (𝜑 → 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝜓)
Theorem	bj-rabeqbid 36530	Version of rabeqbidv 3436 with two disjoint variable conditions removed and the third replaced by a nonfreeness hypothesis. (Contributed by BJ, 27-Apr-2019.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒})
Theorem	bj-seex 36531*	Version of seex 5640 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 36532*	Version of df-nfc 2877 with a disjoint variable condition replaced with a nonfreeness hypothesis. (Contributed by BJ, 2-May-2019.)
⊢ Ⅎ𝑦𝐴    ⇒   ⊢ (Ⅎ𝑥𝐴 ↔ ∀𝑦Ⅎ𝑥 𝑦 ∈ 𝐴)
Theorem	bj-zfauscl 36533*	General version of zfauscl 5302. Remark: the comment in zfauscl 5302 is misleading: the essential use of ax-ext 2696 is the one via eleq2 2814 and not the one via vtocl 3536, since the latter can be proved without ax-ext 2696 (see bj-vtoclg 36529). (Contributed by BJ, 2-Jul-2022.) (Proof modification is discouraged.)
⊢ (𝐴 ∈ 𝑉 → ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝜑)))
21.17.5.7  Class abstractions A few additional theorems on class abstractions and restricted class abstractions.
Theorem	bj-elabd2ALT 36534*	Alternate proof of elabd2 3655 bypassing elab6g 3654 (and using sbiedvw 2088 instead of the ∀𝑥(𝑥 = 𝑦 → 𝜓) idiom). (Contributed by BJ, 16-Oct-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 = {𝑥 ∣ 𝜓})    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (𝐴 ∈ 𝐵 ↔ 𝜒))
Theorem	bj-unrab 36535*	Generalization of unrab 4304. Equality need not hold. (Contributed by BJ, 21-Apr-2019.)
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∪ {𝑥 ∈ 𝐵 ∣ 𝜓}) ⊆ {𝑥 ∈ (𝐴 ∪ 𝐵) ∣ (𝜑 ∨ 𝜓)}
Theorem	bj-inrab 36536	Generalization of inrab 4305. (Contributed by BJ, 21-Apr-2019.)
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ {𝑥 ∈ 𝐵 ∣ 𝜓}) = {𝑥 ∈ (𝐴 ∩ 𝐵) ∣ (𝜑 ∧ 𝜓)}
Theorem	bj-inrab2 36537	Shorter proof of inrab 4305. (Contributed by BJ, 21-Apr-2019.) (Proof modification is discouraged.)
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ {𝑥 ∈ 𝐴 ∣ 𝜓}) = {𝑥 ∈ 𝐴 ∣ (𝜑 ∧ 𝜓)}
Theorem	bj-inrab3 36538*	Generalization of dfrab3ss 4312, which it may shorten. (Contributed by BJ, 21-Apr-2019.) (Revised by OpenAI, 7-Jul-2020.)
⊢ (𝐴 ∩ {𝑥 ∈ 𝐵 ∣ 𝜑}) = ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ 𝐵)
Theorem	bj-rabtr 36539*	Restricted class abstraction with true formula. (Contributed by BJ, 22-Apr-2019.)
⊢ {𝑥 ∈ 𝐴 ∣ ⊤} = 𝐴
Theorem	bj-rabtrALT 36540*	Alternate proof of bj-rabtr 36539. (Contributed by BJ, 22-Apr-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ {𝑥 ∈ 𝐴 ∣ ⊤} = 𝐴
Theorem	bj-rabtrAUTO 36541*	Proof of bj-rabtr 36539 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.17.5.8  Generalized class abstractions
Syntax	bj-cgab 36542	Syntax for generalized class abstractions.
class {𝐴 ∣ 𝑥 ∣ 𝜑}
Definition	df-bj-gab 36543*	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 36544	Inclusion of generalized class abstractions. (Contributed by BJ, 4-Oct-2024.)
⊢ (∀𝑥(𝐴 = 𝐵 ∧ (𝜑 → 𝜓)) → {𝐴 ∣ 𝑥 ∣ 𝜑} ⊆ {𝐵 ∣ 𝑥 ∣ 𝜓})
Theorem	bj-gabssd 36545	Inclusion of generalized class abstractions. Deduction form. (Contributed by BJ, 4-Oct-2024.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → {𝐴 ∣ 𝑥 ∣ 𝜓} ⊆ {𝐵 ∣ 𝑥 ∣ 𝜒})
Theorem	bj-gabeqd 36546	Equality of generalized class abstractions. Deduction form. (Contributed by BJ, 4-Oct-2024.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {𝐴 ∣ 𝑥 ∣ 𝜓} = {𝐵 ∣ 𝑥 ∣ 𝜒})
Theorem	bj-gabeqis 36547*	Equality of generalized class abstractions, with implicit substitution. (Contributed by BJ, 4-Oct-2024.)
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ {𝐴 ∣ 𝑥 ∣ 𝜑} = {𝐵 ∣ 𝑦 ∣ 𝜓}
Theorem	bj-elgab 36548	Elements of a generalized class abstraction. (Contributed by BJ, 4-Oct-2024.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → Ⅎ𝑥𝐴)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → (∃𝑥(𝐴 = 𝐵 ∧ 𝜓) ↔ 𝜒))    ⇒   ⊢ (𝜑 → (𝐴 ∈ {𝐵 ∣ 𝑥 ∣ 𝜓} ↔ 𝜒))
Theorem	bj-gabima 36549	Generalized class abstraction as a direct image. TODO: improve the support lemmas elimag 6068 and fvelima 6963 to nonfreeness hypothesis (and for the latter, biconditional). (Contributed by BJ, 4-Oct-2024.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → Ⅎ𝑥𝐹)    &   ⊢ (𝜑 → Fun 𝐹)    &   ⊢ (𝜑 → {𝑥 ∣ 𝜓} ⊆ dom 𝐹)    ⇒   ⊢ (𝜑 → {(𝐹‘𝑥) ∣ 𝑥 ∣ 𝜓} = (𝐹 “ {𝑥 ∣ 𝜓}))
21.17.5.9  Restricted nonfreeness In this subsection, we define restricted nonfreeness (or relative nonfreeness).
Syntax	wrnf 36550	Syntax for restricted nonfreeness.
wff Ⅎ𝑥 ∈ 𝐴𝜑
Definition	df-bj-rnf 36551	Definition of restricted nonfreeness. Informally, the proposition Ⅎ𝑥 ∈ 𝐴𝜑 means that 𝜑(𝑥) does not vary on 𝐴. (Contributed by BJ, 19-Mar-2021.)
⊢ (Ⅎ𝑥 ∈ 𝐴𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜑))
21.17.5.10  Russell's paradox A few results around Russell's paradox. For clarity, we prove separately its FOL part (bj-ru0 36552) and then two versions (bj-ru1 36553 and bj-ru 36554). Special attention is put on minimizing axiom depencencies.
Theorem	bj-ru0 36552*	The FOL part of Russell's paradox ru 3772 (see also bj-ru1 36553, bj-ru 36554). Use of elequ1 2105, bj-elequ12 36286 (instead of eleq1 2813, eleq12d 2819 as in ru 3772) permits to remove dependency on ax-10 2129, ax-11 2146, ax-12 2166, ax-ext 2696, df-sb 2060, df-clab 2703, df-cleq 2717, df-clel 2802. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.)
⊢ ¬ ∀𝑥(𝑥 ∈ 𝑦 ↔ ¬ 𝑥 ∈ 𝑥)
Theorem	bj-ru1 36553*	A version of Russell's paradox ru 3772 (see also bj-ru 36554). (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.)
⊢ ¬ ∃𝑦 𝑦 = {𝑥 ∣ ¬ 𝑥 ∈ 𝑥}
Theorem	bj-ru 36554	Remove dependency on ax-13 2365 (and df-v 3463) from Russell's paradox ru 3772 expressed with primitive symbols and with a class variable 𝑉. Note the more economical use of elissetv 2806 instead of isset 3474 to avoid use of df-v 3463. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.)
⊢ ¬ {𝑥 ∣ ¬ 𝑥 ∈ 𝑥} ∈ 𝑉
21.17.5.11  Curry's paradox in set theory
Theorem	currysetlem 36555*	Lemma for currysetlem 36555, where it is used with (𝑥 ∈ 𝑥 → 𝜑) substituted for 𝜓. (Contributed by BJ, 23-Sep-2023.) This proof is intuitionistically valid. (Proof modification is discouraged.)
⊢ ({𝑥 ∣ 𝜓} ∈ 𝑉 → ({𝑥 ∣ 𝜓} ∈ {𝑥 ∣ (𝑥 ∈ 𝑥 → 𝜑)} ↔ ({𝑥 ∣ 𝜓} ∈ {𝑥 ∣ 𝜓} → 𝜑)))
Theorem	curryset 36556*	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 36560. (Contributed by BJ, 23-Sep-2023.) This proof is intuitionistically valid. (Proof modification is discouraged.)
⊢ ¬ {𝑥 ∣ (𝑥 ∈ 𝑥 → 𝜑)} ∈ 𝑉
Theorem	currysetlem1 36557*	Lemma for currysetALT 36560. (Contributed by BJ, 23-Sep-2023.) This proof is intuitionistically valid. (Proof modification is discouraged.)
⊢ 𝑋 = {𝑥 ∣ (𝑥 ∈ 𝑥 → 𝜑)}    ⇒   ⊢ (𝑋 ∈ 𝑉 → (𝑋 ∈ 𝑋 ↔ (𝑋 ∈ 𝑋 → 𝜑)))
Theorem	currysetlem2 36558*	Lemma for currysetALT 36560. (Contributed by BJ, 23-Sep-2023.) This proof is intuitionistically valid. (Proof modification is discouraged.)
⊢ 𝑋 = {𝑥 ∣ (𝑥 ∈ 𝑥 → 𝜑)}    ⇒   ⊢ (𝑋 ∈ 𝑉 → (𝑋 ∈ 𝑋 → 𝜑))
Theorem	currysetlem3 36559*	Lemma for currysetALT 36560. (Contributed by BJ, 23-Sep-2023.) This proof is intuitionistically valid. (Proof modification is discouraged.)
⊢ 𝑋 = {𝑥 ∣ (𝑥 ∈ 𝑥 → 𝜑)}    ⇒   ⊢ ¬ 𝑋 ∈ 𝑉
Theorem	currysetALT 36560*	Alternate proof of curryset 36556, 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.17.5.12  Some disjointness results A few utility theorems on disjointness of classes.
Theorem	bj-n0i 36561*	Inference associated with n0 4346. Shortens 2ndcdisj 23404 (2888>2878), notzfaus 5363 (264>253). (Contributed by BJ, 22-Apr-2019.)
⊢ 𝐴 ≠ ∅    ⇒   ⊢ ∃𝑥 𝑥 ∈ 𝐴
Theorem	bj-disjsn01 36562	Disjointness of the singletons containing 0 and 1. This is a consequence of disjcsn 9629 but the present proof does not use regularity. (Contributed by BJ, 4-Apr-2019.) (Proof modification is discouraged.)
⊢ ({∅} ∩ {1o}) = ∅
Theorem	bj-0nel1 36563	The empty set does not belong to {1o}. (Contributed by BJ, 6-Apr-2019.)
⊢ ∅ ∉ {1o}
Theorem	bj-1nel0 36564	1o does not belong to {∅}. (Contributed by BJ, 6-Apr-2019.)
⊢ 1o ∉ {∅}
21.17.5.13  Complements on direct products A few utility theorems on direct products.
Theorem	bj-xpimasn 36565	The image of a singleton, general case. [Change and relabel xpimasn 6191 accordingly, maybe to xpima2sn.] (Contributed by BJ, 6-Apr-2019.)
⊢ ((𝐴 × 𝐵) “ {𝑋}) = if(𝑋 ∈ 𝐴, 𝐵, ∅)
Theorem	bj-xpima1sn 36566	The image of a singleton by a direct product, empty case. [Change and relabel xpimasn 6191 accordingly, maybe to xpima2sn.] (Contributed by BJ, 6-Apr-2019.)
⊢ (¬ 𝑋 ∈ 𝐴 → ((𝐴 × 𝐵) “ {𝑋}) = ∅)
Theorem	bj-xpima1snALT 36567	Alternate proof of bj-xpima1sn 36566. (Contributed by BJ, 6-Apr-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ 𝑋 ∈ 𝐴 → ((𝐴 × 𝐵) “ {𝑋}) = ∅)
Theorem	bj-xpima2sn 36568	The image of a singleton by a direct product, nonempty case. [To replace xpimasn 6191.] (Contributed by BJ, 6-Apr-2019.) (Proof modification is discouraged.)
⊢ (𝑋 ∈ 𝐴 → ((𝐴 × 𝐵) “ {𝑋}) = 𝐵)
Theorem	bj-xpnzex 36569	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 7928 (up to commutation in the product). (Contributed by BJ, 6-Oct-2018.) (Proof modification is discouraged.)
⊢ (𝐴 ≠ ∅ → ((𝐴 × 𝐵) ∈ 𝑉 → 𝐵 ∈ V))
Theorem	bj-xpexg2 36570	Curried (exported) form of xpexg 7753. (Contributed by BJ, 2-Apr-2019.)
⊢ (𝐴 ∈ 𝑉 → (𝐵 ∈ 𝑊 → (𝐴 × 𝐵) ∈ V))
Theorem	bj-xpnzexb 36571	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 36572*	Substitution property for certain classes. (Contributed by BJ, 2-Apr-2019.)
⊢ (𝐴 = 𝐵 → {𝑥 ∣ {𝑥} ∈ (𝐴 “ 𝐶)} = {𝑥 ∣ {𝑥} ∈ (𝐵 “ 𝐶)})
21.17.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 36573*	The class of sets "whose singletons" belong to a set is a set. Nice application of ax-rep 5286. (Contributed by BJ, 6-Oct-2018.)
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V)
Theorem	bj-clexab 36574*	Sethood of certain classes. (Contributed by BJ, 2-Apr-2019.)
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∣ {𝑥} ∈ (𝐴 “ 𝐵)} ∈ V)
Syntax	bj-csngl 36575	Syntax for singletonization. (Contributed by BJ, 6-Oct-2018.)
class sngl 𝐴
Definition	df-bj-sngl 36576*	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 36577	Substitution property for sngl. (Contributed by BJ, 6-Oct-2018.)
⊢ (𝐴 = 𝐵 → sngl 𝐴 = sngl 𝐵)
Theorem	bj-elsngl 36578*	Characterization of the elements of the singletonization of a class. (Contributed by BJ, 6-Oct-2018.)
⊢ (𝐴 ∈ sngl 𝐵 ↔ ∃𝑥 ∈ 𝐵 𝐴 = {𝑥})
Theorem	bj-snglc 36579	Characterization of the elements of 𝐴 in terms of elements of its singletonization. (Contributed by BJ, 6-Oct-2018.)
⊢ (𝐴 ∈ 𝐵 ↔ {𝐴} ∈ sngl 𝐵)
Theorem	bj-snglss 36580	The singletonization of a class is included in its powerclass. (Contributed by BJ, 6-Oct-2018.)
⊢ sngl 𝐴 ⊆ 𝒫 𝐴
Theorem	bj-0nelsngl 36581	The empty set is not a member of a singletonization (neither is any nonsingleton, in particular any von Neuman ordinal except possibly df-1o 8487). (Contributed by BJ, 6-Oct-2018.)
⊢ ∅ ∉ sngl 𝐴
Theorem	bj-snglinv 36582*	Inverse of singletonization. (Contributed by BJ, 6-Oct-2018.)
⊢ 𝐴 = {𝑥 ∣ {𝑥} ∈ sngl 𝐴}
Theorem	bj-snglex 36583	A class is a set if and only if its singletonization is a set. (Contributed by BJ, 6-Oct-2018.)
⊢ (𝐴 ∈ V ↔ sngl 𝐴 ∈ V)
Syntax	bj-ctag 36584	Syntax for the tagged copy of a class. (Contributed by BJ, 6-Oct-2018.)
class tag 𝐴
Definition	df-bj-tag 36585	Definition of the tagged copy of a class, that is, the adjunction to (an isomorph of) 𝐴 of a disjoint element (here, the empty set). Remark: this could be used for the one-point compactification of a topological space. (Contributed by BJ, 6-Oct-2018.)
⊢ tag 𝐴 = (sngl 𝐴 ∪ {∅})
Theorem	bj-tageq 36586	Substitution property for tag. (Contributed by BJ, 6-Oct-2018.)
⊢ (𝐴 = 𝐵 → tag 𝐴 = tag 𝐵)
Theorem	bj-eltag 36587*	Characterization of the elements of the tagging of a class. (Contributed by BJ, 6-Oct-2018.)
⊢ (𝐴 ∈ tag 𝐵 ↔ (∃𝑥 ∈ 𝐵 𝐴 = {𝑥} ∨ 𝐴 = ∅))
Theorem	bj-0eltag 36588	The empty set belongs to the tagging of a class. (Contributed by BJ, 6-Apr-2019.)
⊢ ∅ ∈ tag 𝐴
Theorem	bj-tagn0 36589	The tagging of a class is nonempty. (Contributed by BJ, 6-Apr-2019.)
⊢ tag 𝐴 ≠ ∅
Theorem	bj-tagss 36590	The tagging of a class is included in its powerclass. (Contributed by BJ, 6-Oct-2018.)
⊢ tag 𝐴 ⊆ 𝒫 𝐴
Theorem	bj-snglsstag 36591	The singletonization is included in the tagging. (Contributed by BJ, 6-Oct-2018.)
⊢ sngl 𝐴 ⊆ tag 𝐴
Theorem	bj-sngltagi 36592	The singletonization is included in the tagging. (Contributed by BJ, 6-Oct-2018.)
⊢ (𝐴 ∈ sngl 𝐵 → 𝐴 ∈ tag 𝐵)
Theorem	bj-sngltag 36593	The singletonization and the tagging of a set contain the same singletons. (Contributed by BJ, 6-Oct-2018.)
⊢ (𝐴 ∈ 𝑉 → ({𝐴} ∈ sngl 𝐵 ↔ {𝐴} ∈ tag 𝐵))
Theorem	bj-tagci 36594	Characterization of the elements of 𝐵 in terms of elements of its tagged version. (Contributed by BJ, 6-Oct-2018.)
⊢ (𝐴 ∈ 𝐵 → {𝐴} ∈ tag 𝐵)
Theorem	bj-tagcg 36595	Characterization of the elements of 𝐵 in terms of elements of its tagged version. (Contributed by BJ, 6-Oct-2018.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ {𝐴} ∈ tag 𝐵))
Theorem	bj-taginv 36596*	Inverse of tagging. (Contributed by BJ, 6-Oct-2018.)
⊢ 𝐴 = {𝑥 ∣ {𝑥} ∈ tag 𝐴}
Theorem	bj-tagex 36597	A class is a set if and only if its tagging is a set. (Contributed by BJ, 6-Oct-2018.)
⊢ (𝐴 ∈ V ↔ tag 𝐴 ∈ V)
Theorem	bj-xtageq 36598	The products of a given class and the tagging of either of two equal classes are equal. (Contributed by BJ, 6-Apr-2019.)
⊢ (𝐴 = 𝐵 → (𝐶 × tag 𝐴) = (𝐶 × tag 𝐵))
Theorem	bj-xtagex 36599	The product of a set and the tagging of a set is a set. (Contributed by BJ, 2-Apr-2019.)
⊢ (𝐴 ∈ 𝑉 → (𝐵 ∈ 𝑊 → (𝐴 × tag 𝐵) ∈ V))
21.17.5.15  Tuples of classes This subsection gives a definition of an ordered pair, or couple (2-tuple), that "works" for proper classes, as evidenced by Theorems bj-2uplth 36631 and bj-2uplex 36632, and more importantly, bj-pr21val 36623 and bj-pr22val 36629. In particular, one can define well-behaved tuples of classes. Classes in ZF(C) are only virtual, and in particular they cannot be quantified over. Theorem bj-2uplex 36632 has advantages: in view of df-br 5150, several sethood antecedents could be removed from existing theorems. For instance, relsnopg 5805 (resp. relsnop 5807) would hold without antecedents (resp. hypotheses) thanks to relsnb 5804). Also, the antecedent Rel 𝑅 could be removed from brrelex12 5730 and related theorems brrelex*, and, as a consequence, of multiple later theorems. Similarly, df-struct 17119 could be simplified by removing the exception currently made for the empty set. The projections are denoted by pr1 and pr2 and the couple with projections (or coordinates) 𝐴 and 𝐵 is denoted by ⦅𝐴, 𝐵⦆. Note that this definition uses the Kuratowski definition (df-op 4637) as a preliminary definition, and then "redefines" a couple. It could also use the "short" version of the Kuratowski pair (see opthreg 9643) without needing the axiom of regularity; it could even bypass this definition by "inlining" it. This definition is due to Anthony Morse and is expounded (with idiosyncratic notation) in Anthony P. Morse, A Theory of Sets, Academic Press, 1965 (second edition 1986). Note that this extends in a natural way to tuples. A variation of this definition is justified in opthprc 5742, but here we use "tagged versions" of the factors (see df-bj-tag 36585) so that an m-tuple can equal an n-tuple only when m = n (and the projections are the same). A comparison of the different definitions of tuples (strangely not mentioning Morse's), is given in Dominic McCarty and Dana Scott, Reconsidering ordered pairs, Bull. Symbolic Logic, Volume 14, Issue 3 (Sept. 2008), 379--397. where a recursive definition of tuples is given that avoids the two-step definition of tuples and that can be adapted to various set theories. Finally, another survey is Akihiro Kanamori, The empty set, the singleton, and the ordered pair, Bull. Symbolic Logic, Volume 9, Number 3 (Sept. 2003), 273--298. (available at http://math.bu.edu/people/aki/8.pdf 36585)
Syntax	bj-cproj 36600	Syntax for the class projection. (Contributed by BJ, 6-Apr-2019.)
class (𝐴 Proj 𝐵)