| Metamath
Proof Explorer Theorem List (p. 47 of 494) | < Previous Next > | |
| Bad symbols? Try the
GIF version. |
||
|
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
||
| Color key: | (1-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | pwjust 4601* | Soundness justification theorem for df-pw 4602. (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
| ⊢ {𝑥 ∣ 𝑥 ⊆ 𝐴} = {𝑦 ∣ 𝑦 ⊆ 𝐴} | ||
| Definition | df-pw 4602* | Define power class. Definition 5.10 of [TakeutiZaring] p. 17, but we also let it apply to proper classes, i.e. those that are not members of V. When applied to a set, this produces its power set. A power set of S is the set of all subsets of S, including the empty set and S itself. For example, if 𝐴 = {3, 5, 7}, then 𝒫 𝐴 = {∅, {3}, {5}, {7}, {3, 5}, {3, 7}, {5, 7}, {3, 5, 7}} (ex-pw 30448). We will later introduce the Axiom of Power Sets ax-pow 5365, which can be expressed in class notation per pwexg 5378. Still later we will prove, in hashpw 14475, that the size of the power set of a finite set is 2 raised to the power of the size of the set. (Contributed by NM, 24-Jun-1993.) |
| ⊢ 𝒫 𝐴 = {𝑥 ∣ 𝑥 ⊆ 𝐴} | ||
| Theorem | elpwg 4603 | Membership in a power class. Theorem 86 of [Suppes] p. 47. See also elpw2g 5333. (Contributed by NM, 6-Aug-2000.) (Proof shortened by BJ, 31-Dec-2023.) |
| ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵)) | ||
| Theorem | elpw 4604 | Membership in a power class. Theorem 86 of [Suppes] p. 47. (Contributed by NM, 31-Dec-1993.) (Proof shortened by BJ, 31-Dec-2023.) |
| ⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵) | ||
| Theorem | velpw 4605 | Setvar variable membership in a power class. (Contributed by David A. Wheeler, 8-Dec-2018.) |
| ⊢ (𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴) | ||
| Theorem | elpwd 4606 | Membership in a power class. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝒫 𝐵) | ||
| Theorem | elpwi 4607 | Subset relation implied by membership in a power class. (Contributed by NM, 17-Feb-2007.) |
| ⊢ (𝐴 ∈ 𝒫 𝐵 → 𝐴 ⊆ 𝐵) | ||
| Theorem | elpwb 4608 | Characterization of the elements of a power class. (Contributed by BJ, 29-Apr-2021.) |
| ⊢ (𝐴 ∈ 𝒫 𝐵 ↔ (𝐴 ∈ V ∧ 𝐴 ⊆ 𝐵)) | ||
| Theorem | elpwid 4609 | An element of a power class is a subclass. Deduction form of elpwi 4607. (Contributed by David Moews, 1-May-2017.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝒫 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐵) | ||
| Theorem | elelpwi 4610 | If 𝐴 belongs to a part of 𝐶, then 𝐴 belongs to 𝐶. (Contributed by FL, 3-Aug-2009.) |
| ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝒫 𝐶) → 𝐴 ∈ 𝐶) | ||
| Theorem | sspw 4611 | The powerclass preserves inclusion. See sspwb 5454 for the biconditional version. (Contributed by NM, 13-Oct-1996.) Extract forward implication of sspwb 5454 since it requires fewer axioms. (Revised by BJ, 13-Apr-2024.) |
| ⊢ (𝐴 ⊆ 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵) | ||
| Theorem | sspwi 4612 | The powerclass preserves inclusion (inference form). (Contributed by BJ, 13-Apr-2024.) |
| ⊢ 𝐴 ⊆ 𝐵 ⇒ ⊢ 𝒫 𝐴 ⊆ 𝒫 𝐵 | ||
| Theorem | sspwd 4613 | The powerclass preserves inclusion (deduction form). (Contributed by BJ, 13-Apr-2024.) |
| ⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → 𝒫 𝐴 ⊆ 𝒫 𝐵) | ||
| Theorem | pweq 4614 | Equality theorem for power class. (Contributed by NM, 21-Jun-1993.) (Proof shortened by BJ, 13-Apr-2024.) |
| ⊢ (𝐴 = 𝐵 → 𝒫 𝐴 = 𝒫 𝐵) | ||
| Theorem | pweqALT 4615 | Alternate proof of pweq 4614 directly from the definition. (Contributed by NM, 21-Jun-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝐴 = 𝐵 → 𝒫 𝐴 = 𝒫 𝐵) | ||
| Theorem | pweqi 4616 | Equality inference for power class. (Contributed by NM, 27-Nov-2013.) |
| ⊢ 𝐴 = 𝐵 ⇒ ⊢ 𝒫 𝐴 = 𝒫 𝐵 | ||
| Theorem | pweqd 4617 | Equality deduction for power class. (Contributed by NM, 27-Nov-2013.) |
| ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → 𝒫 𝐴 = 𝒫 𝐵) | ||
| Theorem | pwunss 4618 | The power class of the union of two classes includes the union of their power classes. Exercise 4.12(k) of [Mendelson] p. 235. (Contributed by NM, 23-Nov-2003.) Remove use of ax-sep 5296, ax-nul 5306, ax-pr 5432 and shorten proof. (Revised by BJ, 13-Apr-2024.) |
| ⊢ (𝒫 𝐴 ∪ 𝒫 𝐵) ⊆ 𝒫 (𝐴 ∪ 𝐵) | ||
| Theorem | nfpw 4619 | Bound-variable hypothesis builder for power class. (Contributed by NM, 28-Oct-2003.) (Revised by Mario Carneiro, 13-Oct-2016.) |
| ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥𝒫 𝐴 | ||
| Theorem | pwidg 4620 | A set is an element of its power set. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
| ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ 𝒫 𝐴) | ||
| Theorem | pwidb 4621 | A class is an element of its powerclass if and only if it is a set. (Contributed by BJ, 31-Dec-2023.) |
| ⊢ (𝐴 ∈ V ↔ 𝐴 ∈ 𝒫 𝐴) | ||
| Theorem | pwid 4622 | A set is a member of its power class. Theorem 87 of [Suppes] p. 47. (Contributed by NM, 5-Aug-1993.) |
| ⊢ 𝐴 ∈ V ⇒ ⊢ 𝐴 ∈ 𝒫 𝐴 | ||
| Theorem | pwss 4623* | Subclass relationship for power class. (Contributed by NM, 21-Jun-2009.) |
| ⊢ (𝒫 𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐵)) | ||
| Theorem | pwundif 4624 | Break up the power class of a union into a union of smaller classes. (Contributed by NM, 25-Mar-2007.) (Proof shortened by Thierry Arnoux, 20-Dec-2016.) Remove use of ax-sep 5296, ax-nul 5306, ax-pr 5432 and shorten proof. (Revised by BJ, 14-Apr-2024.) |
| ⊢ 𝒫 (𝐴 ∪ 𝐵) = ((𝒫 (𝐴 ∪ 𝐵) ∖ 𝒫 𝐴) ∪ 𝒫 𝐴) | ||
| Theorem | snjust 4625* | Soundness justification theorem for df-sn 4627. (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
| ⊢ {𝑥 ∣ 𝑥 = 𝐴} = {𝑦 ∣ 𝑦 = 𝐴} | ||
| Syntax | csn 4626 | Extend class notation to include singleton. |
| class {𝐴} | ||
| Definition | df-sn 4627* | Define the singleton of a class. Definition 7.1 of [Quine] p. 48. For convenience, it is well-defined for proper classes, i.e., those that are not elements of V, see snprc 4717. For an alternate definition see dfsn2 4639. (Contributed by NM, 21-Jun-1993.) |
| ⊢ {𝐴} = {𝑥 ∣ 𝑥 = 𝐴} | ||
| Syntax | cpr 4628 | Extend class notation to include unordered pair. |
| class {𝐴, 𝐵} | ||
| Definition | df-pr 4629 |
Define unordered pair of classes. Definition 7.1 of [Quine] p. 48. For
example, 𝐴 ∈ {1, -1} → (𝐴↑2) = 1 (ex-pr 30449). They are
unordered, so {𝐴, 𝐵} = {𝐵, 𝐴} as proven by prcom 4732. For a more
traditional definition, but requiring a dummy variable, see dfpr2 4646.
{𝐴,
𝐴} is also an
unordered pair, but also a singleton because of
{𝐴} =
{𝐴, 𝐴} (see dfsn2 4639). Therefore, {𝐴, 𝐵} is called
a proper (unordered) pair iff 𝐴 ≠ 𝐵 and 𝐴 and 𝐵 are
sets.
Note: ordered pairs are a completely different object defined below in df-op 4633. When the term "pair" is used without qualifier, it generally means "unordered pair", and the context makes it clear which version is meant. (Contributed by NM, 21-Jun-1993.) |
| ⊢ {𝐴, 𝐵} = ({𝐴} ∪ {𝐵}) | ||
| Syntax | ctp 4630 | Extend class notation to include unordered triple (sometimes called "unordered triplet"). |
| class {𝐴, 𝐵, 𝐶} | ||
| Definition | df-tp 4631 |
Define unordered triple of classes. Definition of [Enderton] p. 19.
Note: ordered triples are a completely different object defined below in df-ot 4635. As with all tuples, when the term "triple" is used without qualifier, it means "ordered triple". (Contributed by NM, 9-Apr-1994.) |
| ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶}) | ||
| Syntax | cop 4632 | Extend class notation to include ordered pair. |
| class 〈𝐴, 𝐵〉 | ||
| Definition | df-op 4633* |
Definition of an ordered pair, equivalent to Kuratowski's definition
{{𝐴}, {𝐴, 𝐵}} when the arguments are sets.
Since the
behavior of Kuratowski definition is not very useful for proper classes,
we define it to be empty in this case (see opprc1 4897, opprc2 4898, and
0nelop 5501). For Kuratowski's actual definition when
the arguments are
sets, see dfop 4872. For the justifying theorem (for sets) see
opth 5481.
See dfopif 4870 for an equivalent formulation using the if operation.
Definition 9.1 of [Quine] p. 58 defines an ordered pair unconditionally as 〈𝐴, 𝐵〉 = {{𝐴}, {𝐴, 𝐵}}, which has different behavior from our df-op 4633 when the arguments are proper classes. Ordinarily this difference is not important, since neither definition is meaningful in that case. Our df-op 4633 was chosen because it often makes proofs shorter by eliminating unnecessary sethood hypotheses. There are other ways to define ordered pairs. The basic requirement is that two ordered pairs are equal iff their respective members are equal. In 1914 Norbert Wiener gave the first successful definition 〈𝐴, 𝐵〉2 = {{{𝐴}, ∅}, {{𝐵}}}, justified by opthwiener 5519. This was simplified by Kazimierz Kuratowski in 1921 to our present definition. An even simpler definition 〈𝐴, 𝐵〉3 = {𝐴, {𝐴, 𝐵}} is justified by opthreg 9658, but it requires the Axiom of Regularity for its justification and is not commonly used. A definition that also works for proper classes is 〈𝐴, 𝐵〉4 = ((𝐴 × {∅}) ∪ (𝐵 × {{∅}})), justified by opthprc 5749. Nearly at the same time as Norbert Wiener, Felix Hausdorff proposed the following definition in "Grundzüge der Mengenlehre" ("Basics of Set Theory"), p. 32, in 1914: 〈𝐴, 𝐵〉5 = {{𝐴, 𝑂}, {𝐵, 𝑇}}. Hausdorff used 1 and 2 instead of 𝑂 and 𝑇, but actually any two different fixed sets will do (e.g., 𝑂 = ∅ and 𝑇 = {∅}, see 0nep0 5358). Furthermore, Hausdorff demanded that 𝑂 and 𝑇 are both different from 𝐴 as well as 𝐵, which is actually not necessary (at least not in full extent), see opthhausdorff0 5523 and opthhausdorff 5522. If we restrict our sets to nonnegative integers, an ordered pair definition that involves only elementary arithmetic is provided by nn0opthi 14309. An ordered pair of real numbers can also be represented by a complex number as shown by cru 12258. Kuratowski's ordered pair definition is standard for ZFC set theory, but it is very inconvenient to use in New Foundations theory because it is not type-level; a common alternate definition in New Foundations is the definition from [Rosser] p. 281. Since there are other ways to define ordered pairs, we discourage direct use of this definition so that most theorems won't depend on this particular construction; theorems will instead rely on dfopif 4870. (Contributed by NM, 28-May-1995.) (Revised by Mario Carneiro, 26-Apr-2015.) (Avoid depending on this detail.) |
| ⊢ 〈𝐴, 𝐵〉 = {𝑥 ∣ (𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐵}})} | ||
| Syntax | cotp 4634 | Extend class notation to include ordered triple. |
| class 〈𝐴, 𝐵, 𝐶〉 | ||
| Definition | df-ot 4635 | Define ordered triple of classes. Definition of ordered triple in [Stoll] p. 25. (Contributed by NM, 3-Apr-2015.) |
| ⊢ 〈𝐴, 𝐵, 𝐶〉 = 〈〈𝐴, 𝐵〉, 𝐶〉 | ||
| Theorem | sneq 4636 | Equality theorem for singletons. Part of Exercise 4 of [TakeutiZaring] p. 15. (Contributed by NM, 21-Jun-1993.) |
| ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵}) | ||
| Theorem | sneqi 4637 | Equality inference for singletons. (Contributed by NM, 22-Jan-2004.) |
| ⊢ 𝐴 = 𝐵 ⇒ ⊢ {𝐴} = {𝐵} | ||
| Theorem | sneqd 4638 | Equality deduction for singletons. (Contributed by NM, 22-Jan-2004.) |
| ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → {𝐴} = {𝐵}) | ||
| Theorem | dfsn2 4639 | Alternate definition of singleton. Definition 5.1 of [TakeutiZaring] p. 15. (Contributed by NM, 24-Apr-1994.) |
| ⊢ {𝐴} = {𝐴, 𝐴} | ||
| Theorem | elsng 4640 | There is exactly one element in a singleton. Exercise 2 of [TakeutiZaring] p. 15 (generalized). (Contributed by NM, 13-Sep-1995.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
| ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵)) | ||
| Theorem | elsn 4641 | There is exactly one element in a singleton. Exercise 2 of [TakeutiZaring] p. 15. (Contributed by NM, 13-Sep-1995.) |
| ⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵) | ||
| Theorem | velsn 4642 | There is only one element in a singleton. Exercise 2 of [TakeutiZaring] p. 15. (Contributed by NM, 21-Jun-1993.) |
| ⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴) | ||
| Theorem | elsni 4643 | There is at most one element in a singleton. (Contributed by NM, 5-Jun-1994.) |
| ⊢ (𝐴 ∈ {𝐵} → 𝐴 = 𝐵) | ||
| Theorem | rabsneq 4644* | Equality of class abstractions restricted to a singleton. (Contributed by AV, 17-May-2025.) |
| ⊢ (𝑁 ∈ 𝑉 → {𝑥 ∈ {𝑁} ∣ 𝜓} = {𝑥 ∈ 𝑉 ∣ (𝑥 = 𝑁 ∧ 𝜓)}) | ||
| Theorem | absn 4645* | Condition for a class abstraction to be a singleton. Formerly part of proof of dfiota2 6515. (Contributed by Andrew Salmon, 30-Jun-2011.) (Revised by AV, 24-Aug-2022.) |
| ⊢ ({𝑥 ∣ 𝜑} = {𝑌} ↔ ∀𝑥(𝜑 ↔ 𝑥 = 𝑌)) | ||
| Theorem | dfpr2 4646* | Alternate definition of a pair. Definition 5.1 of [TakeutiZaring] p. 15. (Contributed by NM, 24-Apr-1994.) |
| ⊢ {𝐴, 𝐵} = {𝑥 ∣ (𝑥 = 𝐴 ∨ 𝑥 = 𝐵)} | ||
| Theorem | dfsn2ALT 4647 | 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 4648 | 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 4649 | 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 4650 | 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 4651 | 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 4652 | 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 | nelpr2 4653 | 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 4654 | 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 4655 | 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 4656 | 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 4657 | 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 4658 | Membership in a set with two elements removed. Similar to eldifsn 4786 and eldiftp 4687. (Contributed by Mario Carneiro, 18-Jul-2017.) |
| ⊢ (𝐴 ∈ (𝐵 ∖ {𝐶, 𝐷}) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷)) | ||
| Theorem | rexdifpr 4659 | Restricted existential quantification over a set with two elements removed. (Contributed by Alexander van der Vekens, 7-Feb-2018.) (Proof shortened by Wolf Lammen, 15-May-2025.) |
| ⊢ (∃𝑥 ∈ (𝐴 ∖ {𝐵, 𝐶})𝜑 ↔ ∃𝑥 ∈ 𝐴 (𝑥 ≠ 𝐵 ∧ 𝑥 ≠ 𝐶 ∧ 𝜑)) | ||
| Theorem | snidg 4660 | 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 4661 | A class is a set iff it is a member of its singleton. (Contributed by NM, 5-Apr-2004.) |
| ⊢ (𝐴 ∈ V ↔ 𝐴 ∈ {𝐴}) | ||
| Theorem | snid 4662 | 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 4663 | A setvar variable is a member of its singleton. (Contributed by David A. Wheeler, 8-Dec-2018.) |
| ⊢ 𝑥 ∈ {𝑥} | ||
| Theorem | elsn2g 4664 | 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 4665 | 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 4666 | 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 4667* | 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 4668* | 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 | rabeqsnd 4669* | Conditions for a restricted class abstraction to be a singleton, in deduction form. (Contributed by Thierry Arnoux, 2-Dec-2021.) |
| ⊢ (𝑥 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → 𝐵 ∈ 𝐴) & ⊢ (𝜑 → 𝜒) & ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓) → 𝑥 = 𝐵) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝐵}) | ||
| Theorem | ralsnsg 4670* | Substitution expressed in terms of quantification over a singleton. (Contributed by NM, 14-Dec-2005.) (Revised by Mario Carneiro, 23-Apr-2015.) |
| ⊢ (𝐴 ∈ 𝑉 → (∀𝑥 ∈ {𝐴}𝜑 ↔ [𝐴 / 𝑥]𝜑)) | ||
| Theorem | rexsns 4671* | Restricted existential quantification over a singleton. (Contributed by Mario Carneiro, 23-Apr-2015.) (Revised by NM, 22-Aug-2018.) |
| ⊢ (∃𝑥 ∈ {𝐴}𝜑 ↔ [𝐴 / 𝑥]𝜑) | ||
| Theorem | rexsngf 4672* | Restricted existential quantification over a singleton. (Contributed by NM, 29-Jan-2012.) (Revised by Glauco Siliprandi, 17-Aug-2020.) |
| ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (∃𝑥 ∈ {𝐴}𝜑 ↔ 𝜓)) | ||
| Theorem | ralsngf 4673* | Restricted universal quantification over a singleton. (Contributed by NM, 14-Dec-2005.) (Revised by AV, 3-Apr-2023.) |
| ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (∀𝑥 ∈ {𝐴}𝜑 ↔ 𝜓)) | ||
| Theorem | reusngf 4674* | Restricted existential uniqueness over a singleton. (Contributed by AV, 3-Apr-2023.) |
| ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (∃!𝑥 ∈ {𝐴}𝜑 ↔ 𝜓)) | ||
| Theorem | ralsng 4675* | 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 2141, ax-12 2177. (Revised by GG, 30-Sep-2024.) |
| ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (∀𝑥 ∈ {𝐴}𝜑 ↔ 𝜓)) | ||
| Theorem | rexsng 4676* | Restricted existential quantification over a singleton. (Contributed by NM, 29-Jan-2012.) Avoid ax-10 2141, ax-12 2177. (Revised by GG, 30-Sep-2024.) |
| ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (∃𝑥 ∈ {𝐴}𝜑 ↔ 𝜓)) | ||
| Theorem | reusng 4677* | Restricted existential uniqueness over a singleton. (Contributed by AV, 3-Apr-2023.) |
| ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (∃!𝑥 ∈ {𝐴}𝜑 ↔ 𝜓)) | ||
| Theorem | 2ralsng 4678* | Substitution expressed in terms of two quantifications over singletons. (Contributed by AV, 22-Dec-2019.) |
| ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∀𝑥 ∈ {𝐴}∀𝑦 ∈ {𝐵}𝜑 ↔ 𝜒)) | ||
| Theorem | rexreusng 4679* | Restricted existential uniqueness over a singleton is equivalent to a restricted existential quantification over a singleton. (Contributed by AV, 3-Apr-2023.) |
| ⊢ (𝐴 ∈ 𝑉 → (∃𝑥 ∈ {𝐴}𝜑 ↔ ∃!𝑥 ∈ {𝐴}𝜑)) | ||
| Theorem | exsnrex 4680 | 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 4681* | Convert a universal quantification restricted to a singleton to a substitution. (Contributed by NM, 27-Apr-2009.) |
| ⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ {𝐴}𝜑 ↔ 𝜓) | ||
| Theorem | rexsn 4682* | Convert an existential quantification restricted to a singleton to a substitution. (Contributed by Jeff Madsen, 5-Jan-2011.) |
| ⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ {𝐴}𝜑 ↔ 𝜓) | ||
| Theorem | elunsn 4683 | Elementhood in a union with a singleton. (Contributed by Thierry Arnoux, 14-Dec-2023.) |
| ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ (𝐵 ∪ {𝐶}) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐶))) | ||
| Theorem | elpwunsn 4684 | Membership in an extension of a power class. (Contributed by NM, 26-Mar-2007.) |
| ⊢ (𝐴 ∈ (𝒫 (𝐵 ∪ {𝐶}) ∖ 𝒫 𝐵) → 𝐶 ∈ 𝐴) | ||
| Theorem | eqoreldif 4685 | 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 4686 | Members of an unordered triple of classes. (Contributed by FL, 2-Feb-2014.) (Proof shortened by Mario Carneiro, 11-Feb-2015.) |
| ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝐵, 𝐶, 𝐷} ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶 ∨ 𝐴 = 𝐷))) | ||
| Theorem | eldiftp 4687 | Membership in a set with three elements removed. Similar to eldifsn 4786 and eldifpr 4658. (Contributed by David A. Wheeler, 22-Jul-2017.) |
| ⊢ (𝐴 ∈ (𝐵 ∖ {𝐶, 𝐷, 𝐸}) ↔ (𝐴 ∈ 𝐵 ∧ (𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ∧ 𝐴 ≠ 𝐸))) | ||
| Theorem | eltpi 4688 | A member of an unordered triple of classes is one of them. (Contributed by Mario Carneiro, 11-Feb-2015.) |
| ⊢ (𝐴 ∈ {𝐵, 𝐶, 𝐷} → (𝐴 = 𝐵 ∨ 𝐴 = 𝐶 ∨ 𝐴 = 𝐷)) | ||
| Theorem | eltp 4689 | 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 | el7g 4690 | Members of a set with seven elements. Lemma for usgrexmpl2nb0 47990 etc. (Contributed by AV, 9-Aug-2025.) |
| ⊢ (𝑋 ∈ 𝑉 → (𝑋 ∈ ({𝐴} ∪ ({𝐵, 𝐶, 𝐷} ∪ {𝐸, 𝐹, 𝐺})) ↔ (𝑋 = 𝐴 ∨ ((𝑋 = 𝐵 ∨ 𝑋 = 𝐶 ∨ 𝑋 = 𝐷) ∨ (𝑋 = 𝐸 ∨ 𝑋 = 𝐹 ∨ 𝑋 = 𝐺))))) | ||
| Theorem | dftp2 4691* | 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 4692 | Bound-variable hypothesis builder for unordered pairs. (Contributed by NM, 14-Nov-1995.) |
| ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥{𝐴, 𝐵} | ||
| Theorem | ifpr 4693 | Membership of a conditional operator in an unordered pair. (Contributed by NM, 17-Jun-2007.) |
| ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → if(𝜑, 𝐴, 𝐵) ∈ {𝐴, 𝐵}) | ||
| Theorem | ralprgf 4694* | 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 4695* | 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 4696* | 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 2141, ax-12 2177. (Revised by GG, 30-Sep-2024.) |
| ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∀𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (𝜓 ∧ 𝜒))) | ||
| Theorem | rexprg 4697* | 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 2141, ax-12 2177. (Revised by GG, 30-Sep-2024.) |
| ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∃𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (𝜓 ∨ 𝜒))) | ||
| Theorem | raltpg 4698* | 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 4699* | Convert a restricted existential quantification over a triple to a disjunction. (Contributed by Mario Carneiro, 23-Apr-2015.) |
| ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = 𝐶 → (𝜑 ↔ 𝜃)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (∃𝑥 ∈ {𝐴, 𝐵, 𝐶}𝜑 ↔ (𝜓 ∨ 𝜒 ∨ 𝜃))) | ||
| Theorem | ralpr 4700* | 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 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒)) ⇒ ⊢ (∀𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (𝜓 ∧ 𝜒)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |