![]() |
Metamath
Proof Explorer Theorem List (p. 303 of 454) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-28701) |
![]() (28702-30224) |
![]() (30225-45333) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | sumdmdlem 30201 | Lemma for sumdmdi 30203. 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 30202* | Lemma for sumdmdi 30203. (Contributed by NM, 23-Dec-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (∀𝑥 ∈ HAtoms ((𝑥 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵) → (𝐴 +ℋ 𝐵) = (𝐴 ∨ℋ 𝐵)) | ||
Theorem | sumdmdi 30203 | 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 30204* | Dual modular pair property in terms of atoms. (Contributed by NM, 15-Jan-2005.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 𝑀ℋ* 𝐵 ↔ ∀𝑥 ∈ HAtoms ((𝑥 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵)) | ||
Theorem | dmdbr5ati 30205* | Dual modular pair property in terms of atoms. (Contributed by NM, 14-Jan-2005.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 𝑀ℋ* 𝐵 ↔ ∀𝑥 ∈ HAtoms (𝑥 ⊆ (𝐴 ∨ℋ 𝐵) → 𝑥 ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵))) | ||
Theorem | dmdbr6ati 30206* | 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 30207* | Dual modular pair property in terms of atoms. (Contributed by NM, 18-Jan-2005.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 𝑀ℋ* 𝐵 ↔ ∀𝑥 ∈ HAtoms ((𝐴 ∨ℋ 𝐵) ∩ 𝑥) ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵)) | ||
Theorem | mdoc1i 30208 | Orthocomplements form a modular pair. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ ⇒ ⊢ 𝐴 𝑀ℋ (⊥‘𝐴) | ||
Theorem | mdoc2i 30209 | Orthocomplements form a modular pair. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ ⇒ ⊢ (⊥‘𝐴) 𝑀ℋ 𝐴 | ||
Theorem | dmdoc1i 30210 | Orthocomplements form a dual modular pair. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ ⇒ ⊢ 𝐴 𝑀ℋ* (⊥‘𝐴) | ||
Theorem | dmdoc2i 30211 | Orthocomplements form a dual modular pair. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ ⇒ ⊢ (⊥‘𝐴) 𝑀ℋ* 𝐴 | ||
Theorem | mdcompli 30212 | 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 30213 | A condition equivalent to the dual modular pair property. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 𝑀ℋ* 𝐵 ↔ (𝐴 ∩ (⊥‘(𝐴 ∩ 𝐵))) 𝑀ℋ* (𝐵 ∩ (⊥‘(𝐴 ∩ 𝐵)))) | ||
Theorem | mddmdin0i 30214* | 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 30215* | 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 30216* | 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 30217* | 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 30218* | Lemma for cdj3i 30224. Value of the first-component function 𝑆. (Contributed by NM, 23-May-2005.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Sℋ & ⊢ 𝐵 ∈ Sℋ & ⊢ 𝑆 = (𝑥 ∈ (𝐴 +ℋ 𝐵) ↦ (℩𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑥 = (𝑧 +ℎ 𝑤))) ⇒ ⊢ ((𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ∧ (𝐴 ∩ 𝐵) = 0ℋ) → (𝑆‘(𝐶 +ℎ 𝐷)) = 𝐶) | ||
Theorem | cdj3lem2a 30219* | Lemma for cdj3i 30224. Closure of the first-component function 𝑆. (Contributed by NM, 25-May-2005.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Sℋ & ⊢ 𝐵 ∈ Sℋ & ⊢ 𝑆 = (𝑥 ∈ (𝐴 +ℋ 𝐵) ↦ (℩𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑥 = (𝑧 +ℎ 𝑤))) ⇒ ⊢ ((𝐶 ∈ (𝐴 +ℋ 𝐵) ∧ (𝐴 ∩ 𝐵) = 0ℋ) → (𝑆‘𝐶) ∈ 𝐴) | ||
Theorem | cdj3lem2b 30220* | Lemma for cdj3i 30224. 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 30221* | Lemma for cdj3i 30224. Value of the second-component function 𝑇. (Contributed by NM, 23-May-2005.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Sℋ & ⊢ 𝐵 ∈ Sℋ & ⊢ 𝑇 = (𝑥 ∈ (𝐴 +ℋ 𝐵) ↦ (℩𝑤 ∈ 𝐵 ∃𝑧 ∈ 𝐴 𝑥 = (𝑧 +ℎ 𝑤))) ⇒ ⊢ ((𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ∧ (𝐴 ∩ 𝐵) = 0ℋ) → (𝑇‘(𝐶 +ℎ 𝐷)) = 𝐷) | ||
Theorem | cdj3lem3a 30222* | Lemma for cdj3i 30224. Closure of the second-component function 𝑇. (Contributed by NM, 26-May-2005.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Sℋ & ⊢ 𝐵 ∈ Sℋ & ⊢ 𝑇 = (𝑥 ∈ (𝐴 +ℋ 𝐵) ↦ (℩𝑤 ∈ 𝐵 ∃𝑧 ∈ 𝐴 𝑥 = (𝑧 +ℎ 𝑤))) ⇒ ⊢ ((𝐶 ∈ (𝐴 +ℋ 𝐵) ∧ (𝐴 ∩ 𝐵) = 0ℋ) → (𝑇‘𝐶) ∈ 𝐵) | ||
Theorem | cdj3lem3b 30223* | Lemma for cdj3i 30224. 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 30224* | 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ℋ ∧ 𝜑 ∧ 𝜓)) | ||
Theorem | mathbox 30225 |
(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 28185 for our general style guidelines. For contributing via GitHub, see https://github.com/metamath/set.mm/blob/develop/CONTRIBUTING.md 28185. The Metamath program command "verify markup *" will check that you have followed many of 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 11287. 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.) |
⊢ 𝜑 ⇒ ⊢ 𝜑 | ||
Theorem | sa-abvi 30226 | A theorem about the universal class. Inference associated with bj-abv 34347 (which is proved from fewer axioms). (Contributed by Stefan Allan, 9-Dec-2008.) |
⊢ 𝜑 ⇒ ⊢ V = {𝑥 ∣ 𝜑} | ||
Theorem | xfree 30227 | A partial converse to 19.9t 2202. (Contributed by Stefan Allan, 21-Dec-2008.) (Revised by Mario Carneiro, 11-Dec-2016.) |
⊢ (∀𝑥(𝜑 → ∀𝑥𝜑) ↔ ∀𝑥(∃𝑥𝜑 → 𝜑)) | ||
Theorem | xfree2 30228 | A partial converse to 19.9t 2202. (Contributed by Stefan Allan, 21-Dec-2008.) |
⊢ (∀𝑥(𝜑 → ∀𝑥𝜑) ↔ ∀𝑥(¬ 𝜑 → ∀𝑥 ¬ 𝜑)) | ||
Theorem | addltmulALT 30229 | A proof readability experiment for addltmul 11861. (Contributed by Stefan Allan, 30-Oct-2010.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (2 < 𝐴 ∧ 2 < 𝐵)) → (𝐴 + 𝐵) < (𝐴 · 𝐵)) | ||
Theorem | bian1d 30230 | Adding a superfluous conjunct in a biconditional. (Contributed by Thierry Arnoux, 26-Feb-2017.) |
⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃))) ⇒ ⊢ (𝜑 → ((𝜒 ∧ 𝜓) ↔ (𝜒 ∧ 𝜃))) | ||
Theorem | or3di 30231 | Distributive law for disjunction. (Contributed by Thierry Arnoux, 3-Jul-2017.) |
⊢ ((𝜑 ∨ (𝜓 ∧ 𝜒 ∧ 𝜏)) ↔ ((𝜑 ∨ 𝜓) ∧ (𝜑 ∨ 𝜒) ∧ (𝜑 ∨ 𝜏))) | ||
Theorem | or3dir 30232 | Distributive law for disjunction. (Contributed by Thierry Arnoux, 3-Jul-2017.) |
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∨ 𝜏) ↔ ((𝜑 ∨ 𝜏) ∧ (𝜓 ∨ 𝜏) ∧ (𝜒 ∨ 𝜏))) | ||
Theorem | 3o1cs 30233 | Deduction eliminating disjunct. (Contributed by Thierry Arnoux, 19-Dec-2016.) |
⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) → 𝜃) ⇒ ⊢ (𝜑 → 𝜃) | ||
Theorem | 3o2cs 30234 | Deduction eliminating disjunct. (Contributed by Thierry Arnoux, 19-Dec-2016.) |
⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) → 𝜃) ⇒ ⊢ (𝜓 → 𝜃) | ||
Theorem | 3o3cs 30235 | Deduction eliminating disjunct. (Contributed by Thierry Arnoux, 19-Dec-2016.) |
⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) → 𝜃) ⇒ ⊢ (𝜒 → 𝜃) | ||
Theorem | biadanid 30236 | Deduction associated with biadani 819. Add a conjunction to an equivalence. (Contributed by Thierry Arnoux, 16-Jun-2024.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜒) & ⊢ ((𝜑 ∧ 𝜒) → (𝜓 ↔ 𝜃)) ⇒ ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃))) | ||
Theorem | sbc2iedf 30237* | Conversion of implicit substitution to explicit class substitution. (Contributed by Thierry Arnoux, 4-Jul-2023.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜒 & ⊢ Ⅎ𝑦𝜒 & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ([𝐴 / 𝑥][𝐵 / 𝑦]𝜓 ↔ 𝜒)) | ||
Theorem | rspc2daf 30238* | Double restricted specialization, using implicit substitution. (Contributed by Thierry Arnoux, 4-Jul-2023.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜒 & ⊢ Ⅎ𝑦𝜒 & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑊 𝜓) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | nelbOLD 30239* | Obsolete version of nelb 3227 as of 23-Jan-2024. (Contributed by Thierry Arnoux, 20-Nov-2023.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (¬ 𝐴 ∈ 𝐵 ↔ ∀𝑥 ∈ 𝐵 𝑥 ≠ 𝐴) | ||
Theorem | ralcom4f 30240* | 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 30241* | 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 30242 | A deduction version of one direction of 19.9 2203 with two variables. (Contributed by Thierry Arnoux, 20-Mar-2017.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝜓) & ⊢ (𝜑 → Ⅎ𝑦𝜓) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | 19.9d2r 30243* | A deduction version of one direction of 19.9 2203 with two variables. (Contributed by Thierry Arnoux, 30-Jan-2017.) |
⊢ (𝜑 → Ⅎ𝑥𝜓) & ⊢ (𝜑 → Ⅎ𝑦𝜓) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | r19.29ffa 30244* | A commonly used pattern based on r19.29 3216, version with two restricted quantifiers. (Contributed by Thierry Arnoux, 26-Nov-2017.) |
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ 𝜓) → 𝜒) ⇒ ⊢ ((𝜑 ∧ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓) → 𝜒) | ||
Theorem | eqtrb 30245 | A transposition of equality. (Contributed by Thierry Arnoux, 20-Aug-2023.) |
⊢ ((𝐴 = 𝐵 ∧ 𝐴 = 𝐶) ↔ (𝐴 = 𝐵 ∧ 𝐵 = 𝐶)) | ||
Theorem | opsbc2ie 30246* | Conversion of implicit substitution to explicit class substitution for ordered pairs. (Contributed by Thierry Arnoux, 4-Jul-2023.) |
⊢ (𝑝 = 〈𝑎, 𝑏〉 → (𝜑 ↔ 𝜒)) ⇒ ⊢ (𝑝 = 〈𝑥, 𝑦〉 → (𝜑 ↔ [𝑦 / 𝑏][𝑥 / 𝑎]𝜒)) | ||
Theorem | opreu2reuALT 30247* | Correspondence between uniqueness of ordered pairs and double restricted existential uniqueness quantification. Alternate proof of one direction only, use opreu2reurex 6113 instead. (Contributed by Thierry Arnoux, 4-Jul-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑝 = 〈𝑎, 𝑏〉 → (𝜑 ↔ 𝜒)) ⇒ ⊢ ((∃!𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ ∃!𝑏 ∈ 𝐵 ∃𝑎 ∈ 𝐴 𝜒) → ∃!𝑝 ∈ (𝐴 × 𝐵)𝜑) | ||
Syntax | w2reu 30248 | Syntax for double restricted existential uniqueness quantification. |
wff ∃!𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵𝜑 | ||
Definition | df-2reu 30249 | Define the double restricted existential uniqueness quantifier. (Contributed by Thierry Arnoux, 4-Jul-2023.) |
⊢ (∃!𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵𝜑 ↔ (∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑)) | ||
Theorem | 2reucom 30250 | Double restricted existential uniqueness commutes. (Contributed by Thierry Arnoux, 4-Jul-2023.) |
⊢ (∃!𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵𝜑 ↔ ∃!𝑦 ∈ 𝐵 , 𝑥 ∈ 𝐴𝜑) | ||
Theorem | 2reu2rex1 30251 | Double restricted existential uniqueness implies double restricted existence. (Contributed by Thierry Arnoux, 4-Jul-2023.) |
⊢ (∃!𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) | ||
Theorem | 2reureurex 30252 | Double restricted existential uniqueness implies restricted existential uniqueness with restricted existence. (Contributed by AV, 5-Jul-2023.) |
⊢ (∃!𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵𝜑 → ∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) | ||
Theorem | 2reu2reu2 30253* | Double restricted existential uniqueness implies two nested restricted existential uniqueness. (Contributed by AV, 5-Jul-2023.) |
⊢ (∃!𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵𝜑 → ∃!𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝜑) | ||
Theorem | opreu2reu1 30254* | Equivalent definition of the double restricted existential uniqueness quantifier, using uniqueness of ordered pairs. (Contributed by Thierry Arnoux, 4-Jul-2023.) |
⊢ (𝑝 = 〈𝑥, 𝑦〉 → (𝜒 ↔ 𝜑)) ⇒ ⊢ (∃!𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵𝜑 ↔ ∃!𝑝 ∈ (𝐴 × 𝐵)𝜒) | ||
Theorem | sq2reunnltb 30255* | 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 26045. (Contributed by AV, 5-Jul-2023.) |
⊢ (𝑃 ∈ ℙ → ((𝑃 mod 4) = 1 ↔ ∃!𝑎 ∈ ℕ , 𝑏 ∈ ℕ(𝑎 < 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃))) | ||
Theorem | addsqnot2reu 30256* | 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 26029. (Contributed by AV, 5-Jul-2023.) |
⊢ (𝐶 ∈ ℂ → ¬ ∃!𝑎 ∈ ℂ , 𝑏 ∈ ℂ(𝑎 + (𝑏↑2)) = 𝐶) | ||
Theorem | sbceqbidf 30257 | Equality theorem for class substitution. (Contributed by Thierry Arnoux, 4-Sep-2018.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ [𝐵 / 𝑥]𝜒)) | ||
Theorem | sbcies 30258* | A special version of class substitution commonly used for structures. (Contributed by Thierry Arnoux, 14-Mar-2019.) |
⊢ 𝐴 = (𝐸‘𝑊) & ⊢ (𝑎 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝑤 = 𝑊 → ([(𝐸‘𝑤) / 𝑎]𝜓 ↔ 𝜑)) | ||
Theorem | moel 30259* | "At most one" element in a set. (Contributed by Thierry Arnoux, 26-Jul-2018.) |
⊢ (∃*𝑥 𝑥 ∈ 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝑥 = 𝑦) | ||
Theorem | mo5f 30260* | Alternate definition of "at most one." (Contributed by Thierry Arnoux, 1-Mar-2017.) |
⊢ Ⅎ𝑖𝜑 & ⊢ Ⅎ𝑗𝜑 ⇒ ⊢ (∃*𝑥𝜑 ↔ ∀𝑖∀𝑗(([𝑖 / 𝑥]𝜑 ∧ [𝑗 / 𝑥]𝜑) → 𝑖 = 𝑗)) | ||
Theorem | nmo 30261* | Negation of "at most one". (Contributed by Thierry Arnoux, 26-Feb-2017.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (¬ ∃*𝑥𝜑 ↔ ∀𝑦∃𝑥(𝜑 ∧ 𝑥 ≠ 𝑦)) | ||
Theorem | reuxfrdf 30262* | Transfer existential uniqueness from a variable 𝑥 to another variable 𝑦 contained in expression 𝐴. Cf. reuxfrd 3687 (Contributed by Thierry Arnoux, 7-Apr-2017.) (Revised by Thierry Arnoux, 8-Oct-2017.) (Revised by Thierry Arnoux, 30-Mar-2018.) |
⊢ Ⅎ𝑦𝐵 & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → 𝐴 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∃*𝑦 ∈ 𝐶 𝑥 = 𝐴) ⇒ ⊢ (𝜑 → (∃!𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓) ↔ ∃!𝑦 ∈ 𝐶 𝜓)) | ||
Theorem | rexunirn 30263* | Restricted existential quantification over the union of the range of a function. Cf. rexrn 6830 and eluni2 4804. (Contributed by Thierry Arnoux, 19-Sep-2017.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ (𝑥 ∈ 𝐴 → 𝐵 ∈ 𝑉) ⇒ ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑦 ∈ ∪ ran 𝐹𝜑) | ||
Theorem | rmoxfrd 30264* | 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 30265 | "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 30266* | 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.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ¬ 𝜓) ⇒ ⊢ (𝜑 → (∃*𝑥 ∈ (𝐴 ∪ 𝐵)𝜓 ↔ ∃*𝑥 ∈ 𝐴 𝜓)) | ||
Theorem | dmrab 30267* | Domain of a restricted class abstraction over a cartesian product. (Contributed by Thierry Arnoux, 3-Jul-2023.) |
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (𝜑 ↔ 𝜓)) ⇒ ⊢ dom {𝑧 ∈ (𝐴 × 𝐵) ∣ 𝜑} = {𝑥 ∈ 𝐴 ∣ ∃𝑦 ∈ 𝐵 𝜓} | ||
Theorem | difrab2 30268 | Difference of two restricted class abstractions. Compare with difrab 4229. (Contributed by Thierry Arnoux, 3-Jan-2022.) |
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∖ {𝑥 ∈ 𝐵 ∣ 𝜑}) = {𝑥 ∈ (𝐴 ∖ 𝐵) ∣ 𝜑} | ||
Theorem | rabexgfGS 30269 | 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 30270* | Truth implied by equality of a restricted class abstraction and a singleton. (Contributed by Thierry Arnoux, 15-Sep-2018.) |
⊢ 𝐵 ∈ V ⇒ ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = {𝐵} → 𝐵 ∈ 𝐴) | ||
Theorem | rabeqsnd 30271* | Conditions for a restricted class abstraction to be a singleton, in deduction form. (Contributed by Thierry Arnoux, 2-Dec-2021.) |
⊢ (𝑥 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → 𝐵 ∈ 𝐴) & ⊢ (𝜑 → 𝜒) & ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓) → 𝑥 = 𝐵) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝐵}) | ||
Theorem | eqrrabd 30272* | Deduce equality with a restricted abstraction. (Contributed by Thierry Arnoux, 11-Apr-2024.) |
⊢ (𝜑 → 𝐵 ⊆ 𝐴) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑥 ∈ 𝐵 ↔ 𝜓)) ⇒ ⊢ (𝜑 → 𝐵 = {𝑥 ∈ 𝐴 ∣ 𝜓}) | ||
Theorem | foresf1o 30273* | 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 30274* | Domination relation for restricted abstract class builders, based on a surjective function. (Contributed by Thierry Arnoux, 27-Jan-2020.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = (𝐹‘𝑥)) → (𝜒 ↔ 𝜓)) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴–onto→𝐵) ⇒ ⊢ (𝜑 → {𝑦 ∈ 𝐵 ∣ 𝜒} ≼ {𝑥 ∈ 𝐴 ∣ 𝜓}) | ||
Theorem | abrexdomjm 30275* | An indexed set is dominated by the indexing set. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (𝑦 ∈ 𝐴 → ∃*𝑥𝜑) ⇒ ⊢ (𝐴 ∈ 𝑉 → {𝑥 ∣ ∃𝑦 ∈ 𝐴 𝜑} ≼ 𝐴) | ||
Theorem | abrexdom2jm 30276* | An indexed set is dominated by the indexing set. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∣ ∃𝑦 ∈ 𝐴 𝑥 = 𝐵} ≼ 𝐴) | ||
Theorem | abrexexd 30277* | Existence of a class abstraction of existentially restricted sets. (Contributed by Thierry Arnoux, 10-May-2017.) |
⊢ Ⅎ𝑥𝐴 & ⊢ (𝜑 → 𝐴 ∈ V) ⇒ ⊢ (𝜑 → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ V) | ||
Theorem | elabreximd 30278* | Class substitution in an image set. (Contributed by Thierry Arnoux, 30-Dec-2016.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝜒 & ⊢ (𝐴 = 𝐵 → (𝜒 ↔ 𝜓)) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝜓) ⇒ ⊢ ((𝜑 ∧ 𝐴 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐶 𝑦 = 𝐵}) → 𝜒) | ||
Theorem | elabreximdv 30279* | Class substitution in an image set. (Contributed by Thierry Arnoux, 30-Dec-2016.) |
⊢ (𝐴 = 𝐵 → (𝜒 ↔ 𝜓)) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝜓) ⇒ ⊢ ((𝜑 ∧ 𝐴 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐶 𝑦 = 𝐵}) → 𝜒) | ||
Theorem | abrexss 30280* | A necessary condition for an image set to be a subset. (Contributed by Thierry Arnoux, 6-Feb-2017.) |
⊢ Ⅎ𝑥𝐶 ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ⊆ 𝐶) | ||
Theorem | elunsn 30281 | Elementhood to a union with a singleton. (Contributed by Thierry Arnoux, 14-Dec-2023.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ (𝐵 ∪ {𝐶}) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐶))) | ||
Theorem | nelun 30282 | Negated membership for a union. (Contributed by Thierry Arnoux, 13-Dec-2023.) |
⊢ (𝐴 = (𝐵 ∪ 𝐶) → (¬ 𝑋 ∈ 𝐴 ↔ (¬ 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ∈ 𝐶))) | ||
Theorem | disjdifr 30283 | A class and its relative complement are disjoint. (Contributed by Thierry Arnoux, 29-Nov-2023.) |
⊢ ((𝐵 ∖ 𝐴) ∩ 𝐴) = ∅ | ||
Theorem | snsssng 30284 | 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 | rabss3d 30285* | Subclass law for restricted abstraction. (Contributed by Thierry Arnoux, 25-Sep-2017.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝜓)) → 𝑥 ∈ 𝐵) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} ⊆ {𝑥 ∈ 𝐵 ∣ 𝜓}) | ||
Theorem | inin 30286 | Intersection with an intersection. (Contributed by Thierry Arnoux, 27-Dec-2016.) |
⊢ (𝐴 ∩ (𝐴 ∩ 𝐵)) = (𝐴 ∩ 𝐵) | ||
Theorem | inindif 30287 | See inundif 4385. (Contributed by Thierry Arnoux, 13-Sep-2017.) |
⊢ ((𝐴 ∩ 𝐶) ∩ (𝐴 ∖ 𝐶)) = ∅ | ||
Theorem | difininv 30288 | Condition for the intersections of two sets with a given set to be equal. (Contributed by Thierry Arnoux, 28-Dec-2021.) |
⊢ ((((𝐴 ∖ 𝐶) ∩ 𝐵) = ∅ ∧ ((𝐶 ∖ 𝐴) ∩ 𝐵) = ∅) → (𝐴 ∩ 𝐵) = (𝐶 ∩ 𝐵)) | ||
Theorem | difeq 30289 | Rewriting an equation with class difference, without using quantifiers. (Contributed by Thierry Arnoux, 24-Sep-2017.) |
⊢ ((𝐴 ∖ 𝐵) = 𝐶 ↔ ((𝐶 ∩ 𝐵) = ∅ ∧ (𝐶 ∪ 𝐵) = (𝐴 ∪ 𝐵))) | ||
Theorem | eqdif 30290 | If both set differences of two sets are empty, those sets are equal. (Contributed by Thierry Arnoux, 16-Nov-2023.) |
⊢ (((𝐴 ∖ 𝐵) = ∅ ∧ (𝐵 ∖ 𝐴) = ∅) → 𝐴 = 𝐵) | ||
Theorem | undif5 30291 | An equality involving class union and class difference. (Contributed by Thierry Arnoux, 26-Jun-2024.) |
⊢ ((𝐴 ∩ 𝐵) = ∅ → ((𝐴 ∪ 𝐵) ∖ 𝐵) = 𝐴) | ||
Theorem | indifbi 30292 | Two ways to express equality relative to a class 𝐴. (Contributed by Thierry Arnoux, 23-Jun-2024.) |
⊢ ((𝐴 ∩ 𝐵) = (𝐴 ∩ 𝐶) ↔ (𝐴 ∖ 𝐵) = (𝐴 ∖ 𝐶)) | ||
Theorem | diffib 30293 | Case where diffi 8734 is a biconditional. (Contributed by Thierry Arnoux, 27-Jun-2024.) |
⊢ (𝐵 ∈ Fin → (𝐴 ∈ Fin ↔ (𝐴 ∖ 𝐵) ∈ Fin)) | ||
Theorem | difxp1ss 30294 | Difference law for Cartesian products. (Contributed by Thierry Arnoux, 24-Jul-2023.) |
⊢ ((𝐴 ∖ 𝐶) × 𝐵) ⊆ (𝐴 × 𝐵) | ||
Theorem | difxp2ss 30295 | Difference law for Cartesian products. (Contributed by Thierry Arnoux, 24-Jul-2023.) |
⊢ (𝐴 × (𝐵 ∖ 𝐶)) ⊆ (𝐴 × 𝐵) | ||
Theorem | undifr 30296 | Union of complementary parts into whole. (Contributed by Thierry Arnoux, 21-Nov-2023.) |
⊢ (𝐴 ⊆ 𝐵 ↔ ((𝐵 ∖ 𝐴) ∪ 𝐴) = 𝐵) | ||
Theorem | indifundif 30297 | A remarkable equation with sets. (Contributed by Thierry Arnoux, 18-May-2020.) |
⊢ (((𝐴 ∩ 𝐵) ∖ 𝐶) ∪ (𝐴 ∖ 𝐵)) = (𝐴 ∖ (𝐵 ∩ 𝐶)) | ||
Theorem | elpwincl1 30298 | Closure of intersection with regard to elementhood to a power set. (Contributed by Thierry Arnoux, 18-May-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝒫 𝐶) ⇒ ⊢ (𝜑 → (𝐴 ∩ 𝐵) ∈ 𝒫 𝐶) | ||
Theorem | elpwdifcl 30299 | Closure of class difference with regard to elementhood to a power set. (Contributed by Thierry Arnoux, 18-May-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝒫 𝐶) ⇒ ⊢ (𝜑 → (𝐴 ∖ 𝐵) ∈ 𝒫 𝐶) | ||
Theorem | elpwiuncl 30300* | Closure of indexed union with regard to elementhood to a power set. (Contributed by Thierry Arnoux, 27-May-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ 𝒫 𝐶) ⇒ ⊢ (𝜑 → ∪ 𝑘 ∈ 𝐴 𝐵 ∈ 𝒫 𝐶) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |