P. 335 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 33401-33500   *Has distinct variable group(s)

Type	Label	Description
Statement
20.14.5.5  Proposal for the definitions of class membership and class equality In this section, we show (bj-ax8 33401 and bj-ax9 33404) that the current forms of the definitions of class membership (df-clel 2821) and class equality (df-cleq 2818) are too powerful, and we propose alternate definitions (bj-df-clel 33402 and bj-df-cleq 33407) which also have the advantage of making it clear that these definitions are conservative.
Theorem	bj-ax8 33401	Proof of ax-8 2166 from df-clel 2821 (and FOL). This shows that df-clel 2821 is "too powerful". A possible definition is given by bj-df-clel 33402. (Contributed by BJ, 27-Jun-2019.) Also a direct consequence of eleq1w 2889, which has essentially the same proof. (Proof modification is discouraged.)
⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧))
Theorem	bj-df-clel 33402*	Candidate definition for df-clel 2821 (the need for it is exposed in bj-ax8 33401). The similarity of the hypothesis ⊢ ∀𝑢∀𝑣(𝑢 ∈ 𝑣 ↔ ∃𝑤(𝑤 = 𝑢 ∧ 𝑤 ∈ 𝑣)) and the conclusion, together with all possible disjoint variable conditions, makes it clear that this definition merely extends to class variables something that is true for setvar variables, hence is conservative. This definition should be directly referenced only by bj-dfclel 33403, which should be used instead. The proof is irrelevant since this is a proposal for an axiom. Note: the current definition df-clel 2821 already mentions cleljust 2172 as a justification; here, we merely propose to put it (more preciesly: its universal closure) as a hypothesis to make things more explicit. (Contributed by BJ, 27-Jun-2019.) (Proof modification is discouraged.)
⊢ ∀𝑢∀𝑣(𝑢 ∈ 𝑣 ↔ ∃𝑤(𝑤 = 𝑢 ∧ 𝑤 ∈ 𝑣))    ⇒   ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵))
Theorem	bj-dfclel 33403*	Characterization of the elements of a class. Note: cleljust 2172 could be relabeled "clelhyp". (Contributed by BJ, 27-Jun-2019.) (Proof modification is discouraged.)
⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵))
Theorem	bj-ax9 33404*	Proof of ax-9 2173 from Tarski's FOL=, sp 2224, df-cleq 2818 and ax-ext 2803 (with two extra disjoint variable conditions on 𝑥, 𝑧 and 𝑦, 𝑧). For a version without these disjoint variable conditions, see bj-ax9-2 33405. This shows that df-cleq 2818 is "too powerful". A possible definition is given by bj-df-cleq 33407. (Contributed by BJ, 24-Jun-2019.) (Proof modification is discouraged.)
⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦))
Theorem	bj-ax9-2 33405	Proof of ax-9 2173 from Tarski's FOL=, ax-8 2166 (specifically, ax8v1 2168 and ax8v2 2169) , df-cleq 2818 and ax-ext 2803. For a version not using ax-8 2166, see bj-ax9 33404. This shows that df-cleq 2818 is "too powerful". A possible definition is given by bj-df-cleq 33407. (Contributed by BJ, 24-Jun-2019.) (Proof modification is discouraged.)
⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦))
Theorem	bj-cleqhyp 33406*	The hypothesis of bj-df-cleq 33407. Note that the hypothesis of bj-df-cleq 33407 actually has an additional disjoint variable condition on 𝑥, 𝑦 and therefore is provable by simply using ax-ext 2803 in place of axext3 2805 in the current proof. (Contributed by BJ, 24-Jun-2019.) (Proof modification is discouraged.)
⊢ (𝑥 = 𝑦 ↔ ∀𝑧(𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦))
Theorem	bj-df-cleq 33407*	Candidate definition for df-cleq 2818 (the need for it is exposed in bj-ax9 33404). The similarity of the hypothesis ⊢ ∀𝑢∀𝑣(𝑢 = 𝑣 ↔ ∀𝑤(𝑤 ∈ 𝑢 ↔ 𝑤 ∈ 𝑣)) and the conclusion makes it clear that this definition merely extends to class variables something that is true for setvar variables, hence is conservative. This definition should be directly referenced only by bj-dfcleq 33408, which should be used instead. The proof is irrelevant since this is a proposal for an axiom. Another definition, which would give finer control, is actually the pair of definitions where each has one implication of the present biconditional as hypothesis and conclusion. They assert that extensionality (respectively, the left-substitution axiom for the membership predicate) extends from setvars to classes. (Contributed by BJ, 24-Jun-2019.) (Proof modification is discouraged.)
⊢ ∀𝑢∀𝑣(𝑢 = 𝑣 ↔ ∀𝑤(𝑤 ∈ 𝑢 ↔ 𝑤 ∈ 𝑣))    ⇒   ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
Theorem	bj-dfcleq 33408*	Proof of class extensionality from the axiom of set extensionality (ax-ext 2803) and the definition of class equality (bj-df-cleq 33407). (Contributed by BJ, 24-Jun-2019.) (Proof modification is discouraged.)
⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
20.14.5.6  Lemmas for class substitution Some useful theorems for dealing with substitutions: sbbi 2532, sbcbig 3707, sbcel1g 4211, sbcel2 4213, sbcel12 4207, sbceqg 4208, csbvarg 4227.
Theorem	bj-sbeqALT 33409*	Substitution in an equality (use the more genereal version bj-sbeq 33410 instead, without disjoint variable condition). (Contributed by BJ, 6-Oct-2018.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ ([𝑦 / 𝑥]𝐴 = 𝐵 ↔ ⦋𝑦 / 𝑥⦌𝐴 = ⦋𝑦 / 𝑥⦌𝐵)
Theorem	bj-sbeq 33410	Distribute proper substitution through an equality relation. (See sbceqg 4208). (Contributed by BJ, 6-Oct-2018.)
⊢ ([𝑦 / 𝑥]𝐴 = 𝐵 ↔ ⦋𝑦 / 𝑥⦌𝐴 = ⦋𝑦 / 𝑥⦌𝐵)
Theorem	bj-sbceqgALT 33411	Distribute proper substitution through an equality relation. Alternate proof of sbceqg 4208. (Contributed by BJ, 6-Oct-2018.) Proof modification is discouraged to avoid using sbceqg 4208, but "MM-PA> MINIMIZEWITH * / EXCEPT sbceqg" is ok. (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵 = 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶))
Theorem	bj-csbsnlem 33412*	Lemma for bj-csbsn 33413 (in this lemma, 𝑥 cannot occur in 𝐴). (Contributed by BJ, 6-Oct-2018.) (New usage is discouraged.)
⊢ ⦋𝐴 / 𝑥⦌{𝑥} = {𝐴}
Theorem	bj-csbsn 33413	Substitution in a singleton. (Contributed by BJ, 6-Oct-2018.)
⊢ ⦋𝐴 / 𝑥⦌{𝑥} = {𝐴}
Theorem	bj-sbel1 33414*	Version of sbcel1g 4211 when substituting a set. (Note: one could have a corresponding version of sbcel12 4207 when substituting a set, but the point here is that the antecedent of sbcel1g 4211 is not needed when substituting a set.) (Contributed by BJ, 6-Oct-2018.)
⊢ ([𝑦 / 𝑥]𝐴 ∈ 𝐵 ↔ ⦋𝑦 / 𝑥⦌𝐴 ∈ 𝐵)
Theorem	bj-abv 33415	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 33416	The class of sets verifying a falsity is the empty set (closed form of abf 4203). (Contributed by BJ, 24-Jul-2019.) (Proof modification is discouraged.)
⊢ (∀𝑥 ¬ 𝜑 → {𝑥 ∣ 𝜑} = ∅)
Theorem	bj-abf 33417	Shorter proof of abf 4203 (which should be kept as abfALT). (Contributed by BJ, 24-Jul-2019.) (Proof modification is discouraged.)
⊢ ¬ 𝜑    ⇒   ⊢ {𝑥 ∣ 𝜑} = ∅
Theorem	bj-csbprc 33418	More direct proof of csbprc 4205 (fewer essential steps). (Contributed by BJ, 24-Jul-2019.) (Proof modification is discouraged.)
⊢ (¬ 𝐴 ∈ V → ⦋𝐴 / 𝑥⦌𝐵 = ∅)
20.14.5.7  Removing some axiom requirements and disjoint variable conditions
Theorem	bj-exlimvmpi 33419*	A Fol lemma (exlimiv 2029 followed by mpi 20). (Contributed by BJ, 2-Jul-2022.) (Proof modification is discouraged.)
⊢ (𝜒 → (𝜑 → 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ (∃𝑥𝜒 → 𝜓)
Theorem	bj-exlimmpi 33420	Lemma for bj-vtoclg1f1 33425 (an instance of this lemma is a version of bj-vtoclg1f1 33425 where 𝑥 and 𝑦 are identified). (Contributed by BJ, 30-Apr-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝜒 → (𝜑 → 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ (∃𝑥𝜒 → 𝜓)
Theorem	bj-exlimmpbi 33421	Lemma for theorems of the vtoclg 3482 family. (Contributed by BJ, 3-Oct-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝜒 → (𝜑 ↔ 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ (∃𝑥𝜒 → 𝜓)
Theorem	bj-exlimmpbir 33422	Lemma for theorems of the vtoclg 3482 family. (Contributed by BJ, 3-Oct-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜒 → (𝜑 ↔ 𝜓))    &   ⊢ 𝜓    ⇒   ⊢ (∃𝑥𝜒 → 𝜑)
Theorem	bj-vtoclf 33423*	Remove dependency on ax-ext 2803, df-clab 2812 and df-cleq 2818 (and df-sb 2068 and df-v 3416) from vtoclf 3474. (Contributed by BJ, 6-Oct-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ 𝐴 ∈ 𝑉    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ 𝜓
Theorem	bj-vtocl 33424*	Remove dependency on ax-ext 2803, df-clab 2812 and df-cleq 2818 (and df-sb 2068 and df-v 3416) from vtocl 3475. (Contributed by BJ, 6-Oct-2019.) (Proof modification is discouraged.)
⊢ 𝐴 ∈ 𝑉    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ 𝜓
Theorem	bj-vtoclg1f1 33425*	The FOL content of vtoclg1f 3481 (hence not using ax-ext 2803, df-cleq 2818, df-nfc 2958, df-v 3416). 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 2803; as a byproduct, this dispenses with ax-11 2207 and ax-13 2389). (Contributed by BJ, 30-Apr-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 → 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ (∃𝑦 𝑦 = 𝐴 → 𝜓)
Theorem	bj-vtoclg1f 33426*	Reprove vtoclg1f 3481 from bj-vtoclg1f1 33425. This removes dependency on ax-ext 2803, df-cleq 2818 and df-v 3416. Use bj-vtoclg1fv 33427 instead when sufficient (in particular when 𝑉 is substituted for V). (Contributed by BJ, 14-Sep-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 → 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝜓)
Theorem	bj-vtoclg1fv 33427*	Version of bj-vtoclg1f 33426 with a disjoint variable condition on 𝑥, 𝑉. This removes dependency on df-sb 2068 and df-clab 2812. Prefer its use over bj-vtoclg1f 33426 when sufficient (in particular when 𝑉 is substituted for V). (Contributed by BJ, 14-Sep-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 → 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝜓)
Theorem	bj-vtoclg 33428*	A version of vtoclg 3482 with an additional disjoint variable condition (which is removable if we allow use of df-clab 2812, see bj-vtoclg1f 33426), which requires fewer axioms (i.e., removes dependency on ax-6 2075, ax-7 2112, ax-9 2173, ax-12 2220, ax-ext 2803, df-clab 2812, df-cleq 2818, df-v 3416). (Contributed by BJ, 2-Jul-2022.) (Proof modification is discouraged.)
⊢ (𝑥 = 𝐴 → (𝜑 → 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝜓)
Theorem	bj-rabbida2 33429	Version of rabbidva2 3399 with disjoint variable condition replaced by non-freeness hypothesis. (Contributed by BJ, 27-Apr-2019.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐵 ∧ 𝜒)))    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒})
Theorem	bj-rabbida 33430	Version of rabbidva 3401 with disjoint variable condition replaced by non-freeness hypothesis. (Contributed by BJ, 27-Apr-2019.)
⊢ Ⅎ𝑥𝜑    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒})
Theorem	bj-rabbid 33431	Version of rabbidv 3402 with disjoint variable condition replaced by non-freeness hypothesis. (Contributed by BJ, 27-Apr-2019.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒})
Theorem	bj-rabeqd 33432	Deduction form of rabeq 3405. Note that contrary to rabeq 3405 it has no disjoint variable condition. (Contributed by BJ, 27-Apr-2019.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜓})
Theorem	bj-rabeqbid 33433	Version of rabeqbidv 3408 with two disjoint variable conditions removed and the third replaced by a non-freeness hypothesis. (Contributed by BJ, 27-Apr-2019.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒})
Theorem	bj-rabeqbida 33434	Version of rabeqbidva 3409 with two disjoint variable conditions removed and the third replaced by a non-freeness hypothesis. (Contributed by BJ, 27-Apr-2019.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒})
Theorem	bj-seex 33435*	Version of seex 5305 with a disjoint variable condition replaced by a non-freeness hypothesis (for the sake of illustration). (Contributed by BJ, 27-Apr-2019.)
⊢ Ⅎ𝑥𝐵    ⇒   ⊢ ((𝑅 Se 𝐴 ∧ 𝐵 ∈ 𝐴) → {𝑥 ∈ 𝐴 ∣ 𝑥𝑅𝐵} ∈ V)
Theorem	bj-nfcf 33436*	Version of df-nfc 2958 with a disjoint variable condition replaced with a non-freeness hypothesis. (Contributed by BJ, 2-May-2019.)
⊢ Ⅎ𝑦𝐴    ⇒   ⊢ (Ⅎ𝑥𝐴 ↔ ∀𝑦Ⅎ𝑥 𝑦 ∈ 𝐴)
Theorem	bj-axsep2 33437*	Remove dependency on ax-12 2220 and ax-13 2389 from axsep2 5006 while shortening its proof. (Contributed by BJ, 6-Oct-2019.) (Proof modification is discouraged.)
⊢ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))
Theorem	bj-zfauscl 33438*	General version of zfauscl 5007, removing dependency on ax-12 2220 and df-clab 2812 (and df-tru 1660, df-sb 2068, df-v 3416). Remark: the comment in zfauscl 5007 is misleading: the essential use of ax-ext 2803 is the one via eleq2 2895 and not the one via vtocl 3475, since the latter can be proved without ax-ext 2803 (see bj-vtoclg 33428). (Contributed by BJ, 2-Jul-2022.) (Proof modification is discouraged.)
⊢ (𝐴 ∈ 𝑉 → ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝜑)))
20.14.5.8  Class abstractions A few additional theorems on class abstractions and restricted class abstractions.
Theorem	bj-unrab 33439*	Generalization of unrab 4127. Equality need not hold. (Contributed by BJ, 21-Apr-2019.)
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∪ {𝑥 ∈ 𝐵 ∣ 𝜓}) ⊆ {𝑥 ∈ (𝐴 ∪ 𝐵) ∣ (𝜑 ∨ 𝜓)}
Theorem	bj-inrab 33440	Generalization of inrab 4128. (Contributed by BJ, 21-Apr-2019.)
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ {𝑥 ∈ 𝐵 ∣ 𝜓}) = {𝑥 ∈ (𝐴 ∩ 𝐵) ∣ (𝜑 ∧ 𝜓)}
Theorem	bj-inrab2 33441	Shorter proof of inrab 4128. (Contributed by BJ, 21-Apr-2019.) (Proof modification is discouraged.)
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ {𝑥 ∈ 𝐴 ∣ 𝜓}) = {𝑥 ∈ 𝐴 ∣ (𝜑 ∧ 𝜓)}
Theorem	bj-inrab3 33442*	Generalization of dfrab3ss 4134, which it may shorten. (Contributed by BJ, 21-Apr-2019.) (Revised by OpenAI, 7-Jul-2020.)
⊢ (𝐴 ∩ {𝑥 ∈ 𝐵 ∣ 𝜑}) = ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ 𝐵)
Theorem	bj-rabtr 33443*	Restricted class abstraction with true formula. (Contributed by BJ, 22-Apr-2019.)
⊢ {𝑥 ∈ 𝐴 ∣ ⊤} = 𝐴
Theorem	bj-rabtrALT 33444*	Alternate proof of bj-rabtr 33443. (Contributed by BJ, 22-Apr-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ {𝑥 ∈ 𝐴 ∣ ⊤} = 𝐴
Theorem	bj-rabtrAUTO 33445*	Proof of bj-rabtr 33443 found automatically by "MM-PA> IMPROVE ALL / DEPTH 3 / 3" followed by "MM-PA> MINIMIZEWITH *". (Contributed by BJ, 22-Apr-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ {𝑥 ∈ 𝐴 ∣ ⊤} = 𝐴
20.14.5.9  Restricted non-freeness In this subsection, we define restricted non-freeness (or relative non-freeness).
Syntax	wrnf 33446	Syntax for restricted non-freeness.
wff Ⅎ𝑥 ∈ 𝐴𝜑
Definition	df-bj-rnf 33447	Definition of restricted non-freeness. Informally, the proposition Ⅎ𝑥 ∈ 𝐴𝜑 means that 𝜑(𝑥) does not vary on 𝐴. (Contributed by BJ, 19-Mar-2021.)
⊢ (Ⅎ𝑥 ∈ 𝐴𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜑))
20.14.5.10  Russell's paradox A few results around Russell's paradox. For clarity, we prove separately its FOL part (bj-ru0 33448) and then two versions (bj-ru1 33449 and bj-ru 33450). Special attention is put on minimizing axiom depencencies.
Theorem	bj-ru0 33448*	The FOL part of Russell's paradox ru 3661 (see also bj-ru1 33449, bj-ru 33450). Use of elequ1 2171, bj-elequ12 33196, bj-spvv 33250 (instead of eleq1 2894, eleq12d 2900, spv 2413 as in ru 3661) permits to remove dependency on ax-10 2192, ax-11 2207, ax-12 2220, ax-13 2389, ax-ext 2803, df-sb 2068, df-clab 2812, df-cleq 2818, df-clel 2821. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.)
⊢ ¬ ∀𝑥(𝑥 ∈ 𝑦 ↔ ¬ 𝑥 ∈ 𝑥)
Theorem	bj-ru1 33449*	A version of Russell's paradox ru 3661 (see also bj-ru 33450). Note the more economical use of bj-abeq2 33291 instead of abeq2 2937 to avoid dependency on ax-13 2389. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.)
⊢ ¬ ∃𝑦 𝑦 = {𝑥 ∣ ¬ 𝑥 ∈ 𝑥}
Theorem	bj-ru 33450	Remove dependency on ax-13 2389 (and df-v 3416) from Russell's paradox ru 3661 expressed with primitive symbols and with a class variable 𝑉 (note that axsep2 5006 does require ax-8 2166 and ax-9 2173 since it requires df-clel 2821 and df-cleq 2818--- see bj-df-clel 33402 and bj-df-cleq 33407). Note the more economical use of bj-elissetv 33374 instead of isset 3424 to avoid use of df-v 3416. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.)
⊢ ¬ {𝑥 ∣ ¬ 𝑥 ∈ 𝑥} ∈ 𝑉
20.14.5.11  Some disjointness results A few utility theorems on disjointness of classes.
Theorem	bj-n0i 33451*	Inference associated with n0 4160. Shortens 2ndcdisj 21630 (2888>2878), notzfaus 5062 (264>253). (Contributed by BJ, 22-Apr-2019.)
⊢ 𝐴 ≠ ∅    ⇒   ⊢ ∃𝑥 𝑥 ∈ 𝐴
Theorem	bj-disjcsn 33452	A class is disjoint from its singleton. A consequence of regularity. Shorter proof than bnj521 31341 and does not depend on df-ne 3000. (Contributed by BJ, 4-Apr-2019.)
⊢ (𝐴 ∩ {𝐴}) = ∅
Theorem	bj-disjsn01 33453	Disjointness of the singletons containing 0 and 1. This is a consequence of bj-disjcsn 33452 but the present proof does not use regularity. (Contributed by BJ, 4-Apr-2019.) (Proof modification is discouraged.)
⊢ ({∅} ∩ {1o}) = ∅
Theorem	bj-2ex 33454	2o is a set. (Contributed by BJ, 6-Apr-2019.)
⊢ 2o ∈ V
Theorem	bj-0nel1 33455	The empty set does not belong to {1o}. (Contributed by BJ, 6-Apr-2019.)
⊢ ∅ ∉ {1o}
Theorem	bj-1nel0 33456	1o does not belong to {∅}. (Contributed by BJ, 6-Apr-2019.)
⊢ 1o ∉ {∅}
20.14.5.12  Complements on direct products A few utility theorems on direct products.
Theorem	bj-xpimasn 33457	The image of a singleton, general case. [Change and relabel xpimasn 5820 accordingly, maybe to xpima2sn.] (Contributed by BJ, 6-Apr-2019.)
⊢ ((𝐴 × 𝐵) “ {𝑋}) = if(𝑋 ∈ 𝐴, 𝐵, ∅)
Theorem	bj-xpima1sn 33458	The image of a singleton by a direct product, empty case. [Change and relabel xpimasn 5820 accordingly, maybe to xpima2sn.] (Contributed by BJ, 6-Apr-2019.)
⊢ (𝑋 ∉ 𝐴 → ((𝐴 × 𝐵) “ {𝑋}) = ∅)
Theorem	bj-xpima1snALT 33459	Alternate proof of bj-xpima1sn 33458. (Contributed by BJ, 6-Apr-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑋 ∉ 𝐴 → ((𝐴 × 𝐵) “ {𝑋}) = ∅)
Theorem	bj-xpima2sn 33460	The image of a singleton by a direct product, nonempty case. [To replace xpimasn 5820] (Contributed by BJ, 6-Apr-2019.) (Proof modification is discouraged.)
⊢ (𝑋 ∈ 𝐴 → ((𝐴 × 𝐵) “ {𝑋}) = 𝐵)
Theorem	bj-xpnzex 33461	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 7370 (up to commutation in the product). (Contributed by BJ, 6-Oct-2018.) (Proof modification is discouraged.)
⊢ (𝐴 ≠ ∅ → ((𝐴 × 𝐵) ∈ 𝑉 → 𝐵 ∈ V))
Theorem	bj-xpexg2 33462	Curried (exported) form of xpexg 7220. (Contributed by BJ, 2-Apr-2019.)
⊢ (𝐴 ∈ 𝑉 → (𝐵 ∈ 𝑊 → (𝐴 × 𝐵) ∈ V))
Theorem	bj-xpnzexb 33463	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 33464*	Substitution property for certain classes. (Contributed by BJ, 2-Apr-2019.)
⊢ (𝐴 = 𝐵 → {𝑥 ∣ {𝑥} ∈ (𝐴 “ 𝐶)} = {𝑥 ∣ {𝑥} ∈ (𝐵 “ 𝐶)})
20.14.5.13  "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-sels 33465*	If a class is a set, then it is a member of a set. (Contributed by BJ, 3-Apr-2019.)
⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝐴 ∈ 𝑥)
Theorem	bj-snsetex 33466*	The class of sets "whose singletons" belong to a set is a set. Nice application of ax-rep 4994. (Contributed by BJ, 6-Oct-2018.)
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V)
Theorem	bj-clex 33467*	Sethood of certain classes. (Contributed by BJ, 2-Apr-2019.)
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∣ {𝑥} ∈ (𝐴 “ 𝐵)} ∈ V)
Syntax	bj-csngl 33468	Syntax for singletonization. (Contributed by BJ, 6-Oct-2018.)
class sngl 𝐴
Definition	df-bj-sngl 33469*	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 33470	Substitution property for sngl. (Contributed by BJ, 6-Oct-2018.)
⊢ (𝐴 = 𝐵 → sngl 𝐴 = sngl 𝐵)
Theorem	bj-elsngl 33471*	Characterization of the elements of the singletonization of a class. (Contributed by BJ, 6-Oct-2018.)
⊢ (𝐴 ∈ sngl 𝐵 ↔ ∃𝑥 ∈ 𝐵 𝐴 = {𝑥})
Theorem	bj-snglc 33472	Characterization of the elements of 𝐴 in terms of elements of its singletonization. (Contributed by BJ, 6-Oct-2018.)
⊢ (𝐴 ∈ 𝐵 ↔ {𝐴} ∈ sngl 𝐵)
Theorem	bj-snglss 33473	The singletonization of a class is included in its powerclass. (Contributed by BJ, 6-Oct-2018.)
⊢ sngl 𝐴 ⊆ 𝒫 𝐴
Theorem	bj-0nelsngl 33474	The empty set is not a member of a singletonization (neither is any nonsingleton, in particular any von Neuman ordinal except possibly df-1o 7826). (Contributed by BJ, 6-Oct-2018.)
⊢ ∅ ∉ sngl 𝐴
Theorem	bj-snglinv 33475*	Inverse of singletonization. (Contributed by BJ, 6-Oct-2018.)
⊢ 𝐴 = {𝑥 ∣ {𝑥} ∈ sngl 𝐴}
Theorem	bj-snglex 33476	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 33477	Syntax for the tagged copy of a class. (Contributed by BJ, 6-Oct-2018.)
class tag 𝐴
Definition	df-bj-tag 33478	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 33479	Substitution property for tag. (Contributed by BJ, 6-Oct-2018.)
⊢ (𝐴 = 𝐵 → tag 𝐴 = tag 𝐵)
Theorem	bj-eltag 33480*	Characterization of the elements of the tagging of a class. (Contributed by BJ, 6-Oct-2018.)
⊢ (𝐴 ∈ tag 𝐵 ↔ (∃𝑥 ∈ 𝐵 𝐴 = {𝑥} ∨ 𝐴 = ∅))
Theorem	bj-0eltag 33481	The empty set belongs to the tagging of a class. (Contributed by BJ, 6-Apr-2019.)
⊢ ∅ ∈ tag 𝐴
Theorem	bj-tagn0 33482	The tagging of a class is nonempty. (Contributed by BJ, 6-Apr-2019.)
⊢ tag 𝐴 ≠ ∅
Theorem	bj-tagss 33483	The tagging of a class is included in its powerclass. (Contributed by BJ, 6-Oct-2018.)
⊢ tag 𝐴 ⊆ 𝒫 𝐴
Theorem	bj-snglsstag 33484	The singletonization is included in the tagging. (Contributed by BJ, 6-Oct-2018.)
⊢ sngl 𝐴 ⊆ tag 𝐴
Theorem	bj-sngltagi 33485	The singletonization is included in the tagging. (Contributed by BJ, 6-Oct-2018.)
⊢ (𝐴 ∈ sngl 𝐵 → 𝐴 ∈ tag 𝐵)
Theorem	bj-sngltag 33486	The singletonization and the tagging of a set contain the same singletons. (Contributed by BJ, 6-Oct-2018.)
⊢ (𝐴 ∈ 𝑉 → ({𝐴} ∈ sngl 𝐵 ↔ {𝐴} ∈ tag 𝐵))
Theorem	bj-tagci 33487	Characterization of the elements of 𝐵 in terms of elements of its tagged version. (Contributed by BJ, 6-Oct-2018.)
⊢ (𝐴 ∈ 𝐵 → {𝐴} ∈ tag 𝐵)
Theorem	bj-tagcg 33488	Characterization of the elements of 𝐵 in terms of elements of its tagged version. (Contributed by BJ, 6-Oct-2018.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ {𝐴} ∈ tag 𝐵))
Theorem	bj-taginv 33489*	Inverse of tagging. (Contributed by BJ, 6-Oct-2018.)
⊢ 𝐴 = {𝑥 ∣ {𝑥} ∈ tag 𝐴}
Theorem	bj-tagex 33490	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 33491	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 33492	The product of a set and the tagging of a set is a set. (Contributed by BJ, 2-Apr-2019.)
⊢ (𝐴 ∈ 𝑉 → (𝐵 ∈ 𝑊 → (𝐴 × tag 𝐵) ∈ V))
20.14.5.14  Tuples of classes This subsection gives a definition of an ordered pair, or couple (2-tuple), which "works" for proper classes, as evidenced by Theorems bj-2uplth 33524 and bj-2uplex 33525 (but more importantly, bj-pr21val 33516 and bj-pr22val 33522). 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 33525 has advantages: in view of df-br 4874, several sethood antecedents could be removed from existing theorems. For instance, relsnopg 5461 (resp. relsnop 5463) would hold without antecedents (resp. hypotheses) thanks to relsnb 5460). Similarly, df-struct 16224 could be simplified with the exception of the empty set removed. 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 Kuratowksi definition (df-op 4404) as a preliminary definition, and then "redefines" a couple. It could also use the "short" version of the Kuratowski pair (see opthreg 8790) 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 5400, but here we use "tagged versions" of the factors (see df-bj-tag 33478) 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 2-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)
Syntax	bj-cproj 33493	Syntax for the class projection. (Contributed by BJ, 6-Apr-2019.)
class (𝐴 Proj 𝐵)
Definition	df-bj-proj 33494*	Definition of the class projection corresponding to tagged tuples. The expression (𝐴 Proj 𝐵) denotes the projection on the A^th component. (Contributed by BJ, 6-Apr-2019.) (New usage is discouraged.)
⊢ (𝐴 Proj 𝐵) = {𝑥 ∣ {𝑥} ∈ (𝐵 “ {𝐴})}
Theorem	bj-projeq 33495	Substitution property for Proj. (Contributed by BJ, 6-Apr-2019.)
⊢ (𝐴 = 𝐶 → (𝐵 = 𝐷 → (𝐴 Proj 𝐵) = (𝐶 Proj 𝐷)))
Theorem	bj-projeq2 33496	Substitution property for Proj. (Contributed by BJ, 6-Apr-2019.)
⊢ (𝐵 = 𝐶 → (𝐴 Proj 𝐵) = (𝐴 Proj 𝐶))
Theorem	bj-projun 33497	The class projection on a given component preserves unions. (Contributed by BJ, 6-Apr-2019.)
⊢ (𝐴 Proj (𝐵 ∪ 𝐶)) = ((𝐴 Proj 𝐵) ∪ (𝐴 Proj 𝐶))
Theorem	bj-projex 33498	Sethood of the class projection. (Contributed by BJ, 6-Apr-2019.)
⊢ (𝐵 ∈ 𝑉 → (𝐴 Proj 𝐵) ∈ V)
Theorem	bj-projval 33499	Value of the class projection. (Contributed by BJ, 6-Apr-2019.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 Proj ({𝐵} × tag 𝐶)) = if(𝐵 = 𝐴, 𝐶, ∅))
Syntax	bj-c1upl 33500	Syntax for Morse monuple. (Contributed by BJ, 6-Apr-2019.)
class ⦅𝐴⦆