P. 374 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 37301-37400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	bj-snglsstag 37301	The singletonization is included in the tagging. (Contributed by BJ, 6-Oct-2018.)
⊢ sngl 𝐴 ⊆ tag 𝐴
Theorem	bj-sngltagi 37302	The singletonization is included in the tagging. (Contributed by BJ, 6-Oct-2018.)
⊢ (𝐴 ∈ sngl 𝐵 → 𝐴 ∈ tag 𝐵)
Theorem	bj-sngltag 37303	The singletonization and the tagging of a set contain the same singletons. (Contributed by BJ, 6-Oct-2018.)
⊢ (𝐴 ∈ 𝑉 → ({𝐴} ∈ sngl 𝐵 ↔ {𝐴} ∈ tag 𝐵))
Theorem	bj-tagci 37304	Characterization of the elements of 𝐵 in terms of elements of its tagged version. (Contributed by BJ, 6-Oct-2018.)
⊢ (𝐴 ∈ 𝐵 → {𝐴} ∈ tag 𝐵)
Theorem	bj-tagcg 37305	Characterization of the elements of 𝐵 in terms of elements of its tagged version. (Contributed by BJ, 6-Oct-2018.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ {𝐴} ∈ tag 𝐵))
Theorem	bj-taginv 37306*	Inverse of tagging. (Contributed by BJ, 6-Oct-2018.)
⊢ 𝐴 = {𝑥 ∣ {𝑥} ∈ tag 𝐴}
Theorem	bj-tagex 37307	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 37308	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 37309	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 37341 and bj-2uplex 37342, and more importantly, bj-pr21val 37333 and bj-pr22val 37339. 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 37342 has advantages: in view of df-br 5087, several sethood antecedents could be removed from existing theorems. For instance, relsnopg 5750 (resp. relsnop 5752) would hold without antecedents (resp. hypotheses) thanks to relsnb 5749). Also, the antecedent Rel 𝑅 could be removed from brrelex12 5674 and related theorems brrelex*, and, as a consequence, of multiple later theorems. Similarly, df-struct 17106 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 4575) as a preliminary definition, and then "redefines" a couple. It could also use the "short" version of the Kuratowski pair (see opthreg 9528) 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 5686, but here we use "tagged versions" of the factors (see df-bj-tag 37295) 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 37295)
Syntax	bj-cproj 37310	Syntax for the class projection. (Contributed by BJ, 6-Apr-2019.)
class (𝐴 Proj 𝐵)
Definition	df-bj-proj 37311*	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 37312	Substitution property for Proj. (Contributed by BJ, 6-Apr-2019.)
⊢ (𝐴 = 𝐶 → (𝐵 = 𝐷 → (𝐴 Proj 𝐵) = (𝐶 Proj 𝐷)))
Theorem	bj-projeq2 37313	Substitution property for Proj. (Contributed by BJ, 6-Apr-2019.)
⊢ (𝐵 = 𝐶 → (𝐴 Proj 𝐵) = (𝐴 Proj 𝐶))
Theorem	bj-projun 37314	The class projection on a given component preserves unions. (Contributed by BJ, 6-Apr-2019.)
⊢ (𝐴 Proj (𝐵 ∪ 𝐶)) = ((𝐴 Proj 𝐵) ∪ (𝐴 Proj 𝐶))
Theorem	bj-projex 37315	Sethood of the class projection. (Contributed by BJ, 6-Apr-2019.)
⊢ (𝐵 ∈ 𝑉 → (𝐴 Proj 𝐵) ∈ V)
Theorem	bj-projval 37316	Value of the class projection. (Contributed by BJ, 6-Apr-2019.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 Proj ({𝐵} × tag 𝐶)) = if(𝐵 = 𝐴, 𝐶, ∅))
Syntax	bj-c1upl 37317	Syntax for Morse monuple. (Contributed by BJ, 6-Apr-2019.)
class ⦅𝐴⦆
Definition	df-bj-1upl 37318	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 37332, bj-2uplth 37341, bj-2uplex 37342, and the properties of the projections (see df-bj-pr1 37321 and df-bj-pr2 37335). (Contributed by BJ, 6-Apr-2019.) (New usage is discouraged.)
⊢ ⦅𝐴⦆ = ({∅} × tag 𝐴)
Theorem	bj-1upleq 37319	Substitution property for ⦅ − ⦆. (Contributed by BJ, 6-Apr-2019.)
⊢ (𝐴 = 𝐵 → ⦅𝐴⦆ = ⦅𝐵⦆)
Syntax	bj-cpr1 37320	Syntax for the first class tuple projection. (Contributed by BJ, 6-Apr-2019.)
class pr1 𝐴
Definition	df-bj-pr1 37321	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 37322, bj-pr11val 37325, bj-pr21val 37333, bj-pr1ex 37326. (Contributed by BJ, 6-Apr-2019.) (New usage is discouraged.)
⊢ pr1 𝐴 = (∅ Proj 𝐴)
Theorem	bj-pr1eq 37322	Substitution property for pr1. (Contributed by BJ, 6-Apr-2019.)
⊢ (𝐴 = 𝐵 → pr1 𝐴 = pr1 𝐵)
Theorem	bj-pr1un 37323	The first projection preserves unions. (Contributed by BJ, 6-Apr-2019.)
⊢ pr1 (𝐴 ∪ 𝐵) = (pr1 𝐴 ∪ pr1 𝐵)
Theorem	bj-pr1val 37324	Value of the first projection. (Contributed by BJ, 6-Apr-2019.)
⊢ pr1 ({𝐴} × tag 𝐵) = if(𝐴 = ∅, 𝐵, ∅)
Theorem	bj-pr11val 37325	Value of the first projection of a monuple. (Contributed by BJ, 6-Apr-2019.)
⊢ pr1 ⦅𝐴⦆ = 𝐴
Theorem	bj-pr1ex 37326	Sethood of the first projection. (Contributed by BJ, 6-Oct-2018.)
⊢ (𝐴 ∈ 𝑉 → pr1 𝐴 ∈ V)
Theorem	bj-1uplth 37327	The characteristic property of monuples. Note that this holds without sethood hypotheses. (Contributed by BJ, 6-Apr-2019.)
⊢ (⦅𝐴⦆ = ⦅𝐵⦆ ↔ 𝐴 = 𝐵)
Theorem	bj-1uplex 37328	A monuple is a set if and only if its coordinates are sets. (Contributed by BJ, 6-Apr-2019.)
⊢ (⦅𝐴⦆ ∈ V ↔ 𝐴 ∈ V)
Theorem	bj-1upln0 37329	A monuple is nonempty. (Contributed by BJ, 6-Apr-2019.)
⊢ ⦅𝐴⦆ ≠ ∅
Syntax	bj-c2uple 37330	Syntax for Morse couple. (Contributed by BJ, 6-Oct-2018.)
class ⦅𝐴, 𝐵⦆
Definition	df-bj-2upl 37331	Definition of the Morse couple. See df-bj-1upl 37318. New usage is discouraged because the precise definition is generally unimportant compared to the characteristic properties bj-2upleq 37332, bj-2uplth 37341, bj-2uplex 37342, and the properties of the projections (see df-bj-pr1 37321 and df-bj-pr2 37335). (Contributed by BJ, 6-Oct-2018.) (New usage is discouraged.)
⊢ ⦅𝐴, 𝐵⦆ = (⦅𝐴⦆ ∪ ({1o} × tag 𝐵))
Theorem	bj-2upleq 37332	Substitution property for ⦅ − , − ⦆. (Contributed by BJ, 6-Oct-2018.)
⊢ (𝐴 = 𝐵 → (𝐶 = 𝐷 → ⦅𝐴, 𝐶⦆ = ⦅𝐵, 𝐷⦆))
Theorem	bj-pr21val 37333	Value of the first projection of a couple. (Contributed by BJ, 6-Oct-2018.)
⊢ pr1 ⦅𝐴, 𝐵⦆ = 𝐴
Syntax	bj-cpr2 37334	Syntax for the second class tuple projection. (Contributed by BJ, 6-Oct-2018.)
class pr2 𝐴
Definition	df-bj-pr2 37335	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 37336, bj-pr22val 37339, bj-pr2ex 37340. (Contributed by BJ, 6-Oct-2018.) (New usage is discouraged.)
⊢ pr2 𝐴 = (1o Proj 𝐴)
Theorem	bj-pr2eq 37336	Substitution property for pr2. (Contributed by BJ, 6-Oct-2018.)
⊢ (𝐴 = 𝐵 → pr2 𝐴 = pr2 𝐵)
Theorem	bj-pr2un 37337	The second projection preserves unions. (Contributed by BJ, 6-Apr-2019.)
⊢ pr2 (𝐴 ∪ 𝐵) = (pr2 𝐴 ∪ pr2 𝐵)
Theorem	bj-pr2val 37338	Value of the second projection. (Contributed by BJ, 6-Apr-2019.)
⊢ pr2 ({𝐴} × tag 𝐵) = if(𝐴 = 1o, 𝐵, ∅)
Theorem	bj-pr22val 37339	Value of the second projection of a couple. (Contributed by BJ, 6-Oct-2018.)
⊢ pr2 ⦅𝐴, 𝐵⦆ = 𝐵
Theorem	bj-pr2ex 37340	Sethood of the second projection. (Contributed by BJ, 6-Oct-2018.)
⊢ (𝐴 ∈ 𝑉 → pr2 𝐴 ∈ V)
Theorem	bj-2uplth 37341	The characteristic property of couples. Note that this holds without sethood hypotheses (compare opth 5422). (Contributed by BJ, 6-Oct-2018.)
⊢ (⦅𝐴, 𝐵⦆ = ⦅𝐶, 𝐷⦆ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))
Theorem	bj-2uplex 37342	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 37343	A couple is nonempty. (Contributed by BJ, 21-Apr-2019.)
⊢ ⦅𝐴, 𝐵⦆ ≠ ∅
Theorem	bj-2upln1upl 37344	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 37329 and bj-2upln0 37343 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 37345	Relative version of cleqf 2928. (Contributed by BJ, 27-Dec-2023.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ Ⅎ𝑥𝑉    ⇒   ⊢ ((𝑉 ∩ 𝐴) = (𝑉 ∩ 𝐵) ↔ ∀𝑥 ∈ 𝑉 (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
Theorem	bj-rcleq 37346*	Relative version of dfcleq 2730. (Contributed by BJ, 27-Dec-2023.)
⊢ ((𝑉 ∩ 𝐴) = (𝑉 ∩ 𝐵) ↔ ∀𝑥 ∈ 𝑉 (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
Theorem	bj-reabeq 37347*	Relative form of eqabb 2876. (Contributed by BJ, 27-Dec-2023.)
⊢ ((𝑉 ∩ 𝐴) = {𝑥 ∈ 𝑉 ∣ 𝜑} ↔ ∀𝑥 ∈ 𝑉 (𝑥 ∈ 𝐴 ↔ 𝜑))
Theorem	bj-disj2r 37348	Relative version of ssdifin0 4426, allowing a biconditional, and of disj2 4399. (Contributed by BJ, 11-Nov-2021.) This proof does not rely, even indirectly, on ssdifin0 4426 nor disj2 4399. (Proof modification is discouraged.)
⊢ ((𝐴 ∩ 𝑉) ⊆ (𝑉 ∖ 𝐵) ↔ ((𝐴 ∩ 𝐵) ∩ 𝑉) = ∅)
Theorem	bj-sscon 37349	Contraposition law for relative subclasses. Relative and generalized version of ssconb 4083. Shortens ssconb 4083, conss2 44884. (Contributed by BJ, 11-Nov-2021.) This proof does not rely, even indirectly, on ssconb 4083 nor conss2 44884. (Proof modification is discouraged.)
⊢ ((𝐴 ∩ 𝑉) ⊆ (𝑉 ∖ 𝐵) ↔ (𝐵 ∩ 𝑉) ⊆ (𝑉 ∖ 𝐴))
21.19.5.17  Axioms for finite unions In this section, we introduce the axiom of singleton ax-bj-sn 37353 and the axiom of binary union ax-bj-bun 37357. Both axioms are implied by the standard axioms of unordered pair ax-pr 5368 and of union ax-un 7680 (see snex 5374 and unex 7689). Conversely, the axiom of unordered pair ax-pr 5368 is implied by the axioms of singleton and of binary union, as proved in bj-prexg 37359 and bj-prex 37360. The axioms of union ax-un 7680 and of powerset ax-pow 5300 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 5300 and https://mathoverflow.net/questions/48365 5300. 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 5241). The axiom of binary union is useful in theories without the axioms of union ax-un 7680 and of powerset ax-pow 5300. 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 5212, ax-sep 5231, ax-nul 5241, ax-reg 9498 } 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 37362 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 37366 and conversely how to prove from adjunction singleton (bj-snfromadj 37364) and unordered pair (bj-prfromadj 37365).
Theorem	bj-abex 37350*	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 37351*	Two ways of stating that a class is a set. (Contributed by BJ, 18-Jan-2025.) (Proof modification is discouraged.)
⊢ (𝑥 ∈ 𝐴 ↔ 𝜑)    ⇒   ⊢ (𝐴 ∈ V ↔ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ 𝜑))
Theorem	bj-axsn 37352*	Two ways of stating the axiom of singleton (which is the universal closure of either side, see ax-bj-sn 37353). (Contributed by BJ, 12-Jan-2025.) (Proof modification is discouraged.)
⊢ ({𝑥} ∈ V ↔ ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥))
Axiom	ax-bj-sn 37353*	Axiom of singleton. (Contributed by BJ, 12-Jan-2025.)
⊢ ∀𝑥∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥)
Theorem	bj-snexg 37354	A singleton built on a set is a set. Contrary to bj-snex 37355, this proof is intuitionistically valid and does not require ax-nul 5241. (Contributed by NM, 7-Aug-1994.) Extract it from snex 5374 and prove it from ax-bj-sn 37353. (Revised by BJ, 12-Jan-2025.) (Proof modification is discouraged.)
⊢ (𝐴 ∈ 𝑉 → {𝐴} ∈ V)
Theorem	bj-snex 37355	A singleton is a set. See also snex 5374, snexALT 5318. (Contributed by NM, 7-Aug-1994.) Prove it from ax-bj-sn 37353. (Revised by BJ, 12-Jan-2025.) (Proof modification is discouraged.)
⊢ {𝐴} ∈ V
Theorem	bj-axbun 37356*	Two ways of stating the axiom of binary union (which is the universal closure of either side, see ax-bj-bun 37357). (Contributed by BJ, 12-Jan-2025.) (Proof modification is discouraged.)
⊢ ((𝑥 ∪ 𝑦) ∈ V ↔ ∃𝑧∀𝑡(𝑡 ∈ 𝑧 ↔ (𝑡 ∈ 𝑥 ∨ 𝑡 ∈ 𝑦)))
Axiom	ax-bj-bun 37357*	Axiom of binary union. (Contributed by BJ, 12-Jan-2025.)
⊢ ∀𝑥∀𝑦∃𝑧∀𝑡(𝑡 ∈ 𝑧 ↔ (𝑡 ∈ 𝑥 ∨ 𝑡 ∈ 𝑦))
Theorem	bj-unexg 37358	Existence of binary unions of sets, proved from ax-bj-bun 37357. (Contributed by BJ, 12-Jan-2025.) (Proof modification is discouraged.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ∈ V)
Theorem	bj-prexg 37359	Existence of unordered pairs formed on sets, proved from ax-bj-sn 37353 and ax-bj-bun 37357. Contrary to bj-prex 37360, this proof is intuitionistically valid and does not require ax-nul 5241. (Contributed by BJ, 12-Jan-2025.) (Proof modification is discouraged.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {𝐴, 𝐵} ∈ V)
Theorem	bj-prex 37360	Existence of unordered pairs proved from ax-bj-sn 37353 and ax-bj-bun 37357. (Contributed by BJ, 12-Jan-2025.) (Proof modification is discouraged.)
⊢ {𝐴, 𝐵} ∈ V
Theorem	bj-axadj 37361*	Two ways of stating the axiom of adjunction (which is the universal closure of either side, see ax-bj-adj 37362). (Contributed by BJ, 12-Jan-2025.) (Proof modification is discouraged.)
⊢ ((𝑥 ∪ {𝑦}) ∈ V ↔ ∃𝑧∀𝑡(𝑡 ∈ 𝑧 ↔ (𝑡 ∈ 𝑥 ∨ 𝑡 = 𝑦)))
Axiom	ax-bj-adj 37362*	Axiom of adjunction. (Contributed by BJ, 19-Jan-2025.)
⊢ ∀𝑥∀𝑦∃𝑧∀𝑡(𝑡 ∈ 𝑧 ↔ (𝑡 ∈ 𝑥 ∨ 𝑡 = 𝑦))
Theorem	bj-adjg1 37363	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 37364	Singleton from adjunction and empty set. (Contributed by BJ, 19-Jan-2025.) (Proof modification is discouraged.)
⊢ {𝑥} ∈ V
Theorem	bj-prfromadj 37365	Unordered pair from adjunction. (Contributed by BJ, 19-Jan-2025.) (Proof modification is discouraged.)
⊢ {𝑥, 𝑦} ∈ V
Theorem	bj-adjfrombun 37366	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 37367	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 37368*	Alternate proof of clel3g 3604. (Contributed by BJ, 1-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐵 ∧ 𝐴 ∈ 𝑥)))
Theorem	bj-pw0ALT 37369	Alternate proof of pw0 4756. The proofs have a similar structure: pw0 4756 uses the definitions of powerclass and singleton as class abstractions, whereas bj-pw0ALT 37369 uses characterizations of their elements. Both proofs then use transitivity of a congruence relation (equality for pw0 4756 and biconditional for bj-pw0ALT 37369) to translate the property ss0b 4342 into the wanted result. To translate a biconditional into a class equality, pw0 4756 uses abbii 2804 (which yields an equality of class abstractions), while bj-pw0ALT 37369 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 4547 and velsn 4584 are proved from the definitions of powerclass and singleton using elabg 3620, 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 37370	Quantitative version of ssexg 5258: 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 37371	Quantitative version of uniexr 7708: 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 37372	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 4545 and elpw2g 5268 (the latter of which could be proved from it). (Contributed by BJ, 31-Dec-2023.)
⊢ ((𝐴 ∩ 𝐵) ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))
Theorem	bj-velpwALT 37373*	This theorem bj-velpwALT 37373 and the next theorem bj-elpwgALT 37374 are alternate proofs of velpw 4547 and elpwg 4545 respectively, where one proves first the setvar case and then generalizes using vtoclbg 3503 instead of proving first the general case using elab2g 3624 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 5370 proved before snexg 5375). (Contributed by BJ, 17-Jan-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴)
Theorem	bj-elpwgALT 37374	Alternate proof of elpwg 4545. See comment for bj-velpwALT 37373. (Contributed by BJ, 17-Jan-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))
Theorem	bj-vjust 37375	Justification theorem for dfv2 3433 if it were the definition. See also vjust 3431. (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.)
⊢ {𝑥 ∣ ⊤} = {𝑦 ∣ ⊤}
Theorem	bj-nul 37376*	Two formulations of the axiom of the empty set ax-nul 5241. Proposal: place it right before ax-nul 5241. (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.)
⊢ (∅ ∈ V ↔ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥)
Theorem	bj-nuliota 37377*	Definition of the empty set using the definite description binder. See also bj-nuliotaALT 37378. (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.)
⊢ ∅ = (℩𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥)
Theorem	bj-nuliotaALT 37378*	Alternate proof of bj-nuliota 37377. Note that this alternate proof uses the fact that ℩𝑥𝜑 evaluates to ∅ when there is no 𝑥 satisfying 𝜑 (iotanul 6470). 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.)
⊢ ∅ = (℩𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥)
Theorem	bj-vtoclgfALT 37379	Alternate proof of vtoclgf 3514. Proof from vtoclgft 3498. (This may have been the original proof before shortening.) (Contributed by BJ, 30-Sep-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝜓)
Theorem	bj-elsn12g 37380	Join of elsng 4582 and elsn2g 4609. (Contributed by BJ, 18-Nov-2023.)
⊢ ((𝐴 ∈ 𝑉 ∨ 𝐵 ∈ 𝑊) → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵))
Theorem	bj-elsnb 37381	Biconditional version of elsng 4582. (Contributed by BJ, 18-Nov-2023.)
⊢ (𝐴 ∈ {𝐵} ↔ (𝐴 ∈ V ∧ 𝐴 = 𝐵))
Theorem	bj-pwcfsdom 37382	Remove hypothesis from pwcfsdom 10495. Illustration of how to remove a "proof-facilitating hypothesis". Shortens theorems using pwcfsdom 10495. (Contributed by BJ, 14-Sep-2019.)
⊢ (ℵ‘𝐴) ≺ ((ℵ‘𝐴) ↑m (cf‘(ℵ‘𝐴)))
Theorem	bj-grur1 37383	Remove hypothesis from grur1 10732. Illustration of how to remove a "definitional hypothesis". This makes its uses longer, but the theorem feels more self-contained. It looks preferable when the defined term appears only once in the conclusion. (Contributed by BJ, 14-Sep-2019.)
⊢ ((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) → 𝑈 = (𝑅1‘(𝑈 ∩ On)))
Theorem	bj-bm1.3ii 37384*	The extension of a predicate (𝜑(𝑧)) is included in a set (𝑥) if and only if it is a set (𝑦). Sufficiency is obvious, and necessity is the content of the axiom of separation ax-sep 5231. Similar to Theorem 1.3(ii) of [BellMachover] p. 463. (Contributed by NM, 21-Jun-1993.) Generalized to a closed form biconditional with existential quantifications using two different setvars 𝑥, 𝑦 (which need not be disjoint). (Revised by BJ, 8-Aug-2022.) TODO: move after sepexi 5236. Relabel ("sepbi"?).
⊢ (∃𝑥∀𝑧(𝜑 → 𝑧 ∈ 𝑥) ↔ ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ 𝜑))
Theorem	bj-dfid2ALT 37385	Alternate version of dfid2 5519. (Contributed by BJ, 9-Nov-2024.) (Proof modification is discouraged.) Use df-id 5517 instead to make the semantics of the construction df-opab 5149 clearer. (New usage is discouraged.)
⊢ I = {⟨𝑥, 𝑥⟩ ∣ ⊤}
Theorem	bj-0nelopab 37386	The empty set is never an element in an ordered-pair class abstraction. (Contributed by Alexander van der Vekens, 5-Nov-2017.) (Proof shortened by BJ, 22-Jul-2023.) TODO: move to the main section when one can reorder sections so that we can use relopab 5771 (this is a very limited reordering).
⊢ ¬ ∅ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑}
Theorem	bj-brrelex12ALT 37387	Two classes related by a binary relation are both sets. Alternate proof of brrelex12 5674. (Contributed by BJ, 14-Jul-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → (𝐴 ∈ V ∧ 𝐵 ∈ V))
Theorem	bj-epelg 37388	The membership relation and the membership predicate agree when the "containing" class is a set. General version of epel 5525 and closed form of epeli 5524. (Contributed by Scott Fenton, 27-Mar-2011.) (Revised by Mario Carneiro, 28-Apr-2015.) TODO: move it to the main section after reordering to have brrelex1i 5678 available. (Proof shortened by BJ, 14-Jul-2023.) (Proof modification is discouraged.)
⊢ (𝐵 ∈ 𝑉 → (𝐴 E 𝐵 ↔ 𝐴 ∈ 𝐵))
Theorem	bj-epelb 37389	Two classes are related by the membership relation if and only if they are related by the membership relation (i.e., the first is an element of the second) and the second is a set (hence so is the first). TODO: move to Main after reordering to have brrelex2i 5679 available. Check if it is shorter to prove bj-epelg 37388 first or bj-epelb 37389 first. (Contributed by BJ, 14-Jul-2023.)
⊢ (𝐴 E 𝐵 ↔ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ V))
Theorem	bj-nsnid 37390	A set does not contain the singleton formed on it. More precisely, one can prove that a class contains the singleton formed on it if and only if it is proper and contains the empty set (since it is "the singleton formed on" any proper class, see snprc 4662): ⊢ ¬ ({𝐴} ∈ 𝐴 ↔ (∅ ∈ 𝐴 → 𝐴 ∈ V)). (Contributed by BJ, 4-Feb-2023.)
⊢ (𝐴 ∈ 𝑉 → ¬ {𝐴} ∈ 𝐴)
Theorem	bj-rdg0gALT 37391	Alternate proof of rdg0g 8357. More direct since it bypasses tz7.44-1 8336 and rdg0 8351 (and vtoclg 3500, vtoclga 3521). (Contributed by NM, 25-Apr-1995.) More direct proof. (Revised by BJ, 17-Nov-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ∈ 𝑉 → (rec(𝐹, 𝐴)‘∅) = 𝐴)
21.19.5.19  Axioms of separation and replacement This section proves basic relations among some standard axioms of set theory, in particular the axiom of separation (the universal closure of ax-sep 5231) and the version of the axiom of replacement requiring the functional relation in the axiom to be a (total) function, bj-rep 37393. These axioms often appear (as specific instances) in the hypotheses of the theorems in this section.
Theorem	bj-axnul 37392*	Over the base theory ax-1 6-- ax-5 1912, the axiom of separation implies the weak emptyset axiom. By "weak emptyset axiom", we mean the axiom asserting existence of an empty set (which can be called "the" empty set when the axiom of extensionality ax-ext 2709 is posited) provided existence of a set (the True truth constant existentially quantified over a fresh variable, extru 1977). This is the conclusion of bj-axnul 37392. Note that the weak emptyset axiom implies ⊢ (∃𝑥⊤ → ∃𝑦⊤) without DV conditions hence also the same statement as the weak emptyset axiom without DV conditions on 𝑥, but only on 𝑦, 𝑧. By "axiom of separation", we mean the universal closure of ax-sep 5231, simulated here by its instance with ⊥ substituted for 𝜑 (and with the variable used to assert existence in the weak emptyset axiom substituted for the containing set) as the hypothesis of bj-axnul 37392. In particular, the axiom of existence extru 1977 and the axiom of separation together imply the emptyset axiom (and conversely, the emptyset axiom implies the axiom of existence). Note: this theorem does not require a disjointness condition on 𝑦, 𝑧, although both axioms should be stated with all variables disjoint. This proof only uses an instance of the axiom of separation with a bounded formula, so is valid in a constructive setting (see the CZF section in the "Intuitionistic Logic Explorer" iset.mm). (Contributed by BJ, 8-Mar-2026.) (Proof modification is discouraged.)
⊢ ∀𝑥∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ ⊥))    ⇒   ⊢ (∃𝑥⊤ → ∃𝑦∀𝑧 ∈ 𝑦 ⊥)
Theorem	bj-rep 37393*	Version of the axiom of replacement requiring the functional relation in the axiom to be a (total) function from ax-rep 5212 (in the form of axrep6 5221). (Contributed by BJ, 14-Mar-2026.) The proof proves the statement without the DV condition on 𝑥, 𝜑, but the DV condition is added to this statement to show that this weaker version is sufficient. (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∀𝑥(∀𝑦 ∈ 𝑥 ∃!𝑧𝜑 → ∃𝑡∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑥 𝜑))
Theorem	bj-axseprep 37394*	Axiom of separation (universal closure of ax-sep 5231) from a weak form of the axiom of replacement requiring that the functional relation in it be a (total) function and the weak emptyset axiom (existence of an empty set provided existence of a set), as written in the theorem's hypotheses. This result shows that the weak emptyset axiom is not only the result of a cheap way to avoid an axiom redundancy (in this case, the existence axiom extru 1977) by adding it as an antecedent, but also permits to prove nontrivial results that hold in nonnecessarily nonempty universes. This proof is by cases so is not intuitionistic. The statement does not require a nonempty universe; most of the proof does not either, and the parts that do (e.g., near sb8ef 2360 and sbequ12r 2260 and eueq2 3657) could be reworked to avoid it. Proof modifications should not introduce steps relying on a nonempty universe, like alrimiv 1929. (Contributed by BJ, 14-Mar-2026.) (Proof modification is discouraged.)
⊢ (∃𝑥⊤ → ∃𝑦∀𝑧 ∈ 𝑦 ⊥)    &   ⊢ ∀𝑥(∀𝑧 ∈ 𝑥 ∃!𝑡𝜓 → ∃𝑦∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 𝜓))    &   ⊢ (𝜓 ↔ ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎)))    ⇒   ⊢ ∀𝑥∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑))
Theorem	bj-axreprepsep 37395*	Strong axiom of replacement (universal closure of ax-rep 5212) from the axioms of separation and replacement as written in the theorem's hypotheses. The statement does not require a nonempty universe; most of the proof does not either, except for the use of 19.8a 2189, which could be removed by reworking the proof, since it is applied in a subexpression bound by the variable it introduces. Proof modifications should not introduce steps relying on a nonempty universe, like alrimiv 1929. (Contributed by BJ, 14-Mar-2026.) (Proof modification is discouraged.)
⊢ ∀𝑥∃𝑠∀𝑦(𝑦 ∈ 𝑠 ↔ (𝑦 ∈ 𝑥 ∧ ∃𝑧𝜑))    &   ⊢ ∀𝑠(∀𝑦 ∈ 𝑠 ∃!𝑧𝜑 → ∃𝑡∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑠 𝜑))    ⇒   ⊢ ∀𝑥(∀𝑦 ∈ 𝑥 ∃*𝑧𝜑 → ∃𝑡∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑥 𝜑))
21.19.5.20  Evaluation at a class This section treats the existing predicate Slot (df-slot 17141) as "evaluation at a class" and for the moment does not introduce new syntax for it.
Theorem	bj-evaleq 37396	Equality theorem for the Slot construction. This is currently a duplicate of sloteq 17142 but may diverge from it if/when a token Eval is introduced for evaluation in order to separate it from Slot and any of its possible modifications. (Contributed by BJ, 27-Dec-2021.) (Proof modification is discouraged.)
⊢ (𝐴 = 𝐵 → Slot 𝐴 = Slot 𝐵)
Theorem	bj-evalfun 37397	The evaluation at a class is a function. (Contributed by BJ, 27-Dec-2021.)
⊢ Fun Slot 𝐴
Theorem	bj-evalfn 37398	The evaluation at a class is a function on the universal class. (General form of slotfn 17143). (Contributed by Mario Carneiro, 22-Sep-2015.) (Revised by BJ, 27-Dec-2021.)
⊢ Slot 𝐴 Fn V
Theorem	bj-evalf 37399	The evaluation at a class is a function from the universal class into the universal class. (Contributed by BJ, 17-Mar-2026.)
⊢ Slot 𝐴:V⟶V
Theorem	bj-evalval 37400	Value of the evaluation at a class. Closed form of strfvnd 17144 and strfvn 17145. (Contributed by NM, 9-Sep-2011.) (Revised by Mario Carneiro, 15-Nov-2014.) (Revised by BJ, 27-Dec-2021.)
⊢ (𝐹 ∈ 𝑉 → (Slot 𝐴‘𝐹) = (𝐹‘𝐴))