P. 382 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 38101-38200   *Has distinct variable group(s)

Type	Label	Description
Statement
Syntax	bj-c2uple 38101	Syntax for Morse couple. (Contributed by BJ, 6-Oct-2018.)
class ⦅𝐴, 𝐵⦆
Definition	df-bj-2upl 38102	Definition of the Morse couple. See df-bj-1upl 38089. New usage is discouraged because the precise definition is generally unimportant compared to the characteristic properties bj-2upleq 38103, bj-2uplth 38112, bj-2uplex 38113, and the properties of the projections (see df-bj-pr1 38092 and df-bj-pr2 38106). (Contributed by BJ, 6-Oct-2018.) (New usage is discouraged.)
⊢ ⦅𝐴, 𝐵⦆ = (⦅𝐴⦆ ∪ ({1o} × tag 𝐵))
Theorem	bj-2upleq 38103	Substitution property for ⦅ − , − ⦆. (Contributed by BJ, 6-Oct-2018.)
⊢ (𝐴 = 𝐵 → (𝐶 = 𝐷 → ⦅𝐴, 𝐶⦆ = ⦅𝐵, 𝐷⦆))
Theorem	bj-pr21val 38104	Value of the first projection of a couple. (Contributed by BJ, 6-Oct-2018.)
⊢ pr1 ⦅𝐴, 𝐵⦆ = 𝐴
Syntax	bj-cpr2 38105	Syntax for the second class tuple projection. (Contributed by BJ, 6-Oct-2018.)
class pr2 𝐴
Definition	df-bj-pr2 38106	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 38107, bj-pr22val 38110, bj-pr2ex 38111. (Contributed by BJ, 6-Oct-2018.) (New usage is discouraged.)
⊢ pr2 𝐴 = (1o Proj 𝐴)
Theorem	bj-pr2eq 38107	Substitution property for pr2. (Contributed by BJ, 6-Oct-2018.)
⊢ (𝐴 = 𝐵 → pr2 𝐴 = pr2 𝐵)
Theorem	bj-pr2un 38108	The second projection preserves unions. (Contributed by BJ, 6-Apr-2019.)
⊢ pr2 (𝐴 ∪ 𝐵) = (pr2 𝐴 ∪ pr2 𝐵)
Theorem	bj-pr2val 38109	Value of the second projection. (Contributed by BJ, 6-Apr-2019.)
⊢ pr2 ({𝐴} × tag 𝐵) = if(𝐴 = 1o, 𝐵, ∅)
Theorem	bj-pr22val 38110	Value of the second projection of a couple. (Contributed by BJ, 6-Oct-2018.)
⊢ pr2 ⦅𝐴, 𝐵⦆ = 𝐵
Theorem	bj-pr2ex 38111	Sethood of the second projection. (Contributed by BJ, 6-Oct-2018.)
⊢ (𝐴 ∈ 𝑉 → pr2 𝐴 ∈ V)
Theorem	bj-2uplth 38112	The characteristic property of couples. This holds without sethood hypotheses (compare opth 5449). (Contributed by BJ, 6-Oct-2018.)
⊢ (⦅𝐴, 𝐵⦆ = ⦅𝐶, 𝐷⦆ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))
Theorem	bj-2uplex 38113	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 38114	A couple is nonempty. (Contributed by BJ, 21-Apr-2019.)
⊢ ⦅𝐴, 𝐵⦆ ≠ ∅
Theorem	bj-2upln1upl 38115	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 38100 and bj-2upln0 38114 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 38116	Relative version of cleqf 2954. (Contributed by BJ, 27-Dec-2023.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ Ⅎ𝑥𝑉    ⇒   ⊢ ((𝑉 ∩ 𝐴) = (𝑉 ∩ 𝐵) ↔ ∀𝑥 ∈ 𝑉 (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
Theorem	bj-rcleq 38117*	Relative version of dfcleq 2756. (Contributed by BJ, 27-Dec-2023.)
⊢ ((𝑉 ∩ 𝐴) = (𝑉 ∩ 𝐵) ↔ ∀𝑥 ∈ 𝑉 (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
Theorem	bj-reabeq 38118*	Relative form of eqabb 2903. (Contributed by BJ, 27-Dec-2023.)
⊢ ((𝑉 ∩ 𝐴) = {𝑥 ∈ 𝑉 ∣ 𝜑} ↔ ∀𝑥 ∈ 𝑉 (𝑥 ∈ 𝐴 ↔ 𝜑))
Theorem	bj-disj2r 38119	Relative version of ssdifin0 4444, allowing a biconditional, and of disj2 4414. (Contributed by BJ, 11-Nov-2021.) This proof does not rely, even indirectly, on ssdifin0 4444 nor disj2 4414. (Proof modification is discouraged.)
⊢ ((𝐴 ∩ 𝑉) ⊆ (𝑉 ∖ 𝐵) ↔ ((𝐴 ∩ 𝐵) ∩ 𝑉) = ∅)
Theorem	bj-sscon 38120	Contraposition law for relative subclasses. Relative and generalized version of ssconb 4081. Shortens ssconb 4081, conss2 45617. (Contributed by BJ, 11-Nov-2021.) This proof does not rely, even indirectly, on ssconb 4081 nor conss2 45617. (Proof modification is discouraged.)
⊢ ((𝐴 ∩ 𝑉) ⊆ (𝑉 ∖ 𝐵) ↔ (𝐵 ∩ 𝑉) ⊆ (𝑉 ∖ 𝐴))
21.20.5.17  Axioms for finite unions In this section, we introduce the axiom of singleton ax-bj-sn 38124 and the axiom of binary union ax-bj-bun 38128. Both axioms are implied by the standard axioms of unordered pair ax-pr 5395 and of union ax-un 7775 (see snex 5401 and unex 7785). Conversely, the axiom of unordered pair ax-pr 5395 is implied by the axioms of singleton and of binary union, as proved in bj-prexg 38130 and bj-prex 38131. The axioms of union ax-un 7775 and of powerset ax-pow 5331 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 5331 and https://mathoverflow.net/questions/48365 5331. 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 5263). The axiom of binary union is useful in theories without the axioms of union ax-un 7775 and of powerset ax-pow 5331. For instance, the class of well-founded sets hereditarily of cardinality at most 𝑛 ∈ ℕ0 with ordinary membership relation is a model of { ax-ext 2735, ax-rep 5235, ax-sep 5252, ax-nul 5263, ax-reg 9613 } 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 38133 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 38137 and conversely how to prove from adjunction singleton (bj-snfromadj 38135) and unordered pair (bj-prfromadj 38136).
Theorem	bj-abex 38121*	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 38122*	Two ways of stating that a class is a set. (Contributed by BJ, 18-Jan-2025.) (Proof modification is discouraged.)
⊢ (𝑥 ∈ 𝐴 ↔ 𝜑)    ⇒   ⊢ (𝐴 ∈ V ↔ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ 𝜑))
Theorem	bj-axsn 38123*	Two ways of stating the axiom of singleton (which is the universal closure of either side, see ax-bj-sn 38124). (Contributed by BJ, 12-Jan-2025.) (Proof modification is discouraged.)
⊢ ({𝑥} ∈ V ↔ ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥))
Axiom	ax-bj-sn 38124*	Axiom of singleton. (Contributed by BJ, 12-Jan-2025.)
⊢ ∀𝑥∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥)
Theorem	bj-snexg 38125	A singleton built on a set is a set. Contrary to bj-snex 38126, this proof is intuitionistically valid and does not require ax-nul 5263. (Contributed by NM, 7-Aug-1994.) Extract it from snex 5401 and prove it from ax-bj-sn 38124. (Revised by BJ, 12-Jan-2025.) (Proof modification is discouraged.)
⊢ (𝐴 ∈ 𝑉 → {𝐴} ∈ V)
Theorem	bj-snex 38126	A singleton is a set. See also snex 5401, snexALT 5349. (Contributed by NM, 7-Aug-1994.) Prove it from ax-bj-sn 38124. (Revised by BJ, 12-Jan-2025.) (Proof modification is discouraged.)
⊢ {𝐴} ∈ V
Theorem	bj-axbun 38127*	Two ways of stating the axiom of binary union (which is the universal closure of either side, see ax-bj-bun 38128). (Contributed by BJ, 12-Jan-2025.) (Proof modification is discouraged.)
⊢ ((𝑥 ∪ 𝑦) ∈ V ↔ ∃𝑧∀𝑡(𝑡 ∈ 𝑧 ↔ (𝑡 ∈ 𝑥 ∨ 𝑡 ∈ 𝑦)))
Axiom	ax-bj-bun 38128*	Axiom of binary union. (Contributed by BJ, 12-Jan-2025.)
⊢ ∀𝑥∀𝑦∃𝑧∀𝑡(𝑡 ∈ 𝑧 ↔ (𝑡 ∈ 𝑥 ∨ 𝑡 ∈ 𝑦))
Theorem	bj-unexg 38129	Existence of binary unions of sets, proved from ax-bj-bun 38128. (Contributed by BJ, 12-Jan-2025.) (Proof modification is discouraged.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ∈ V)
Theorem	bj-prexg 38130	Existence of unordered pairs formed on sets, proved from ax-bj-sn 38124 and ax-bj-bun 38128. Contrary to bj-prex 38131, this proof is intuitionistically valid and does not require ax-nul 5263. (Contributed by BJ, 12-Jan-2025.) (Proof modification is discouraged.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {𝐴, 𝐵} ∈ V)
Theorem	bj-prex 38131	Existence of unordered pairs proved from ax-bj-sn 38124 and ax-bj-bun 38128. (Contributed by BJ, 12-Jan-2025.) (Proof modification is discouraged.)
⊢ {𝐴, 𝐵} ∈ V
Theorem	bj-axadj 38132*	Two ways of stating the axiom of adjunction (which is the universal closure of either side, see ax-bj-adj 38133). (Contributed by BJ, 12-Jan-2025.) (Proof modification is discouraged.)
⊢ ((𝑥 ∪ {𝑦}) ∈ V ↔ ∃𝑧∀𝑡(𝑡 ∈ 𝑧 ↔ (𝑡 ∈ 𝑥 ∨ 𝑡 = 𝑦)))
Axiom	ax-bj-adj 38133*	Axiom of adjunction. (Contributed by BJ, 19-Jan-2025.)
⊢ ∀𝑥∀𝑦∃𝑧∀𝑡(𝑡 ∈ 𝑧 ↔ (𝑡 ∈ 𝑥 ∨ 𝑡 = 𝑦))
Theorem	bj-adjg1 38134	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 38135	Singleton from adjunction and empty set. (Contributed by BJ, 19-Jan-2025.) (Proof modification is discouraged.)
⊢ {𝑥} ∈ V
Theorem	bj-prfromadj 38136	Unordered pair from adjunction. (Contributed by BJ, 19-Jan-2025.) (Proof modification is discouraged.)
⊢ {𝑥, 𝑦} ∈ V
Theorem	bj-adjfrombun 38137	Adjunction from singleton and binary union. (Contributed by BJ, 19-Jan-2025.) (Proof modification is discouraged.)
⊢ (𝑥 ∪ {𝑦}) ∈ V
21.20.5.18  Relations, functions, composition: supplements Some shortenings and proof modifications that allow the following re-structuring of sections: 2.3.10. Cartesian product 2.3.11. Relations 2.3.11.1. Restriction 2.3.11.2. Relations 2.3.11.3. Domain 2.3.11.4. Converse 2.3.11.5. Range 2.3.11.6. Image 2.3.11.7. Composition
Theorem	bj-elinxp 38138*	Membership in an intersection with a Cartesian product. (Contributed by Peter Mazsa, 9-Sep-2022.) Use the 𝑥𝑅𝑦 idiom and give a shorter proof not depending on df-rel 5662. (Revised by BJ, 16-Oct-2026.) Note to remove when moving to main section: a shortening of the exact statement elinxp 6020 is possible along the same line.
⊢ (𝐶 ∈ (𝑅 ∩ (𝐴 × 𝐵)) ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝐶 = ⟨𝑥, 𝑦⟩ ∧ 𝑥𝑅𝑦))
Theorem	resssres 38139	A restricted class is included in a class if and only if it is included in that class restricted to any class including the first restricting class. (Contributed by BJ, 25-Oct-2026.)
⊢ (𝑋 ⊆ 𝑌 → ((𝐴 ↾ 𝑋) ⊆ 𝐵 ↔ (𝐴 ↾ 𝑋) ⊆ (𝐵 ↾ 𝑌)))
Theorem	bj-elres 38140*	Membership in a restriction. (Contributed by Scott Fenton, 17-Mar-2011.) (Proof shortened by Peter Mazsa, 9-Sep-2022.) Use the 𝑥𝐵𝑦 idiom. (Revised by BJ, 16-Oct-2026.)
⊢ (𝐴 ∈ (𝐵 ↾ 𝐶) ↔ ∃𝑥 ∈ 𝐶 ∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝑥𝐵𝑦))
Theorem	bj-dfres2 38141*	Alternate definition of the restriction of a class to another, as an ordered pair class abstraction: the restriction of a class to another is the class of ordered pairs whose first component is in the restricting class and whose components are related by the restricted class. (Contributed by Mario Carneiro, 5-Nov-2013.) Do not depend on df-rel 5662. (Revised by BJ, 16-Oct-2026.)
⊢ (𝑅 ↾ 𝐴) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑥𝑅𝑦)}
Theorem	bj-resss2 38142	The restriction of a class to a class is included in the Cartesian product of the restricting class with the universal class. (Contributed by BJ, 16-Oct-2026.)
⊢ (𝑅 ↾ 𝐴) ⊆ (𝐴 × V)
Theorem	relpart 38143*	Two ways of expressing the "relation part" of a class: its restriction to the universal class (that is, its intersection with the Cartesian square of the universal class) equals the class of ordered pairs it contains (the class of ordered pairs whose components are related by it). The "relation part" of a class is a relation (see df-rel 5662 and relres 6007) and is the largest relation included in that class (that follows from relssresv 38145). Taking the relation part of a class is a projection onto the collection of relations, that is, it is an idempotent operation (residm 6013) with image the collection of relations (by relres 6007 for one inclusion and the forward implication of dfrel3 6205 for the other). As with any projection, a class is in its image if and only if its is a fixpoint of that projection (which is precisely dfrel3 6205). Other expressions giving the relation part of a class are cnvcnv 6196, coi1res 38151. (Contributed by BJ, 16-Oct-2026.)
⊢ (𝐴 ↾ V) = {⟨𝑥, 𝑦⟩ ∣ 𝑥𝐴𝑦}
Theorem	bj-dfrel3 38144	Alternate definition of relation: a class is a relation if and only if it is equal to its "relation part" (see relpart 38143). (Contributed by NM, 14-May-2008.) Do not depend on df-cnv 5663 to move it earlier. (Revised by BJ, 16-Oct-2026.)
⊢ (Rel 𝑅 ↔ (𝑅 ↾ V) = 𝑅)
Theorem	relssresv 38145	A relation is included in a class if and only if it is included in its "relation part" (see relpart 38143). (Contributed by BJ, 16-Oct-2026.)
⊢ (Rel 𝐵 → (𝐵 ⊆ 𝐴 ↔ 𝐵 ⊆ (𝐴 ↾ V)))
Theorem	bj-dfrel4v 38146*	A relation can be expressed as the set of ordered pairs in it. An analogue of dffn5 6966 for relations. (Contributed by Mario Carneiro, 16-Aug-2015.) Do not depend on df-cnv 5663, reverse equality. (Revised by BJ, 16-Oct-2026.) Note: this theorem could be used in place of opabid2 5812, which could be deleted.
⊢ (Rel 𝑅 ↔ {⟨𝑥, 𝑦⟩ ∣ 𝑥𝑅𝑦} = 𝑅)
Theorem	bj-dfrel2 38147	Alternate definition of relation. Exercise 2 of [TakeutiZaring] p. 25. (Contributed by NM, 29-Dec-1996.) (Proof shortened by BJ, 16-Oct-2026.) Do not use opabid2 5812. (Proof modification is discouraged.)
⊢ (Rel 𝑅 ↔ ◡◡𝑅 = 𝑅)
Theorem	bj-cnvcnv2 38148	The double converse of a class equals its restriction to the universe. (Contributed by NM, 8-Oct-2007.) Do not depend on cnvcnv 6196 in order to prove it from cnvcnv2 6197. (Revised by BJ, 16-Oct-2026.) Do not depend on cnvcnv 6196. (Proof modification is discouraged.)
⊢ ◡◡𝐴 = (𝐴 ↾ V)
Theorem	bj-cnvcnv 38149	The double converse of a class strips out all elements that are not ordered pairs. (Contributed by NM, 8-Dec-2003.) (Proof shortened by BJ, 26-Nov-2021.) (Proof shortened by BJ, 16-Oct-2026.) Prefer use of bj-cnvcnv2 38148. (Proof modification is discouraged.)
⊢ ◡◡𝐴 = (𝐴 ∩ (V × V))
Theorem	elco 38150*	Membership in a composition. (Contributed by BJ, 16-Aug-2026.)
⊢ (𝐴 ∈ (𝐶 ∘ 𝐵) ↔ ∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ ∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐶𝑦)))
Theorem	coi1res 38151	Precomposing with the identity is the same as taking the relation part of a class. (Contributed by BJ, 16-Aug-2026.)
⊢ (𝐴 ∘ I ) = (𝐴 ↾ V)
Theorem	bj-coi1 38152	The identity relation is a right-unit for composition. Part of Theorem 3.7(i) of [Monk1] p. 36. (Contributed by NM, 22-Apr-2004.) Strengthen to biconditional form and shorten (Revised by BJ, 16-Oct-2026.)
⊢ (Rel 𝐴 ↔ (𝐴 ∘ I ) = 𝐴)
21.20.5.19  Set theory: miscellaneous Miscellaneous theorems of set theory.
Theorem	eleq2w2ALT 38153	Alternate proof of eleq2w2 2759 and special instance of eleq2 2853. (Contributed by BJ, 22-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
Theorem	bj-clel3gALT 38154*	Alternate proof of clel3g 3618. (Contributed by BJ, 1-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐵 ∧ 𝐴 ∈ 𝑥)))
Theorem	bj-pw0ALT 38155	Alternate proof of pw0 4833. The proofs have a similar structure: pw0 4833 uses the definitions of powerclass and singleton as class abstractions, whereas bj-pw0ALT 38155 uses characterizations of their elements. Both proofs then use transitivity of a congruence relation (equality for pw0 4833 and biconditional for bj-pw0ALT 38155) to translate the property ss0b 4354 into the wanted result. To translate a biconditional into a class equality, pw0 4833 uses abbii 2830 (which yields an equality of class abstractions), while bj-pw0ALT 38155 uses eqriv 2760 (which requires a biconditional of membership of a given setvar variable). Theorem abbii 2830, through its closed form abbi 2828, is proved from eqrdv 2761, which is the deduction form of eqriv 2760. In the other direction, velpw 4565 and velsn 4600 are proved from the definitions of powerclass and singleton using elabg 3633, which is a version of abbii 2830 suited for membership characterizations. (Contributed by BJ, 14-Apr-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝒫 ∅ = {∅}
Theorem	bj-sselpwuni 38156	Quantitative version of ssexg 5285: 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 38157	Quantitative version of uniexr 7801: 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 38158	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 4563 and elpw2g 5299 (the latter of which could be proved from it). (Contributed by BJ, 31-Dec-2023.)
⊢ ((𝐴 ∩ 𝐵) ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))
Theorem	bj-velpwALT 38159*	This theorem bj-velpwALT 38159 and the next theorem bj-elpwgALT 38160 are alternate proofs of velpw 4565 and elpwg 4563 respectively, where one proves first the setvar case and then generalizes using vtoclbg 3523 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 2216. In other cases, that order is better (e.g., vsnex 5397 proved before snexg 5402). (Contributed by BJ, 17-Jan-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴)
Theorem	bj-elpwgALT 38160	Alternate proof of elpwg 4563. See comment for bj-velpwALT 38159. (Contributed by BJ, 17-Jan-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))
Theorem	bj-vjust 38161	Justification theorem for dfv2 3457 if it were the definition. See also vjust 3455. (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.)
⊢ {𝑥 ∣ ⊤} = {𝑦 ∣ ⊤}
Theorem	bj-nul 38162*	Two formulations of the axiom of the empty set ax-nul 5263. Proposal: place it right before ax-nul 5263. (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.)
⊢ (∅ ∈ V ↔ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥)
Theorem	bj-nuliota 38163*	Definition of the empty set using the definite description binder. See also bj-nuliotaALT 38164. (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.)
⊢ ∅ = (℩𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥)
Theorem	bj-nuliotaALT 38164*	Alternate proof of bj-nuliota 38163. This alternate proof uses the fact that ℩𝑥𝜑 evaluates to ∅ when there is no 𝑥 satisfying 𝜑 (iotanul 6537). 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 38165	Alternate proof of vtoclgf 3533. Proof from vtoclgft 3519. (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 38166	Join of elsng 4598 and elsn2g 4625. (Contributed by BJ, 18-Nov-2023.)
⊢ ((𝐴 ∈ 𝑉 ∨ 𝐵 ∈ 𝑊) → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵))
Theorem	bj-elsnb 38167	Biconditional version of elsng 4598. (Contributed by BJ, 18-Nov-2023.)
⊢ (𝐴 ∈ {𝐵} ↔ (𝐴 ∈ V ∧ 𝐴 = 𝐵))
Theorem	bj-pwcfsdom 38168	Remove hypothesis from pwcfsdom 10695. Illustration of how to remove a "proof-facilitating hypothesis". Shortens theorems using pwcfsdom 10695. (Contributed by BJ, 14-Sep-2019.)
⊢ (ℵ‘𝐴) ≺ ((ℵ‘𝐴) ↑m (cf‘(ℵ‘𝐴)))
Theorem	bj-grur1 38169	Remove hypothesis from grur1 10932. 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 38170*	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 5252. 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 5259. Relabel ("sepbi"?).
⊢ (∃𝑥∀𝑧(𝜑 → 𝑧 ∈ 𝑥) ↔ ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ 𝜑))
Theorem	bj-dfid2ALT 38171	Alternate version of dfid2 5552. (Contributed by BJ, 9-Nov-2024.) (Proof modification is discouraged.) Use df-id 5550 instead to make the semantics of the construction df-opab 5171 clearer. (New usage is discouraged.)
⊢ I = {⟨𝑥, 𝑥⟩ ∣ ⊤}
Theorem	bj-0nelopab 38172	The empty set is not an element of 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 5808 (this is a very limited reordering).
⊢ ¬ ∅ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑}
Theorem	bj-brrelex12ALT 38173	Two classes related by a binary relation are both sets. Alternate proof of brrelex12 5707. (Contributed by BJ, 14-Jul-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → (𝐴 ∈ V ∧ 𝐵 ∈ V))
Theorem	bj-epelg 38174	The membership relation and the membership predicate agree when the "containing" class is a set. General version of epel 5558 and closed form of epeli 5557. (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 5711 available. (Proof shortened by BJ, 14-Jul-2023.) (Proof modification is discouraged.)
⊢ (𝐵 ∈ 𝑉 → (𝐴 E 𝐵 ↔ 𝐴 ∈ 𝐵))
Theorem	bj-epelb 38175	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 5712 available. Check if it is shorter to prove bj-epelg 38174 first or bj-epelb 38175 first. (Contributed by BJ, 14-Jul-2023.)
⊢ (𝐴 E 𝐵 ↔ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ V))
Theorem	bj-nsnid 38176	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 4678): ⊢ ¬ ({𝐴} ∈ 𝐴 ↔ (∅ ∈ 𝐴 → 𝐴 ∈ V)). (Contributed by BJ, 4-Feb-2023.)
⊢ (𝐴 ∈ 𝑉 → ¬ {𝐴} ∈ 𝐴)
Theorem	bj-rdg0gALT 38177	Alternate proof of rdg0g 8463. More direct since it bypasses tz7.44-1 8442 and rdg0 8457 (and vtoclg 3521, vtoclga 3540). (Contributed by NM, 25-Apr-1995.) More direct proof. (Revised by BJ, 17-Nov-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ∈ 𝑉 → (rec(𝐹, 𝐴)‘∅) = 𝐴)
Theorem	bj-vn0ALT 38178	Alternate proof of vn0 4294 which does not use eqabbw 2837 (and is shorter than vn0 4294 when eqabbw 2837 is inlined). (Contributed by BJ, 12-Jul-2026.) Using the same dummy variable for 𝑦 and 𝑧 slightly reduces the proof size. (Proof modification is discouraged.) (New usage is discouraged.)
⊢ V ≠ ∅
21.20.5.20  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 5252) and the version of the axiom of replacement requiring the functional relation in the axiom to be a (total) function, bj-rep 38180. These axioms often appear (as specific instances) in the hypotheses of the theorems in this section.
Theorem	bj-axnul 38179*	Over the base theory ax-1 6-- ax-5 1945, 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 2735 is posited) provided existence of a set (the True truth constant existentially quantified over a fresh variable, extru 2010). This is the conclusion of bj-axnul 38179. 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 5252, 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 38179. In particular, the axiom of existence extru 2010 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 38180*	Version of the axiom of replacement requiring the functional relation in the axiom to be a (total) function from ax-rep 5235 (in the form of axrep6 5243). (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 38181*	Axiom of separation (universal closure of ax-sep 5252) 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 2010) 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 2387 and sbequ12r 2291 and eueq2 3671) could be reworked to avoid it. Proof modifications should not introduce steps relying on a nonempty universe, like alrimiv 1962. (Contributed by BJ, 14-Mar-2026.) (Proof modification is discouraged.)
⊢ (∃𝑥⊤ → ∃𝑦∀𝑧 ∈ 𝑦 ⊥)    &   ⊢ ∀𝑥(∀𝑧 ∈ 𝑥 ∃!𝑡𝜓 → ∃𝑦∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 𝜓))    &   ⊢ (𝜓 ↔ ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎)))    ⇒   ⊢ ∀𝑥∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑))
Theorem	bj-axreprepsep 38182*	Strong axiom of replacement (universal closure of ax-rep 5235) 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 2221, 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 1962. (Contributed by BJ, 14-Mar-2026.) (Proof modification is discouraged.)
⊢ ∀𝑥∃𝑠∀𝑦(𝑦 ∈ 𝑠 ↔ (𝑦 ∈ 𝑥 ∧ ∃𝑧𝜑))    &   ⊢ ∀𝑠(∀𝑦 ∈ 𝑠 ∃!𝑧𝜑 → ∃𝑡∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑠 𝜑))    ⇒   ⊢ ∀𝑥(∀𝑦 ∈ 𝑥 ∃*𝑧𝜑 → ∃𝑡∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑥 𝜑))
21.20.5.21  Evaluation at a class This section treats the existing predicate Slot (df-slot 17389) as "evaluation at a class" and for the moment does not introduce new syntax for it.
Theorem	bj-evaleq 38183	Equality theorem for the Slot construction. This is currently a duplicate of sloteq 17390 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 38184	The evaluation at a class is a function. (Contributed by BJ, 27-Dec-2021.)
⊢ Fun Slot 𝐴
Theorem	bj-evalfn 38185	The evaluation at a class is a function on the universal class. (General form of slotfn 17391). (Contributed by Mario Carneiro, 22-Sep-2015.) (Revised by BJ, 27-Dec-2021.)
⊢ Slot 𝐴 Fn V
Theorem	bj-evalf 38186	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 38187	Value of the evaluation at a class. Closed form of strfvnd 17392 and strfvn 17393. (Contributed by NM, 9-Sep-2011.) (Revised by Mario Carneiro, 15-Nov-2014.) (Revised by BJ, 27-Dec-2021.)
⊢ (𝐹 ∈ 𝑉 → (Slot 𝐴‘𝐹) = (𝐹‘𝐴))
Theorem	bj-evalid 38188	The evaluation at a set of the identity function is that set. General form of ndxarg 17403. The restriction to a set 𝑉 is necessary since the argument of the function Slot 𝐴 (like that of any function) has to be a set for the evaluation to be meaningful. (Contributed by BJ, 27-Dec-2021.)
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉) → (Slot 𝐴‘( I ↾ 𝑉)) = 𝐴)
Theorem	bj-ndxarg 38189	Proof of ndxarg 17403 from bj-evalid 38188. (Contributed by BJ, 27-Dec-2021.) (Proof modification is discouraged.)
⊢ 𝐸 = Slot 𝑁    &   ⊢ 𝑁 ∈ ℕ    ⇒   ⊢ (𝐸‘ndx) = 𝑁
Theorem	bj-evalidval 38190	Closed general form of strndxid 17405. Both sides are equal to (𝐹‘𝐴) by bj-evalid 38188 and bj-evalval 38187 respectively, but bj-evalidval 38190 adds something to bj-evalid 38188 and bj-evalval 38187 in that Slot 𝐴 appears on both sides. (Contributed by BJ, 27-Dec-2021.)
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐹 ∈ 𝑈) → (𝐹‘(Slot 𝐴‘( I ↾ 𝑉))) = (Slot 𝐴‘𝐹))
21.20.5.22  Elementwise operations
Syntax	celwise 38191	Syntax for elementwise operations.
class elwise
Definition	df-elwise 38192*	Define the elementwise operation associated with a given operation. For instance, + is the addition of complex numbers (axaddf 11257), so if 𝐴 and 𝐵 are sets of complex numbers, then (𝐴(elwise‘ + )𝐵) is the set of numbers of the form (𝑥 + 𝑦) with 𝑥 ∈ 𝐴 and 𝑦 ∈ 𝐵. The set of odd natural numbers is (({2}(elwise‘ · )ℕ0)(elwise‘ + ){1}), or less formally 2ℕ0 + 1. (Contributed by BJ, 22-Dec-2021.)
⊢ elwise = (𝑜 ∈ V ↦ (𝑥 ∈ V, 𝑦 ∈ V ↦ {𝑧 ∣ ∃𝑢 ∈ 𝑥 ∃𝑣 ∈ 𝑦 𝑧 = (𝑢𝑜𝑣)}))
21.20.5.23  Elementwise intersection (families of sets induced on a subset) Many kinds of structures are given by families of subsets of a given set: Moore collections (df-mre 17785), topologies (df-top 23242), pi-systems, rings of sets, delta-rings, lambda-systems/Dynkin systems, algebras/fields of sets, sigma-algebras/sigma-fields/tribes (df-siga 34811), sigma rings, monotone classes, matroids/independent sets, bornologies, filters. There is a natural notion of structure induced on a subset. It is often given by an elementwise intersection, namely, the family of intersections of sets in the original family with the given subset. In this subsection, we define this notion and prove its main properties. Classical conditions on families of subsets include being nonempty, containing the whole set, containing the empty set, being stable under unions, intersections, subsets, supersets, (relative) complements. Therefore, we prove related properties for the elementwise intersection. We will call (𝑋 ↾t 𝐴) the elementwise intersection on the family 𝑋 by the class 𝐴. REMARK: many theorems are already in set.mm: "MM> SEARCH *rest* / JOIN".
Theorem	bj-rest00 38193	An elementwise intersection on the empty family is the empty set. TODO: this is 0rest 17629. (Contributed by BJ, 27-Apr-2021.)
⊢ (∅ ↾t 𝐴) = ∅
Theorem	bj-restsn 38194	An elementwise intersection on the singleton on a set is the singleton on the intersection by that set. Generalization of bj-restsn0 38197 and bj-restsnid 38199. (Contributed by BJ, 27-Apr-2021.)
⊢ ((𝑌 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → ({𝑌} ↾t 𝐴) = {(𝑌 ∩ 𝐴)})
Theorem	bj-restsnss 38195	Special case of bj-restsn 38194. (Contributed by BJ, 27-Apr-2021.)
⊢ ((𝑌 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑌) → ({𝑌} ↾t 𝐴) = {𝐴})
Theorem	bj-restsnss2 38196	Special case of bj-restsn 38194. (Contributed by BJ, 27-Apr-2021.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑌 ⊆ 𝐴) → ({𝑌} ↾t 𝐴) = {𝑌})
Theorem	bj-restsn0 38197	An elementwise intersection on the singleton on the empty set is the singleton on the empty set. Special case of bj-restsn 38194 and bj-restsnss2 38196. TODO: this is restsn 23518. (Contributed by BJ, 27-Apr-2021.)
⊢ (𝐴 ∈ 𝑉 → ({∅} ↾t 𝐴) = {∅})
Theorem	bj-restsn10 38198	Special case of bj-restsn 38194, bj-restsnss 38195, and bj-rest10 38200. (Contributed by BJ, 27-Apr-2021.)
⊢ (𝑋 ∈ 𝑉 → ({𝑋} ↾t ∅) = {∅})
Theorem	bj-restsnid 38199	The elementwise intersection on the singleton on a class by that class is the singleton on that class. Special case of bj-restsn 38194 and bj-restsnss 38195. (Contributed by BJ, 27-Apr-2021.)
⊢ ({𝐴} ↾t 𝐴) = {𝐴}
Theorem	bj-rest10 38200	An elementwise intersection on a nonempty family by the empty set is the singleton on the empty set. TODO: this generalizes rest0 23517 and could replace it. (Contributed by BJ, 27-Apr-2021.)
⊢ (𝑋 ∈ 𝑉 → (𝑋 ≠ ∅ → (𝑋 ↾t ∅) = {∅}))