HomeTheorem List (p. 329 of 506)
GIF version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 329 of 506) | < 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-31236) |
Hilbert Space Explorer
(31237-32759) |
Users' Mathboxes
(32760-50572) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | mo5f 32801* | Alternate definition of "at most one." (Contributed by Thierry Arnoux, 1-Mar-2017.) |
| ⊢ Ⅎ𝑖𝜑 & ⊢ Ⅎ𝑗𝜑 ⇒ ⊢ (∃*𝑥𝜑 ↔ ∀𝑖∀𝑗(([𝑖 / 𝑥]𝜑 ∧ [𝑗 / 𝑥]𝜑) → 𝑖 = 𝑗)) | ||
| Theorem | nmo 32802* | Negation of "at most one". (Contributed by Thierry Arnoux, 26-Feb-2017.) |
| ⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (¬ ∃*𝑥𝜑 ↔ ∀𝑦∃𝑥(𝜑 ∧ 𝑥 ≠ 𝑦)) | ||
| Theorem | reuxfrdf 32803* | Transfer existential uniqueness from a variable 𝑥 to another variable 𝑦 contained in expression 𝐴. Cf. reuxfrd 3710 (Contributed by Thierry Arnoux, 7-Apr-2017.) (Revised by Thierry Arnoux, 8-Oct-2017.) (Revised by Thierry Arnoux, 30-Mar-2018.) |
| ⊢ Ⅎ𝑦𝐵 & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → 𝐴 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∃*𝑦 ∈ 𝐶 𝑥 = 𝐴) ⇒ ⊢ (𝜑 → (∃!𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 (𝑥 = 𝐴 ∧ 𝜓) ↔ ∃!𝑦 ∈ 𝐶 𝜓)) | ||
| Theorem | rexunirn 32804* | Restricted existential quantification over the union of the range of a function. Cf. rexrn 7082 and eluni2 4875. (Contributed by Thierry Arnoux, 19-Sep-2017.) |
| ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ (𝑥 ∈ 𝐴 → 𝐵 ∈ 𝑉) ⇒ ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑦 ∈ ∪ ran 𝐹𝜑) | ||
| Theorem | rmoxfrd 32805* | 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 32806 | "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 32807* | 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 | riotaeqbidva 32808* | Equivalent wff's yield equal restricted definition binders (deduction form). (raleqbidva 3327 analog.) (Contributed by Thierry Arnoux, 29-Jan-2025.) |
| ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜓) = (℩𝑥 ∈ 𝐵 𝜒)) | ||
| Theorem | dmrab 32809* | Domain of a restricted class abstraction over a cartesian product. (Contributed by Thierry Arnoux, 3-Jul-2023.) |
| ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ 𝜓)) ⇒ ⊢ dom {𝑧 ∈ (𝐴 × 𝐵) ∣ 𝜑} = {𝑥 ∈ 𝐴 ∣ ∃𝑦 ∈ 𝐵 𝜓} | ||
| Theorem | difrab2 32810 | Difference of two restricted class abstractions. Compare with difrab 4270. (Contributed by Thierry Arnoux, 3-Jan-2022.) |
| ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∖ {𝑥 ∈ 𝐵 ∣ 𝜑}) = {𝑥 ∈ (𝐴 ∖ 𝐵) ∣ 𝜑} | ||
| Theorem | rabexgfGS 32811 | 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 32812* | Truth implied by equality of a restricted class abstraction and a singleton. (Contributed by Thierry Arnoux, 15-Sep-2018.) |
| ⊢ 𝐵 ∈ V ⇒ ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = {𝐵} → 𝐵 ∈ 𝐴) | ||
| Theorem | rabsspr 32813* | Conditions for a restricted class abstraction to be a subset of an unordered pair. (Contributed by Thierry Arnoux, 6-Jul-2025.) |
| ⊢ ({𝑥 ∈ 𝑉 ∣ 𝜑} ⊆ {𝑋, 𝑌} ↔ ∀𝑥 ∈ 𝑉 (𝜑 → (𝑥 = 𝑋 ∨ 𝑥 = 𝑌))) | ||
| Theorem | rabsstp 32814* | Conditions for a restricted class abstraction to be a subset of an unordered triple. (Contributed by Thierry Arnoux, 6-Jul-2025.) |
| ⊢ ({𝑥 ∈ 𝑉 ∣ 𝜑} ⊆ {𝑋, 𝑌, 𝑍} ↔ ∀𝑥 ∈ 𝑉 (𝜑 → (𝑥 = 𝑋 ∨ 𝑥 = 𝑌 ∨ 𝑥 = 𝑍))) | ||
| Theorem | 3unrab 32815 | Union of three restricted class abstractions. (Contributed by Thierry Arnoux, 6-Jul-2025.) |
| ⊢ (({𝑥 ∈ 𝐴 ∣ 𝜑} ∪ {𝑥 ∈ 𝐴 ∣ 𝜓}) ∪ {𝑥 ∈ 𝐴 ∣ 𝜒}) = {𝑥 ∈ 𝐴 ∣ (𝜑 ∨ 𝜓 ∨ 𝜒)} | ||
| Theorem | foresf1o 32816* | 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 32817* | Domination relation for restricted abstract class builders, based on a surjective function. (Contributed by Thierry Arnoux, 27-Jan-2020.) |
| ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = (𝐹‘𝑥)) → (𝜒 ↔ 𝜓)) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴–onto→𝐵) ⇒ ⊢ (𝜑 → {𝑦 ∈ 𝐵 ∣ 𝜒} ≼ {𝑥 ∈ 𝐴 ∣ 𝜓}) | ||
| Theorem | rabrexfi 32818* | Conditions for a class abstraction with a restricted existential quantification to be finite. (Contributed by Thierry Arnoux, 6-Jul-2025.) |
| ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → {𝑥 ∈ 𝐴 ∣ 𝜓} ∈ Fin) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ ∃𝑦 ∈ 𝐵 𝜓} ∈ Fin) | ||
| Theorem | abrexdomjm 32819* | An indexed set is dominated by the indexing set. (Contributed by Jeff Madsen, 2-Sep-2009.) |
| ⊢ (𝑦 ∈ 𝐴 → ∃*𝑥𝜑) ⇒ ⊢ (𝐴 ∈ 𝑉 → {𝑥 ∣ ∃𝑦 ∈ 𝐴 𝜑} ≼ 𝐴) | ||
| Theorem | abrexdom2jm 32820* | An indexed set is dominated by the indexing set. (Contributed by Jeff Madsen, 2-Sep-2009.) |
| ⊢ (𝐴 ∈ 𝑉 → {𝑥 ∣ ∃𝑦 ∈ 𝐴 𝑥 = 𝐵} ≼ 𝐴) | ||
| Theorem | abrexexd 32821* | Existence of a class abstraction of existentially restricted sets. (Contributed by Thierry Arnoux, 10-May-2017.) |
| ⊢ Ⅎ𝑥𝐴 & ⊢ (𝜑 → 𝐴 ∈ V) ⇒ ⊢ (𝜑 → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ V) | ||
| Theorem | elabreximd 32822* | Class substitution in an image set. (Contributed by Thierry Arnoux, 30-Dec-2016.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝜒 & ⊢ (𝐴 = 𝐵 → (𝜒 ↔ 𝜓)) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝜓) ⇒ ⊢ ((𝜑 ∧ 𝐴 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐶 𝑦 = 𝐵}) → 𝜒) | ||
| Theorem | elabreximdv 32823* | Class substitution in an image set. (Contributed by Thierry Arnoux, 30-Dec-2016.) |
| ⊢ (𝐴 = 𝐵 → (𝜒 ↔ 𝜓)) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝜓) ⇒ ⊢ ((𝜑 ∧ 𝐴 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐶 𝑦 = 𝐵}) → 𝜒) | ||
| Theorem | abrexss 32824* | A necessary condition for an image set to be a subset. (Contributed by Thierry Arnoux, 6-Feb-2017.) |
| ⊢ Ⅎ𝑥𝐶 ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ⊆ 𝐶) | ||
| Theorem | nelun 32825 | Negated membership for a union. (Contributed by Thierry Arnoux, 13-Dec-2023.) |
| ⊢ (𝐴 = (𝐵 ∪ 𝐶) → (¬ 𝑋 ∈ 𝐴 ↔ (¬ 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ∈ 𝐶))) | ||
| Theorem | snsssng 32826 | 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 32827* | 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 32828 | Intersection with an intersection. (Contributed by Thierry Arnoux, 27-Dec-2016.) |
| ⊢ (𝐴 ∩ (𝐴 ∩ 𝐵)) = (𝐴 ∩ 𝐵) | ||
| Theorem | difininv 32829 | Condition for the intersections of two sets with a given set to be equal. (Contributed by Thierry Arnoux, 28-Dec-2021.) |
| ⊢ ((((𝐴 ∖ 𝐶) ∩ 𝐵) = ∅ ∧ ((𝐶 ∖ 𝐴) ∩ 𝐵) = ∅) → (𝐴 ∩ 𝐵) = (𝐶 ∩ 𝐵)) | ||
| Theorem | difeq 32830 | Rewriting an equation with class difference, without using quantifiers. (Contributed by Thierry Arnoux, 24-Sep-2017.) |
| ⊢ ((𝐴 ∖ 𝐵) = 𝐶 ↔ ((𝐶 ∩ 𝐵) = ∅ ∧ (𝐶 ∪ 𝐵) = (𝐴 ∪ 𝐵))) | ||
| Theorem | eqdif 32831 | If both set differences of two sets are empty, those sets are equal. (Contributed by Thierry Arnoux, 16-Nov-2023.) |
| ⊢ (((𝐴 ∖ 𝐵) = ∅ ∧ (𝐵 ∖ 𝐴) = ∅) → 𝐴 = 𝐵) | ||
| Theorem | indifbi 32832 | Two ways to express equality relative to a class 𝐴. (Contributed by Thierry Arnoux, 23-Jun-2024.) |
| ⊢ ((𝐴 ∩ 𝐵) = (𝐴 ∩ 𝐶) ↔ (𝐴 ∖ 𝐵) = (𝐴 ∖ 𝐶)) | ||
| Theorem | diffib 32833 | Case where diffi 9158 is a biconditional. (Contributed by Thierry Arnoux, 27-Jun-2024.) |
| ⊢ (𝐵 ∈ Fin → (𝐴 ∈ Fin ↔ (𝐴 ∖ 𝐵) ∈ Fin)) | ||
| Theorem | difxp1ss 32834 | Difference law for Cartesian products. (Contributed by Thierry Arnoux, 24-Jul-2023.) |
| ⊢ ((𝐴 ∖ 𝐶) × 𝐵) ⊆ (𝐴 × 𝐵) | ||
| Theorem | difxp2ss 32835 | Difference law for Cartesian products. (Contributed by Thierry Arnoux, 24-Jul-2023.) |
| ⊢ (𝐴 × (𝐵 ∖ 𝐶)) ⊆ (𝐴 × 𝐵) | ||
| Theorem | indifundif 32836 | A remarkable equation with sets. (Contributed by Thierry Arnoux, 18-May-2020.) |
| ⊢ (((𝐴 ∩ 𝐵) ∖ 𝐶) ∪ (𝐴 ∖ 𝐵)) = (𝐴 ∖ (𝐵 ∩ 𝐶)) | ||
| Theorem | elpwincl1 32837 | Closure of intersection with regard to elementhood to a power set. (Contributed by Thierry Arnoux, 18-May-2020.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝒫 𝐶) ⇒ ⊢ (𝜑 → (𝐴 ∩ 𝐵) ∈ 𝒫 𝐶) | ||
| Theorem | elpwdifcl 32838 | Closure of class difference with regard to elementhood to a power set. (Contributed by Thierry Arnoux, 18-May-2020.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝒫 𝐶) ⇒ ⊢ (𝜑 → (𝐴 ∖ 𝐵) ∈ 𝒫 𝐶) | ||
| Theorem | elpwiuncl 32839* | Closure of indexed union with regard to elementhood to a power set. (Contributed by Thierry Arnoux, 27-May-2020.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ 𝒫 𝐶) ⇒ ⊢ (𝜑 → ∪ 𝑘 ∈ 𝐴 𝐵 ∈ 𝒫 𝐶) | ||
| Theorem | elpreq 32840 | Equality wihin a pair. (Contributed by Thierry Arnoux, 23-Aug-2017.) |
| ⊢ (𝜑 → 𝑋 ∈ {𝐴, 𝐵}) & ⊢ (𝜑 → 𝑌 ∈ {𝐴, 𝐵}) & ⊢ (𝜑 → (𝑋 = 𝐴 ↔ 𝑌 = 𝐴)) ⇒ ⊢ (𝜑 → 𝑋 = 𝑌) | ||
| Theorem | prssad 32841 | If a pair is a subset of a class, the first element of the pair is an element of that class. (Contributed by Thierry Arnoux, 2-Nov-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → {𝐴, 𝐵} ⊆ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝐶) | ||
| Theorem | prssbd 32842 | If a pair is a subset of a class, the second element of the pair is an element of that class. (Contributed by Thierry Arnoux, 2-Nov-2025.) |
| ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → {𝐴, 𝐵} ⊆ 𝐶) ⇒ ⊢ (𝜑 → 𝐵 ∈ 𝐶) | ||
| Theorem | nelpr 32843 | A set 𝐴 not in a pair is neither element of the pair. (Contributed by Thierry Arnoux, 20-Nov-2023.) |
| ⊢ (𝐴 ∈ 𝑉 → (¬ 𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶))) | ||
| Theorem | inpr0 32844 | Rewrite an empty intersection with a pair. (Contributed by Thierry Arnoux, 20-Nov-2023.) |
| ⊢ ((𝐴 ∩ {𝐵, 𝐶}) = ∅ ↔ (¬ 𝐵 ∈ 𝐴 ∧ ¬ 𝐶 ∈ 𝐴)) | ||
| Theorem | neldifpr1 32845 | 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 32846 | 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 32847 | The other element of a pair is an element of the pair. (Contributed by Thierry Arnoux, 26-Aug-2017.) |
| ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o) → ∪ (𝑃 ∖ {𝑋}) ∈ 𝑃) | ||
| Theorem | unidifsnne 32848 | The other element of a pair is not the known element. (Contributed by Thierry Arnoux, 26-Aug-2017.) |
| ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o) → ∪ (𝑃 ∖ {𝑋}) ≠ 𝑋) | ||
| Theorem | tpssg 32849 | An unordered triple of elements of a class is a subset of the class. (Contributed by Thierry Arnoux, 2-Nov-2025.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → ((𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐷) ↔ {𝐴, 𝐵, 𝐶} ⊆ 𝐷)) | ||
| Theorem | tpssd 32850 | Deduction version of tpssi : An unordered triple of elements of a class is a subset of that class. (Contributed by Thierry Arnoux, 2-Nov-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝐷) & ⊢ (𝜑 → 𝐵 ∈ 𝐷) & ⊢ (𝜑 → 𝐶 ∈ 𝐷) ⇒ ⊢ (𝜑 → {𝐴, 𝐵, 𝐶} ⊆ 𝐷) | ||
| Theorem | tpssad 32851 | If an ordered triple is a subset of a class, the first element of the triple is an element of that class. (Contributed by Thierry Arnoux, 2-Nov-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → {𝐴, 𝐵, 𝐶} ⊆ 𝐷) ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝐷) | ||
| Theorem | tpssbd 32852 | If an ordered triple is a subset of a class, the second element of the triple is an element of that class. (Contributed by Thierry Arnoux, 2-Nov-2025.) |
| ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → {𝐴, 𝐵, 𝐶} ⊆ 𝐷) ⇒ ⊢ (𝜑 → 𝐵 ∈ 𝐷) | ||
| Theorem | tpsscd 32853 | If an ordered triple is a subset of a class, the third element of the triple is an element of that class. (Contributed by Thierry Arnoux, 2-Nov-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → {𝐴, 𝐵, 𝐶} ⊆ 𝐷) ⇒ ⊢ (𝜑 → 𝐶 ∈ 𝐷) | ||
| Theorem | ifeqeqx 32854* | An equality theorem tailored for ballotlemsf1o 34870. (Contributed by Thierry Arnoux, 14-Apr-2017.) |
| ⊢ (𝑥 = 𝑋 → 𝐴 = 𝐶) & ⊢ (𝑥 = 𝑌 → 𝐵 = 𝑎) & ⊢ (𝑥 = 𝑋 → (𝜒 ↔ 𝜃)) & ⊢ (𝑥 = 𝑌 → (𝜒 ↔ 𝜓)) & ⊢ (𝜑 → 𝑎 = 𝐶) & ⊢ ((𝜑 ∧ 𝜓) → 𝜃) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝑊) ⇒ ⊢ ((𝜑 ∧ 𝑥 = if(𝜓, 𝑋, 𝑌)) → 𝑎 = if(𝜒, 𝐴, 𝐵)) | ||
| Theorem | elimifd 32855 | Elimination of a conditional operator contained in a wff 𝜒. (Contributed by Thierry Arnoux, 25-Jan-2017.) |
| ⊢ (𝜑 → (if(𝜓, 𝐴, 𝐵) = 𝐴 → (𝜒 ↔ 𝜃))) & ⊢ (𝜑 → (if(𝜓, 𝐴, 𝐵) = 𝐵 → (𝜒 ↔ 𝜏))) ⇒ ⊢ (𝜑 → (𝜒 ↔ ((𝜓 ∧ 𝜃) ∨ (¬ 𝜓 ∧ 𝜏)))) | ||
| Theorem | elim2if 32856 | Elimination of two conditional operators contained in a wff 𝜒. (Contributed by Thierry Arnoux, 25-Jan-2017.) |
| ⊢ (if(𝜑, 𝐴, if(𝜓, 𝐵, 𝐶)) = 𝐴 → (𝜒 ↔ 𝜃)) & ⊢ (if(𝜑, 𝐴, if(𝜓, 𝐵, 𝐶)) = 𝐵 → (𝜒 ↔ 𝜏)) & ⊢ (if(𝜑, 𝐴, if(𝜓, 𝐵, 𝐶)) = 𝐶 → (𝜒 ↔ 𝜂)) ⇒ ⊢ (𝜒 ↔ ((𝜑 ∧ 𝜃) ∨ (¬ 𝜑 ∧ ((𝜓 ∧ 𝜏) ∨ (¬ 𝜓 ∧ 𝜂))))) | ||
| Theorem | elim2ifim 32857 | Elimination of two conditional operators for an implication. (Contributed by Thierry Arnoux, 25-Jan-2017.) |
| ⊢ (if(𝜑, 𝐴, if(𝜓, 𝐵, 𝐶)) = 𝐴 → (𝜒 ↔ 𝜃)) & ⊢ (if(𝜑, 𝐴, if(𝜓, 𝐵, 𝐶)) = 𝐵 → (𝜒 ↔ 𝜏)) & ⊢ (if(𝜑, 𝐴, if(𝜓, 𝐵, 𝐶)) = 𝐶 → (𝜒 ↔ 𝜂)) & ⊢ (𝜑 → 𝜃) & ⊢ ((¬ 𝜑 ∧ 𝜓) → 𝜏) & ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → 𝜂) ⇒ ⊢ 𝜒 | ||
| Theorem | ifeq3da 32858 | 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(𝜓, 𝐴, 𝐵) = 𝐶) | ||
| Theorem | ifnetrue 32859 | Deduce truth from a conditional operator value. (Contributed by Thierry Arnoux, 20-Feb-2025.) |
| ⊢ ((𝐴 ≠ 𝐵 ∧ if(𝜑, 𝐴, 𝐵) = 𝐴) → 𝜑) | ||
| Theorem | ifnefals 32860 | Deduce falsehood from a conditional operator value. (Contributed by Thierry Arnoux, 20-Feb-2025.) |
| ⊢ ((𝐴 ≠ 𝐵 ∧ if(𝜑, 𝐴, 𝐵) = 𝐵) → ¬ 𝜑) | ||
| Theorem | ifnebib 32861 | The converse of ifbi 4509 holds if the two values are not equal. (Contributed by Thierry Arnoux, 20-Feb-2025.) |
| ⊢ (𝐴 ≠ 𝐵 → (if(𝜑, 𝐴, 𝐵) = if(𝜓, 𝐴, 𝐵) ↔ (𝜑 ↔ 𝜓))) | ||
| Theorem | ififcom 32862 | Commute two nested conditionals. (Contributed by Thierry Arnoux, 4-May-2026.) |
| ⊢ if(𝜑, if(𝜓, 𝐴, 𝐵), 𝐵) = if(𝜓, if(𝜑, 𝐴, 𝐵), 𝐵) | ||
| Theorem | uniinn0 32863* | Sufficient and necessary condition for a union to intersect with a given set. (Contributed by Thierry Arnoux, 27-Jan-2020.) |
| ⊢ ((∪ 𝐴 ∩ 𝐵) ≠ ∅ ↔ ∃𝑥 ∈ 𝐴 (𝑥 ∩ 𝐵) ≠ ∅) | ||
| Theorem | difuncomp 32864 | Express a class difference using unions and class complements. (Contributed by Thierry Arnoux, 21-Jun-2020.) |
| ⊢ (𝐴 ⊆ 𝐶 → (𝐴 ∖ 𝐵) = (𝐶 ∖ ((𝐶 ∖ 𝐴) ∪ 𝐵))) | ||
| Theorem | elpwunicl 32865 | Closure of a set union with regard to elementhood to a power set. (Contributed by Thierry Arnoux, 21-Jun-2020.) (Proof shortened by BJ, 6-Apr-2024.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝒫 𝒫 𝐵) ⇒ ⊢ (𝜑 → ∪ 𝐴 ∈ 𝒫 𝐵) | ||
| Theorem | cbviunf 32866* | Rule used to change the bound variables in an indexed union, with the substitution specified implicitly by the hypothesis. (Contributed by NM, 26-Mar-2006.) (Revised by Andrew Salmon, 25-Jul-2011.) |
| ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑦𝐵 & ⊢ Ⅎ𝑥𝐶 & ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) ⇒ ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐴 𝐶 | ||
| Theorem | iuneq12daf 32867 | Equality deduction for indexed union, deduction version. (Contributed by Thierry Arnoux, 13-Mar-2017.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐷) | ||
| Theorem | iunin1f 32868 | Indexed union of intersection. Generalization of half of theorem "Distributive laws" in [Enderton] p. 30. Use uniiun 5022 to recover Enderton's theorem. (Contributed by NM, 26-Mar-2004.) (Revised by Thierry Arnoux, 2-May-2020.) |
| ⊢ Ⅎ𝑥𝐶 ⇒ ⊢ ∪ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) | ||
| Theorem | ssiun3 32869* | Subset equivalence for an indexed union. (Contributed by Thierry Arnoux, 17-Oct-2016.) |
| ⊢ (∀𝑦 ∈ 𝐶 ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 ↔ 𝐶 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵) | ||
| Theorem | ssiun2sf 32870 | Subset relationship for an indexed union. (Contributed by Thierry Arnoux, 31-Dec-2016.) |
| ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐶 & ⊢ Ⅎ𝑥𝐷 & ⊢ (𝑥 = 𝐶 → 𝐵 = 𝐷) ⇒ ⊢ (𝐶 ∈ 𝐴 → 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵) | ||
| Theorem | iuninc 32871* | The union of an increasing collection of sets is its last element. (Contributed by Thierry Arnoux, 22-Jan-2017.) |
| ⊢ (𝜑 → 𝐹 Fn ℕ) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ⇒ ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → ∪ 𝑛 ∈ (1...𝑖)(𝐹‘𝑛) = (𝐹‘𝑖)) | ||
| Theorem | iundifdifd 32872* | The intersection of a set is the complement of the union of the complements. (Contributed by Thierry Arnoux, 19-Dec-2016.) |
| ⊢ (𝐴 ⊆ 𝒫 𝑂 → (𝐴 ≠ ∅ → ∩ 𝐴 = (𝑂 ∖ ∪ 𝑥 ∈ 𝐴 (𝑂 ∖ 𝑥)))) | ||
| Theorem | iundifdif 32873* | The intersection of a set is the complement of the union of the complements. TODO: shorten using iundifdifd 32872. (Contributed by Thierry Arnoux, 4-Sep-2016.) |
| ⊢ 𝑂 ∈ V & ⊢ 𝐴 ⊆ 𝒫 𝑂 ⇒ ⊢ (𝐴 ≠ ∅ → ∩ 𝐴 = (𝑂 ∖ ∪ 𝑥 ∈ 𝐴 (𝑂 ∖ 𝑥))) | ||
| Theorem | iunrdx 32874* | Re-index an indexed union. (Contributed by Thierry Arnoux, 6-Apr-2017.) |
| ⊢ (𝜑 → 𝐹:𝐴–onto→𝐶) & ⊢ ((𝜑 ∧ 𝑦 = (𝐹‘𝑥)) → 𝐷 = 𝐵) ⇒ ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐶 𝐷) | ||
| Theorem | iunpreima 32875* | Preimage of an indexed union. (Contributed by Thierry Arnoux, 27-Mar-2018.) |
| ⊢ (Fun 𝐹 → (◡𝐹 “ ∪ 𝑥 ∈ 𝐴 𝐵) = ∪ 𝑥 ∈ 𝐴 (◡𝐹 “ 𝐵)) | ||
| Theorem | iunrnmptss 32876* | A subset relation for an indexed union over the range of function expressed as a mapping. (Contributed by Thierry Arnoux, 27-Mar-2018.) |
| ⊢ (𝑦 = 𝐵 → 𝐶 = 𝐷) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) ⇒ ⊢ (𝜑 → ∪ 𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝐶 ⊆ ∪ 𝑥 ∈ 𝐴 𝐷) | ||
| Theorem | iunxunsn 32877* | Appending a set to an indexed union. (Contributed by Thierry Arnoux, 20-Nov-2023.) |
| ⊢ (𝑥 = 𝑋 → 𝐵 = 𝐶) ⇒ ⊢ (𝑋 ∈ 𝑉 → ∪ 𝑥 ∈ (𝐴 ∪ {𝑋})𝐵 = (∪ 𝑥 ∈ 𝐴 𝐵 ∪ 𝐶)) | ||
| Theorem | iunxunpr 32878* | Appending two sets to an indexed union. (Contributed by Thierry Arnoux, 20-Nov-2023.) |
| ⊢ (𝑥 = 𝑋 → 𝐵 = 𝐶) & ⊢ (𝑥 = 𝑌 → 𝐵 = 𝐷) ⇒ ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → ∪ 𝑥 ∈ (𝐴 ∪ {𝑋, 𝑌})𝐵 = (∪ 𝑥 ∈ 𝐴 𝐵 ∪ (𝐶 ∪ 𝐷))) | ||
| Theorem | iunxpssiun1 32879* | Provide an upper bound for the indexed union of cartesian products. (Contributed by Thierry Arnoux, 13-Oct-2025.) |
| ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ⊆ 𝐸) ⇒ ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 (𝐵 × 𝐶) ⊆ (∪ 𝑥 ∈ 𝐴 𝐵 × 𝐸)) | ||
| Theorem | iinabrex 32880* | Rewriting an indexed intersection into an intersection of its image set. (Contributed by Thierry Arnoux, 15-Jun-2024.) |
| ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}) | ||
| Theorem | disjnf 32881* | In case 𝑥 is not free in 𝐵, disjointness is not so interesting since it reduces to cases where 𝐴 is a singleton. (Google Groups discussion with Peter Mazsa.) (Contributed by Thierry Arnoux, 26-Jul-2018.) |
| ⊢ (Disj 𝑥 ∈ 𝐴 𝐵 ↔ (𝐵 = ∅ ∨ ∃*𝑥 𝑥 ∈ 𝐴)) | ||
| Theorem | cbvdisjf 32882* | Change bound variables in a disjoint collection. (Contributed by Thierry Arnoux, 6-Apr-2017.) |
| ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑦𝐵 & ⊢ Ⅎ𝑥𝐶 & ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) ⇒ ⊢ (Disj 𝑥 ∈ 𝐴 𝐵 ↔ Disj 𝑦 ∈ 𝐴 𝐶) | ||
| Theorem | disjss1f 32883 | A subset of a disjoint collection is disjoint. (Contributed by Thierry Arnoux, 6-Apr-2017.) |
| ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (𝐴 ⊆ 𝐵 → (Disj 𝑥 ∈ 𝐵 𝐶 → Disj 𝑥 ∈ 𝐴 𝐶)) | ||
| Theorem | disjeq1f 32884 | Equality theorem for disjoint collection. (Contributed by Mario Carneiro, 14-Nov-2016.) |
| ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (𝐴 = 𝐵 → (Disj 𝑥 ∈ 𝐴 𝐶 ↔ Disj 𝑥 ∈ 𝐵 𝐶)) | ||
| Theorem | disjxun0 32885* | Simplify a disjoint union. (Contributed by Thierry Arnoux, 27-Nov-2023.) |
| ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 = ∅) ⇒ ⊢ (𝜑 → (Disj 𝑥 ∈ (𝐴 ∪ 𝐵)𝐶 ↔ Disj 𝑥 ∈ 𝐴 𝐶)) | ||
| Theorem | disjdifprg 32886* | A trivial partition into a subset and its complement. (Contributed by Thierry Arnoux, 25-Dec-2016.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → Disj 𝑥 ∈ {(𝐵 ∖ 𝐴), 𝐴}𝑥) | ||
| Theorem | disjdifprg2 32887* | A trivial partition of a set into its difference and intersection with another set. (Contributed by Thierry Arnoux, 25-Dec-2016.) |
| ⊢ (𝐴 ∈ 𝑉 → Disj 𝑥 ∈ {(𝐴 ∖ 𝐵), (𝐴 ∩ 𝐵)}𝑥) | ||
| Theorem | disji2f 32888* | Property of a disjoint collection: if 𝐵(𝑥) = 𝐶 and 𝐵(𝑌) = 𝐷, and 𝑥 ≠ 𝑌, then 𝐵 and 𝐶 are disjoint. (Contributed by Thierry Arnoux, 30-Dec-2016.) |
| ⊢ Ⅎ𝑥𝐶 & ⊢ (𝑥 = 𝑌 → 𝐵 = 𝐶) ⇒ ⊢ ((Disj 𝑥 ∈ 𝐴 𝐵 ∧ (𝑥 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) ∧ 𝑥 ≠ 𝑌) → (𝐵 ∩ 𝐶) = ∅) | ||
| Theorem | disjif 32889* | Property of a disjoint collection: if 𝐵(𝑥) and 𝐵(𝑌) = 𝐷 have a common element 𝑍, then 𝑥 = 𝑌. (Contributed by Thierry Arnoux, 30-Dec-2016.) |
| ⊢ Ⅎ𝑥𝐶 & ⊢ (𝑥 = 𝑌 → 𝐵 = 𝐶) ⇒ ⊢ ((Disj 𝑥 ∈ 𝐴 𝐵 ∧ (𝑥 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) ∧ (𝑍 ∈ 𝐵 ∧ 𝑍 ∈ 𝐶)) → 𝑥 = 𝑌) | ||
| Theorem | disjorf 32890* | Two ways to say that a collection 𝐵(𝑖) for 𝑖 ∈ 𝐴 is disjoint. (Contributed by Thierry Arnoux, 8-Mar-2017.) |
| ⊢ Ⅎ𝑖𝐴 & ⊢ Ⅎ𝑗𝐴 & ⊢ (𝑖 = 𝑗 → 𝐵 = 𝐶) ⇒ ⊢ (Disj 𝑖 ∈ 𝐴 𝐵 ↔ ∀𝑖 ∈ 𝐴 ∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (𝐵 ∩ 𝐶) = ∅)) | ||
| Theorem | disjorsf 32891* | Two ways to say that a collection 𝐵(𝑖) for 𝑖 ∈ 𝐴 is disjoint. (Contributed by Thierry Arnoux, 8-Mar-2017.) |
| ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ (Disj 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑖 ∈ 𝐴 ∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅)) | ||
| Theorem | disjif2 32892* | Property of a disjoint collection: if 𝐵(𝑥) and 𝐵(𝑌) = 𝐷 have a common element 𝑍, then 𝑥 = 𝑌. (Contributed by Thierry Arnoux, 6-Apr-2017.) |
| ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐶 & ⊢ (𝑥 = 𝑌 → 𝐵 = 𝐶) ⇒ ⊢ ((Disj 𝑥 ∈ 𝐴 𝐵 ∧ (𝑥 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) ∧ (𝑍 ∈ 𝐵 ∧ 𝑍 ∈ 𝐶)) → 𝑥 = 𝑌) | ||
| Theorem | disjabrex 32893* | Rewriting a disjoint collection into a partition of its image set. (Contributed by Thierry Arnoux, 30-Dec-2016.) |
| ⊢ (Disj 𝑥 ∈ 𝐴 𝐵 → Disj 𝑦 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵}𝑦) | ||
| Theorem | disjabrexf 32894* | Rewriting a disjoint collection into a partition of its image set. (Contributed by Thierry Arnoux, 30-Dec-2016.) (Revised by Thierry Arnoux, 9-Mar-2017.) |
| ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ (Disj 𝑥 ∈ 𝐴 𝐵 → Disj 𝑦 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵}𝑦) | ||
| Theorem | disjpreima 32895* | A preimage of a disjoint set is disjoint. (Contributed by Thierry Arnoux, 7-Feb-2017.) |
| ⊢ ((Fun 𝐹 ∧ Disj 𝑥 ∈ 𝐴 𝐵) → Disj 𝑥 ∈ 𝐴 (◡𝐹 “ 𝐵)) | ||
| Theorem | disjrnmpt 32896* | Rewriting a disjoint collection using the range of a mapping. (Contributed by Thierry Arnoux, 27-May-2020.) |
| ⊢ (Disj 𝑥 ∈ 𝐴 𝐵 → Disj 𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑦) | ||
| Theorem | disjin 32897 | If a collection is disjoint, so is the collection of the intersections with a given set. (Contributed by Thierry Arnoux, 14-Feb-2017.) |
| ⊢ (Disj 𝑥 ∈ 𝐵 𝐶 → Disj 𝑥 ∈ 𝐵 (𝐶 ∩ 𝐴)) | ||
| Theorem | disjin2 32898 | If a collection is disjoint, so is the collection of the intersections with a given set. (Contributed by Thierry Arnoux, 21-Jun-2020.) |
| ⊢ (Disj 𝑥 ∈ 𝐵 𝐶 → Disj 𝑥 ∈ 𝐵 (𝐴 ∩ 𝐶)) | ||
| Theorem | disjxpin 32899* | Derive a disjunction over a Cartesian product from the disjunctions over its first and second elements. (Contributed by Thierry Arnoux, 9-Mar-2018.) |
| ⊢ (𝑥 = (1st ‘𝑝) → 𝐶 = 𝐸) & ⊢ (𝑦 = (2nd ‘𝑝) → 𝐷 = 𝐹) & ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐶) & ⊢ (𝜑 → Disj 𝑦 ∈ 𝐵 𝐷) ⇒ ⊢ (𝜑 → Disj 𝑝 ∈ (𝐴 × 𝐵)(𝐸 ∩ 𝐹)) | ||
| Theorem | iundisjf 32900* | Rewrite a countable union as a disjoint union. Cf. iundisj 25686. (Contributed by Thierry Arnoux, 31-Dec-2016.) |
| ⊢ Ⅎ𝑘𝐴 & ⊢ Ⅎ𝑛𝐵 & ⊢ (𝑛 = 𝑘 → 𝐴 = 𝐵) ⇒ ⊢ ∪ 𝑛 ∈ ℕ 𝐴 = ∪ 𝑛 ∈ ℕ (𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |