P. 380 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 37901-38000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	curryset 37901*	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 37905. (Contributed by BJ, 23-Sep-2023.) This proof is intuitionistically valid. (Proof modification is discouraged.)
⊢ ¬ {𝑥 ∣ (𝑥 ∈ 𝑥 → 𝜑)} ∈ 𝑉
Theorem	currysetlem1 37902*	Lemma for currysetALT 37905. (Contributed by BJ, 23-Sep-2023.) This proof is intuitionistically valid. (Proof modification is discouraged.)
⊢ 𝑋 = {𝑥 ∣ (𝑥 ∈ 𝑥 → 𝜑)}    ⇒   ⊢ (𝑋 ∈ 𝑉 → (𝑋 ∈ 𝑋 ↔ (𝑋 ∈ 𝑋 → 𝜑)))
Theorem	currysetlem2 37903*	Lemma for currysetALT 37905. (Contributed by BJ, 23-Sep-2023.) This proof is intuitionistically valid. (Proof modification is discouraged.)
⊢ 𝑋 = {𝑥 ∣ (𝑥 ∈ 𝑥 → 𝜑)}    ⇒   ⊢ (𝑋 ∈ 𝑉 → (𝑋 ∈ 𝑋 → 𝜑))
Theorem	currysetlem3 37904*	Lemma for currysetALT 37905. (Contributed by BJ, 23-Sep-2023.) This proof is intuitionistically valid. (Proof modification is discouraged.)
⊢ 𝑋 = {𝑥 ∣ (𝑥 ∈ 𝑥 → 𝜑)}    ⇒   ⊢ ¬ 𝑋 ∈ 𝑉
Theorem	currysetALT 37905*	Alternate proof of curryset 37901, 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.20.5.12  Some disjointness results A few utility theorems on disjointness of classes.
Theorem	bj-n0i 37906*	Inference associated with n0 4299. Shortens 2ndcdisj 23775 (2888>2878), notsep 5324 (264>253). (Contributed by BJ, 22-Apr-2019.)
⊢ 𝐴 ≠ ∅    ⇒   ⊢ ∃𝑥 𝑥 ∈ 𝐴
Theorem	bj-disjsn01 37907	Disjointness of the singletons containing 0 and 1. This is a consequence of disjcsn 9604 but the present proof does not use regularity. (Contributed by BJ, 4-Apr-2019.) (Proof modification is discouraged.)
⊢ ({∅} ∩ {1o}) = ∅
Theorem	bj-0nel1 37908	The empty set does not belong to {1o}. (Contributed by BJ, 6-Apr-2019.)
⊢ ∅ ∉ {1o}
Theorem	bj-1nel0 37909	1o does not belong to {∅}. (Contributed by BJ, 6-Apr-2019.)
⊢ 1o ∉ {∅}
21.20.5.13  Complements on direct products A few utility theorems on direct products.
Theorem	bj-xpimasn 37910	The image of a singleton, general case. [Change and relabel xpimasn 6176 accordingly, maybe to xpima2sn.] (Contributed by BJ, 6-Apr-2019.)
⊢ ((𝐴 × 𝐵) “ {𝑋}) = if(𝑋 ∈ 𝐴, 𝐵, ∅)
Theorem	bj-xpima1sn 37911	The image of a singleton by a direct product, empty case. [Change and relabel xpimasn 6176 accordingly, maybe to xpima2sn.] (Contributed by BJ, 6-Apr-2019.)
⊢ (¬ 𝑋 ∈ 𝐴 → ((𝐴 × 𝐵) “ {𝑋}) = ∅)
Theorem	bj-xpima1snALT 37912	Alternate proof of bj-xpima1sn 37911. (Contributed by BJ, 6-Apr-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ 𝑋 ∈ 𝐴 → ((𝐴 × 𝐵) “ {𝑋}) = ∅)
Theorem	bj-xpima2sn 37913	The image of a singleton by a direct product, nonempty case. [To replace xpimasn 6176.] (Contributed by BJ, 6-Apr-2019.) (Proof modification is discouraged.)
⊢ (𝑋 ∈ 𝐴 → ((𝐴 × 𝐵) “ {𝑋}) = 𝐵)
Theorem	bj-xpnzex 37914	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 7932 (up to commutation in the product). (Contributed by BJ, 6-Oct-2018.) (Proof modification is discouraged.)
⊢ (𝐴 ≠ ∅ → ((𝐴 × 𝐵) ∈ 𝑉 → 𝐵 ∈ V))
Theorem	bj-xpexg2 37915	Curried (exported) form of xpexg 7764. (Contributed by BJ, 2-Apr-2019.)
⊢ (𝐴 ∈ 𝑉 → (𝐵 ∈ 𝑊 → (𝐴 × 𝐵) ∈ V))
Theorem	bj-xpnzexb 37916	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 37917*	Substitution property for certain classes. (Contributed by BJ, 2-Apr-2019.)
⊢ (𝐴 = 𝐵 → {𝑥 ∣ {𝑥} ∈ (𝐴 “ 𝐶)} = {𝑥 ∣ {𝑥} ∈ (𝐵 “ 𝐶)})
21.20.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 37918*	The class of sets "whose singletons" belong to a set is a set. Nice application of ax-rep 5231. (Contributed by BJ, 6-Oct-2018.)
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V)
Theorem	bj-clexab 37919*	Sethood of certain classes. (Contributed by BJ, 2-Apr-2019.)
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∣ {𝑥} ∈ (𝐴 “ 𝐵)} ∈ V)
Syntax	bj-csngl 37920	Syntax for singletonization. (Contributed by BJ, 6-Oct-2018.)
class sngl 𝐴
Definition	df-bj-sngl 37921*	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 37922	Substitution property for sngl. (Contributed by BJ, 6-Oct-2018.)
⊢ (𝐴 = 𝐵 → sngl 𝐴 = sngl 𝐵)
Theorem	bj-elsngl 37923*	Characterization of the elements of the singletonization of a class. (Contributed by BJ, 6-Oct-2018.)
⊢ (𝐴 ∈ sngl 𝐵 ↔ ∃𝑥 ∈ 𝐵 𝐴 = {𝑥})
Theorem	bj-snglc 37924	Characterization of the elements of 𝐴 in terms of elements of its singletonization. (Contributed by BJ, 6-Oct-2018.)
⊢ (𝐴 ∈ 𝐵 ↔ {𝐴} ∈ sngl 𝐵)
Theorem	bj-snglss 37925	The singletonization of a class is included in its powerclass. (Contributed by BJ, 6-Oct-2018.)
⊢ sngl 𝐴 ⊆ 𝒫 𝐴
Theorem	bj-0nelsngl 37926	The empty set is not a member of a singletonization (neither is any nonsingleton, in particular any von Neuman ordinal except possibly df-1o 8476). (Contributed by BJ, 6-Oct-2018.)
⊢ ∅ ∉ sngl 𝐴
Theorem	bj-snglinv 37927*	Inverse of singletonization. (Contributed by BJ, 6-Oct-2018.)
⊢ 𝐴 = {𝑥 ∣ {𝑥} ∈ sngl 𝐴}
Theorem	bj-snglex 37928	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 37929	Syntax for the tagged copy of a class. (Contributed by BJ, 6-Oct-2018.)
class tag 𝐴
Definition	df-bj-tag 37930	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 37931	Substitution property for tag. (Contributed by BJ, 6-Oct-2018.)
⊢ (𝐴 = 𝐵 → tag 𝐴 = tag 𝐵)
Theorem	bj-eltag 37932*	Characterization of the elements of the tagging of a class. (Contributed by BJ, 6-Oct-2018.)
⊢ (𝐴 ∈ tag 𝐵 ↔ (∃𝑥 ∈ 𝐵 𝐴 = {𝑥} ∨ 𝐴 = ∅))
Theorem	bj-0eltag 37933	The empty set belongs to the tagging of a class. (Contributed by BJ, 6-Apr-2019.)
⊢ ∅ ∈ tag 𝐴
Theorem	bj-tagn0 37934	The tagging of a class is nonempty. (Contributed by BJ, 6-Apr-2019.)
⊢ tag 𝐴 ≠ ∅
Theorem	bj-tagss 37935	The tagging of a class is included in its powerclass. (Contributed by BJ, 6-Oct-2018.)
⊢ tag 𝐴 ⊆ 𝒫 𝐴
Theorem	bj-snglsstag 37936	The singletonization is included in the tagging. (Contributed by BJ, 6-Oct-2018.)
⊢ sngl 𝐴 ⊆ tag 𝐴
Theorem	bj-sngltagi 37937	The singletonization is included in the tagging. (Contributed by BJ, 6-Oct-2018.)
⊢ (𝐴 ∈ sngl 𝐵 → 𝐴 ∈ tag 𝐵)
Theorem	bj-sngltag 37938	The singletonization and the tagging of a set contain the same singletons. (Contributed by BJ, 6-Oct-2018.)
⊢ (𝐴 ∈ 𝑉 → ({𝐴} ∈ sngl 𝐵 ↔ {𝐴} ∈ tag 𝐵))
Theorem	bj-tagci 37939	Characterization of the elements of 𝐵 in terms of elements of its tagged version. (Contributed by BJ, 6-Oct-2018.)
⊢ (𝐴 ∈ 𝐵 → {𝐴} ∈ tag 𝐵)
Theorem	bj-tagcg 37940	Characterization of the elements of 𝐵 in terms of elements of its tagged version. (Contributed by BJ, 6-Oct-2018.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ {𝐴} ∈ tag 𝐵))
Theorem	bj-taginv 37941*	Inverse of tagging. (Contributed by BJ, 6-Oct-2018.)
⊢ 𝐴 = {𝑥 ∣ {𝑥} ∈ tag 𝐴}
Theorem	bj-tagex 37942	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 37943	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 37944	The product of a set and the tagging of a set is a set. (Contributed by BJ, 2-Apr-2019.)
⊢ (𝐴 ∈ 𝑉 → (𝐵 ∈ 𝑊 → (𝐴 × tag 𝐵) ∈ V))
21.20.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 37976 and bj-2uplex 37977, and more importantly, bj-pr21val 37968 and bj-pr22val 37974. 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 37977 has advantages: in view of df-br 5103, several sethood antecedents could be removed from existing theorems. For instance, relsnopg 5780 (resp. relsnop 5782) would hold without antecedents (resp. hypotheses) thanks to relsnb 5779). Also, the antecedent Rel 𝑅 could be removed from brrelex12 5702 and related theorems brrelex*, and, as a consequence, of multiple later theorems. Similarly, df-struct 17325 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 ⦅𝐴, 𝐵⦆. This definition uses the Kuratowski definition (df-op 4590) as a preliminary definition, and then "redefines" a couple. It could also use the "short" version of the Kuratowski pair (see opthreg 9619) 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). This extends in a natural way to tuples. A variation of this definition is justified in opthprc 5714, but here we use "tagged versions" of the factors (see df-bj-tag 37930) 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 37930)
Syntax	bj-cproj 37945	Syntax for the class projection. (Contributed by BJ, 6-Apr-2019.)
class (𝐴 Proj 𝐵)
Definition	df-bj-proj 37946*	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 37947	Substitution property for Proj. (Contributed by BJ, 6-Apr-2019.)
⊢ (𝐴 = 𝐶 → (𝐵 = 𝐷 → (𝐴 Proj 𝐵) = (𝐶 Proj 𝐷)))
Theorem	bj-projeq2 37948	Substitution property for Proj. (Contributed by BJ, 6-Apr-2019.)
⊢ (𝐵 = 𝐶 → (𝐴 Proj 𝐵) = (𝐴 Proj 𝐶))
Theorem	bj-projun 37949	The class projection on a given component preserves unions. (Contributed by BJ, 6-Apr-2019.)
⊢ (𝐴 Proj (𝐵 ∪ 𝐶)) = ((𝐴 Proj 𝐵) ∪ (𝐴 Proj 𝐶))
Theorem	bj-projex 37950	Sethood of the class projection. (Contributed by BJ, 6-Apr-2019.)
⊢ (𝐵 ∈ 𝑉 → (𝐴 Proj 𝐵) ∈ V)
Theorem	bj-projval 37951	Value of the class projection. (Contributed by BJ, 6-Apr-2019.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 Proj ({𝐵} × tag 𝐶)) = if(𝐵 = 𝐴, 𝐶, ∅))
Syntax	bj-c1upl 37952	Syntax for Morse monuple. (Contributed by BJ, 6-Apr-2019.)
class ⦅𝐴⦆
Definition	df-bj-1upl 37953	Definition of the Morse monuple (1-tuple). This is not useful per se, but is used as a step towards the definition of couples (2-tuples, or ordered pairs). The reason for "tagging" the set is so that an m-tuple and an n-tuple be equal only when m = n. With this definition, the 0-tuple is the empty set. New usage is discouraged because the precise definition is generally unimportant compared to the characteristic properties bj-2upleq 37967, bj-2uplth 37976, bj-2uplex 37977, and the properties of the projections (see df-bj-pr1 37956 and df-bj-pr2 37970). (Contributed by BJ, 6-Apr-2019.) (New usage is discouraged.)
⊢ ⦅𝐴⦆ = ({∅} × tag 𝐴)
Theorem	bj-1upleq 37954	Substitution property for ⦅ − ⦆. (Contributed by BJ, 6-Apr-2019.)
⊢ (𝐴 = 𝐵 → ⦅𝐴⦆ = ⦅𝐵⦆)
Syntax	bj-cpr1 37955	Syntax for the first class tuple projection. (Contributed by BJ, 6-Apr-2019.)
class pr1 𝐴
Definition	df-bj-pr1 37956	Definition of the first projection of a class tuple. New usage is discouraged because the precise definition is generally unimportant compared to the characteristic properties bj-pr1eq 37957, bj-pr11val 37960, bj-pr21val 37968, bj-pr1ex 37961. (Contributed by BJ, 6-Apr-2019.) (New usage is discouraged.)
⊢ pr1 𝐴 = (∅ Proj 𝐴)
Theorem	bj-pr1eq 37957	Substitution property for pr1. (Contributed by BJ, 6-Apr-2019.)
⊢ (𝐴 = 𝐵 → pr1 𝐴 = pr1 𝐵)
Theorem	bj-pr1un 37958	The first projection preserves unions. (Contributed by BJ, 6-Apr-2019.)
⊢ pr1 (𝐴 ∪ 𝐵) = (pr1 𝐴 ∪ pr1 𝐵)
Theorem	bj-pr1val 37959	Value of the first projection. (Contributed by BJ, 6-Apr-2019.)
⊢ pr1 ({𝐴} × tag 𝐵) = if(𝐴 = ∅, 𝐵, ∅)
Theorem	bj-pr11val 37960	Value of the first projection of a monuple. (Contributed by BJ, 6-Apr-2019.)
⊢ pr1 ⦅𝐴⦆ = 𝐴
Theorem	bj-pr1ex 37961	Sethood of the first projection. (Contributed by BJ, 6-Oct-2018.)
⊢ (𝐴 ∈ 𝑉 → pr1 𝐴 ∈ V)
Theorem	bj-1uplth 37962	The characteristic property of monuples. This holds without sethood hypotheses. (Contributed by BJ, 6-Apr-2019.)
⊢ (⦅𝐴⦆ = ⦅𝐵⦆ ↔ 𝐴 = 𝐵)
Theorem	bj-1uplex 37963	A monuple is a set if and only if its coordinates are sets. (Contributed by BJ, 6-Apr-2019.)
⊢ (⦅𝐴⦆ ∈ V ↔ 𝐴 ∈ V)
Theorem	bj-1upln0 37964	A monuple is nonempty. (Contributed by BJ, 6-Apr-2019.)
⊢ ⦅𝐴⦆ ≠ ∅
Syntax	bj-c2uple 37965	Syntax for Morse couple. (Contributed by BJ, 6-Oct-2018.)
class ⦅𝐴, 𝐵⦆
Definition	df-bj-2upl 37966	Definition of the Morse couple. See df-bj-1upl 37953. New usage is discouraged because the precise definition is generally unimportant compared to the characteristic properties bj-2upleq 37967, bj-2uplth 37976, bj-2uplex 37977, and the properties of the projections (see df-bj-pr1 37956 and df-bj-pr2 37970). (Contributed by BJ, 6-Oct-2018.) (New usage is discouraged.)
⊢ ⦅𝐴, 𝐵⦆ = (⦅𝐴⦆ ∪ ({1o} × tag 𝐵))
Theorem	bj-2upleq 37967	Substitution property for ⦅ − , − ⦆. (Contributed by BJ, 6-Oct-2018.)
⊢ (𝐴 = 𝐵 → (𝐶 = 𝐷 → ⦅𝐴, 𝐶⦆ = ⦅𝐵, 𝐷⦆))
Theorem	bj-pr21val 37968	Value of the first projection of a couple. (Contributed by BJ, 6-Oct-2018.)
⊢ pr1 ⦅𝐴, 𝐵⦆ = 𝐴
Syntax	bj-cpr2 37969	Syntax for the second class tuple projection. (Contributed by BJ, 6-Oct-2018.)
class pr2 𝐴
Definition	df-bj-pr2 37970	Definition of the second projection of a class tuple. New usage is discouraged because the precise definition is generally unimportant compared to the characteristic properties bj-pr2eq 37971, bj-pr22val 37974, bj-pr2ex 37975. (Contributed by BJ, 6-Oct-2018.) (New usage is discouraged.)
⊢ pr2 𝐴 = (1o Proj 𝐴)
Theorem	bj-pr2eq 37971	Substitution property for pr2. (Contributed by BJ, 6-Oct-2018.)
⊢ (𝐴 = 𝐵 → pr2 𝐴 = pr2 𝐵)
Theorem	bj-pr2un 37972	The second projection preserves unions. (Contributed by BJ, 6-Apr-2019.)
⊢ pr2 (𝐴 ∪ 𝐵) = (pr2 𝐴 ∪ pr2 𝐵)
Theorem	bj-pr2val 37973	Value of the second projection. (Contributed by BJ, 6-Apr-2019.)
⊢ pr2 ({𝐴} × tag 𝐵) = if(𝐴 = 1o, 𝐵, ∅)
Theorem	bj-pr22val 37974	Value of the second projection of a couple. (Contributed by BJ, 6-Oct-2018.)
⊢ pr2 ⦅𝐴, 𝐵⦆ = 𝐵
Theorem	bj-pr2ex 37975	Sethood of the second projection. (Contributed by BJ, 6-Oct-2018.)
⊢ (𝐴 ∈ 𝑉 → pr2 𝐴 ∈ V)
Theorem	bj-2uplth 37976	The characteristic property of couples. This holds without sethood hypotheses (compare opth 5444). (Contributed by BJ, 6-Oct-2018.)
⊢ (⦅𝐴, 𝐵⦆ = ⦅𝐶, 𝐷⦆ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))
Theorem	bj-2uplex 37977	A couple is a set if and only if its coordinates are sets. For the advantages offered by the reverse closure property, see the section head comment. (Contributed by BJ, 6-Oct-2018.)
⊢ (⦅𝐴, 𝐵⦆ ∈ V ↔ (𝐴 ∈ V ∧ 𝐵 ∈ V))
Theorem	bj-2upln0 37978	A couple is nonempty. (Contributed by BJ, 21-Apr-2019.)
⊢ ⦅𝐴, 𝐵⦆ ≠ ∅
Theorem	bj-2upln1upl 37979	A couple is never equal to a monuple. It is in order to have this "non-clashing" result that tagging was used. Without tagging, we would have ⦅𝐴, ∅⦆ = ⦅𝐴⦆. In the context of Morse tuples, it is natural to define the 0-tuple as the empty set. Therefore, the present theorem together with bj-1upln0 37964 and bj-2upln0 37978 tell us that an m-tuple may equal an n-tuple only when m = n, at least for m, n <= 2, but this result would extend as soon as we define n-tuples for higher values of n. (Contributed by BJ, 21-Apr-2019.)
⊢ ⦅𝐴, 𝐵⦆ ≠ ⦅𝐶⦆
21.20.5.16  Set theory: elementary operations relative to a universe Some elementary set-theoretic operations "relative to a universe" (by which is merely meant some given class considered as a universe).
Theorem	bj-rcleqf 37980	Relative version of cleqf 2950. (Contributed by BJ, 27-Dec-2023.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ Ⅎ𝑥𝑉    ⇒   ⊢ ((𝑉 ∩ 𝐴) = (𝑉 ∩ 𝐵) ↔ ∀𝑥 ∈ 𝑉 (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
Theorem	bj-rcleq 37981*	Relative version of dfcleq 2753. (Contributed by BJ, 27-Dec-2023.)
⊢ ((𝑉 ∩ 𝐴) = (𝑉 ∩ 𝐵) ↔ ∀𝑥 ∈ 𝑉 (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
Theorem	bj-reabeq 37982*	Relative form of eqabb 2899. (Contributed by BJ, 27-Dec-2023.)
⊢ ((𝑉 ∩ 𝐴) = {𝑥 ∈ 𝑉 ∣ 𝜑} ↔ ∀𝑥 ∈ 𝑉 (𝑥 ∈ 𝐴 ↔ 𝜑))
Theorem	bj-disj2r 37983	Relative version of ssdifin0 4440, allowing a biconditional, and of disj2 4410. (Contributed by BJ, 11-Nov-2021.) This proof does not rely, even indirectly, on ssdifin0 4440 nor disj2 4410. (Proof modification is discouraged.)
⊢ ((𝐴 ∩ 𝑉) ⊆ (𝑉 ∖ 𝐵) ↔ ((𝐴 ∩ 𝐵) ∩ 𝑉) = ∅)
Theorem	bj-sscon 37984	Contraposition law for relative subclasses. Relative and generalized version of ssconb 4078. Shortens ssconb 4078, conss2 45468. (Contributed by BJ, 11-Nov-2021.) This proof does not rely, even indirectly, on ssconb 4078 nor conss2 45468. (Proof modification is discouraged.)
⊢ ((𝐴 ∩ 𝑉) ⊆ (𝑉 ∖ 𝐵) ↔ (𝐵 ∩ 𝑉) ⊆ (𝑉 ∖ 𝐴))
21.20.5.17  Axioms for finite unions In this section, we introduce the axiom of singleton ax-bj-sn 37988 and the axiom of binary union ax-bj-bun 37992. Both axioms are implied by the standard axioms of unordered pair ax-pr 5390 and of union ax-un 7751 (see snex 5396 and unex 7761). Conversely, the axiom of unordered pair ax-pr 5390 is implied by the axioms of singleton and of binary union, as proved in bj-prexg 37994 and bj-prex 37995. The axioms of union ax-un 7751 and of powerset ax-pow 5326 are independent of these axioms: consider respectively the class of pseudo-hereditarily sets of cardinality less than a given singular strong limit cardinal, see Greg Oman, On the axiom of union, Arch. Math. Logic (2010) 49:283--289 (that model does have finite unions), and the class of well-founded hereditarily countable sets (or hereditarily less than a given uncountable regular cardinal). See also https://mathoverflow.net/questions/81815 5326 and https://mathoverflow.net/questions/48365 5326. A proof by finite induction shows that the existence of finite unions is equivalent to the existence of binary unions and of nullary unions (the latter being the axiom of the empty set ax-nul 5259). The axiom of binary union is useful in theories without the axioms of union ax-un 7751 and of powerset ax-pow 5326. For instance, the class of well-founded sets hereditarily of cardinality at most 𝑛 ∈ ℕ0 with ordinary membership relation is a model of { ax-ext 2732, ax-rep 5231, ax-sep 5248, ax-nul 5259, ax-reg 9586 } and the axioms of existence of unordered 𝑚-tuples for all 𝑚 ≤ 𝑛, and in most cases one would like to rule out such models, hence the need for extra axioms, typically variants of powersets or unions. The axiom of adjunction ax-bj-adj 37997 is more widely used, and is an axiom of General Set Theory. We prove how to retrieve it from binary union and singleton in bj-adjfrombun 38001 and conversely how to prove from adjunction singleton (bj-snfromadj 37999) and unordered pair (bj-prfromadj 38000).
Theorem	bj-abex 37985*	Two ways of stating that the extension of a formula is a set. (Contributed by BJ, 18-Jan-2025.) (Proof modification is discouraged.)
⊢ ({𝑥 ∣ 𝜑} ∈ V ↔ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ 𝜑))
Theorem	bj-clex 37986*	Two ways of stating that a class is a set. (Contributed by BJ, 18-Jan-2025.) (Proof modification is discouraged.)
⊢ (𝑥 ∈ 𝐴 ↔ 𝜑)    ⇒   ⊢ (𝐴 ∈ V ↔ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ 𝜑))
Theorem	bj-axsn 37987*	Two ways of stating the axiom of singleton (which is the universal closure of either side, see ax-bj-sn 37988). (Contributed by BJ, 12-Jan-2025.) (Proof modification is discouraged.)
⊢ ({𝑥} ∈ V ↔ ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥))
Axiom	ax-bj-sn 37988*	Axiom of singleton. (Contributed by BJ, 12-Jan-2025.)
⊢ ∀𝑥∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥)
Theorem	bj-snexg 37989	A singleton built on a set is a set. Contrary to bj-snex 37990, this proof is intuitionistically valid and does not require ax-nul 5259. (Contributed by NM, 7-Aug-1994.) Extract it from snex 5396 and prove it from ax-bj-sn 37988. (Revised by BJ, 12-Jan-2025.) (Proof modification is discouraged.)
⊢ (𝐴 ∈ 𝑉 → {𝐴} ∈ V)
Theorem	bj-snex 37990	A singleton is a set. See also snex 5396, snexALT 5344. (Contributed by NM, 7-Aug-1994.) Prove it from ax-bj-sn 37988. (Revised by BJ, 12-Jan-2025.) (Proof modification is discouraged.)
⊢ {𝐴} ∈ V
Theorem	bj-axbun 37991*	Two ways of stating the axiom of binary union (which is the universal closure of either side, see ax-bj-bun 37992). (Contributed by BJ, 12-Jan-2025.) (Proof modification is discouraged.)
⊢ ((𝑥 ∪ 𝑦) ∈ V ↔ ∃𝑧∀𝑡(𝑡 ∈ 𝑧 ↔ (𝑡 ∈ 𝑥 ∨ 𝑡 ∈ 𝑦)))
Axiom	ax-bj-bun 37992*	Axiom of binary union. (Contributed by BJ, 12-Jan-2025.)
⊢ ∀𝑥∀𝑦∃𝑧∀𝑡(𝑡 ∈ 𝑧 ↔ (𝑡 ∈ 𝑥 ∨ 𝑡 ∈ 𝑦))
Theorem	bj-unexg 37993	Existence of binary unions of sets, proved from ax-bj-bun 37992. (Contributed by BJ, 12-Jan-2025.) (Proof modification is discouraged.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ∈ V)
Theorem	bj-prexg 37994	Existence of unordered pairs formed on sets, proved from ax-bj-sn 37988 and ax-bj-bun 37992. Contrary to bj-prex 37995, this proof is intuitionistically valid and does not require ax-nul 5259. (Contributed by BJ, 12-Jan-2025.) (Proof modification is discouraged.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {𝐴, 𝐵} ∈ V)
Theorem	bj-prex 37995	Existence of unordered pairs proved from ax-bj-sn 37988 and ax-bj-bun 37992. (Contributed by BJ, 12-Jan-2025.) (Proof modification is discouraged.)
⊢ {𝐴, 𝐵} ∈ V
Theorem	bj-axadj 37996*	Two ways of stating the axiom of adjunction (which is the universal closure of either side, see ax-bj-adj 37997). (Contributed by BJ, 12-Jan-2025.) (Proof modification is discouraged.)
⊢ ((𝑥 ∪ {𝑦}) ∈ V ↔ ∃𝑧∀𝑡(𝑡 ∈ 𝑧 ↔ (𝑡 ∈ 𝑥 ∨ 𝑡 = 𝑦)))
Axiom	ax-bj-adj 37997*	Axiom of adjunction. (Contributed by BJ, 19-Jan-2025.)
⊢ ∀𝑥∀𝑦∃𝑧∀𝑡(𝑡 ∈ 𝑧 ↔ (𝑡 ∈ 𝑥 ∨ 𝑡 = 𝑦))
Theorem	bj-adjg1 37998	Existence of the result of the adjunction (generalized only in the first term since this suffices for current applications). (Contributed by BJ, 19-Jan-2025.) (Proof modification is discouraged.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∪ {𝑥}) ∈ V)
Theorem	bj-snfromadj 37999	Singleton from adjunction and empty set. (Contributed by BJ, 19-Jan-2025.) (Proof modification is discouraged.)
⊢ {𝑥} ∈ V
Theorem	bj-prfromadj 38000	Unordered pair from adjunction. (Contributed by BJ, 19-Jan-2025.) (Proof modification is discouraged.)
⊢ {𝑥, 𝑦} ∈ V