P. 330 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 32901-33000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	mdsym 32901	M-symmetry of the Hilbert lattice. Lemma 5 of [Maeda] p. 168. (Contributed by NM, 6-Jul-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 𝑀ℋ 𝐵 ↔ 𝐵 𝑀ℋ 𝐴))
Theorem	dmdsym 32902	Dual M-symmetry of the Hilbert lattice. (Contributed by NM, 25-Jul-2007.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 𝑀ℋ* 𝐵 ↔ 𝐵 𝑀ℋ* 𝐴))
Theorem	atdmd2 32903	Two Hilbert lattice elements have the dual modular pair property if the second is an atom. (Contributed by NM, 6-Jul-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ HAtoms) → 𝐴 𝑀ℋ* 𝐵)
Theorem	sumdmdii 32904	If the subspace sum of two Hilbert lattice elements is closed, then the elements are a dual modular pair. Remark in [MaedaMaeda] p. 139. (Contributed by NM, 12-Jul-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ ((𝐴 +ℋ 𝐵) = (𝐴 ∨ℋ 𝐵) → 𝐴 𝑀ℋ* 𝐵)
Theorem	cmmdi 32905	Commuting subspaces form a modular pair. (Contributed by NM, 16-Jan-2005.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝐴 𝐶ℋ 𝐵 → 𝐴 𝑀ℋ 𝐵)
Theorem	cmdmdi 32906	Commuting subspaces form a dual modular pair. (Contributed by NM, 25-Apr-2006.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝐴 𝐶ℋ 𝐵 → 𝐴 𝑀ℋ* 𝐵)
Theorem	sumdmdlem 32907	Lemma for sumdmdi 32909. The span of vector 𝐶 not in the subspace sum is "trimmed off." (Contributed by NM, 18-Dec-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ ((𝐶 ∈ ℋ ∧ ¬ 𝐶 ∈ (𝐴 +ℋ 𝐵)) → ((𝐵 +ℋ (span‘{𝐶})) ∩ 𝐴) = (𝐵 ∩ 𝐴))
Theorem	sumdmdlem2 32908*	Lemma for sumdmdi 32909. (Contributed by NM, 23-Dec-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (∀𝑥 ∈ HAtoms ((𝑥 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵) → (𝐴 +ℋ 𝐵) = (𝐴 ∨ℋ 𝐵))
Theorem	sumdmdi 32909	The subspace sum of two Hilbert lattice elements is closed iff the elements are a dual modular pair. Theorem 2 of [Holland] p. 1519. (Contributed by NM, 14-Dec-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ ((𝐴 +ℋ 𝐵) = (𝐴 ∨ℋ 𝐵) ↔ 𝐴 𝑀ℋ* 𝐵)
Theorem	dmdbr4ati 32910*	Dual modular pair property in terms of atoms. (Contributed by NM, 15-Jan-2005.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝐴 𝑀ℋ* 𝐵 ↔ ∀𝑥 ∈ HAtoms ((𝑥 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵))
Theorem	dmdbr5ati 32911*	Dual modular pair property in terms of atoms. (Contributed by NM, 14-Jan-2005.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝐴 𝑀ℋ* 𝐵 ↔ ∀𝑥 ∈ HAtoms (𝑥 ⊆ (𝐴 ∨ℋ 𝐵) → 𝑥 ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵)))
Theorem	dmdbr6ati 32912*	Dual modular pair property in terms of atoms. The modular law takes the form of the shearing identity. (Contributed by NM, 18-Jan-2005.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝐴 𝑀ℋ* 𝐵 ↔ ∀𝑥 ∈ HAtoms ((𝐴 ∨ℋ 𝐵) ∩ 𝑥) = ((((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵) ∩ 𝑥))
Theorem	dmdbr7ati 32913*	Dual modular pair property in terms of atoms. (Contributed by NM, 18-Jan-2005.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝐴 𝑀ℋ* 𝐵 ↔ ∀𝑥 ∈ HAtoms ((𝐴 ∨ℋ 𝐵) ∩ 𝑥) ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵))
Theorem	mdoc1i 32914	Orthocomplements form a modular pair. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    ⇒   ⊢ 𝐴 𝑀ℋ (⊥‘𝐴)
Theorem	mdoc2i 32915	Orthocomplements form a modular pair. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    ⇒   ⊢ (⊥‘𝐴) 𝑀ℋ 𝐴
Theorem	dmdoc1i 32916	Orthocomplements form a dual modular pair. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    ⇒   ⊢ 𝐴 𝑀ℋ* (⊥‘𝐴)
Theorem	dmdoc2i 32917	Orthocomplements form a dual modular pair. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    ⇒   ⊢ (⊥‘𝐴) 𝑀ℋ* 𝐴
Theorem	mdcompli 32918	A condition equivalent to the modular pair property. Part of proof of Theorem 1.14 of [MaedaMaeda] p. 4. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝐴 𝑀ℋ 𝐵 ↔ (𝐴 ∩ (⊥‘(𝐴 ∩ 𝐵))) 𝑀ℋ (𝐵 ∩ (⊥‘(𝐴 ∩ 𝐵))))
Theorem	dmdcompli 32919	A condition equivalent to the dual modular pair property. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝐴 𝑀ℋ* 𝐵 ↔ (𝐴 ∩ (⊥‘(𝐴 ∩ 𝐵))) 𝑀ℋ* (𝐵 ∩ (⊥‘(𝐴 ∩ 𝐵))))
Theorem	mddmdin0i 32920*	If dual modular implies modular whenever meet is zero, then dual modular implies modular for arbitrary lattice elements. This theorem is needed for the remark after Lemma 7 of [Holland] p. 1524 to hold. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ ∀𝑥 ∈ Cℋ ∀𝑦 ∈ Cℋ ((𝑥 𝑀ℋ* 𝑦 ∧ (𝑥 ∩ 𝑦) = 0ℋ) → 𝑥 𝑀ℋ 𝑦)    ⇒   ⊢ (𝐴 𝑀ℋ* 𝐵 → 𝐴 𝑀ℋ 𝐵)
Theorem	cdjreui 32921*	A member of the sum of disjoint subspaces has a unique decomposition. Part of Lemma 5 of [Holland] p. 1520. (Contributed by NM, 20-May-2005.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    ⇒   ⊢ ((𝐶 ∈ (𝐴 +ℋ 𝐵) ∧ (𝐴 ∩ 𝐵) = 0ℋ) → ∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝐶 = (𝑥 +ℎ 𝑦))
Theorem	cdj1i 32922*	Two ways to express "𝐴 and 𝐵 are completely disjoint subspaces." (1) => (2) in Lemma 5 of [Holland] p. 1520. (Contributed by NM, 21-May-2005.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    ⇒   ⊢ (∃𝑤 ∈ ℝ (0 < 𝑤 ∧ ∀𝑦 ∈ 𝐴 ∀𝑣 ∈ 𝐵 ((normℎ‘𝑦) + (normℎ‘𝑣)) ≤ (𝑤 · (normℎ‘(𝑦 +ℎ 𝑣)))) → ∃𝑥 ∈ ℝ (0 < 𝑥 ∧ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 ((normℎ‘𝑦) = 1 → 𝑥 ≤ (normℎ‘(𝑦 −ℎ 𝑧)))))
Theorem	cdj3lem1 32923*	A property of "𝐴 and 𝐵 are completely disjoint subspaces." Part of Lemma 5 of [Holland] p. 1520. (Contributed by NM, 23-May-2005.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    ⇒   ⊢ (∃𝑥 ∈ ℝ (0 < 𝑥 ∧ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 ((normℎ‘𝑦) + (normℎ‘𝑧)) ≤ (𝑥 · (normℎ‘(𝑦 +ℎ 𝑧)))) → (𝐴 ∩ 𝐵) = 0ℋ)
Theorem	cdj3lem2 32924*	Lemma for cdj3i 32930. Value of the first-component function 𝑆. (Contributed by NM, 23-May-2005.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    &   ⊢ 𝑆 = (𝑥 ∈ (𝐴 +ℋ 𝐵) ↦ (℩𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑥 = (𝑧 +ℎ 𝑤)))    ⇒   ⊢ ((𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ∧ (𝐴 ∩ 𝐵) = 0ℋ) → (𝑆‘(𝐶 +ℎ 𝐷)) = 𝐶)
Theorem	cdj3lem2a 32925*	Lemma for cdj3i 32930. Closure of the first-component function 𝑆. (Contributed by NM, 25-May-2005.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    &   ⊢ 𝑆 = (𝑥 ∈ (𝐴 +ℋ 𝐵) ↦ (℩𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑥 = (𝑧 +ℎ 𝑤)))    ⇒   ⊢ ((𝐶 ∈ (𝐴 +ℋ 𝐵) ∧ (𝐴 ∩ 𝐵) = 0ℋ) → (𝑆‘𝐶) ∈ 𝐴)
Theorem	cdj3lem2b 32926*	Lemma for cdj3i 32930. The first-component function 𝑆 is bounded if the subspaces are completely disjoint. (Contributed by NM, 26-May-2005.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    &   ⊢ 𝑆 = (𝑥 ∈ (𝐴 +ℋ 𝐵) ↦ (℩𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑥 = (𝑧 +ℎ 𝑤)))    ⇒   ⊢ (∃𝑣 ∈ ℝ (0 < 𝑣 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ((normℎ‘𝑥) + (normℎ‘𝑦)) ≤ (𝑣 · (normℎ‘(𝑥 +ℎ 𝑦)))) → ∃𝑣 ∈ ℝ (0 < 𝑣 ∧ ∀𝑢 ∈ (𝐴 +ℋ 𝐵)(normℎ‘(𝑆‘𝑢)) ≤ (𝑣 · (normℎ‘𝑢))))
Theorem	cdj3lem3 32927*	Lemma for cdj3i 32930. Value of the second-component function 𝑇. (Contributed by NM, 23-May-2005.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    &   ⊢ 𝑇 = (𝑥 ∈ (𝐴 +ℋ 𝐵) ↦ (℩𝑤 ∈ 𝐵 ∃𝑧 ∈ 𝐴 𝑥 = (𝑧 +ℎ 𝑤)))    ⇒   ⊢ ((𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ∧ (𝐴 ∩ 𝐵) = 0ℋ) → (𝑇‘(𝐶 +ℎ 𝐷)) = 𝐷)
Theorem	cdj3lem3a 32928*	Lemma for cdj3i 32930. Closure of the second-component function 𝑇. (Contributed by NM, 26-May-2005.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    &   ⊢ 𝑇 = (𝑥 ∈ (𝐴 +ℋ 𝐵) ↦ (℩𝑤 ∈ 𝐵 ∃𝑧 ∈ 𝐴 𝑥 = (𝑧 +ℎ 𝑤)))    ⇒   ⊢ ((𝐶 ∈ (𝐴 +ℋ 𝐵) ∧ (𝐴 ∩ 𝐵) = 0ℋ) → (𝑇‘𝐶) ∈ 𝐵)
Theorem	cdj3lem3b 32929*	Lemma for cdj3i 32930. The second-component function 𝑇 is bounded if the subspaces are completely disjoint. (Contributed by NM, 31-May-2005.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    &   ⊢ 𝑇 = (𝑥 ∈ (𝐴 +ℋ 𝐵) ↦ (℩𝑤 ∈ 𝐵 ∃𝑧 ∈ 𝐴 𝑥 = (𝑧 +ℎ 𝑤)))    ⇒   ⊢ (∃𝑣 ∈ ℝ (0 < 𝑣 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ((normℎ‘𝑥) + (normℎ‘𝑦)) ≤ (𝑣 · (normℎ‘(𝑥 +ℎ 𝑦)))) → ∃𝑣 ∈ ℝ (0 < 𝑣 ∧ ∀𝑢 ∈ (𝐴 +ℋ 𝐵)(normℎ‘(𝑇‘𝑢)) ≤ (𝑣 · (normℎ‘𝑢))))
Theorem	cdj3i 32930*	Two ways to express "𝐴 and 𝐵 are completely disjoint subspaces." (1) <=> (3) in Lemma 5 of [Holland] p. 1520. (Contributed by NM, 1-Jun-2005.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    &   ⊢ 𝑆 = (𝑥 ∈ (𝐴 +ℋ 𝐵) ↦ (℩𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑥 = (𝑧 +ℎ 𝑤)))    &   ⊢ 𝑇 = (𝑥 ∈ (𝐴 +ℋ 𝐵) ↦ (℩𝑤 ∈ 𝐵 ∃𝑧 ∈ 𝐴 𝑥 = (𝑧 +ℎ 𝑤)))    &   ⊢ (𝜑 ↔ ∃𝑣 ∈ ℝ (0 < 𝑣 ∧ ∀𝑢 ∈ (𝐴 +ℋ 𝐵)(normℎ‘(𝑆‘𝑢)) ≤ (𝑣 · (normℎ‘𝑢))))    &   ⊢ (𝜓 ↔ ∃𝑣 ∈ ℝ (0 < 𝑣 ∧ ∀𝑢 ∈ (𝐴 +ℋ 𝐵)(normℎ‘(𝑇‘𝑢)) ≤ (𝑣 · (normℎ‘𝑢))))    ⇒   ⊢ (∃𝑣 ∈ ℝ (0 < 𝑣 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ((normℎ‘𝑥) + (normℎ‘𝑦)) ≤ (𝑣 · (normℎ‘(𝑥 +ℎ 𝑦)))) ↔ ((𝐴 ∩ 𝐵) = 0ℋ ∧ 𝜑 ∧ 𝜓))
PART 21  SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
21.1  Mathboxes for user contributions
21.1.1  Mathbox guidelines
Theorem	mathbox 32931	(This theorem is a dummy placeholder for these guidelines. The label of this theorem, "mathbox", is hard-coded into the Metamath program to identify the start of the mathbox section for web page generation.) A "mathbox" is a user-contributed section that is maintained by its contributor independently from the main part of set.mm. For contributors: By making a contribution, you agree to release it into the public domain, according to the statement at the beginning of set.mm. Mathboxes are provided to help keep your work synchronized with changes in set.mm while allowing you to work independently without affecting other contributors. Even though in a sense your mathbox belongs to you, it is still part of the shared body of knowledge contained in set.mm, and occasionally other people may make maintenance edits to your mathbox for things like keeping it synchronized with the rest of set.mm, reducing proof lengths, moving your theorems to the main part of set.mm when needed, and fixing typos or other errors. If you want to preserve it the way you left it, you can keep a local copy or keep track of the GitHub commit number. Guidelines: 1. See conventions 30888 for our general style guidelines. For contributing via GitHub, see https://github.com/metamath/set.mm/blob/develop/CONTRIBUTING.md 30888. The Metamath program command "verify markup *" will check that you have followed many of the conventions we use. 2. If at all possible, please use only nullary class constants for new definitions, for example as in df-div 11900. 3. Each $p and $a statement must be immediately preceded with the comment that will be shown on its web page description. The Metamath program "MM> WRITE SOURCE set.mm / REWRAP" command will take care of indentation conventions and line wrapping. 4. All mathbox content will be on public display and should hopefully reflect the overall quality of the website. 5. Mathboxes must be independent from one another (checked by "verify markup *"). If you need a theorem from another mathbox, typically it is moved to the main part of set.mm. New users should consult with more experienced users before doing this. 6. If a contributor is no longer active, we will continue the usual maintenance edits. As time goes on, often theorems will be moved to main or removed in favor of similar replacements. But we are also willing to maintain mathboxes in place, as work by others from years ago may form the foundation of future work; you could even argue that all of mathematics is like that. 7. For theorems of importance (for example, a Metamath 100 theorem or a dependency of one), we prefer to eventually move them out of mathboxes (although a mathbox is perfectly appropriate as proofs are being developed and refined). (Contributed by NM, 20-Feb-2007.) (Revised by the Metamath team, 9-Sep-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    ⇒   ⊢ 𝜑
21.2  Mathbox for Stefan Allan
Theorem	sa-abvi 32932	A theorem about the universal class. Inference associated with bj-abv 37657 (which is proved from fewer axioms). (Contributed by Stefan Allan, 9-Dec-2008.)
⊢ 𝜑    ⇒   ⊢ V = {𝑥 ∣ 𝜑}
Theorem	xfree 32933	A partial converse to 19.9t 2242. (Contributed by Stefan Allan, 21-Dec-2008.) (Revised by Mario Carneiro, 11-Dec-2016.)
⊢ (∀𝑥(𝜑 → ∀𝑥𝜑) ↔ ∀𝑥(∃𝑥𝜑 → 𝜑))
Theorem	xfree2 32934	A partial converse to 19.9t 2242. (Contributed by Stefan Allan, 21-Dec-2008.)
⊢ (∀𝑥(𝜑 → ∀𝑥𝜑) ↔ ∀𝑥(¬ 𝜑 → ∀𝑥 ¬ 𝜑))
Theorem	addltmulALT 32935	A proof readability experiment for addltmul 12508. (Contributed by Stefan Allan, 30-Oct-2010.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (2 < 𝐴 ∧ 2 < 𝐵)) → (𝐴 + 𝐵) < (𝐴 · 𝐵))
21.3  Mathbox for Thierry Arnoux
21.3.1  Propositional Calculus - misc additions
Theorem	ad11antr 32936	Deduction adding 11 conjuncts to antecedent. (Contributed by Thierry Arnoux, 27-Sep-2025.) (New usage is discouraged.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ ((((((((((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) ∧ 𝜆) ∧ 𝜅) ∧ 𝜈) → 𝜓)
Theorem	simp-12l 32937	Simplification of a conjunction. (Contributed by Thierry Arnoux, 5-Oct-2025.) (New usage is discouraged.)
⊢ (((((((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) ∧ 𝜆) ∧ 𝜅) ∧ 𝜈) → 𝜑)
Theorem	simp-12r 32938	Simplification of a conjunction. (Contributed by Thierry Arnoux, 5-Oct-2025.) (New usage is discouraged.)
⊢ (((((((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) ∧ 𝜆) ∧ 𝜅) ∧ 𝜈) → 𝜓)
Theorem	an52ds 32939	Inference exchanging the last antecedent with the second. (Contributed by Thierry Arnoux, 3-Jun-2025.)
⊢ (((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜂)    ⇒   ⊢ (((((𝜑 ∧ 𝜏) ∧ 𝜒) ∧ 𝜃) ∧ 𝜓) → 𝜂)
Theorem	an62ds 32940	Inference exchanging the last antecedent with the second one. (Contributed by Thierry Arnoux, 3-Jun-2025.)
⊢ ((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜁)    ⇒   ⊢ ((((((𝜑 ∧ 𝜂) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜓) → 𝜁)
Theorem	an72ds 32941	Inference exchanging the last antecedent with the second one. (Contributed by Thierry Arnoux, 3-Jun-2025.)
⊢ (((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜎)    ⇒   ⊢ (((((((𝜑 ∧ 𝜁) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜓) → 𝜎)
Theorem	an82ds 32942	Inference exchanging the last antecedent with the second one. (Contributed by Thierry Arnoux, 3-Jun-2025.)
⊢ ((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) → 𝜌)    ⇒   ⊢ ((((((((𝜑 ∧ 𝜎) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜓) → 𝜌)
Theorem	syl22anbrc 32943	Syllogism inference. (Contributed by Thierry Arnoux, 19-Oct-2025.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜂 ↔ ((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)))    ⇒   ⊢ (𝜑 → 𝜂)
Theorem	or3di 32944	Distributive law for disjunction. (Contributed by Thierry Arnoux, 3-Jul-2017.)
⊢ ((𝜑 ∨ (𝜓 ∧ 𝜒 ∧ 𝜏)) ↔ ((𝜑 ∨ 𝜓) ∧ (𝜑 ∨ 𝜒) ∧ (𝜑 ∨ 𝜏)))
Theorem	or3dir 32945	Distributive law for disjunction. (Contributed by Thierry Arnoux, 3-Jul-2017.)
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∨ 𝜏) ↔ ((𝜑 ∨ 𝜏) ∧ (𝜓 ∨ 𝜏) ∧ (𝜒 ∨ 𝜏)))
Theorem	3o1cs 32946	Deduction eliminating disjunct. (Contributed by Thierry Arnoux, 19-Dec-2016.)
⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) → 𝜃)    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	3o2cs 32947	Deduction eliminating disjunct. (Contributed by Thierry Arnoux, 19-Dec-2016.)
⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) → 𝜃)    ⇒   ⊢ (𝜓 → 𝜃)
Theorem	3o3cs 32948	Deduction eliminating disjunct. (Contributed by Thierry Arnoux, 19-Dec-2016.)
⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) → 𝜃)    ⇒   ⊢ (𝜒 → 𝜃)
21.3.2  Predicate Calculus
21.3.2.1  Predicate Calculus - misc additions
Theorem	sbc2iedf 32949*	Conversion of implicit substitution to explicit class substitution. (Contributed by Thierry Arnoux, 4-Jul-2023.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜒    &   ⊢ Ⅎ𝑦𝜒    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ([𝐴 / 𝑥][𝐵 / 𝑦]𝜓 ↔ 𝜒))
Theorem	rspc2daf 32950*	Double restricted specialization, using implicit substitution. (Contributed by Thierry Arnoux, 4-Jul-2023.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜒    &   ⊢ Ⅎ𝑦𝜒    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑊 𝜓)    ⇒   ⊢ (𝜑 → 𝜒)
21.3.2.2  Restricted quantification - misc additions
Theorem	ralcom4f 32951*	Commutation of restricted and unrestricted universal quantifiers. (Contributed by NM, 26-Mar-2004.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) (Revised by Thierry Arnoux, 8-Mar-2017.)
⊢ Ⅎ𝑦𝐴    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦𝜑 ↔ ∀𝑦∀𝑥 ∈ 𝐴 𝜑)
Theorem	rexcom4f 32952*	Commutation of restricted and unrestricted existential quantifiers. (Contributed by NM, 12-Apr-2004.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) (Revised by Thierry Arnoux, 8-Mar-2017.)
⊢ Ⅎ𝑦𝐴    ⇒   ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦𝜑 ↔ ∃𝑦∃𝑥 ∈ 𝐴 𝜑)
Theorem	19.9d2rf 32953	A deduction version of one direction of 19.9 2243 with two variables. (Contributed by Thierry Arnoux, 20-Mar-2017.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    &   ⊢ (𝜑 → Ⅎ𝑦𝜓)    &   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	19.9d2r 32954*	A deduction version of one direction of 19.9 2243 with two variables. (Contributed by Thierry Arnoux, 30-Jan-2017.)
⊢ (𝜑 → Ⅎ𝑥𝜓)    &   ⊢ (𝜑 → Ⅎ𝑦𝜓)    &   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	r19.29ffa 32955*	A commonly used pattern based on r19.29 3127, version with two restricted quantifiers. (Contributed by Thierry Arnoux, 26-Nov-2017.)
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ 𝜓) → 𝜒)    ⇒   ⊢ ((𝜑 ∧ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓) → 𝜒)
Theorem	reu6dv 32956*	A condition which implies existential uniqueness. (Contributed by Thierry Arnoux, 13-Oct-2025.)
⊢ (𝜑 → 𝐵 ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝑥 = 𝐵))    ⇒   ⊢ (𝜑 → ∃!𝑥 ∈ 𝐴 𝜓)
21.3.2.3  Equality
Theorem	eqtrb 32957	A transposition of equality. (Contributed by Thierry Arnoux, 20-Aug-2023.)
⊢ ((𝐴 = 𝐵 ∧ 𝐴 = 𝐶) ↔ (𝐴 = 𝐵 ∧ 𝐵 = 𝐶))
Theorem	eqelbid 32958*	A variable elimination law for equality within a given set 𝐴. See equvel 2487. (Contributed by Thierry Arnoux, 20-Feb-2025.)
⊢ (𝜑 → 𝐵 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐴)    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 (𝑥 = 𝐵 ↔ 𝑥 = 𝐶) ↔ 𝐵 = 𝐶))
21.3.2.4  Double restricted existential uniqueness quantification
Theorem	opsbc2ie 32959*	Conversion of implicit substitution to explicit class substitution for ordered pairs. (Contributed by Thierry Arnoux, 4-Jul-2023.)
⊢ (𝑝 = ⟨𝑎, 𝑏⟩ → (𝜑 ↔ 𝜒))    ⇒   ⊢ (𝑝 = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ [𝑦 / 𝑏][𝑥 / 𝑎]𝜒))
Theorem	opreu2reuALT 32960*	Correspondence between uniqueness of ordered pairs and double restricted existential uniqueness quantification. Alternate proof of one direction only, use opreu2reurex 6296 instead. (Contributed by Thierry Arnoux, 4-Jul-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑝 = ⟨𝑎, 𝑏⟩ → (𝜑 ↔ 𝜒))    ⇒   ⊢ ((∃!𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ ∃!𝑏 ∈ 𝐵 ∃𝑎 ∈ 𝐴 𝜒) → ∃!𝑝 ∈ (𝐴 × 𝐵)𝜑)
21.3.2.5  Double restricted existential uniqueness quantification syntax
Syntax	w2reu 32961	Syntax for double restricted existential uniqueness quantification.
wff ∃!𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵𝜑
Definition	df-2reu 32962	Define the double restricted existential uniqueness quantifier. (Contributed by Thierry Arnoux, 4-Jul-2023.)
⊢ (∃!𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵𝜑 ↔ (∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑))
Theorem	2reucom 32963	Double restricted existential uniqueness commutes. (Contributed by Thierry Arnoux, 4-Jul-2023.)
⊢ (∃!𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵𝜑 ↔ ∃!𝑦 ∈ 𝐵 , 𝑥 ∈ 𝐴𝜑)
Theorem	2reu2rex1 32964	Double restricted existential uniqueness implies double restricted existence. (Contributed by Thierry Arnoux, 4-Jul-2023.)
⊢ (∃!𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑)
Theorem	2reureurex 32965	Double restricted existential uniqueness implies restricted existential uniqueness with restricted existence. (Contributed by AV, 5-Jul-2023.)
⊢ (∃!𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵𝜑 → ∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑)
Theorem	2reu2reu2 32966*	Double restricted existential uniqueness implies two nested restricted existential uniqueness. (Contributed by AV, 5-Jul-2023.)
⊢ (∃!𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵𝜑 → ∃!𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝜑)
Theorem	opreu2reu1 32967*	Equivalent definition of the double restricted existential uniqueness quantifier, using uniqueness of ordered pairs. (Contributed by Thierry Arnoux, 4-Jul-2023.)
⊢ (𝑝 = ⟨𝑥, 𝑦⟩ → (𝜒 ↔ 𝜑))    ⇒   ⊢ (∃!𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵𝜑 ↔ ∃!𝑝 ∈ (𝐴 × 𝐵)𝜒)
Theorem	sq2reunnltb 32968*	There exists a unique decomposition of a prime as a sum of squares of two different positive integers iff the prime is of the form 4𝑘 + 1. Double restricted existential uniqueness variant of 2sqreunnltb 27705. (Contributed by AV, 5-Jul-2023.)
⊢ (𝑃 ∈ ℙ → ((𝑃 mod 4) = 1 ↔ ∃!𝑎 ∈ ℕ , 𝑏 ∈ ℕ(𝑎 < 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃)))
Theorem	addsqnot2reu 32969*	For each complex number 𝐶, there does not uniquely exist two complex numbers 𝑎 and 𝑏, with 𝑏 squared and added to 𝑎 resulting in the given complex number 𝐶. Double restricted existential uniqueness variant of addsqn2reurex2 27689. (Contributed by AV, 5-Jul-2023.)
⊢ (𝐶 ∈ ℂ → ¬ ∃!𝑎 ∈ ℂ , 𝑏 ∈ ℂ(𝑎 + (𝑏↑2)) = 𝐶)
21.3.2.6  Substitution (without distinct variables) - misc additions
Theorem	sbceqbidf 32970	Equality theorem for class substitution. (Contributed by Thierry Arnoux, 4-Sep-2018.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ [𝐵 / 𝑥]𝜒))
Theorem	sbcies 32971*	A special version of class substitution commonly used for structures. (Contributed by Thierry Arnoux, 14-Mar-2019.)
⊢ 𝐴 = (𝐸‘𝑊)    &   ⊢ (𝑎 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝑤 = 𝑊 → ([(𝐸‘𝑤) / 𝑎]𝜓 ↔ 𝜑))
21.3.2.7  Existential "at most one" - misc additions
Theorem	mo5f 32972*	Alternate definition of "at most one." (Contributed by Thierry Arnoux, 1-Mar-2017.)
⊢ Ⅎ𝑖𝜑    &   ⊢ Ⅎ𝑗𝜑    ⇒   ⊢ (∃*𝑥𝜑 ↔ ∀𝑖∀𝑗(([𝑖 / 𝑥]𝜑 ∧ [𝑗 / 𝑥]𝜑) → 𝑖 = 𝑗))
Theorem	nmo 32973*	Negation of "at most one". (Contributed by Thierry Arnoux, 26-Feb-2017.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (¬ ∃*𝑥𝜑 ↔ ∀𝑦∃𝑥(𝜑 ∧ 𝑥 ≠ 𝑦))
21.3.2.8  Existential uniqueness - misc additions
Theorem	reuxfrdf 32974*	Transfer existential uniqueness from a variable 𝑥 to another variable 𝑦 contained in expression 𝐴. Cf. reuxfrd 3709 (Contributed by Thierry Arnoux, 7-Apr-2017.) (Revised by Thierry Arnoux, 8-Oct-2017.) (Revised by Thierry Arnoux, 30-Mar-2018.)
⊢ Ⅎ𝑦𝐵    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → 𝐴 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∃*𝑦 ∈ 𝐶 𝑥 = 𝐴)    ⇒   ⊢ (𝜑 → (∃!𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓) ↔ ∃!𝑦 ∈ 𝐶 𝜓))
Theorem	rexunirn 32975*	Restricted existential quantification over the union of the range of a function. Cf. rexrn 7084 and eluni2 4874. (Contributed by Thierry Arnoux, 19-Sep-2017.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    &   ⊢ (𝑥 ∈ 𝐴 → 𝐵 ∈ 𝑉)    ⇒   ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑦 ∈ ∪ ran 𝐹𝜑)
21.3.2.9  Restricted "at most one" - misc additions
Theorem	rmoxfrd 32976*	Transfer "at most one" restricted quantification from a variable 𝑥 to another variable 𝑦 contained in expression 𝐴. (Contributed by Thierry Arnoux, 7-Apr-2017.) (Revised by Thierry Arnoux, 8-Oct-2017.)
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → 𝐴 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∃!𝑦 ∈ 𝐶 𝑥 = 𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃*𝑥 ∈ 𝐵 𝜓 ↔ ∃*𝑦 ∈ 𝐶 𝜒))
Theorem	rmoun 32977	"At most one" restricted existential quantifier for a union implies the same quantifier on both sets. (Contributed by Thierry Arnoux, 27-Nov-2023.)
⊢ (∃*𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 → (∃*𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥 ∈ 𝐵 𝜑))
Theorem	rmounid 32978*	A case where an "at most one" restricted existential quantifier for a union is equivalent to such a quantifier for one of the sets. (Contributed by Thierry Arnoux, 27-Nov-2023.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ¬ 𝜓)    ⇒   ⊢ (𝜑 → (∃*𝑥 ∈ (𝐴 ∪ 𝐵)𝜓 ↔ ∃*𝑥 ∈ 𝐴 𝜓))
21.3.2.10  Restricted iota (description binder)
Theorem	riotaeqbidva 32979*	Equivalent wff's yield equal restricted definition binders (deduction form). (raleqbidva 3327 analog.) (Contributed by Thierry Arnoux, 29-Jan-2025.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜓) = (℩𝑥 ∈ 𝐵 𝜒))
21.3.3  General Set Theory
21.3.3.1  Class abstractions (a.k.a. class builders)
Theorem	dmrab 32980*	Domain of a restricted class abstraction over a cartesian product. (Contributed by Thierry Arnoux, 3-Jul-2023.)
⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ 𝜓))    ⇒   ⊢ dom {𝑧 ∈ (𝐴 × 𝐵) ∣ 𝜑} = {𝑥 ∈ 𝐴 ∣ ∃𝑦 ∈ 𝐵 𝜓}
Theorem	difrab2 32981	Difference of two restricted class abstractions. Compare with difrab 4267. (Contributed by Thierry Arnoux, 3-Jan-2022.)
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∖ {𝑥 ∈ 𝐵 ∣ 𝜑}) = {𝑥 ∈ (𝐴 ∖ 𝐵) ∣ 𝜑}
Theorem	rabexgfGS 32982	Separation Scheme in terms of a restricted class abstraction. To be removed in profit of Glauco's equivalent version. (Contributed by Thierry Arnoux, 11-May-2017.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ V)
Theorem	rabsnel 32983*	Truth implied by equality of a restricted class abstraction and a singleton. (Contributed by Thierry Arnoux, 15-Sep-2018.)
⊢ 𝐵 ∈ V    ⇒   ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = {𝐵} → 𝐵 ∈ 𝐴)
Theorem	rabsspr 32984*	Conditions for a restricted class abstraction to be a subset of an unordered pair. (Contributed by Thierry Arnoux, 6-Jul-2025.)
⊢ ({𝑥 ∈ 𝑉 ∣ 𝜑} ⊆ {𝑋, 𝑌} ↔ ∀𝑥 ∈ 𝑉 (𝜑 → (𝑥 = 𝑋 ∨ 𝑥 = 𝑌)))
Theorem	rabsstp 32985*	Conditions for a restricted class abstraction to be a subset of an unordered triple. (Contributed by Thierry Arnoux, 6-Jul-2025.)
⊢ ({𝑥 ∈ 𝑉 ∣ 𝜑} ⊆ {𝑋, 𝑌, 𝑍} ↔ ∀𝑥 ∈ 𝑉 (𝜑 → (𝑥 = 𝑋 ∨ 𝑥 = 𝑌 ∨ 𝑥 = 𝑍)))
Theorem	3unrab 32986	Union of three restricted class abstractions. (Contributed by Thierry Arnoux, 6-Jul-2025.)
⊢ (({𝑥 ∈ 𝐴 ∣ 𝜑} ∪ {𝑥 ∈ 𝐴 ∣ 𝜓}) ∪ {𝑥 ∈ 𝐴 ∣ 𝜒}) = {𝑥 ∈ 𝐴 ∣ (𝜑 ∨ 𝜓 ∨ 𝜒)}
Theorem	foresf1o 32987*	From a surjective function, *choose* a subset of the domain, such that the restricted function is bijective. (Contributed by Thierry Arnoux, 27-Jan-2020.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴–onto→𝐵) → ∃𝑥 ∈ 𝒫 𝐴(𝐹 ↾ 𝑥):𝑥–1-1-onto→𝐵)
Theorem	rabfodom 32988*	Domination relation for restricted abstract class builders, based on a surjective function. (Contributed by Thierry Arnoux, 27-Jan-2020.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = (𝐹‘𝑥)) → (𝜒 ↔ 𝜓))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐴–onto→𝐵)    ⇒   ⊢ (𝜑 → {𝑦 ∈ 𝐵 ∣ 𝜒} ≼ {𝑥 ∈ 𝐴 ∣ 𝜓})
Theorem	rabrexfi 32989*	Conditions for a class abstraction with a restricted existential quantification to be finite. (Contributed by Thierry Arnoux, 6-Jul-2025.)
⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → {𝑥 ∈ 𝐴 ∣ 𝜓} ∈ Fin)    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ ∃𝑦 ∈ 𝐵 𝜓} ∈ Fin)
21.3.3.2  Image Sets
Theorem	abrexdomjm 32990*	An indexed set is dominated by the indexing set. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (𝑦 ∈ 𝐴 → ∃*𝑥𝜑)    ⇒   ⊢ (𝐴 ∈ 𝑉 → {𝑥 ∣ ∃𝑦 ∈ 𝐴 𝜑} ≼ 𝐴)
Theorem	abrexdom2jm 32991*	An indexed set is dominated by the indexing set. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∣ ∃𝑦 ∈ 𝐴 𝑥 = 𝐵} ≼ 𝐴)
Theorem	abrexexd 32992*	Existence of a class abstraction of existentially restricted sets. (Contributed by Thierry Arnoux, 10-May-2017.)
⊢ Ⅎ𝑥𝐴    &   ⊢ (𝜑 → 𝐴 ∈ V)    ⇒   ⊢ (𝜑 → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ V)
Theorem	elabreximd 32993*	Class substitution in an image set. (Contributed by Thierry Arnoux, 30-Dec-2016.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝜒    &   ⊢ (𝐴 = 𝐵 → (𝜒 ↔ 𝜓))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝜓)    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐶 𝑦 = 𝐵}) → 𝜒)
Theorem	elabreximdv 32994*	Class substitution in an image set. (Contributed by Thierry Arnoux, 30-Dec-2016.)
⊢ (𝐴 = 𝐵 → (𝜒 ↔ 𝜓))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝜓)    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐶 𝑦 = 𝐵}) → 𝜒)
Theorem	abrexss 32995*	A necessary condition for an image set to be a subset. (Contributed by Thierry Arnoux, 6-Feb-2017.)
⊢ Ⅎ𝑥𝐶    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ⊆ 𝐶)
21.3.3.3  Set relations and operations - misc additions
Theorem	nelun 32996	Negated membership for a union. (Contributed by Thierry Arnoux, 13-Dec-2023.)
⊢ (𝐴 = (𝐵 ∪ 𝐶) → (¬ 𝑋 ∈ 𝐴 ↔ (¬ 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ∈ 𝐶)))
Theorem	snsssng 32997	If a singleton is a subset of another, their members are equal. (Contributed by NM, 28-May-2006.) (Revised by Thierry Arnoux, 11-Apr-2024.)
⊢ ((𝐴 ∈ 𝑉 ∧ {𝐴} ⊆ {𝐵}) → 𝐴 = 𝐵)
Theorem	n0nsnel 32998*	If a class with one element is not a singleton, there is at least another element in this class. (Contributed by AV, 6-Mar-2025.) (Revised by Thierry Arnoux, 28-May-2025.)
⊢ ((𝐶 ∈ 𝐵 ∧ 𝐵 ≠ {𝐴}) → ∃𝑥 ∈ 𝐵 𝑥 ≠ 𝐴)
Theorem	inin 32999	Intersection with an intersection. (Contributed by Thierry Arnoux, 27-Dec-2016.)
⊢ (𝐴 ∩ (𝐴 ∩ 𝐵)) = (𝐴 ∩ 𝐵)
Theorem	difininv 33000	Condition for the intersections of two sets with a given set to be equal. (Contributed by Thierry Arnoux, 28-Dec-2021.)
⊢ ((((𝐴 ∖ 𝐶) ∩ 𝐵) = ∅ ∧ ((𝐶 ∖ 𝐴) ∩ 𝐵) = ∅) → (𝐴 ∩ 𝐵) = (𝐶 ∩ 𝐵))