P. 373 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 37201-37300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	bj-xpnzex 37201	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 7872 (up to commutation in the product). (Contributed by BJ, 6-Oct-2018.) (Proof modification is discouraged.)
⊢ (𝐴 ≠ ∅ → ((𝐴 × 𝐵) ∈ 𝑉 → 𝐵 ∈ V))
Theorem	bj-xpexg2 37202	Curried (exported) form of xpexg 7705. (Contributed by BJ, 2-Apr-2019.)
⊢ (𝐴 ∈ 𝑉 → (𝐵 ∈ 𝑊 → (𝐴 × 𝐵) ∈ V))
Theorem	bj-xpnzexb 37203	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 37204*	Substitution property for certain classes. (Contributed by BJ, 2-Apr-2019.)
⊢ (𝐴 = 𝐵 → {𝑥 ∣ {𝑥} ∈ (𝐴 “ 𝐶)} = {𝑥 ∣ {𝑥} ∈ (𝐵 “ 𝐶)})
21.19.5.14  "Singletonization" and tagging This subsection introduces the "singletonization" and the "tagging" of a class. The singletonization of a class is the class of singletons of elements of that class. It is useful since all nonsingletons are disjoint from it, so one can easily adjoin to it disjoint elements, which is what the tagging does: it adjoins the empty set. This can be used for instance to define the one-point compactification of a topological space. It will be used in the next section to define tuples which work for proper classes.
Theorem	bj-snsetex 37205*	The class of sets "whose singletons" belong to a set is a set. Nice application of ax-rep 5226. (Contributed by BJ, 6-Oct-2018.)
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V)
Theorem	bj-clexab 37206*	Sethood of certain classes. (Contributed by BJ, 2-Apr-2019.)
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∣ {𝑥} ∈ (𝐴 “ 𝐵)} ∈ V)
Syntax	bj-csngl 37207	Syntax for singletonization. (Contributed by BJ, 6-Oct-2018.)
class sngl 𝐴
Definition	df-bj-sngl 37208*	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 37209	Substitution property for sngl. (Contributed by BJ, 6-Oct-2018.)
⊢ (𝐴 = 𝐵 → sngl 𝐴 = sngl 𝐵)
Theorem	bj-elsngl 37210*	Characterization of the elements of the singletonization of a class. (Contributed by BJ, 6-Oct-2018.)
⊢ (𝐴 ∈ sngl 𝐵 ↔ ∃𝑥 ∈ 𝐵 𝐴 = {𝑥})
Theorem	bj-snglc 37211	Characterization of the elements of 𝐴 in terms of elements of its singletonization. (Contributed by BJ, 6-Oct-2018.)
⊢ (𝐴 ∈ 𝐵 ↔ {𝐴} ∈ sngl 𝐵)
Theorem	bj-snglss 37212	The singletonization of a class is included in its powerclass. (Contributed by BJ, 6-Oct-2018.)
⊢ sngl 𝐴 ⊆ 𝒫 𝐴
Theorem	bj-0nelsngl 37213	The empty set is not a member of a singletonization (neither is any nonsingleton, in particular any von Neuman ordinal except possibly df-1o 8407). (Contributed by BJ, 6-Oct-2018.)
⊢ ∅ ∉ sngl 𝐴
Theorem	bj-snglinv 37214*	Inverse of singletonization. (Contributed by BJ, 6-Oct-2018.)
⊢ 𝐴 = {𝑥 ∣ {𝑥} ∈ sngl 𝐴}
Theorem	bj-snglex 37215	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 37216	Syntax for the tagged copy of a class. (Contributed by BJ, 6-Oct-2018.)
class tag 𝐴
Definition	df-bj-tag 37217	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 37218	Substitution property for tag. (Contributed by BJ, 6-Oct-2018.)
⊢ (𝐴 = 𝐵 → tag 𝐴 = tag 𝐵)
Theorem	bj-eltag 37219*	Characterization of the elements of the tagging of a class. (Contributed by BJ, 6-Oct-2018.)
⊢ (𝐴 ∈ tag 𝐵 ↔ (∃𝑥 ∈ 𝐵 𝐴 = {𝑥} ∨ 𝐴 = ∅))
Theorem	bj-0eltag 37220	The empty set belongs to the tagging of a class. (Contributed by BJ, 6-Apr-2019.)
⊢ ∅ ∈ tag 𝐴
Theorem	bj-tagn0 37221	The tagging of a class is nonempty. (Contributed by BJ, 6-Apr-2019.)
⊢ tag 𝐴 ≠ ∅
Theorem	bj-tagss 37222	The tagging of a class is included in its powerclass. (Contributed by BJ, 6-Oct-2018.)
⊢ tag 𝐴 ⊆ 𝒫 𝐴
Theorem	bj-snglsstag 37223	The singletonization is included in the tagging. (Contributed by BJ, 6-Oct-2018.)
⊢ sngl 𝐴 ⊆ tag 𝐴
Theorem	bj-sngltagi 37224	The singletonization is included in the tagging. (Contributed by BJ, 6-Oct-2018.)
⊢ (𝐴 ∈ sngl 𝐵 → 𝐴 ∈ tag 𝐵)
Theorem	bj-sngltag 37225	The singletonization and the tagging of a set contain the same singletons. (Contributed by BJ, 6-Oct-2018.)
⊢ (𝐴 ∈ 𝑉 → ({𝐴} ∈ sngl 𝐵 ↔ {𝐴} ∈ tag 𝐵))
Theorem	bj-tagci 37226	Characterization of the elements of 𝐵 in terms of elements of its tagged version. (Contributed by BJ, 6-Oct-2018.)
⊢ (𝐴 ∈ 𝐵 → {𝐴} ∈ tag 𝐵)
Theorem	bj-tagcg 37227	Characterization of the elements of 𝐵 in terms of elements of its tagged version. (Contributed by BJ, 6-Oct-2018.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ {𝐴} ∈ tag 𝐵))
Theorem	bj-taginv 37228*	Inverse of tagging. (Contributed by BJ, 6-Oct-2018.)
⊢ 𝐴 = {𝑥 ∣ {𝑥} ∈ tag 𝐴}
Theorem	bj-tagex 37229	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 37230	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 37231	The product of a set and the tagging of a set is a set. (Contributed by BJ, 2-Apr-2019.)
⊢ (𝐴 ∈ 𝑉 → (𝐵 ∈ 𝑊 → (𝐴 × tag 𝐵) ∈ V))
21.19.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 37263 and bj-2uplex 37264, and more importantly, bj-pr21val 37255 and bj-pr22val 37261. 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 37264 has advantages: in view of df-br 5101, several sethood antecedents could be removed from existing theorems. For instance, relsnopg 5760 (resp. relsnop 5762) would hold without antecedents (resp. hypotheses) thanks to relsnb 5759). Also, the antecedent Rel 𝑅 could be removed from brrelex12 5684 and related theorems brrelex*, and, as a consequence, of multiple later theorems. Similarly, df-struct 17086 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 4589) as a preliminary definition, and then "redefines" a couple. It could also use the "short" version of the Kuratowski pair (see opthreg 9539) 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 5696, but here we use "tagged versions" of the factors (see df-bj-tag 37217) 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 37217)
Syntax	bj-cproj 37232	Syntax for the class projection. (Contributed by BJ, 6-Apr-2019.)
class (𝐴 Proj 𝐵)
Definition	df-bj-proj 37233*	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 37234	Substitution property for Proj. (Contributed by BJ, 6-Apr-2019.)
⊢ (𝐴 = 𝐶 → (𝐵 = 𝐷 → (𝐴 Proj 𝐵) = (𝐶 Proj 𝐷)))
Theorem	bj-projeq2 37235	Substitution property for Proj. (Contributed by BJ, 6-Apr-2019.)
⊢ (𝐵 = 𝐶 → (𝐴 Proj 𝐵) = (𝐴 Proj 𝐶))
Theorem	bj-projun 37236	The class projection on a given component preserves unions. (Contributed by BJ, 6-Apr-2019.)
⊢ (𝐴 Proj (𝐵 ∪ 𝐶)) = ((𝐴 Proj 𝐵) ∪ (𝐴 Proj 𝐶))
Theorem	bj-projex 37237	Sethood of the class projection. (Contributed by BJ, 6-Apr-2019.)
⊢ (𝐵 ∈ 𝑉 → (𝐴 Proj 𝐵) ∈ V)
Theorem	bj-projval 37238	Value of the class projection. (Contributed by BJ, 6-Apr-2019.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 Proj ({𝐵} × tag 𝐶)) = if(𝐵 = 𝐴, 𝐶, ∅))
Syntax	bj-c1upl 37239	Syntax for Morse monuple. (Contributed by BJ, 6-Apr-2019.)
class ⦅𝐴⦆
Definition	df-bj-1upl 37240	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. Note that 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 37254, bj-2uplth 37263, bj-2uplex 37264, and the properties of the projections (see df-bj-pr1 37243 and df-bj-pr2 37257). (Contributed by BJ, 6-Apr-2019.) (New usage is discouraged.)
⊢ ⦅𝐴⦆ = ({∅} × tag 𝐴)
Theorem	bj-1upleq 37241	Substitution property for ⦅ − ⦆. (Contributed by BJ, 6-Apr-2019.)
⊢ (𝐴 = 𝐵 → ⦅𝐴⦆ = ⦅𝐵⦆)
Syntax	bj-cpr1 37242	Syntax for the first class tuple projection. (Contributed by BJ, 6-Apr-2019.)
class pr1 𝐴
Definition	df-bj-pr1 37243	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 37244, bj-pr11val 37247, bj-pr21val 37255, bj-pr1ex 37248. (Contributed by BJ, 6-Apr-2019.) (New usage is discouraged.)
⊢ pr1 𝐴 = (∅ Proj 𝐴)
Theorem	bj-pr1eq 37244	Substitution property for pr1. (Contributed by BJ, 6-Apr-2019.)
⊢ (𝐴 = 𝐵 → pr1 𝐴 = pr1 𝐵)
Theorem	bj-pr1un 37245	The first projection preserves unions. (Contributed by BJ, 6-Apr-2019.)
⊢ pr1 (𝐴 ∪ 𝐵) = (pr1 𝐴 ∪ pr1 𝐵)
Theorem	bj-pr1val 37246	Value of the first projection. (Contributed by BJ, 6-Apr-2019.)
⊢ pr1 ({𝐴} × tag 𝐵) = if(𝐴 = ∅, 𝐵, ∅)
Theorem	bj-pr11val 37247	Value of the first projection of a monuple. (Contributed by BJ, 6-Apr-2019.)
⊢ pr1 ⦅𝐴⦆ = 𝐴
Theorem	bj-pr1ex 37248	Sethood of the first projection. (Contributed by BJ, 6-Oct-2018.)
⊢ (𝐴 ∈ 𝑉 → pr1 𝐴 ∈ V)
Theorem	bj-1uplth 37249	The characteristic property of monuples. Note that this holds without sethood hypotheses. (Contributed by BJ, 6-Apr-2019.)
⊢ (⦅𝐴⦆ = ⦅𝐵⦆ ↔ 𝐴 = 𝐵)
Theorem	bj-1uplex 37250	A monuple is a set if and only if its coordinates are sets. (Contributed by BJ, 6-Apr-2019.)
⊢ (⦅𝐴⦆ ∈ V ↔ 𝐴 ∈ V)
Theorem	bj-1upln0 37251	A monuple is nonempty. (Contributed by BJ, 6-Apr-2019.)
⊢ ⦅𝐴⦆ ≠ ∅
Syntax	bj-c2uple 37252	Syntax for Morse couple. (Contributed by BJ, 6-Oct-2018.)
class ⦅𝐴, 𝐵⦆
Definition	df-bj-2upl 37253	Definition of the Morse couple. See df-bj-1upl 37240. New usage is discouraged because the precise definition is generally unimportant compared to the characteristic properties bj-2upleq 37254, bj-2uplth 37263, bj-2uplex 37264, and the properties of the projections (see df-bj-pr1 37243 and df-bj-pr2 37257). (Contributed by BJ, 6-Oct-2018.) (New usage is discouraged.)
⊢ ⦅𝐴, 𝐵⦆ = (⦅𝐴⦆ ∪ ({1o} × tag 𝐵))
Theorem	bj-2upleq 37254	Substitution property for ⦅ − , − ⦆. (Contributed by BJ, 6-Oct-2018.)
⊢ (𝐴 = 𝐵 → (𝐶 = 𝐷 → ⦅𝐴, 𝐶⦆ = ⦅𝐵, 𝐷⦆))
Theorem	bj-pr21val 37255	Value of the first projection of a couple. (Contributed by BJ, 6-Oct-2018.)
⊢ pr1 ⦅𝐴, 𝐵⦆ = 𝐴
Syntax	bj-cpr2 37256	Syntax for the second class tuple projection. (Contributed by BJ, 6-Oct-2018.)
class pr2 𝐴
Definition	df-bj-pr2 37257	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 37258, bj-pr22val 37261, bj-pr2ex 37262. (Contributed by BJ, 6-Oct-2018.) (New usage is discouraged.)
⊢ pr2 𝐴 = (1o Proj 𝐴)
Theorem	bj-pr2eq 37258	Substitution property for pr2. (Contributed by BJ, 6-Oct-2018.)
⊢ (𝐴 = 𝐵 → pr2 𝐴 = pr2 𝐵)
Theorem	bj-pr2un 37259	The second projection preserves unions. (Contributed by BJ, 6-Apr-2019.)
⊢ pr2 (𝐴 ∪ 𝐵) = (pr2 𝐴 ∪ pr2 𝐵)
Theorem	bj-pr2val 37260	Value of the second projection. (Contributed by BJ, 6-Apr-2019.)
⊢ pr2 ({𝐴} × tag 𝐵) = if(𝐴 = 1o, 𝐵, ∅)
Theorem	bj-pr22val 37261	Value of the second projection of a couple. (Contributed by BJ, 6-Oct-2018.)
⊢ pr2 ⦅𝐴, 𝐵⦆ = 𝐵
Theorem	bj-pr2ex 37262	Sethood of the second projection. (Contributed by BJ, 6-Oct-2018.)
⊢ (𝐴 ∈ 𝑉 → pr2 𝐴 ∈ V)
Theorem	bj-2uplth 37263	The characteristic property of couples. Note that this holds without sethood hypotheses (compare opth 5432). (Contributed by BJ, 6-Oct-2018.)
⊢ (⦅𝐴, 𝐵⦆ = ⦅𝐶, 𝐷⦆ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))
Theorem	bj-2uplex 37264	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 37265	A couple is nonempty. (Contributed by BJ, 21-Apr-2019.)
⊢ ⦅𝐴, 𝐵⦆ ≠ ∅
Theorem	bj-2upln1upl 37266	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 ⦅𝐴, ∅⦆ = ⦅𝐴⦆. Note that 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 37251 and bj-2upln0 37265 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.19.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 37267	Relative version of cleqf 2928. (Contributed by BJ, 27-Dec-2023.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ Ⅎ𝑥𝑉    ⇒   ⊢ ((𝑉 ∩ 𝐴) = (𝑉 ∩ 𝐵) ↔ ∀𝑥 ∈ 𝑉 (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
Theorem	bj-rcleq 37268*	Relative version of dfcleq 2730. (Contributed by BJ, 27-Dec-2023.)
⊢ ((𝑉 ∩ 𝐴) = (𝑉 ∩ 𝐵) ↔ ∀𝑥 ∈ 𝑉 (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
Theorem	bj-reabeq 37269*	Relative form of eqabb 2876. (Contributed by BJ, 27-Dec-2023.)
⊢ ((𝑉 ∩ 𝐴) = {𝑥 ∈ 𝑉 ∣ 𝜑} ↔ ∀𝑥 ∈ 𝑉 (𝑥 ∈ 𝐴 ↔ 𝜑))
Theorem	bj-disj2r 37270	Relative version of ssdifin0 4440, allowing a biconditional, and of disj2 4412. (Contributed by BJ, 11-Nov-2021.) This proof does not rely, even indirectly, on ssdifin0 4440 nor disj2 4412. (Proof modification is discouraged.)
⊢ ((𝐴 ∩ 𝑉) ⊆ (𝑉 ∖ 𝐵) ↔ ((𝐴 ∩ 𝐵) ∩ 𝑉) = ∅)
Theorem	bj-sscon 37271	Contraposition law for relative subclasses. Relative and generalized version of ssconb 4096, which it can shorten, as well as conss2 44792. (Contributed by BJ, 11-Nov-2021.) This proof does not rely, even indirectly, on ssconb 4096 nor conss2 44792. (Proof modification is discouraged.)
⊢ ((𝐴 ∩ 𝑉) ⊆ (𝑉 ∖ 𝐵) ↔ (𝐵 ∩ 𝑉) ⊆ (𝑉 ∖ 𝐴))
21.19.5.17  Axioms for finite unions In this section, we introduce the axiom of singleton ax-bj-sn 37275 and the axiom of binary union ax-bj-bun 37279. Both axioms are implied by the standard axioms of unordered pair ax-pr 5379 and of union ax-un 7690 (see snex 5385 and unex 7699). Conversely, the axiom of unordered pair ax-pr 5379 is implied by the axioms of singleton and of binary union, as proved in bj-prexg 37281 and bj-prex 37282. The axioms of union ax-un 7690 and of powerset ax-pow 5312 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 5312 and https://mathoverflow.net/questions/48365 5312. 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 5253). The axiom of binary union is useful in theories without the axioms of union ax-un 7690 and of powerset ax-pow 5312. For instance, the class of well-founded sets hereditarily of cardinality at most 𝑛 ∈ ℕ0 with ordinary membership relation is a model of { ax-ext 2709, ax-rep 5226, ax-sep 5243, ax-nul 5253, ax-reg 9509 } 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 37284 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 37288 and conversely how to prove from adjunction singleton (bj-snfromadj 37286) and unordered pair (bj-prfromadj 37287).
Theorem	bj-abex 37272*	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 37273*	Two ways of stating that a class is a set. (Contributed by BJ, 18-Jan-2025.) (Proof modification is discouraged.)
⊢ (𝑥 ∈ 𝐴 ↔ 𝜑)    ⇒   ⊢ (𝐴 ∈ V ↔ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ 𝜑))
Theorem	bj-axsn 37274*	Two ways of stating the axiom of singleton (which is the universal closure of either side, see ax-bj-sn 37275). (Contributed by BJ, 12-Jan-2025.) (Proof modification is discouraged.)
⊢ ({𝑥} ∈ V ↔ ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥))
Axiom	ax-bj-sn 37275*	Axiom of singleton. (Contributed by BJ, 12-Jan-2025.)
⊢ ∀𝑥∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥)
Theorem	bj-snexg 37276	A singleton built on a set is a set. Contrary to bj-snex 37277, this proof is intuitionistically valid and does not require ax-nul 5253. (Contributed by NM, 7-Aug-1994.) Extract it from snex 5385 and prove it from ax-bj-sn 37275. (Revised by BJ, 12-Jan-2025.) (Proof modification is discouraged.)
⊢ (𝐴 ∈ 𝑉 → {𝐴} ∈ V)
Theorem	bj-snex 37277	A singleton is a set. See also snex 5385, snexALT 5330. (Contributed by NM, 7-Aug-1994.) Prove it from ax-bj-sn 37275. (Revised by BJ, 12-Jan-2025.) (Proof modification is discouraged.)
⊢ {𝐴} ∈ V
Theorem	bj-axbun 37278*	Two ways of stating the axiom of binary union (which is the universal closure of either side, see ax-bj-bun 37279). (Contributed by BJ, 12-Jan-2025.) (Proof modification is discouraged.)
⊢ ((𝑥 ∪ 𝑦) ∈ V ↔ ∃𝑧∀𝑡(𝑡 ∈ 𝑧 ↔ (𝑡 ∈ 𝑥 ∨ 𝑡 ∈ 𝑦)))
Axiom	ax-bj-bun 37279*	Axiom of binary union. (Contributed by BJ, 12-Jan-2025.)
⊢ ∀𝑥∀𝑦∃𝑧∀𝑡(𝑡 ∈ 𝑧 ↔ (𝑡 ∈ 𝑥 ∨ 𝑡 ∈ 𝑦))
Theorem	bj-unexg 37280	Existence of binary unions of sets, proved from ax-bj-bun 37279. (Contributed by BJ, 12-Jan-2025.) (Proof modification is discouraged.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ∈ V)
Theorem	bj-prexg 37281	Existence of unordered pairs formed on sets, proved from ax-bj-sn 37275 and ax-bj-bun 37279. Contrary to bj-prex 37282, this proof is intuitionistically valid and does not require ax-nul 5253. (Contributed by BJ, 12-Jan-2025.) (Proof modification is discouraged.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {𝐴, 𝐵} ∈ V)
Theorem	bj-prex 37282	Existence of unordered pairs proved from ax-bj-sn 37275 and ax-bj-bun 37279. (Contributed by BJ, 12-Jan-2025.) (Proof modification is discouraged.)
⊢ {𝐴, 𝐵} ∈ V
Theorem	bj-axadj 37283*	Two ways of stating the axiom of adjunction (which is the universal closure of either side, see ax-bj-adj 37284). (Contributed by BJ, 12-Jan-2025.) (Proof modification is discouraged.)
⊢ ((𝑥 ∪ {𝑦}) ∈ V ↔ ∃𝑧∀𝑡(𝑡 ∈ 𝑧 ↔ (𝑡 ∈ 𝑥 ∨ 𝑡 = 𝑦)))
Axiom	ax-bj-adj 37284*	Axiom of adjunction. (Contributed by BJ, 19-Jan-2025.)
⊢ ∀𝑥∀𝑦∃𝑧∀𝑡(𝑡 ∈ 𝑧 ↔ (𝑡 ∈ 𝑥 ∨ 𝑡 = 𝑦))
Theorem	bj-adjg1 37285	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 37286	Singleton from adjunction and empty set. (Contributed by BJ, 19-Jan-2025.) (Proof modification is discouraged.)
⊢ {𝑥} ∈ V
Theorem	bj-prfromadj 37287	Unordered pair from adjunction. (Contributed by BJ, 19-Jan-2025.) (Proof modification is discouraged.)
⊢ {𝑥, 𝑦} ∈ V
Theorem	bj-adjfrombun 37288	Adjunction from singleton and binary union. (Contributed by BJ, 19-Jan-2025.) (Proof modification is discouraged.)
⊢ (𝑥 ∪ {𝑦}) ∈ V
21.19.5.18  Set theory: miscellaneous Miscellaneous theorems of set theory.
Theorem	eleq2w2ALT 37289	Alternate proof of eleq2w2 2733 and special instance of eleq2 2826. (Contributed by BJ, 22-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
Theorem	bj-clel3gALT 37290*	Alternate proof of clel3g 3617. (Contributed by BJ, 1-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐵 ∧ 𝐴 ∈ 𝑥)))
Theorem	bj-pw0ALT 37291	Alternate proof of pw0 4770. The proofs have a similar structure: pw0 4770 uses the definitions of powerclass and singleton as class abstractions, whereas bj-pw0ALT 37291 uses characterizations of their elements. Both proofs then use transitivity of a congruence relation (equality for pw0 4770 and biconditional for bj-pw0ALT 37291) to translate the property ss0b 4355 into the wanted result. To translate a biconditional into a class equality, pw0 4770 uses abbii 2804 (which yields an equality of class abstractions), while bj-pw0ALT 37291 uses eqriv 2734 (which requires a biconditional of membership of a given setvar variable). Note that abbii 2804, through its closed form abbi 2802, is proved from eqrdv 2735, which is the deduction form of eqriv 2734. In the other direction, velpw 4561 and velsn 4598 are proved from the definitions of powerclass and singleton using elabg 3633, which is a version of abbii 2804 suited for membership characterizations. (Contributed by BJ, 14-Apr-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝒫 ∅ = {∅}
Theorem	bj-sselpwuni 37292	Quantitative version of ssexg 5270: a subset of an element of a class is an element of the powerclass of the union of that class. (Contributed by BJ, 6-Apr-2024.)
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ 𝒫 ∪ 𝑉)
Theorem	bj-unirel 37293	Quantitative version of uniexr 7718: if the union of a class is an element of a class, then that class is an element of the double powerclass of the union of this class. (Contributed by BJ, 6-Apr-2024.)
⊢ (∪ 𝐴 ∈ 𝑉 → 𝐴 ∈ 𝒫 𝒫 ∪ 𝑉)
Theorem	bj-elpwg 37294	If the intersection of two classes is a set, then inclusion among these classes is equivalent to membership in the powerclass. Common generalization of elpwg 4559 and elpw2g 5280 (the latter of which could be proved from it). (Contributed by BJ, 31-Dec-2023.)
⊢ ((𝐴 ∩ 𝐵) ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))
Theorem	bj-velpwALT 37295*	This theorem bj-velpwALT 37295 and the next theorem bj-elpwgALT 37296 are alternate proofs of velpw 4561 and elpwg 4559 respectively, where one proves first the setvar case and then generalizes using vtoclbg 3516 instead of proving first the general case using elab2g 3637 and then specifying. Here, this results in needing an extra DV condition, a longer combined proof and use of ax-12 2185. In other cases, that order is better (e.g., vsnex 5381 proved before snexg 5386). (Contributed by BJ, 17-Jan-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴)
Theorem	bj-elpwgALT 37296	Alternate proof of elpwg 4559. See comment for bj-velpwALT 37295. (Contributed by BJ, 17-Jan-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))
Theorem	bj-vjust 37297	Justification theorem for dfv2 3445 if it were the definition. See also vjust 3443. (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.)
⊢ {𝑥 ∣ ⊤} = {𝑦 ∣ ⊤}
Theorem	bj-nul 37298*	Two formulations of the axiom of the empty set ax-nul 5253. Proposal: place it right before ax-nul 5253. (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.)
⊢ (∅ ∈ V ↔ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥)
Theorem	bj-nuliota 37299*	Definition of the empty set using the definite description binder. See also bj-nuliotaALT 37300. (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.)
⊢ ∅ = (℩𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥)
Theorem	bj-nuliotaALT 37300*	Alternate proof of bj-nuliota 37299. Note that this alternate proof uses the fact that ℩𝑥𝜑 evaluates to ∅ when there is no 𝑥 satisfying 𝜑 (iotanul 6480). This is an implementation detail of the encoding currently used in set.mm and should be avoided. (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∅ = (℩𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥)