HomeTheorem List (p. 326 of 499)
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. 326 of 499) | < 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-30888) |
Hilbert Space Explorer
(30889-32411) |
Users' Mathboxes
(32412-49816) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | nelpr 32501 | A set 𝐴 not in a pair is neither element of the pair. (Contributed by Thierry Arnoux, 20-Nov-2023.) |
| ⊢ (𝐴 ∈ 𝑉 → (¬ 𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶))) | ||
| Theorem | inpr0 32502 | Rewrite an empty intersection with a pair. (Contributed by Thierry Arnoux, 20-Nov-2023.) |
| ⊢ ((𝐴 ∩ {𝐵, 𝐶}) = ∅ ↔ (¬ 𝐵 ∈ 𝐴 ∧ ¬ 𝐶 ∈ 𝐴)) | ||
| Theorem | neldifpr1 32503 | 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 32504 | 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 32505 | The other element of a pair is an element of the pair. (Contributed by Thierry Arnoux, 26-Aug-2017.) |
| ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o) → ∪ (𝑃 ∖ {𝑋}) ∈ 𝑃) | ||
| Theorem | unidifsnne 32506 | The other element of a pair is not the known element. (Contributed by Thierry Arnoux, 26-Aug-2017.) |
| ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o) → ∪ (𝑃 ∖ {𝑋}) ≠ 𝑋) | ||
| Theorem | tpssg 32507 | An unordered triple of elements of a class is a subset of the class. (Contributed by Thierry Arnoux, 2-Nov-2025.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → ((𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐷) ↔ {𝐴, 𝐵, 𝐶} ⊆ 𝐷)) | ||
| Theorem | tpssd 32508 | 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 32509 | 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 32510 | 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 32511 | 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 32512* | An equality theorem tailored for ballotlemsf1o 34517. (Contributed by Thierry Arnoux, 14-Apr-2017.) |
| ⊢ (𝑥 = 𝑋 → 𝐴 = 𝐶) & ⊢ (𝑥 = 𝑌 → 𝐵 = 𝑎) & ⊢ (𝑥 = 𝑋 → (𝜒 ↔ 𝜃)) & ⊢ (𝑥 = 𝑌 → (𝜒 ↔ 𝜓)) & ⊢ (𝜑 → 𝑎 = 𝐶) & ⊢ ((𝜑 ∧ 𝜓) → 𝜃) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝑊) ⇒ ⊢ ((𝜑 ∧ 𝑥 = if(𝜓, 𝑋, 𝑌)) → 𝑎 = if(𝜒, 𝐴, 𝐵)) | ||
| Theorem | elimifd 32513 | Elimination of a conditional operator contained in a wff 𝜒. (Contributed by Thierry Arnoux, 25-Jan-2017.) |
| ⊢ (𝜑 → (if(𝜓, 𝐴, 𝐵) = 𝐴 → (𝜒 ↔ 𝜃))) & ⊢ (𝜑 → (if(𝜓, 𝐴, 𝐵) = 𝐵 → (𝜒 ↔ 𝜏))) ⇒ ⊢ (𝜑 → (𝜒 ↔ ((𝜓 ∧ 𝜃) ∨ (¬ 𝜓 ∧ 𝜏)))) | ||
| Theorem | elim2if 32514 | Elimination of two conditional operators contained in a wff 𝜒. (Contributed by Thierry Arnoux, 25-Jan-2017.) |
| ⊢ (if(𝜑, 𝐴, if(𝜓, 𝐵, 𝐶)) = 𝐴 → (𝜒 ↔ 𝜃)) & ⊢ (if(𝜑, 𝐴, if(𝜓, 𝐵, 𝐶)) = 𝐵 → (𝜒 ↔ 𝜏)) & ⊢ (if(𝜑, 𝐴, if(𝜓, 𝐵, 𝐶)) = 𝐶 → (𝜒 ↔ 𝜂)) ⇒ ⊢ (𝜒 ↔ ((𝜑 ∧ 𝜃) ∨ (¬ 𝜑 ∧ ((𝜓 ∧ 𝜏) ∨ (¬ 𝜓 ∧ 𝜂))))) | ||
| Theorem | elim2ifim 32515 | Elimination of two conditional operators for an implication. (Contributed by Thierry Arnoux, 25-Jan-2017.) |
| ⊢ (if(𝜑, 𝐴, if(𝜓, 𝐵, 𝐶)) = 𝐴 → (𝜒 ↔ 𝜃)) & ⊢ (if(𝜑, 𝐴, if(𝜓, 𝐵, 𝐶)) = 𝐵 → (𝜒 ↔ 𝜏)) & ⊢ (if(𝜑, 𝐴, if(𝜓, 𝐵, 𝐶)) = 𝐶 → (𝜒 ↔ 𝜂)) & ⊢ (𝜑 → 𝜃) & ⊢ ((¬ 𝜑 ∧ 𝜓) → 𝜏) & ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → 𝜂) ⇒ ⊢ 𝜒 | ||
| Theorem | ifeq3da 32516 | 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 32517 | Deduce truth from a conditional operator value. (Contributed by Thierry Arnoux, 20-Feb-2025.) |
| ⊢ ((𝐴 ≠ 𝐵 ∧ if(𝜑, 𝐴, 𝐵) = 𝐴) → 𝜑) | ||
| Theorem | ifnefals 32518 | Deduce falsehood from a conditional operator value. (Contributed by Thierry Arnoux, 20-Feb-2025.) |
| ⊢ ((𝐴 ≠ 𝐵 ∧ if(𝜑, 𝐴, 𝐵) = 𝐵) → ¬ 𝜑) | ||
| Theorem | ifnebib 32519 | The converse of ifbi 4496 holds if the two values are not equal. (Contributed by Thierry Arnoux, 20-Feb-2025.) |
| ⊢ (𝐴 ≠ 𝐵 → (if(𝜑, 𝐴, 𝐵) = if(𝜓, 𝐴, 𝐵) ↔ (𝜑 ↔ 𝜓))) | ||
| Theorem | uniinn0 32520* | Sufficient and necessary condition for a union to intersect with a given set. (Contributed by Thierry Arnoux, 27-Jan-2020.) |
| ⊢ ((∪ 𝐴 ∩ 𝐵) ≠ ∅ ↔ ∃𝑥 ∈ 𝐴 (𝑥 ∩ 𝐵) ≠ ∅) | ||
| Theorem | uniin1 32521* | Union of intersection. Generalization of half of theorem "Distributive laws" in [Enderton] p. 30. (Contributed by Thierry Arnoux, 21-Jun-2020.) |
| ⊢ ∪ 𝑥 ∈ 𝐴 (𝑥 ∩ 𝐵) = (∪ 𝐴 ∩ 𝐵) | ||
| Theorem | uniin2 32522* | Union of intersection. Generalization of half of theorem "Distributive laws" in [Enderton] p. 30. (Contributed by Thierry Arnoux, 21-Jun-2020.) |
| ⊢ ∪ 𝑥 ∈ 𝐵 (𝐴 ∩ 𝑥) = (𝐴 ∩ ∪ 𝐵) | ||
| Theorem | difuncomp 32523 | Express a class difference using unions and class complements. (Contributed by Thierry Arnoux, 21-Jun-2020.) |
| ⊢ (𝐴 ⊆ 𝐶 → (𝐴 ∖ 𝐵) = (𝐶 ∖ ((𝐶 ∖ 𝐴) ∪ 𝐵))) | ||
| Theorem | elpwunicl 32524 | 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 32525* | 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 32526 | Equality deduction for indexed union, deduction version. (Contributed by Thierry Arnoux, 13-Mar-2017.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐷) | ||
| Theorem | iunin1f 32527 | Indexed union of intersection. Generalization of half of theorem "Distributive laws" in [Enderton] p. 30. Use uniiun 5005 to recover Enderton's theorem. (Contributed by NM, 26-Mar-2004.) (Revised by Thierry Arnoux, 2-May-2020.) |
| ⊢ Ⅎ𝑥𝐶 ⇒ ⊢ ∪ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) | ||
| Theorem | ssiun3 32528* | Subset equivalence for an indexed union. (Contributed by Thierry Arnoux, 17-Oct-2016.) |
| ⊢ (∀𝑦 ∈ 𝐶 ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 ↔ 𝐶 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵) | ||
| Theorem | ssiun2sf 32529 | Subset relationship for an indexed union. (Contributed by Thierry Arnoux, 31-Dec-2016.) |
| ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐶 & ⊢ Ⅎ𝑥𝐷 & ⊢ (𝑥 = 𝐶 → 𝐵 = 𝐷) ⇒ ⊢ (𝐶 ∈ 𝐴 → 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵) | ||
| Theorem | iuninc 32530* | The union of an increasing collection of sets is its last element. (Contributed by Thierry Arnoux, 22-Jan-2017.) |
| ⊢ (𝜑 → 𝐹 Fn ℕ) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ⇒ ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → ∪ 𝑛 ∈ (1...𝑖)(𝐹‘𝑛) = (𝐹‘𝑖)) | ||
| Theorem | iundifdifd 32531* | The intersection of a set is the complement of the union of the complements. (Contributed by Thierry Arnoux, 19-Dec-2016.) |
| ⊢ (𝐴 ⊆ 𝒫 𝑂 → (𝐴 ≠ ∅ → ∩ 𝐴 = (𝑂 ∖ ∪ 𝑥 ∈ 𝐴 (𝑂 ∖ 𝑥)))) | ||
| Theorem | iundifdif 32532* | The intersection of a set is the complement of the union of the complements. TODO: shorten using iundifdifd 32531. (Contributed by Thierry Arnoux, 4-Sep-2016.) |
| ⊢ 𝑂 ∈ V & ⊢ 𝐴 ⊆ 𝒫 𝑂 ⇒ ⊢ (𝐴 ≠ ∅ → ∩ 𝐴 = (𝑂 ∖ ∪ 𝑥 ∈ 𝐴 (𝑂 ∖ 𝑥))) | ||
| Theorem | iunrdx 32533* | Re-index an indexed union. (Contributed by Thierry Arnoux, 6-Apr-2017.) |
| ⊢ (𝜑 → 𝐹:𝐴–onto→𝐶) & ⊢ ((𝜑 ∧ 𝑦 = (𝐹‘𝑥)) → 𝐷 = 𝐵) ⇒ ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐶 𝐷) | ||
| Theorem | iunpreima 32534* | Preimage of an indexed union. (Contributed by Thierry Arnoux, 27-Mar-2018.) |
| ⊢ (Fun 𝐹 → (◡𝐹 “ ∪ 𝑥 ∈ 𝐴 𝐵) = ∪ 𝑥 ∈ 𝐴 (◡𝐹 “ 𝐵)) | ||
| Theorem | iunrnmptss 32535* | 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 32536* | Appending a set to an indexed union. (Contributed by Thierry Arnoux, 20-Nov-2023.) |
| ⊢ (𝑥 = 𝑋 → 𝐵 = 𝐶) ⇒ ⊢ (𝑋 ∈ 𝑉 → ∪ 𝑥 ∈ (𝐴 ∪ {𝑋})𝐵 = (∪ 𝑥 ∈ 𝐴 𝐵 ∪ 𝐶)) | ||
| Theorem | iunxunpr 32537* | Appending two sets to an indexed union. (Contributed by Thierry Arnoux, 20-Nov-2023.) |
| ⊢ (𝑥 = 𝑋 → 𝐵 = 𝐶) & ⊢ (𝑥 = 𝑌 → 𝐵 = 𝐷) ⇒ ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → ∪ 𝑥 ∈ (𝐴 ∪ {𝑋, 𝑌})𝐵 = (∪ 𝑥 ∈ 𝐴 𝐵 ∪ (𝐶 ∪ 𝐷))) | ||
| Theorem | iunxpssiun1 32538* | Provide an upper bound for the indexed union of cartesian products. (Contributed by Thierry Arnoux, 13-Oct-2025.) |
| ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ⊆ 𝐸) ⇒ ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 (𝐵 × 𝐶) ⊆ (∪ 𝑥 ∈ 𝐴 𝐵 × 𝐸)) | ||
| Theorem | iinabrex 32539* | Rewriting an indexed intersection into an intersection of its image set. (Contributed by Thierry Arnoux, 15-Jun-2024.) |
| ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}) | ||
| Theorem | disjnf 32540* | 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 32541* | Change bound variables in a disjoint collection. (Contributed by Thierry Arnoux, 6-Apr-2017.) |
| ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑦𝐵 & ⊢ Ⅎ𝑥𝐶 & ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) ⇒ ⊢ (Disj 𝑥 ∈ 𝐴 𝐵 ↔ Disj 𝑦 ∈ 𝐴 𝐶) | ||
| Theorem | disjss1f 32542 | A subset of a disjoint collection is disjoint. (Contributed by Thierry Arnoux, 6-Apr-2017.) |
| ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (𝐴 ⊆ 𝐵 → (Disj 𝑥 ∈ 𝐵 𝐶 → Disj 𝑥 ∈ 𝐴 𝐶)) | ||
| Theorem | disjeq1f 32543 | Equality theorem for disjoint collection. (Contributed by Mario Carneiro, 14-Nov-2016.) |
| ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (𝐴 = 𝐵 → (Disj 𝑥 ∈ 𝐴 𝐶 ↔ Disj 𝑥 ∈ 𝐵 𝐶)) | ||
| Theorem | disjxun0 32544* | Simplify a disjoint union. (Contributed by Thierry Arnoux, 27-Nov-2023.) |
| ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 = ∅) ⇒ ⊢ (𝜑 → (Disj 𝑥 ∈ (𝐴 ∪ 𝐵)𝐶 ↔ Disj 𝑥 ∈ 𝐴 𝐶)) | ||
| Theorem | disjdifprg 32545* | A trivial partition into a subset and its complement. (Contributed by Thierry Arnoux, 25-Dec-2016.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → Disj 𝑥 ∈ {(𝐵 ∖ 𝐴), 𝐴}𝑥) | ||
| Theorem | disjdifprg2 32546* | A trivial partition of a set into its difference and intersection with another set. (Contributed by Thierry Arnoux, 25-Dec-2016.) |
| ⊢ (𝐴 ∈ 𝑉 → Disj 𝑥 ∈ {(𝐴 ∖ 𝐵), (𝐴 ∩ 𝐵)}𝑥) | ||
| Theorem | disji2f 32547* | Property of a disjoint collection: if 𝐵(𝑥) = 𝐶 and 𝐵(𝑌) = 𝐷, and 𝑥 ≠ 𝑌, then 𝐵 and 𝐶 are disjoint. (Contributed by Thierry Arnoux, 30-Dec-2016.) |
| ⊢ Ⅎ𝑥𝐶 & ⊢ (𝑥 = 𝑌 → 𝐵 = 𝐶) ⇒ ⊢ ((Disj 𝑥 ∈ 𝐴 𝐵 ∧ (𝑥 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) ∧ 𝑥 ≠ 𝑌) → (𝐵 ∩ 𝐶) = ∅) | ||
| Theorem | disjif 32548* | Property of a disjoint collection: if 𝐵(𝑥) and 𝐵(𝑌) = 𝐷 have a common element 𝑍, then 𝑥 = 𝑌. (Contributed by Thierry Arnoux, 30-Dec-2016.) |
| ⊢ Ⅎ𝑥𝐶 & ⊢ (𝑥 = 𝑌 → 𝐵 = 𝐶) ⇒ ⊢ ((Disj 𝑥 ∈ 𝐴 𝐵 ∧ (𝑥 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) ∧ (𝑍 ∈ 𝐵 ∧ 𝑍 ∈ 𝐶)) → 𝑥 = 𝑌) | ||
| Theorem | disjorf 32549* | Two ways to say that a collection 𝐵(𝑖) for 𝑖 ∈ 𝐴 is disjoint. (Contributed by Thierry Arnoux, 8-Mar-2017.) |
| ⊢ Ⅎ𝑖𝐴 & ⊢ Ⅎ𝑗𝐴 & ⊢ (𝑖 = 𝑗 → 𝐵 = 𝐶) ⇒ ⊢ (Disj 𝑖 ∈ 𝐴 𝐵 ↔ ∀𝑖 ∈ 𝐴 ∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (𝐵 ∩ 𝐶) = ∅)) | ||
| Theorem | disjorsf 32550* | Two ways to say that a collection 𝐵(𝑖) for 𝑖 ∈ 𝐴 is disjoint. (Contributed by Thierry Arnoux, 8-Mar-2017.) |
| ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ (Disj 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑖 ∈ 𝐴 ∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅)) | ||
| Theorem | disjif2 32551* | Property of a disjoint collection: if 𝐵(𝑥) and 𝐵(𝑌) = 𝐷 have a common element 𝑍, then 𝑥 = 𝑌. (Contributed by Thierry Arnoux, 6-Apr-2017.) |
| ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐶 & ⊢ (𝑥 = 𝑌 → 𝐵 = 𝐶) ⇒ ⊢ ((Disj 𝑥 ∈ 𝐴 𝐵 ∧ (𝑥 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) ∧ (𝑍 ∈ 𝐵 ∧ 𝑍 ∈ 𝐶)) → 𝑥 = 𝑌) | ||
| Theorem | disjabrex 32552* | Rewriting a disjoint collection into a partition of its image set. (Contributed by Thierry Arnoux, 30-Dec-2016.) |
| ⊢ (Disj 𝑥 ∈ 𝐴 𝐵 → Disj 𝑦 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵}𝑦) | ||
| Theorem | disjabrexf 32553* | 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 32554* | A preimage of a disjoint set is disjoint. (Contributed by Thierry Arnoux, 7-Feb-2017.) |
| ⊢ ((Fun 𝐹 ∧ Disj 𝑥 ∈ 𝐴 𝐵) → Disj 𝑥 ∈ 𝐴 (◡𝐹 “ 𝐵)) | ||
| Theorem | disjrnmpt 32555* | Rewriting a disjoint collection using the range of a mapping. (Contributed by Thierry Arnoux, 27-May-2020.) |
| ⊢ (Disj 𝑥 ∈ 𝐴 𝐵 → Disj 𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑦) | ||
| Theorem | disjin 32556 | 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 32557 | 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 32558* | 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 32559* | Rewrite a countable union as a disjoint union. Cf. iundisj 25469. (Contributed by Thierry Arnoux, 31-Dec-2016.) |
| ⊢ Ⅎ𝑘𝐴 & ⊢ Ⅎ𝑛𝐵 & ⊢ (𝑛 = 𝑘 → 𝐴 = 𝐵) ⇒ ⊢ ∪ 𝑛 ∈ ℕ 𝐴 = ∪ 𝑛 ∈ ℕ (𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) | ||
| Theorem | iundisj2f 32560* | A disjoint union is disjoint. Cf. iundisj2 25470. (Contributed by Thierry Arnoux, 30-Dec-2016.) |
| ⊢ Ⅎ𝑘𝐴 & ⊢ Ⅎ𝑛𝐵 & ⊢ (𝑛 = 𝑘 → 𝐴 = 𝐵) ⇒ ⊢ Disj 𝑛 ∈ ℕ (𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) | ||
| Theorem | disjrdx 32561* | Re-index a disjunct collection statement. (Contributed by Thierry Arnoux, 7-Apr-2017.) |
| ⊢ (𝜑 → 𝐹:𝐴–1-1-onto→𝐶) & ⊢ ((𝜑 ∧ 𝑦 = (𝐹‘𝑥)) → 𝐷 = 𝐵) ⇒ ⊢ (𝜑 → (Disj 𝑥 ∈ 𝐴 𝐵 ↔ Disj 𝑦 ∈ 𝐶 𝐷)) | ||
| Theorem | disjex 32562* | Two ways to say that two classes are disjoint (or equal). (Contributed by Thierry Arnoux, 4-Oct-2016.) |
| ⊢ ((∃𝑧(𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵) → 𝐴 = 𝐵) ↔ (𝐴 = 𝐵 ∨ (𝐴 ∩ 𝐵) = ∅)) | ||
| Theorem | disjexc 32563* | A variant of disjex 32562, applicable for more generic families. (Contributed by Thierry Arnoux, 4-Oct-2016.) |
| ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) ⇒ ⊢ ((∃𝑧(𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵) → 𝑥 = 𝑦) → (𝐴 = 𝐵 ∨ (𝐴 ∩ 𝐵) = ∅)) | ||
| Theorem | disjunsn 32564* | Append an element to a disjoint collection. Similar to ralunsn 4844, gsumunsn 19865, etc. (Contributed by Thierry Arnoux, 28-Mar-2018.) |
| ⊢ (𝑥 = 𝑀 → 𝐵 = 𝐶) ⇒ ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → (Disj 𝑥 ∈ (𝐴 ∪ {𝑀})𝐵 ↔ (Disj 𝑥 ∈ 𝐴 𝐵 ∧ (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅))) | ||
| Theorem | disjun0 32565* | Adding the empty element preserves disjointness. (Contributed by Thierry Arnoux, 30-May-2020.) |
| ⊢ (Disj 𝑥 ∈ 𝐴 𝑥 → Disj 𝑥 ∈ (𝐴 ∪ {∅})𝑥) | ||
| Theorem | disjiunel 32566* | A set of elements B of a disjoint set A is disjoint with another element of that set. (Contributed by Thierry Arnoux, 24-May-2020.) |
| ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐵) & ⊢ (𝑥 = 𝑌 → 𝐵 = 𝐷) & ⊢ (𝜑 → 𝐸 ⊆ 𝐴) & ⊢ (𝜑 → 𝑌 ∈ (𝐴 ∖ 𝐸)) ⇒ ⊢ (𝜑 → (∪ 𝑥 ∈ 𝐸 𝐵 ∩ 𝐷) = ∅) | ||
| Theorem | disjuniel 32567* | A set of elements B of a disjoint set A is disjoint with another element of that set. (Contributed by Thierry Arnoux, 24-May-2020.) |
| ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝑥) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) & ⊢ (𝜑 → 𝐶 ∈ (𝐴 ∖ 𝐵)) ⇒ ⊢ (𝜑 → (∪ 𝐵 ∩ 𝐶) = ∅) | ||
| Theorem | xpdisjres 32568 | Restriction of a constant function (or other Cartesian product) outside of its domain. (Contributed by Thierry Arnoux, 25-Jan-2017.) |
| ⊢ ((𝐴 ∩ 𝐶) = ∅ → ((𝐴 × 𝐵) ↾ 𝐶) = ∅) | ||
| Theorem | opeldifid 32569 | Ordered pair elementhood outside of the diagonal. (Contributed by Thierry Arnoux, 1-Jan-2020.) |
| ⊢ (Rel 𝐴 → (⟨𝑋, 𝑌⟩ ∈ (𝐴 ∖ I ) ↔ (⟨𝑋, 𝑌⟩ ∈ 𝐴 ∧ 𝑋 ≠ 𝑌))) | ||
| Theorem | difres 32570 | Case when class difference in unaffected by restriction. (Contributed by Thierry Arnoux, 1-Jan-2020.) |
| ⊢ (𝐴 ⊆ (𝐵 × V) → (𝐴 ∖ (𝐶 ↾ 𝐵)) = (𝐴 ∖ 𝐶)) | ||
| Theorem | imadifxp 32571 | Image of the difference with a Cartesian product. (Contributed by Thierry Arnoux, 13-Dec-2017.) |
| ⊢ (𝐶 ⊆ 𝐴 → ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) = ((𝑅 “ 𝐶) ∖ 𝐵)) | ||
| Theorem | relfi 32572 | A relation (set) is finite if and only if both its domain and range are finite. (Contributed by Thierry Arnoux, 27-Aug-2017.) |
| ⊢ (Rel 𝐴 → (𝐴 ∈ Fin ↔ (dom 𝐴 ∈ Fin ∧ ran 𝐴 ∈ Fin))) | ||
| Theorem | 0res 32573 | Restriction of the empty function. (Contributed by Thierry Arnoux, 20-Nov-2023.) |
| ⊢ (∅ ↾ 𝐴) = ∅ | ||
| Theorem | fcoinver 32574 | Build an equivalence relation from a function. Two values are equivalent if they have the same image by the function. See also fcoinvbr 32575. (Contributed by Thierry Arnoux, 3-Jan-2020.) |
| ⊢ (𝐹 Fn 𝑋 → (◡𝐹 ∘ 𝐹) Er 𝑋) | ||
| Theorem | fcoinvbr 32575 | Binary relation for the equivalence relation from fcoinver 32574. (Contributed by Thierry Arnoux, 3-Jan-2020.) |
| ⊢ ∼ = (◡𝐹 ∘ 𝐹) ⇒ ⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝑋 ∼ 𝑌 ↔ (𝐹‘𝑋) = (𝐹‘𝑌))) | ||
| Theorem | breq1dd 32576 | Equality deduction for a binary relation. (Contributed by Thierry Arnoux, 10-Jan-2026.) |
| ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐴𝑅𝐶) ⇒ ⊢ (𝜑 → 𝐵𝑅𝐶) | ||
| Theorem | breq2dd 32577 | Equality deduction for a binary relation. (Contributed by Thierry Arnoux, 10-Jan-2026.) |
| ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶𝑅𝐴) ⇒ ⊢ (𝜑 → 𝐶𝑅𝐵) | ||
| Theorem | brab2d 32578* | Expressing that two sets are related by a binary relation which is expressed as a class abstraction of ordered pairs. (Contributed by Thierry Arnoux, 4-May-2025.) |
| ⊢ (𝜑 → 𝑅 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑉) ∧ 𝜓)}) & ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (𝐴𝑅𝐵 ↔ ((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉) ∧ 𝜒))) | ||
| Theorem | brabgaf 32579* | The law of concretion for a binary relation. (Contributed by Mario Carneiro, 19-Dec-2013.) (Revised by Thierry Arnoux, 17-May-2020.) |
| ⊢ Ⅎ𝑥𝜓 & ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) & ⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝜑} ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴𝑅𝐵 ↔ 𝜓)) | ||
| Theorem | brelg 32580 | Two things in a binary relation belong to the relation's domain. (Contributed by Thierry Arnoux, 29-Aug-2017.) |
| ⊢ ((𝑅 ⊆ (𝐶 × 𝐷) ∧ 𝐴𝑅𝐵) → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)) | ||
| Theorem | br8d 32581* | Substitution for an eight-place predicate. (Contributed by Scott Fenton, 26-Sep-2013.) (Revised by Mario Carneiro, 3-May-2015.) (Revised by Thierry Arnoux, 21-Mar-2019.) |
| ⊢ (𝑎 = 𝐴 → (𝜓 ↔ 𝜒)) & ⊢ (𝑏 = 𝐵 → (𝜒 ↔ 𝜃)) & ⊢ (𝑐 = 𝐶 → (𝜃 ↔ 𝜏)) & ⊢ (𝑑 = 𝐷 → (𝜏 ↔ 𝜂)) & ⊢ (𝑒 = 𝐸 → (𝜂 ↔ 𝜁)) & ⊢ (𝑓 = 𝐹 → (𝜁 ↔ 𝜎)) & ⊢ (𝑔 = 𝐺 → (𝜎 ↔ 𝜌)) & ⊢ (ℎ = 𝐻 → (𝜌 ↔ 𝜇)) & ⊢ (𝜑 → 𝑅 = {⟨𝑝, 𝑞⟩ ∣ ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜓)}) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 𝐺 ∈ 𝑃) & ⊢ (𝜑 → 𝐻 ∈ 𝑃) ⇒ ⊢ (𝜑 → (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩𝑅⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ ↔ 𝜇)) | ||
| Theorem | fnfvor 32582 | Relation between two functions implies the same relation for the function value at a given 𝑋. See also fnfvof 7622. (Contributed by Thierry Arnoux, 15-Jan-2026.) |
| ⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐺 Fn 𝐴) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹 ∘r 𝑅𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝐹‘𝑋)𝑅(𝐺‘𝑋)) | ||
| Theorem | ofrco 32583 | Function relation between function compositions. (Contributed by Thierry Arnoux, 15-Jan-2026.) |
| ⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐺 Fn 𝐴) & ⊢ (𝜑 → 𝐻:𝐶⟶𝐴) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑊) & ⊢ (𝜑 → 𝐹 ∘r 𝑅𝐺) ⇒ ⊢ (𝜑 → (𝐹 ∘ 𝐻) ∘r 𝑅(𝐺 ∘ 𝐻)) | ||
| Theorem | opabdm 32584* | Domain of an ordered-pair class abstraction. (Contributed by Thierry Arnoux, 31-Aug-2017.) |
| ⊢ (𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝜑} → dom 𝑅 = {𝑥 ∣ ∃𝑦𝜑}) | ||
| Theorem | opabrn 32585* | Range of an ordered-pair class abstraction. (Contributed by Thierry Arnoux, 31-Aug-2017.) |
| ⊢ (𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝜑} → ran 𝑅 = {𝑦 ∣ ∃𝑥𝜑}) | ||
| Theorem | opabssi 32586* | Sufficient condition for a collection of ordered pairs to be a subclass of a relation. (Contributed by Peter Mazsa, 21-Oct-2019.) (Revised by Thierry Arnoux, 18-Feb-2022.) |
| ⊢ (𝜑 → ⟨𝑥, 𝑦⟩ ∈ 𝐴) ⇒ ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ⊆ 𝐴 | ||
| Theorem | opabid2ss 32587* | One direction of opabid2 5766 which holds without a Rel 𝐴 requirement. (Contributed by Thierry Arnoux, 18-Feb-2022.) |
| ⊢ {⟨𝑥, 𝑦⟩ ∣ ⟨𝑥, 𝑦⟩ ∈ 𝐴} ⊆ 𝐴 | ||
| Theorem | ssrelf 32588* | A subclass relationship depends only on a relation's ordered pairs. Theorem 3.2(i) of [Monk1] p. 33. (Contributed by NM, 2-Aug-1994.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) (Revised by Thierry Arnoux, 6-Nov-2017.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ Ⅎ𝑦𝐵 ⇒ ⊢ (Rel 𝐴 → (𝐴 ⊆ 𝐵 ↔ ∀𝑥∀𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵))) | ||
| Theorem | eqrelrd2 32589* | A version of eqrelrdv2 5733 with explicit nonfree declarations. (Contributed by Thierry Arnoux, 28-Aug-2017.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ Ⅎ𝑦𝐵 & ⊢ (𝜑 → (⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐵)) ⇒ ⊢ (((Rel 𝐴 ∧ Rel 𝐵) ∧ 𝜑) → 𝐴 = 𝐵) | ||
| Theorem | erbr3b 32590 | Biconditional for equivalent elements. (Contributed by Thierry Arnoux, 6-Jan-2020.) |
| ⊢ ((𝑅 Er 𝑋 ∧ 𝐴𝑅𝐵) → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶)) | ||
| Theorem | iunsnima 32591 | Image of a singleton by an indexed union involving that singleton. (Contributed by Thierry Arnoux, 10-Apr-2020.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) “ {𝑥}) = 𝐵) | ||
| Theorem | iunsnima2 32592* | Version of iunsnima 32591 with different variables. (Contributed by Thierry Arnoux, 22-Jun-2024.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊) & ⊢ Ⅎ𝑥𝐶 & ⊢ (𝑥 = 𝑌 → 𝐵 = 𝐶) ⇒ ⊢ ((𝜑 ∧ 𝑌 ∈ 𝐴) → (∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) “ {𝑌}) = 𝐶) | ||
| Theorem | fconst7v 32593* | An alternative way to express a constant function. (Contributed by Glauco Siliprandi, 5-Feb-2022.) Removed hyphotheses as suggested by SN (Revised by Thierry Arnoux, 10-Jan-2026.) |
| ⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 𝐵) ⇒ ⊢ (𝜑 → 𝐹 = (𝐴 × {𝐵})) | ||
| Theorem | constcof 32594 | Composition with a constant function. See also fcoconst 7062. (Contributed by Thierry Arnoux, 11-Jan-2026.) |
| ⊢ (𝜑 → 𝐹:𝑋⟶𝐼) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) ⇒ ⊢ (𝜑 → ((𝐼 × {𝑌}) ∘ 𝐹) = (𝑋 × {𝑌})) | ||
| Theorem | ac6sf2 32595* | Alternate version of ac6 10363 with bound-variable hypothesis. (Contributed by NM, 2-Mar-2008.) (Revised by Thierry Arnoux, 17-May-2020.) |
| ⊢ Ⅎ𝑦𝐵 & ⊢ Ⅎ𝑦𝜓 & ⊢ 𝐴 ∈ V & ⊢ (𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑓(𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 𝜓)) | ||
| Theorem | ac6mapd 32596* | Axiom of choice equivalent, deduction form. (Contributed by Thierry Arnoux, 13-Oct-2025.) |
| ⊢ (𝑦 = (𝑓‘𝑥) → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∃𝑦 ∈ 𝐵 𝜓) ⇒ ⊢ (𝜑 → ∃𝑓 ∈ (𝐵 ↑m 𝐴)∀𝑥 ∈ 𝐴 𝜒) | ||
| Theorem | fnresin 32597 | Restriction of a function with a subclass of its domain. (Contributed by Thierry Arnoux, 10-Oct-2017.) |
| ⊢ (𝐹 Fn 𝐴 → (𝐹 ↾ 𝐵) Fn (𝐴 ∩ 𝐵)) | ||
| Theorem | f1o3d 32598* | Describe an implicit one-to-one onto function. (Contributed by Thierry Arnoux, 23-Apr-2017.) |
| ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝐷 ∈ 𝐴) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝑥 = 𝐷 ↔ 𝑦 = 𝐶)) ⇒ ⊢ (𝜑 → (𝐹:𝐴–1-1-onto→𝐵 ∧ ◡𝐹 = (𝑦 ∈ 𝐵 ↦ 𝐷))) | ||
| Theorem | eldmne0 32599 | A function of nonempty domain is not empty. (Contributed by Thierry Arnoux, 20-Nov-2023.) |
| ⊢ (𝑋 ∈ dom 𝐹 → 𝐹 ≠ ∅) | ||
| Theorem | f1rnen 32600 | Equinumerosity of the range of an injective function. (Contributed by Thierry Arnoux, 7-Jul-2023.) |
| ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉) → ran 𝐹 ≈ 𝐴) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |