Home | Metamath
Proof Explorer Theorem List (p. 303 of 450) | < 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: | Metamath Proof Explorer
(1-28694) |
Hilbert Space Explorer
(28695-30217) |
Users' Mathboxes
(30218-44905) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | mdoc1i 30201 | Orthocomplements form a modular pair. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ ⇒ ⊢ 𝐴 𝑀ℋ (⊥‘𝐴) | ||
Theorem | mdoc2i 30202 | Orthocomplements form a modular pair. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ ⇒ ⊢ (⊥‘𝐴) 𝑀ℋ 𝐴 | ||
Theorem | dmdoc1i 30203 | Orthocomplements form a dual modular pair. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ ⇒ ⊢ 𝐴 𝑀ℋ* (⊥‘𝐴) | ||
Theorem | dmdoc2i 30204 | Orthocomplements form a dual modular pair. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ ⇒ ⊢ (⊥‘𝐴) 𝑀ℋ* 𝐴 | ||
Theorem | mdcompli 30205 | 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 30206 | A condition equivalent to the dual modular pair property. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 𝑀ℋ* 𝐵 ↔ (𝐴 ∩ (⊥‘(𝐴 ∩ 𝐵))) 𝑀ℋ* (𝐵 ∩ (⊥‘(𝐴 ∩ 𝐵)))) | ||
Theorem | mddmdin0i 30207* | 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 30208* | 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 30209* | 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 30210* | 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 30211* | Lemma for cdj3i 30217. Value of the first-component function 𝑆. (Contributed by NM, 23-May-2005.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Sℋ & ⊢ 𝐵 ∈ Sℋ & ⊢ 𝑆 = (𝑥 ∈ (𝐴 +ℋ 𝐵) ↦ (℩𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑥 = (𝑧 +ℎ 𝑤))) ⇒ ⊢ ((𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ∧ (𝐴 ∩ 𝐵) = 0ℋ) → (𝑆‘(𝐶 +ℎ 𝐷)) = 𝐶) | ||
Theorem | cdj3lem2a 30212* | Lemma for cdj3i 30217. Closure of the first-component function 𝑆. (Contributed by NM, 25-May-2005.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Sℋ & ⊢ 𝐵 ∈ Sℋ & ⊢ 𝑆 = (𝑥 ∈ (𝐴 +ℋ 𝐵) ↦ (℩𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑥 = (𝑧 +ℎ 𝑤))) ⇒ ⊢ ((𝐶 ∈ (𝐴 +ℋ 𝐵) ∧ (𝐴 ∩ 𝐵) = 0ℋ) → (𝑆‘𝐶) ∈ 𝐴) | ||
Theorem | cdj3lem2b 30213* | Lemma for cdj3i 30217. 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 30214* | Lemma for cdj3i 30217. Value of the second-component function 𝑇. (Contributed by NM, 23-May-2005.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Sℋ & ⊢ 𝐵 ∈ Sℋ & ⊢ 𝑇 = (𝑥 ∈ (𝐴 +ℋ 𝐵) ↦ (℩𝑤 ∈ 𝐵 ∃𝑧 ∈ 𝐴 𝑥 = (𝑧 +ℎ 𝑤))) ⇒ ⊢ ((𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ∧ (𝐴 ∩ 𝐵) = 0ℋ) → (𝑇‘(𝐶 +ℎ 𝐷)) = 𝐷) | ||
Theorem | cdj3lem3a 30215* | Lemma for cdj3i 30217. Closure of the second-component function 𝑇. (Contributed by NM, 26-May-2005.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Sℋ & ⊢ 𝐵 ∈ Sℋ & ⊢ 𝑇 = (𝑥 ∈ (𝐴 +ℋ 𝐵) ↦ (℩𝑤 ∈ 𝐵 ∃𝑧 ∈ 𝐴 𝑥 = (𝑧 +ℎ 𝑤))) ⇒ ⊢ ((𝐶 ∈ (𝐴 +ℋ 𝐵) ∧ (𝐴 ∩ 𝐵) = 0ℋ) → (𝑇‘𝐶) ∈ 𝐵) | ||
Theorem | cdj3lem3b 30216* | Lemma for cdj3i 30217. 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 30217* | 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 30218 |
(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 28178 for our general style guidelines. For contributing via GitHub, see https://github.com/metamath/set.mm/blob/develop/CONTRIBUTING.md 28178. 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 11297. 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 30219 | A theorem about the universal class. Inference associated with bj-abv 34223 (which is proved from fewer axioms). (Contributed by Stefan Allan, 9-Dec-2008.) |
⊢ 𝜑 ⇒ ⊢ V = {𝑥 ∣ 𝜑} | ||
Theorem | xfree 30220 | A partial converse to 19.9t 2200. (Contributed by Stefan Allan, 21-Dec-2008.) (Revised by Mario Carneiro, 11-Dec-2016.) |
⊢ (∀𝑥(𝜑 → ∀𝑥𝜑) ↔ ∀𝑥(∃𝑥𝜑 → 𝜑)) | ||
Theorem | xfree2 30221 | A partial converse to 19.9t 2200. (Contributed by Stefan Allan, 21-Dec-2008.) |
⊢ (∀𝑥(𝜑 → ∀𝑥𝜑) ↔ ∀𝑥(¬ 𝜑 → ∀𝑥 ¬ 𝜑)) | ||
Theorem | addltmulALT 30222 | A proof readability experiment for addltmul 11872. (Contributed by Stefan Allan, 30-Oct-2010.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (2 < 𝐴 ∧ 2 < 𝐵)) → (𝐴 + 𝐵) < (𝐴 · 𝐵)) | ||
Theorem | bian1d 30223 | Adding a superfluous conjunct in a biconditional. (Contributed by Thierry Arnoux, 26-Feb-2017.) |
⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃))) ⇒ ⊢ (𝜑 → ((𝜒 ∧ 𝜓) ↔ (𝜒 ∧ 𝜃))) | ||
Theorem | or3di 30224 | Distributive law for disjunction. (Contributed by Thierry Arnoux, 3-Jul-2017.) |
⊢ ((𝜑 ∨ (𝜓 ∧ 𝜒 ∧ 𝜏)) ↔ ((𝜑 ∨ 𝜓) ∧ (𝜑 ∨ 𝜒) ∧ (𝜑 ∨ 𝜏))) | ||
Theorem | or3dir 30225 | Distributive law for disjunction. (Contributed by Thierry Arnoux, 3-Jul-2017.) |
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∨ 𝜏) ↔ ((𝜑 ∨ 𝜏) ∧ (𝜓 ∨ 𝜏) ∧ (𝜒 ∨ 𝜏))) | ||
Theorem | 3o1cs 30226 | Deduction eliminating disjunct. (Contributed by Thierry Arnoux, 19-Dec-2016.) |
⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) → 𝜃) ⇒ ⊢ (𝜑 → 𝜃) | ||
Theorem | 3o2cs 30227 | Deduction eliminating disjunct. (Contributed by Thierry Arnoux, 19-Dec-2016.) |
⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) → 𝜃) ⇒ ⊢ (𝜓 → 𝜃) | ||
Theorem | 3o3cs 30228 | Deduction eliminating disjunct. (Contributed by Thierry Arnoux, 19-Dec-2016.) |
⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) → 𝜃) ⇒ ⊢ (𝜒 → 𝜃) | ||
Theorem | sbc2iedf 30229* | Conversion of implicit substitution to explicit class substitution. (Contributed by Thierry Arnoux, 4-Jul-2023.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜒 & ⊢ Ⅎ𝑦𝜒 & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ([𝐴 / 𝑥][𝐵 / 𝑦]𝜓 ↔ 𝜒)) | ||
Theorem | rspc2daf 30230* | Double restricted specialization, using implicit substitution. (Contributed by Thierry Arnoux, 4-Jul-2023.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜒 & ⊢ Ⅎ𝑦𝜒 & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑊 𝜓) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | nelbOLD 30231* | Obsolete version of nelb 3268 as of 23-Jan-2024. (Contributed by Thierry Arnoux, 20-Nov-2023.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (¬ 𝐴 ∈ 𝐵 ↔ ∀𝑥 ∈ 𝐵 𝑥 ≠ 𝐴) | ||
Theorem | ralcom4f 30232* | 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 30233* | 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 30234 | A deduction version of one direction of 19.9 2201 with two variables. (Contributed by Thierry Arnoux, 20-Mar-2017.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝜓) & ⊢ (𝜑 → Ⅎ𝑦𝜓) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | 19.9d2r 30235* | A deduction version of one direction of 19.9 2201 with two variables. (Contributed by Thierry Arnoux, 30-Jan-2017.) |
⊢ (𝜑 → Ⅎ𝑥𝜓) & ⊢ (𝜑 → Ⅎ𝑦𝜓) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | r19.29ffa 30236* | A commonly used pattern based on r19.29 3254, version with two restricted quantifiers. (Contributed by Thierry Arnoux, 26-Nov-2017.) |
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ 𝜓) → 𝜒) ⇒ ⊢ ((𝜑 ∧ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓) → 𝜒) | ||
Theorem | eqtrb 30237 | A transposition of equality. (Contributed by Thierry Arnoux, 20-Aug-2023.) |
⊢ ((𝐴 = 𝐵 ∧ 𝐴 = 𝐶) ↔ (𝐴 = 𝐵 ∧ 𝐵 = 𝐶)) | ||
Theorem | opsbc2ie 30238* | Conversion of implicit substitution to explicit class substitution for ordered pairs. (Contributed by Thierry Arnoux, 4-Jul-2023.) |
⊢ (𝑝 = 〈𝑎, 𝑏〉 → (𝜑 ↔ 𝜒)) ⇒ ⊢ (𝑝 = 〈𝑥, 𝑦〉 → (𝜑 ↔ [𝑦 / 𝑏][𝑥 / 𝑎]𝜒)) | ||
Theorem | opreu2reuALT 30239* | Correspondence between uniqueness of ordered pairs and double restricted existential uniqueness quantification. Alternate proof of one direction only, use opreu2reurex 6144 instead. (Contributed by Thierry Arnoux, 4-Jul-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑝 = 〈𝑎, 𝑏〉 → (𝜑 ↔ 𝜒)) ⇒ ⊢ ((∃!𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ ∃!𝑏 ∈ 𝐵 ∃𝑎 ∈ 𝐴 𝜒) → ∃!𝑝 ∈ (𝐴 × 𝐵)𝜑) | ||
Syntax | w2reu 30240 | Syntax for double restricted existential uniqueness quantification. |
wff ∃!𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵𝜑 | ||
Definition | df-2reu 30241 | Define the double restricted existential uniqueness quantifier. (Contributed by Thierry Arnoux, 4-Jul-2023.) |
⊢ (∃!𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵𝜑 ↔ (∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑)) | ||
Theorem | 2reucom 30242 | Double restricted existential uniqueness commutes. (Contributed by Thierry Arnoux, 4-Jul-2023.) |
⊢ (∃!𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵𝜑 ↔ ∃!𝑦 ∈ 𝐵 , 𝑥 ∈ 𝐴𝜑) | ||
Theorem | 2reu2rex1 30243 | Double restricted existential uniqueness implies double restricted existence. (Contributed by Thierry Arnoux, 4-Jul-2023.) |
⊢ (∃!𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) | ||
Theorem | 2reureurex 30244 | Double restricted existential uniqueness implies restricted existential uniqueness with restricted existence. (Contributed by AV, 5-Jul-2023.) |
⊢ (∃!𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵𝜑 → ∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) | ||
Theorem | 2reu2reu2 30245* | Double restricted existential uniqueness implies two nested restricted existential uniqueness. (Contributed by AV, 5-Jul-2023.) |
⊢ (∃!𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵𝜑 → ∃!𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝜑) | ||
Theorem | opreu2reu1 30246* | Equivalent definition of the double restricted existential uniqueness quantifier, using uniqueness of ordered pairs. (Contributed by Thierry Arnoux, 4-Jul-2023.) |
⊢ (𝑝 = 〈𝑥, 𝑦〉 → (𝜒 ↔ 𝜑)) ⇒ ⊢ (∃!𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵𝜑 ↔ ∃!𝑝 ∈ (𝐴 × 𝐵)𝜒) | ||
Theorem | sq2reunnltb 30247* | 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 26036. (Contributed by AV, 5-Jul-2023.) |
⊢ (𝑃 ∈ ℙ → ((𝑃 mod 4) = 1 ↔ ∃!𝑎 ∈ ℕ , 𝑏 ∈ ℕ(𝑎 < 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃))) | ||
Theorem | addsqnot2reu 30248* | 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 26020. (Contributed by AV, 5-Jul-2023.) |
⊢ (𝐶 ∈ ℂ → ¬ ∃!𝑎 ∈ ℂ , 𝑏 ∈ ℂ(𝑎 + (𝑏↑2)) = 𝐶) | ||
Theorem | sbceqbidf 30249 | Equality theorem for class substitution. (Contributed by Thierry Arnoux, 4-Sep-2018.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ [𝐵 / 𝑥]𝜒)) | ||
Theorem | sbcies 30250* | A special version of class substitution commonly used for structures. (Contributed by Thierry Arnoux, 14-Mar-2019.) |
⊢ 𝐴 = (𝐸‘𝑊) & ⊢ (𝑎 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝑤 = 𝑊 → ([(𝐸‘𝑤) / 𝑎]𝜓 ↔ 𝜑)) | ||
Theorem | moel 30251* | "At most one" element in a set. (Contributed by Thierry Arnoux, 26-Jul-2018.) |
⊢ (∃*𝑥 𝑥 ∈ 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝑥 = 𝑦) | ||
Theorem | mo5f 30252* | Alternate definition of "at most one." (Contributed by Thierry Arnoux, 1-Mar-2017.) |
⊢ Ⅎ𝑖𝜑 & ⊢ Ⅎ𝑗𝜑 ⇒ ⊢ (∃*𝑥𝜑 ↔ ∀𝑖∀𝑗(([𝑖 / 𝑥]𝜑 ∧ [𝑗 / 𝑥]𝜑) → 𝑖 = 𝑗)) | ||
Theorem | nmo 30253* | Negation of "at most one". (Contributed by Thierry Arnoux, 26-Feb-2017.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (¬ ∃*𝑥𝜑 ↔ ∀𝑦∃𝑥(𝜑 ∧ 𝑥 ≠ 𝑦)) | ||
Theorem | reuxfrdf 30254* | Transfer existential uniqueness from a variable 𝑥 to another variable 𝑦 contained in expression 𝐴. Cf. reuxfrd 3738 (Contributed by Thierry Arnoux, 7-Apr-2017.) (Revised by Thierry Arnoux, 8-Oct-2017.) (Revised by Thierry Arnoux, 30-Mar-2018.) |
⊢ Ⅎ𝑦𝐵 & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → 𝐴 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∃*𝑦 ∈ 𝐶 𝑥 = 𝐴) ⇒ ⊢ (𝜑 → (∃!𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓) ↔ ∃!𝑦 ∈ 𝐶 𝜓)) | ||
Theorem | rexunirn 30255* | Restricted existential quantification over the union of the range of a function. Cf. rexrn 6852 and eluni2 4841. (Contributed by Thierry Arnoux, 19-Sep-2017.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ (𝑥 ∈ 𝐴 → 𝐵 ∈ 𝑉) ⇒ ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑦 ∈ ∪ ran 𝐹𝜑) | ||
Theorem | rmoxfrd 30256* | 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 30257 | "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 30258* | 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 30259* | Domain of a restricted class abstraction over a cartesian product. (Contributed by Thierry Arnoux, 3-Jul-2023.) |
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (𝜑 ↔ 𝜓)) ⇒ ⊢ dom {𝑧 ∈ (𝐴 × 𝐵) ∣ 𝜑} = {𝑥 ∈ 𝐴 ∣ ∃𝑦 ∈ 𝐵 𝜓} | ||
Theorem | difrab2 30260 | Difference of two restricted class abstractions. Compare with difrab 4276. (Contributed by Thierry Arnoux, 3-Jan-2022.) |
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∖ {𝑥 ∈ 𝐵 ∣ 𝜑}) = {𝑥 ∈ (𝐴 ∖ 𝐵) ∣ 𝜑} | ||
Theorem | rabexgfGS 30261 | 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 30262* | Truth implied by equality of a restricted class abstraction and a singleton. (Contributed by Thierry Arnoux, 15-Sep-2018.) |
⊢ 𝐵 ∈ V ⇒ ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = {𝐵} → 𝐵 ∈ 𝐴) | ||
Theorem | rabeqsnd 30263* | Conditions for a restricted class abstraction to be a singleton, in deduction form. (Contributed by Thierry Arnoux, 2-Dec-2021.) |
⊢ (𝑥 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → 𝐵 ∈ 𝐴) & ⊢ (𝜑 → 𝜒) & ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓) → 𝑥 = 𝐵) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝐵}) | ||
Theorem | foresf1o 30264* | 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 30265* | Domination relation for restricted abstract class builders, based on a surjective function. (Contributed by Thierry Arnoux, 27-Jan-2020.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = (𝐹‘𝑥)) → (𝜒 ↔ 𝜓)) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴–onto→𝐵) ⇒ ⊢ (𝜑 → {𝑦 ∈ 𝐵 ∣ 𝜒} ≼ {𝑥 ∈ 𝐴 ∣ 𝜓}) | ||
Theorem | abrexdomjm 30266* | An indexed set is dominated by the indexing set. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (𝑦 ∈ 𝐴 → ∃*𝑥𝜑) ⇒ ⊢ (𝐴 ∈ 𝑉 → {𝑥 ∣ ∃𝑦 ∈ 𝐴 𝜑} ≼ 𝐴) | ||
Theorem | abrexdom2jm 30267* | An indexed set is dominated by the indexing set. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∣ ∃𝑦 ∈ 𝐴 𝑥 = 𝐵} ≼ 𝐴) | ||
Theorem | abrexexd 30268* | Existence of a class abstraction of existentially restricted sets. (Contributed by Thierry Arnoux, 10-May-2017.) |
⊢ Ⅎ𝑥𝐴 & ⊢ (𝜑 → 𝐴 ∈ V) ⇒ ⊢ (𝜑 → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ V) | ||
Theorem | elabreximd 30269* | Class substitution in an image set. (Contributed by Thierry Arnoux, 30-Dec-2016.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝜒 & ⊢ (𝐴 = 𝐵 → (𝜒 ↔ 𝜓)) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝜓) ⇒ ⊢ ((𝜑 ∧ 𝐴 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐶 𝑦 = 𝐵}) → 𝜒) | ||
Theorem | elabreximdv 30270* | Class substitution in an image set. (Contributed by Thierry Arnoux, 30-Dec-2016.) |
⊢ (𝐴 = 𝐵 → (𝜒 ↔ 𝜓)) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝜓) ⇒ ⊢ ((𝜑 ∧ 𝐴 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐶 𝑦 = 𝐵}) → 𝜒) | ||
Theorem | abrexss 30271* | A necessary condition for an image set to be a subset. (Contributed by Thierry Arnoux, 6-Feb-2017.) |
⊢ Ⅎ𝑥𝐶 ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ⊆ 𝐶) | ||
Theorem | elunsn 30272 | Elementhood to a union with a singleton. (Contributed by Thierry Arnoux, 14-Dec-2023.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ (𝐵 ∪ {𝐶}) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐶))) | ||
Theorem | nelun 30273 | Negated membership for a union. (Contributed by Thierry Arnoux, 13-Dec-2023.) |
⊢ (𝐴 = (𝐵 ∪ 𝐶) → (¬ 𝑋 ∈ 𝐴 ↔ (¬ 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ∈ 𝐶))) | ||
Theorem | disjdifr 30274 | A class and its relative complement are disjoint. (Contributed by Thierry Arnoux, 29-Nov-2023.) |
⊢ ((𝐵 ∖ 𝐴) ∩ 𝐴) = ∅ | ||
Theorem | rabss3d 30275* | Subclass law for restricted abstraction. (Contributed by Thierry Arnoux, 25-Sep-2017.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝜓)) → 𝑥 ∈ 𝐵) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} ⊆ {𝑥 ∈ 𝐵 ∣ 𝜓}) | ||
Theorem | inin 30276 | Intersection with an intersection. (Contributed by Thierry Arnoux, 27-Dec-2016.) |
⊢ (𝐴 ∩ (𝐴 ∩ 𝐵)) = (𝐴 ∩ 𝐵) | ||
Theorem | inindif 30277 | See inundif 4426. (Contributed by Thierry Arnoux, 13-Sep-2017.) |
⊢ ((𝐴 ∩ 𝐶) ∩ (𝐴 ∖ 𝐶)) = ∅ | ||
Theorem | difininv 30278 | Condition for the intersections of two sets with a given set to be equal. (Contributed by Thierry Arnoux, 28-Dec-2021.) |
⊢ ((((𝐴 ∖ 𝐶) ∩ 𝐵) = ∅ ∧ ((𝐶 ∖ 𝐴) ∩ 𝐵) = ∅) → (𝐴 ∩ 𝐵) = (𝐶 ∩ 𝐵)) | ||
Theorem | difeq 30279 | Rewriting an equation with class difference, without using quantifiers. (Contributed by Thierry Arnoux, 24-Sep-2017.) |
⊢ ((𝐴 ∖ 𝐵) = 𝐶 ↔ ((𝐶 ∩ 𝐵) = ∅ ∧ (𝐶 ∪ 𝐵) = (𝐴 ∪ 𝐵))) | ||
Theorem | eqdif 30280 | If both set differences of two sets are empty, those sets are equal. (Contributed by Thierry Arnoux, 16-Nov-2023.) |
⊢ (((𝐴 ∖ 𝐵) = ∅ ∧ (𝐵 ∖ 𝐴) = ∅) → 𝐴 = 𝐵) | ||
Theorem | difxp1ss 30281 | Difference law for Cartesian products. (Contributed by Thierry Arnoux, 24-Jul-2023.) |
⊢ ((𝐴 ∖ 𝐶) × 𝐵) ⊆ (𝐴 × 𝐵) | ||
Theorem | difxp2ss 30282 | Difference law for Cartesian products. (Contributed by Thierry Arnoux, 24-Jul-2023.) |
⊢ (𝐴 × (𝐵 ∖ 𝐶)) ⊆ (𝐴 × 𝐵) | ||
Theorem | undifr 30283 | Union of complementary parts into whole. (Contributed by Thierry Arnoux, 21-Nov-2023.) |
⊢ (𝐴 ⊆ 𝐵 ↔ ((𝐵 ∖ 𝐴) ∪ 𝐴) = 𝐵) | ||
Theorem | indifundif 30284 | A remarkable equation with sets. (Contributed by Thierry Arnoux, 18-May-2020.) |
⊢ (((𝐴 ∩ 𝐵) ∖ 𝐶) ∪ (𝐴 ∖ 𝐵)) = (𝐴 ∖ (𝐵 ∩ 𝐶)) | ||
Theorem | elpwincl1 30285 | Closure of intersection with regard to elementhood to a power set. (Contributed by Thierry Arnoux, 18-May-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝒫 𝐶) ⇒ ⊢ (𝜑 → (𝐴 ∩ 𝐵) ∈ 𝒫 𝐶) | ||
Theorem | elpwdifcl 30286 | Closure of class difference with regard to elementhood to a power set. (Contributed by Thierry Arnoux, 18-May-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝒫 𝐶) ⇒ ⊢ (𝜑 → (𝐴 ∖ 𝐵) ∈ 𝒫 𝐶) | ||
Theorem | elpwiuncl 30287* | Closure of indexed union with regard to elementhood to a power set. (Contributed by Thierry Arnoux, 27-May-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ 𝒫 𝐶) ⇒ ⊢ (𝜑 → ∪ 𝑘 ∈ 𝐴 𝐵 ∈ 𝒫 𝐶) | ||
Theorem | eqsnd 30288* | Deduce that a set is a singleton. (Contributed by Thierry Arnoux, 10-May-2023.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 = 𝐵) & ⊢ (𝜑 → 𝐵 ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝐴 = {𝐵}) | ||
Theorem | elpreq 30289 | Equality wihin a pair. (Contributed by Thierry Arnoux, 23-Aug-2017.) |
⊢ (𝜑 → 𝑋 ∈ {𝐴, 𝐵}) & ⊢ (𝜑 → 𝑌 ∈ {𝐴, 𝐵}) & ⊢ (𝜑 → (𝑋 = 𝐴 ↔ 𝑌 = 𝐴)) ⇒ ⊢ (𝜑 → 𝑋 = 𝑌) | ||
Theorem | nelpr 30290 | A set 𝐴 not in a pair is neither element of the pair. (Contributed by Thierry Arnoux, 20-Nov-2023.) |
⊢ (𝐴 ∈ 𝑉 → (¬ 𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶))) | ||
Theorem | inpr0 30291 | Rewrite an empty intersection with a pair. (Contributed by Thierry Arnoux, 20-Nov-2023.) |
⊢ ((𝐴 ∩ {𝐵, 𝐶}) = ∅ ↔ (¬ 𝐵 ∈ 𝐴 ∧ ¬ 𝐶 ∈ 𝐴)) | ||
Theorem | neldifpr1 30292 | The first element of a pair is not an element of a difference with this pair. (Contributed by Thierry Arnoux, 20-Nov-2023.) |
⊢ ¬ 𝐴 ∈ (𝐶 ∖ {𝐴, 𝐵}) | ||
Theorem | neldifpr2 30293 | The second element of a pair is not an element of a difference with this pair. (Contributed by Thierry Arnoux, 20-Nov-2023.) |
⊢ ¬ 𝐵 ∈ (𝐶 ∖ {𝐴, 𝐵}) | ||
Theorem | unidifsnel 30294 | The other element of a pair is an element of the pair. (Contributed by Thierry Arnoux, 26-Aug-2017.) |
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o) → ∪ (𝑃 ∖ {𝑋}) ∈ 𝑃) | ||
Theorem | unidifsnne 30295 | The other element of a pair is not the known element. (Contributed by Thierry Arnoux, 26-Aug-2017.) |
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o) → ∪ (𝑃 ∖ {𝑋}) ≠ 𝑋) | ||
Theorem | ifeqeqx 30296* | An equality theorem tailored for ballotlemsf1o 31771. (Contributed by Thierry Arnoux, 14-Apr-2017.) |
⊢ (𝑥 = 𝑋 → 𝐴 = 𝐶) & ⊢ (𝑥 = 𝑌 → 𝐵 = 𝑎) & ⊢ (𝑥 = 𝑋 → (𝜒 ↔ 𝜃)) & ⊢ (𝑥 = 𝑌 → (𝜒 ↔ 𝜓)) & ⊢ (𝜑 → 𝑎 = 𝐶) & ⊢ ((𝜑 ∧ 𝜓) → 𝜃) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝑊) ⇒ ⊢ ((𝜑 ∧ 𝑥 = if(𝜓, 𝑋, 𝑌)) → 𝑎 = if(𝜒, 𝐴, 𝐵)) | ||
Theorem | elimifd 30297 | Elimination of a conditional operator contained in a wff 𝜒. (Contributed by Thierry Arnoux, 25-Jan-2017.) |
⊢ (𝜑 → (if(𝜓, 𝐴, 𝐵) = 𝐴 → (𝜒 ↔ 𝜃))) & ⊢ (𝜑 → (if(𝜓, 𝐴, 𝐵) = 𝐵 → (𝜒 ↔ 𝜏))) ⇒ ⊢ (𝜑 → (𝜒 ↔ ((𝜓 ∧ 𝜃) ∨ (¬ 𝜓 ∧ 𝜏)))) | ||
Theorem | elim2if 30298 | Elimination of two conditional operators contained in a wff 𝜒. (Contributed by Thierry Arnoux, 25-Jan-2017.) |
⊢ (if(𝜑, 𝐴, if(𝜓, 𝐵, 𝐶)) = 𝐴 → (𝜒 ↔ 𝜃)) & ⊢ (if(𝜑, 𝐴, if(𝜓, 𝐵, 𝐶)) = 𝐵 → (𝜒 ↔ 𝜏)) & ⊢ (if(𝜑, 𝐴, if(𝜓, 𝐵, 𝐶)) = 𝐶 → (𝜒 ↔ 𝜂)) ⇒ ⊢ (𝜒 ↔ ((𝜑 ∧ 𝜃) ∨ (¬ 𝜑 ∧ ((𝜓 ∧ 𝜏) ∨ (¬ 𝜓 ∧ 𝜂))))) | ||
Theorem | elim2ifim 30299 | Elimination of two conditional operators for an implication. (Contributed by Thierry Arnoux, 25-Jan-2017.) |
⊢ (if(𝜑, 𝐴, if(𝜓, 𝐵, 𝐶)) = 𝐴 → (𝜒 ↔ 𝜃)) & ⊢ (if(𝜑, 𝐴, if(𝜓, 𝐵, 𝐶)) = 𝐵 → (𝜒 ↔ 𝜏)) & ⊢ (if(𝜑, 𝐴, if(𝜓, 𝐵, 𝐶)) = 𝐶 → (𝜒 ↔ 𝜂)) & ⊢ (𝜑 → 𝜃) & ⊢ ((¬ 𝜑 ∧ 𝜓) → 𝜏) & ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → 𝜂) ⇒ ⊢ 𝜒 | ||
Theorem | ifeq3da 30300 | Given an expression 𝐶 containing if(𝜓, 𝐸, 𝐹), substitute (hypotheses .1 and .2) and evaluate (hypotheses .3 and .4) it for both cases at the same time. (Contributed by Thierry Arnoux, 13-Dec-2021.) |
⊢ (if(𝜓, 𝐸, 𝐹) = 𝐸 → 𝐶 = 𝐺) & ⊢ (if(𝜓, 𝐸, 𝐹) = 𝐹 → 𝐶 = 𝐻) & ⊢ (𝜑 → 𝐺 = 𝐴) & ⊢ (𝜑 → 𝐻 = 𝐵) ⇒ ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) = 𝐶) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |