Home | Metamath
Proof Explorer Theorem List (p. 47 of 470) | < 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-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46966) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | velsn 4601 | There is only one element in a singleton. Exercise 2 of [TakeutiZaring] p. 15. (Contributed by NM, 21-Jun-1993.) |
⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴) | ||
Theorem | elsni 4602 | There is at most one element in a singleton. (Contributed by NM, 5-Jun-1994.) |
⊢ (𝐴 ∈ {𝐵} → 𝐴 = 𝐵) | ||
Theorem | absn 4603* | Condition for a class abstraction to be a singleton. Formerly part of proof of dfiota2 6445. (Contributed by Andrew Salmon, 30-Jun-2011.) (Revised by AV, 24-Aug-2022.) |
⊢ ({𝑥 ∣ 𝜑} = {𝑌} ↔ ∀𝑥(𝜑 ↔ 𝑥 = 𝑌)) | ||
Theorem | dfpr2 4604* | Alternate definition of a pair. Definition 5.1 of [TakeutiZaring] p. 15. (Contributed by NM, 24-Apr-1994.) |
⊢ {𝐴, 𝐵} = {𝑥 ∣ (𝑥 = 𝐴 ∨ 𝑥 = 𝐵)} | ||
Theorem | dfsn2ALT 4605 | Alternate definition of singleton, based on the (alternate) definition of pair. Definition 5.1 of [TakeutiZaring] p. 15. (Contributed by AV, 12-Jun-2022.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ {𝐴} = {𝐴, 𝐴} | ||
Theorem | elprg 4606 | A member of a pair of classes is one or the other of them, and conversely as soon as it is a set. Exercise 1 of [TakeutiZaring] p. 15, generalized. (Contributed by NM, 13-Sep-1995.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶))) | ||
Theorem | elpri 4607 | If a class is an element of a pair, then it is one of the two paired elements. (Contributed by Scott Fenton, 1-Apr-2011.) |
⊢ (𝐴 ∈ {𝐵, 𝐶} → (𝐴 = 𝐵 ∨ 𝐴 = 𝐶)) | ||
Theorem | elpr 4608 | A member of a pair of classes is one or the other of them, and conversely as soon as it is a set. Exercise 1 of [TakeutiZaring] p. 15. (Contributed by NM, 13-Sep-1995.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶)) | ||
Theorem | elpr2g 4609 | A member of a pair of sets is one or the other of them, and conversely. Exercise 1 of [TakeutiZaring] p. 15. (Contributed by NM, 14-Oct-2005.) Generalize from sethood hypothesis to sethood antecedent. (Revised by BJ, 25-May-2024.) |
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶))) | ||
Theorem | elpr2 4610 | A member of a pair of sets is one or the other of them, and conversely. Exercise 1 of [TakeutiZaring] p. 15. (Contributed by NM, 14-Oct-2005.) (Proof shortened by JJ, 23-Jul-2021.) |
⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V ⇒ ⊢ (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶)) | ||
Theorem | elpr2OLD 4611 | Obsolete version of elpr2 4610 as of 25-May-2024. (Contributed by NM, 14-Oct-2005.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V ⇒ ⊢ (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶)) | ||
Theorem | nelpr2 4612 | If a class is not an element of an unordered pair, it is not the second listed element. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝐴 ∈ {𝐵, 𝐶}) ⇒ ⊢ (𝜑 → 𝐴 ≠ 𝐶) | ||
Theorem | nelpr1 4613 | If a class is not an element of an unordered pair, it is not the first listed element. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝐴 ∈ {𝐵, 𝐶}) ⇒ ⊢ (𝜑 → 𝐴 ≠ 𝐵) | ||
Theorem | nelpri 4614 | If an element doesn't match the items in an unordered pair, it is not in the unordered pair. (Contributed by David A. Wheeler, 10-May-2015.) |
⊢ 𝐴 ≠ 𝐵 & ⊢ 𝐴 ≠ 𝐶 ⇒ ⊢ ¬ 𝐴 ∈ {𝐵, 𝐶} | ||
Theorem | prneli 4615 | If an element doesn't match the items in an unordered pair, it is not in the unordered pair, using ∉. (Contributed by David A. Wheeler, 10-May-2015.) |
⊢ 𝐴 ≠ 𝐵 & ⊢ 𝐴 ≠ 𝐶 ⇒ ⊢ 𝐴 ∉ {𝐵, 𝐶} | ||
Theorem | nelprd 4616 | If an element doesn't match the items in an unordered pair, it is not in the unordered pair, deduction version. (Contributed by Alexander van der Vekens, 25-Jan-2018.) |
⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → 𝐴 ≠ 𝐶) ⇒ ⊢ (𝜑 → ¬ 𝐴 ∈ {𝐵, 𝐶}) | ||
Theorem | eldifpr 4617 | Membership in a set with two elements removed. Similar to eldifsn 4746 and eldiftp 4646. (Contributed by Mario Carneiro, 18-Jul-2017.) |
⊢ (𝐴 ∈ (𝐵 ∖ {𝐶, 𝐷}) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷)) | ||
Theorem | rexdifpr 4618 | Restricted existential quantification over a set with two elements removed. (Contributed by Alexander van der Vekens, 7-Feb-2018.) |
⊢ (∃𝑥 ∈ (𝐴 ∖ {𝐵, 𝐶})𝜑 ↔ ∃𝑥 ∈ 𝐴 (𝑥 ≠ 𝐵 ∧ 𝑥 ≠ 𝐶 ∧ 𝜑)) | ||
Theorem | snidg 4619 | A set is a member of its singleton. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by NM, 28-Oct-2003.) |
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝐴}) | ||
Theorem | snidb 4620 | A class is a set iff it is a member of its singleton. (Contributed by NM, 5-Apr-2004.) |
⊢ (𝐴 ∈ V ↔ 𝐴 ∈ {𝐴}) | ||
Theorem | snid 4621 | A set is a member of its singleton. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by NM, 31-Dec-1993.) |
⊢ 𝐴 ∈ V ⇒ ⊢ 𝐴 ∈ {𝐴} | ||
Theorem | vsnid 4622 | A setvar variable is a member of its singleton. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ 𝑥 ∈ {𝑥} | ||
Theorem | elsn2g 4623 | There is exactly one element in a singleton. Exercise 2 of [TakeutiZaring] p. 15. This variation requires only that 𝐵, rather than 𝐴, be a set. (Contributed by NM, 28-Oct-2003.) |
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵)) | ||
Theorem | elsn2 4624 | There is exactly one element in a singleton. Exercise 2 of [TakeutiZaring] p. 15. This variation requires only that 𝐵, rather than 𝐴, be a set. (Contributed by NM, 12-Jun-1994.) |
⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵) | ||
Theorem | nelsn 4625 | If a class is not equal to the class in a singleton, then it is not in the singleton. (Contributed by Glauco Siliprandi, 17-Aug-2020.) (Proof shortened by BJ, 4-May-2021.) |
⊢ (𝐴 ≠ 𝐵 → ¬ 𝐴 ∈ {𝐵}) | ||
Theorem | rabeqsn 4626* | Conditions for a restricted class abstraction to be a singleton. (Contributed by AV, 18-Apr-2019.) (Proof shortened by AV, 26-Aug-2022.) |
⊢ ({𝑥 ∈ 𝑉 ∣ 𝜑} = {𝑋} ↔ ∀𝑥((𝑥 ∈ 𝑉 ∧ 𝜑) ↔ 𝑥 = 𝑋)) | ||
Theorem | rabsssn 4627* | Conditions for a restricted class abstraction to be a subset of a singleton, i.e. to be a singleton or the empty set. (Contributed by AV, 18-Apr-2019.) |
⊢ ({𝑥 ∈ 𝑉 ∣ 𝜑} ⊆ {𝑋} ↔ ∀𝑥 ∈ 𝑉 (𝜑 → 𝑥 = 𝑋)) | ||
Theorem | ralsnsg 4628* | Substitution expressed in terms of quantification over a singleton. (Contributed by NM, 14-Dec-2005.) (Revised by Mario Carneiro, 23-Apr-2015.) |
⊢ (𝐴 ∈ 𝑉 → (∀𝑥 ∈ {𝐴}𝜑 ↔ [𝐴 / 𝑥]𝜑)) | ||
Theorem | rexsns 4629* | Restricted existential quantification over a singleton. (Contributed by Mario Carneiro, 23-Apr-2015.) (Revised by NM, 22-Aug-2018.) |
⊢ (∃𝑥 ∈ {𝐴}𝜑 ↔ [𝐴 / 𝑥]𝜑) | ||
Theorem | rexsngf 4630* | Restricted existential quantification over a singleton. (Contributed by NM, 29-Jan-2012.) (Revised by Glauco Siliprandi, 17-Aug-2020.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (∃𝑥 ∈ {𝐴}𝜑 ↔ 𝜓)) | ||
Theorem | ralsngf 4631* | Restricted universal quantification over a singleton. (Contributed by NM, 14-Dec-2005.) (Revised by AV, 3-Apr-2023.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (∀𝑥 ∈ {𝐴}𝜑 ↔ 𝜓)) | ||
Theorem | reusngf 4632* | Restricted existential uniqueness over a singleton. (Contributed by AV, 3-Apr-2023.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (∃!𝑥 ∈ {𝐴}𝜑 ↔ 𝜓)) | ||
Theorem | ralsng 4633* | Substitution expressed in terms of quantification over a singleton. (Contributed by NM, 14-Dec-2005.) (Revised by Mario Carneiro, 23-Apr-2015.) Avoid ax-10 2138, ax-12 2172. (Revised by Gino Giotto, 30-Sep-2024.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (∀𝑥 ∈ {𝐴}𝜑 ↔ 𝜓)) | ||
Theorem | rexsng 4634* | Restricted existential quantification over a singleton. (Contributed by NM, 29-Jan-2012.) Avoid ax-10 2138, ax-12 2172. (Revised by Gino Giotto, 30-Sep-2024.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (∃𝑥 ∈ {𝐴}𝜑 ↔ 𝜓)) | ||
Theorem | reusng 4635* | Restricted existential uniqueness over a singleton. (Contributed by AV, 3-Apr-2023.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (∃!𝑥 ∈ {𝐴}𝜑 ↔ 𝜓)) | ||
Theorem | 2ralsng 4636* | Substitution expressed in terms of two quantifications over singletons. (Contributed by AV, 22-Dec-2019.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∀𝑥 ∈ {𝐴}∀𝑦 ∈ {𝐵}𝜑 ↔ 𝜒)) | ||
Theorem | ralsngOLD 4637* | Obsolete version of ralsng 4633 as of 30-Sep-2024. (Contributed by NM, 14-Dec-2005.) (Revised by Mario Carneiro, 23-Apr-2015.) (Proof shortened by AV, 7-Apr-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (∀𝑥 ∈ {𝐴}𝜑 ↔ 𝜓)) | ||
Theorem | rexsngOLD 4638* | Obsolete version of rexsng 4634 as of 30-Sep-2024. (Contributed by NM, 29-Jan-2012.) (Proof shortened by AV, 7-Apr-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (∃𝑥 ∈ {𝐴}𝜑 ↔ 𝜓)) | ||
Theorem | rexreusng 4639* | Restricted existential uniqueness over a singleton is equivalent to a restricted existential quantification over a singleton. (Contributed by AV, 3-Apr-2023.) |
⊢ (𝐴 ∈ 𝑉 → (∃𝑥 ∈ {𝐴}𝜑 ↔ ∃!𝑥 ∈ {𝐴}𝜑)) | ||
Theorem | exsnrex 4640 | There is a set being the element of a singleton if and only if there is an element of the singleton. (Contributed by Alexander van der Vekens, 1-Jan-2018.) |
⊢ (∃𝑥 𝑀 = {𝑥} ↔ ∃𝑥 ∈ 𝑀 𝑀 = {𝑥}) | ||
Theorem | ralsn 4641* | Convert a universal quantification restricted to a singleton to a substitution. (Contributed by NM, 27-Apr-2009.) |
⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ {𝐴}𝜑 ↔ 𝜓) | ||
Theorem | rexsn 4642* | Convert an existential quantification restricted to a singleton to a substitution. (Contributed by Jeff Madsen, 5-Jan-2011.) |
⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ {𝐴}𝜑 ↔ 𝜓) | ||
Theorem | elpwunsn 4643 | Membership in an extension of a power class. (Contributed by NM, 26-Mar-2007.) |
⊢ (𝐴 ∈ (𝒫 (𝐵 ∪ {𝐶}) ∖ 𝒫 𝐵) → 𝐶 ∈ 𝐴) | ||
Theorem | eqoreldif 4644 | An element of a set is either equal to another element of the set or a member of the difference of the set and the singleton containing the other element. (Contributed by AV, 25-Aug-2020.) (Proof shortened by JJ, 23-Jul-2021.) |
⊢ (𝐵 ∈ 𝐶 → (𝐴 ∈ 𝐶 ↔ (𝐴 = 𝐵 ∨ 𝐴 ∈ (𝐶 ∖ {𝐵})))) | ||
Theorem | eltpg 4645 | Members of an unordered triple of classes. (Contributed by FL, 2-Feb-2014.) (Proof shortened by Mario Carneiro, 11-Feb-2015.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝐵, 𝐶, 𝐷} ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶 ∨ 𝐴 = 𝐷))) | ||
Theorem | eldiftp 4646 | Membership in a set with three elements removed. Similar to eldifsn 4746 and eldifpr 4617. (Contributed by David A. Wheeler, 22-Jul-2017.) |
⊢ (𝐴 ∈ (𝐵 ∖ {𝐶, 𝐷, 𝐸}) ↔ (𝐴 ∈ 𝐵 ∧ (𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ∧ 𝐴 ≠ 𝐸))) | ||
Theorem | eltpi 4647 | A member of an unordered triple of classes is one of them. (Contributed by Mario Carneiro, 11-Feb-2015.) |
⊢ (𝐴 ∈ {𝐵, 𝐶, 𝐷} → (𝐴 = 𝐵 ∨ 𝐴 = 𝐶 ∨ 𝐴 = 𝐷)) | ||
Theorem | eltp 4648 | A member of an unordered triple of classes is one of them. Special case of Exercise 1 of [TakeutiZaring] p. 17. (Contributed by NM, 8-Apr-1994.) (Revised by Mario Carneiro, 11-Feb-2015.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ {𝐵, 𝐶, 𝐷} ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶 ∨ 𝐴 = 𝐷)) | ||
Theorem | dftp2 4649* | Alternate definition of unordered triple of classes. Special case of Definition 5.3 of [TakeutiZaring] p. 16. (Contributed by NM, 8-Apr-1994.) |
⊢ {𝐴, 𝐵, 𝐶} = {𝑥 ∣ (𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ∨ 𝑥 = 𝐶)} | ||
Theorem | nfpr 4650 | Bound-variable hypothesis builder for unordered pairs. (Contributed by NM, 14-Nov-1995.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥{𝐴, 𝐵} | ||
Theorem | ifpr 4651 | Membership of a conditional operator in an unordered pair. (Contributed by NM, 17-Jun-2007.) |
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → if(𝜑, 𝐴, 𝐵) ∈ {𝐴, 𝐵}) | ||
Theorem | ralprgf 4652* | Convert a restricted universal quantification over a pair to a conjunction, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 17-Sep-2011.) (Revised by AV, 8-Apr-2023.) |
⊢ Ⅎ𝑥𝜓 & ⊢ Ⅎ𝑥𝜒 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∀𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (𝜓 ∧ 𝜒))) | ||
Theorem | rexprgf 4653* | Convert a restricted existential quantification over a pair to a disjunction, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 17-Sep-2011.) (Revised by AV, 2-Apr-2023.) |
⊢ Ⅎ𝑥𝜓 & ⊢ Ⅎ𝑥𝜒 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∃𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (𝜓 ∨ 𝜒))) | ||
Theorem | ralprg 4654* | Convert a restricted universal quantification over a pair to a conjunction. (Contributed by NM, 17-Sep-2011.) (Revised by Mario Carneiro, 23-Apr-2015.) Avoid ax-10 2138, ax-12 2172. (Revised by Gino Giotto, 30-Sep-2024.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∀𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (𝜓 ∧ 𝜒))) | ||
Theorem | ralprgOLD 4655* | Obsolete version of ralprg 4654 as of 30-Sep-2024. (Contributed by NM, 17-Sep-2011.) (Revised by Mario Carneiro, 23-Apr-2015.) (Proof shortened by AV, 8-Apr-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∀𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (𝜓 ∧ 𝜒))) | ||
Theorem | rexprg 4656* | Convert a restricted existential quantification over a pair to a disjunction. (Contributed by NM, 17-Sep-2011.) (Revised by Mario Carneiro, 23-Apr-2015.) Avoid ax-10 2138, ax-12 2172. (Revised by Gino Giotto, 30-Sep-2024.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∃𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (𝜓 ∨ 𝜒))) | ||
Theorem | rexprgOLD 4657* | Obsolete version of rexprg 4656 as of 30-Sep-2024. (Contributed by NM, 17-Sep-2011.) (Revised by Mario Carneiro, 23-Apr-2015.) (Proof shortened by AV, 8-Apr-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∃𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (𝜓 ∨ 𝜒))) | ||
Theorem | raltpg 4658* | Convert a restricted universal quantification over a triple to a conjunction. (Contributed by NM, 17-Sep-2011.) (Revised by Mario Carneiro, 23-Apr-2015.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = 𝐶 → (𝜑 ↔ 𝜃)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (∀𝑥 ∈ {𝐴, 𝐵, 𝐶}𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃))) | ||
Theorem | rextpg 4659* | Convert a restricted existential quantification over a triple to a disjunction. (Contributed by Mario Carneiro, 23-Apr-2015.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = 𝐶 → (𝜑 ↔ 𝜃)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (∃𝑥 ∈ {𝐴, 𝐵, 𝐶}𝜑 ↔ (𝜓 ∨ 𝜒 ∨ 𝜃))) | ||
Theorem | ralpr 4660* | Convert a restricted universal quantification over a pair to a conjunction. (Contributed by NM, 3-Jun-2007.) (Revised by Mario Carneiro, 23-Apr-2015.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒)) ⇒ ⊢ (∀𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (𝜓 ∧ 𝜒)) | ||
Theorem | rexpr 4661* | Convert a restricted existential quantification over a pair to a disjunction. (Contributed by NM, 3-Jun-2007.) (Revised by Mario Carneiro, 23-Apr-2015.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒)) ⇒ ⊢ (∃𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (𝜓 ∨ 𝜒)) | ||
Theorem | reuprg0 4662* | Convert a restricted existential uniqueness over a pair to a disjunction of conjunctions. (Contributed by AV, 2-Apr-2023.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∃!𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ ((𝜓 ∧ (𝜒 → 𝐴 = 𝐵)) ∨ (𝜒 ∧ (𝜓 → 𝐴 = 𝐵))))) | ||
Theorem | reuprg 4663* | Convert a restricted existential uniqueness over a pair to a disjunction and an implication . (Contributed by AV, 2-Apr-2023.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∃!𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ ((𝜓 ∨ 𝜒) ∧ ((𝜒 ∧ 𝜓) → 𝐴 = 𝐵)))) | ||
Theorem | reurexprg 4664* | Convert a restricted existential uniqueness over a pair to a restricted existential quantification and an implication . (Contributed by AV, 3-Apr-2023.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∃!𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (∃𝑥 ∈ {𝐴, 𝐵}𝜑 ∧ ((𝜒 ∧ 𝜓) → 𝐴 = 𝐵)))) | ||
Theorem | raltp 4665* | Convert a universal quantification over an unordered triple to a conjunction. (Contributed by NM, 13-Sep-2011.) (Revised by Mario Carneiro, 23-Apr-2015.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = 𝐶 → (𝜑 ↔ 𝜃)) ⇒ ⊢ (∀𝑥 ∈ {𝐴, 𝐵, 𝐶}𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃)) | ||
Theorem | rextp 4666* | Convert an existential quantification over an unordered triple to a disjunction. (Contributed by Mario Carneiro, 23-Apr-2015.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = 𝐶 → (𝜑 ↔ 𝜃)) ⇒ ⊢ (∃𝑥 ∈ {𝐴, 𝐵, 𝐶}𝜑 ↔ (𝜓 ∨ 𝜒 ∨ 𝜃)) | ||
Theorem | nfsn 4667 | Bound-variable hypothesis builder for singletons. (Contributed by NM, 14-Nov-1995.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥{𝐴} | ||
Theorem | csbsng 4668 | Distribute proper substitution through the singleton of a class. csbsng 4668 is derived from the virtual deduction proof csbsngVD 42908. (Contributed by Alan Sare, 10-Nov-2012.) |
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌{𝐵} = {⦋𝐴 / 𝑥⦌𝐵}) | ||
Theorem | csbprg 4669 | Distribute proper substitution through a pair of classes. (Contributed by Alexander van der Vekens, 4-Sep-2018.) |
⊢ (𝐶 ∈ 𝑉 → ⦋𝐶 / 𝑥⦌{𝐴, 𝐵} = {⦋𝐶 / 𝑥⦌𝐴, ⦋𝐶 / 𝑥⦌𝐵}) | ||
Theorem | elinsn 4670 | If the intersection of two classes is a (proper) singleton, then the singleton element is a member of both classes. (Contributed by AV, 30-Dec-2021.) |
⊢ ((𝐴 ∈ 𝑉 ∧ (𝐵 ∩ 𝐶) = {𝐴}) → (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)) | ||
Theorem | disjsn 4671 | Intersection with the singleton of a non-member is disjoint. (Contributed by NM, 22-May-1998.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) (Proof shortened by Wolf Lammen, 30-Sep-2014.) |
⊢ ((𝐴 ∩ {𝐵}) = ∅ ↔ ¬ 𝐵 ∈ 𝐴) | ||
Theorem | disjsn2 4672 | Two distinct singletons are disjoint. (Contributed by NM, 25-May-1998.) |
⊢ (𝐴 ≠ 𝐵 → ({𝐴} ∩ {𝐵}) = ∅) | ||
Theorem | disjpr2 4673 | Two completely distinct unordered pairs are disjoint. (Contributed by Alexander van der Vekens, 11-Nov-2017.) (Proof shortened by JJ, 23-Jul-2021.) |
⊢ (((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) ∧ (𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷)) → ({𝐴, 𝐵} ∩ {𝐶, 𝐷}) = ∅) | ||
Theorem | disjprsn 4674 | The disjoint intersection of an unordered pair and a singleton. (Contributed by AV, 23-Jan-2021.) |
⊢ ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({𝐴, 𝐵} ∩ {𝐶}) = ∅) | ||
Theorem | disjtpsn 4675 | The disjoint intersection of an unordered triple and a singleton. (Contributed by AV, 14-Nov-2021.) |
⊢ ((𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷) → ({𝐴, 𝐵, 𝐶} ∩ {𝐷}) = ∅) | ||
Theorem | disjtp2 4676 | Two completely distinct unordered triples are disjoint. (Contributed by AV, 14-Nov-2021.) |
⊢ (((𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷) ∧ (𝐴 ≠ 𝐸 ∧ 𝐵 ≠ 𝐸 ∧ 𝐶 ≠ 𝐸) ∧ (𝐴 ≠ 𝐹 ∧ 𝐵 ≠ 𝐹 ∧ 𝐶 ≠ 𝐹)) → ({𝐴, 𝐵, 𝐶} ∩ {𝐷, 𝐸, 𝐹}) = ∅) | ||
Theorem | snprc 4677 | The singleton of a proper class (one that doesn't exist) is the empty set. Theorem 7.2 of [Quine] p. 48. (Contributed by NM, 21-Jun-1993.) |
⊢ (¬ 𝐴 ∈ V ↔ {𝐴} = ∅) | ||
Theorem | snnzb 4678 | A singleton is nonempty iff its argument is a set. (Contributed by Scott Fenton, 8-May-2018.) |
⊢ (𝐴 ∈ V ↔ {𝐴} ≠ ∅) | ||
Theorem | rmosn 4679* | A restricted at-most-one quantifier over a singleton is always true. (Contributed by AV, 3-Apr-2023.) |
⊢ ∃*𝑥 ∈ {𝐴}𝜑 | ||
Theorem | r19.12sn 4680* | Special case of r19.12 3296 where its converse holds. (Contributed by NM, 19-May-2008.) (Revised by Mario Carneiro, 23-Apr-2015.) (Revised by BJ, 18-Mar-2020.) |
⊢ (𝐴 ∈ 𝑉 → (∃𝑥 ∈ {𝐴}∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ {𝐴}𝜑)) | ||
Theorem | rabsn 4681* | Condition where a restricted class abstraction is a singleton. (Contributed by NM, 28-May-2006.) (Proof shortened by AV, 26-Aug-2022.) |
⊢ (𝐵 ∈ 𝐴 → {𝑥 ∈ 𝐴 ∣ 𝑥 = 𝐵} = {𝐵}) | ||
Theorem | rabsnifsb 4682* | A restricted class abstraction restricted to a singleton is either the empty set or the singleton itself. (Contributed by AV, 21-Jul-2019.) |
⊢ {𝑥 ∈ {𝐴} ∣ 𝜑} = if([𝐴 / 𝑥]𝜑, {𝐴}, ∅) | ||
Theorem | rabsnif 4683* | A restricted class abstraction restricted to a singleton is either the empty set or the singleton itself. (Contributed by AV, 12-Apr-2019.) (Proof shortened by AV, 21-Jul-2019.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {𝑥 ∈ {𝐴} ∣ 𝜑} = if(𝜓, {𝐴}, ∅) | ||
Theorem | rabrsn 4684* | A restricted class abstraction restricted to a singleton is either the empty set or the singleton itself. (Contributed by Alexander van der Vekens, 22-Dec-2017.) (Proof shortened by AV, 21-Jul-2019.) |
⊢ (𝑀 = {𝑥 ∈ {𝐴} ∣ 𝜑} → (𝑀 = ∅ ∨ 𝑀 = {𝐴})) | ||
Theorem | euabsn2 4685* | Another way to express existential uniqueness of a wff: its class abstraction is a singleton. (Contributed by Mario Carneiro, 14-Nov-2016.) |
⊢ (∃!𝑥𝜑 ↔ ∃𝑦{𝑥 ∣ 𝜑} = {𝑦}) | ||
Theorem | euabsn 4686 | Another way to express existential uniqueness of a wff: its class abstraction is a singleton. (Contributed by NM, 22-Feb-2004.) |
⊢ (∃!𝑥𝜑 ↔ ∃𝑥{𝑥 ∣ 𝜑} = {𝑥}) | ||
Theorem | reusn 4687* | A way to express restricted existential uniqueness of a wff: its restricted class abstraction is a singleton. (Contributed by NM, 30-May-2006.) (Proof shortened by Mario Carneiro, 14-Nov-2016.) |
⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦{𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦}) | ||
Theorem | absneu 4688 | Restricted existential uniqueness determined by a singleton. (Contributed by NM, 29-May-2006.) |
⊢ ((𝐴 ∈ 𝑉 ∧ {𝑥 ∣ 𝜑} = {𝐴}) → ∃!𝑥𝜑) | ||
Theorem | rabsneu 4689 | Restricted existential uniqueness determined by a singleton. (Contributed by NM, 29-May-2006.) (Revised by Mario Carneiro, 23-Dec-2016.) |
⊢ ((𝐴 ∈ 𝑉 ∧ {𝑥 ∈ 𝐵 ∣ 𝜑} = {𝐴}) → ∃!𝑥 ∈ 𝐵 𝜑) | ||
Theorem | eusn 4690* | Two ways to express "𝐴 is a singleton". (Contributed by NM, 30-Oct-2010.) |
⊢ (∃!𝑥 𝑥 ∈ 𝐴 ↔ ∃𝑥 𝐴 = {𝑥}) | ||
Theorem | rabsnt 4691* | Truth implied by equality of a restricted class abstraction and a singleton. (Contributed by NM, 29-May-2006.) (Proof shortened by Mario Carneiro, 23-Dec-2016.) |
⊢ 𝐵 ∈ V & ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = {𝐵} → 𝜓) | ||
Theorem | prcom 4692 | Commutative law for unordered pairs. (Contributed by NM, 15-Jul-1993.) |
⊢ {𝐴, 𝐵} = {𝐵, 𝐴} | ||
Theorem | preq1 4693 | Equality theorem for unordered pairs. (Contributed by NM, 29-Mar-1998.) |
⊢ (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶}) | ||
Theorem | preq2 4694 | Equality theorem for unordered pairs. (Contributed by NM, 15-Jul-1993.) |
⊢ (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵}) | ||
Theorem | preq12 4695 | Equality theorem for unordered pairs. (Contributed by NM, 19-Oct-2012.) |
⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → {𝐴, 𝐵} = {𝐶, 𝐷}) | ||
Theorem | preq1i 4696 | Equality inference for unordered pairs. (Contributed by NM, 19-Oct-2012.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ {𝐴, 𝐶} = {𝐵, 𝐶} | ||
Theorem | preq2i 4697 | Equality inference for unordered pairs. (Contributed by NM, 19-Oct-2012.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ {𝐶, 𝐴} = {𝐶, 𝐵} | ||
Theorem | preq12i 4698 | Equality inference for unordered pairs. (Contributed by NM, 19-Oct-2012.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐶 = 𝐷 ⇒ ⊢ {𝐴, 𝐶} = {𝐵, 𝐷} | ||
Theorem | preq1d 4699 | Equality deduction for unordered pairs. (Contributed by NM, 19-Oct-2012.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → {𝐴, 𝐶} = {𝐵, 𝐶}) | ||
Theorem | preq2d 4700 | Equality deduction for unordered pairs. (Contributed by NM, 19-Oct-2012.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → {𝐶, 𝐴} = {𝐶, 𝐵}) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |