![]() |
Metamath
Proof Explorer Theorem List (p. 47 of 484) | < 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-30767) |
![]() (30768-32290) |
![]() (32291-48346) |
Type | Label | Description |
---|---|---|
Statement | ||
Definition | df-pw 4601* | 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 30278). We will later introduce the Axiom of Power Sets ax-pow 5360, which can be expressed in class notation per pwexg 5373. Still later we will prove, in hashpw 14422, 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 4602 | Membership in a power class. Theorem 86 of [Suppes] p. 47. See also elpw2g 5342. (Contributed by NM, 6-Aug-2000.) (Proof shortened by BJ, 31-Dec-2023.) |
β’ (π΄ β π β (π΄ β π« π΅ β π΄ β π΅)) | ||
Theorem | elpw 4603 | 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 4604 | Setvar variable membership in a power class. (Contributed by David A. Wheeler, 8-Dec-2018.) |
β’ (π₯ β π« π΄ β π₯ β π΄) | ||
Theorem | elpwd 4605 | Membership in a power class. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ (π β π΄ β π) & β’ (π β π΄ β π΅) β β’ (π β π΄ β π« π΅) | ||
Theorem | elpwi 4606 | Subset relation implied by membership in a power class. (Contributed by NM, 17-Feb-2007.) |
β’ (π΄ β π« π΅ β π΄ β π΅) | ||
Theorem | elpwb 4607 | Characterization of the elements of a power class. (Contributed by BJ, 29-Apr-2021.) |
β’ (π΄ β π« π΅ β (π΄ β V β§ π΄ β π΅)) | ||
Theorem | elpwid 4608 | An element of a power class is a subclass. Deduction form of elpwi 4606. (Contributed by David Moews, 1-May-2017.) |
β’ (π β π΄ β π« π΅) β β’ (π β π΄ β π΅) | ||
Theorem | elelpwi 4609 | If π΄ belongs to a part of πΆ, then π΄ belongs to πΆ. (Contributed by FL, 3-Aug-2009.) |
β’ ((π΄ β π΅ β§ π΅ β π« πΆ) β π΄ β πΆ) | ||
Theorem | sspw 4610 | The powerclass preserves inclusion. See sspwb 5446 for the biconditional version. (Contributed by NM, 13-Oct-1996.) Extract forward implication of sspwb 5446 since it requires fewer axioms. (Revised by BJ, 13-Apr-2024.) |
β’ (π΄ β π΅ β π« π΄ β π« π΅) | ||
Theorem | sspwi 4611 | The powerclass preserves inclusion (inference form). (Contributed by BJ, 13-Apr-2024.) |
β’ π΄ β π΅ β β’ π« π΄ β π« π΅ | ||
Theorem | sspwd 4612 | The powerclass preserves inclusion (deduction form). (Contributed by BJ, 13-Apr-2024.) |
β’ (π β π΄ β π΅) β β’ (π β π« π΄ β π« π΅) | ||
Theorem | pweq 4613 | Equality theorem for power class. (Contributed by NM, 21-Jun-1993.) (Proof shortened by BJ, 13-Apr-2024.) |
β’ (π΄ = π΅ β π« π΄ = π« π΅) | ||
Theorem | pweqALT 4614 | Alternate proof of pweq 4613 directly from the definition. (Contributed by NM, 21-Jun-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (π΄ = π΅ β π« π΄ = π« π΅) | ||
Theorem | pweqi 4615 | Equality inference for power class. (Contributed by NM, 27-Nov-2013.) |
β’ π΄ = π΅ β β’ π« π΄ = π« π΅ | ||
Theorem | pweqd 4616 | Equality deduction for power class. (Contributed by NM, 27-Nov-2013.) |
β’ (π β π΄ = π΅) β β’ (π β π« π΄ = π« π΅) | ||
Theorem | pwunss 4617 | 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 5295, ax-nul 5302, ax-pr 5424 and shorten proof. (Revised by BJ, 13-Apr-2024.) |
β’ (π« π΄ βͺ π« π΅) β π« (π΄ βͺ π΅) | ||
Theorem | nfpw 4618 | Bound-variable hypothesis builder for power class. (Contributed by NM, 28-Oct-2003.) (Revised by Mario Carneiro, 13-Oct-2016.) |
β’ β²π₯π΄ β β’ β²π₯π« π΄ | ||
Theorem | pwidg 4619 | A set is an element of its power set. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
β’ (π΄ β π β π΄ β π« π΄) | ||
Theorem | pwidb 4620 | 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 4621 | A set is a member of its power class. Theorem 87 of [Suppes] p. 47. (Contributed by NM, 5-Aug-1993.) |
β’ π΄ β V β β’ π΄ β π« π΄ | ||
Theorem | pwss 4622* | Subclass relationship for power class. (Contributed by NM, 21-Jun-2009.) |
β’ (π« π΄ β π΅ β βπ₯(π₯ β π΄ β π₯ β π΅)) | ||
Theorem | pwundif 4623 | 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 5295, ax-nul 5302, ax-pr 5424 and shorten proof. (Revised by BJ, 14-Apr-2024.) |
β’ π« (π΄ βͺ π΅) = ((π« (π΄ βͺ π΅) β π« π΄) βͺ π« π΄) | ||
Theorem | snjust 4624* | Soundness justification theorem for df-sn 4626. (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
β’ {π₯ β£ π₯ = π΄} = {π¦ β£ π¦ = π΄} | ||
Syntax | csn 4625 | Extend class notation to include singleton. |
class {π΄} | ||
Definition | df-sn 4626* | 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 4718. For an alternate definition see dfsn2 4638. (Contributed by NM, 21-Jun-1993.) |
β’ {π΄} = {π₯ β£ π₯ = π΄} | ||
Syntax | cpr 4627 | Extend class notation to include unordered pair. |
class {π΄, π΅} | ||
Definition | df-pr 4628 |
Define unordered pair of classes. Definition 7.1 of [Quine] p. 48. For
example, π΄ β {1, -1} β (π΄β2) = 1 (ex-pr 30279). They are
unordered, so {π΄, π΅} = {π΅, π΄} as proven by prcom 4733. For a more
traditional definition, but requiring a dummy variable, see dfpr2 4645.
{π΄,
π΄} is also an
unordered pair, but also a singleton because of
{π΄} =
{π΄, π΄} (see dfsn2 4638). 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 4632. 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 4629 | Extend class notation to include unordered triple (sometimes called "unordered triplet"). |
class {π΄, π΅, πΆ} | ||
Definition | df-tp 4630 |
Define unordered triple of classes. Definition of [Enderton] p. 19.
Note: ordered triples are a completely different object defined below in df-ot 4634. As with all tuples, when the term "triple" is used without qualifier, it means "ordered triple". (Contributed by NM, 9-Apr-1994.) |
β’ {π΄, π΅, πΆ} = ({π΄, π΅} βͺ {πΆ}) | ||
Syntax | cop 4631 | Extend class notation to include ordered pair. |
class β¨π΄, π΅β© | ||
Definition | df-op 4632* |
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 4894, opprc2 4895, and
0nelop 5493). For Kuratowski's actual definition when
the arguments are
sets, see dfop 4869. For the justifying theorem (for sets) see
opth 5473.
See dfopif 4867 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 4632 when the arguments are proper classes. Ordinarily this difference is not important, since neither definition is meaningful in that case. Our df-op 4632 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 5511. This was simplified by Kazimierz Kuratowski in 1921 to our present definition. An even simpler definition β¨π΄, π΅β©3 = {π΄, {π΄, π΅}} is justified by opthreg 9636, 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 5737. 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 5353). 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 5515 and opthhausdorff 5514. If we restrict our sets to nonnegative integers, an ordered pair definition that involves only elementary arithmetic is provided by nn0opthi 14256. An ordered pair of real numbers can also be represented by a complex number as shown by cru 12229. 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 4867. (Contributed by NM, 28-May-1995.) (Revised by Mario Carneiro, 26-Apr-2015.) (Avoid depending on this detail.) |
β’ β¨π΄, π΅β© = {π₯ β£ (π΄ β V β§ π΅ β V β§ π₯ β {{π΄}, {π΄, π΅}})} | ||
Syntax | cotp 4633 | Extend class notation to include ordered triple. |
class β¨π΄, π΅, πΆβ© | ||
Definition | df-ot 4634 | Define ordered triple of classes. Definition of ordered triple in [Stoll] p. 25. (Contributed by NM, 3-Apr-2015.) |
β’ β¨π΄, π΅, πΆβ© = β¨β¨π΄, π΅β©, πΆβ© | ||
Theorem | sneq 4635 | Equality theorem for singletons. Part of Exercise 4 of [TakeutiZaring] p. 15. (Contributed by NM, 21-Jun-1993.) |
β’ (π΄ = π΅ β {π΄} = {π΅}) | ||
Theorem | sneqi 4636 | Equality inference for singletons. (Contributed by NM, 22-Jan-2004.) |
β’ π΄ = π΅ β β’ {π΄} = {π΅} | ||
Theorem | sneqd 4637 | Equality deduction for singletons. (Contributed by NM, 22-Jan-2004.) |
β’ (π β π΄ = π΅) β β’ (π β {π΄} = {π΅}) | ||
Theorem | dfsn2 4638 | Alternate definition of singleton. Definition 5.1 of [TakeutiZaring] p. 15. (Contributed by NM, 24-Apr-1994.) |
β’ {π΄} = {π΄, π΄} | ||
Theorem | elsng 4639 | 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 4640 | There is exactly one element in a singleton. Exercise 2 of [TakeutiZaring] p. 15. (Contributed by NM, 13-Sep-1995.) |
β’ π΄ β V β β’ (π΄ β {π΅} β π΄ = π΅) | ||
Theorem | velsn 4641 | There is only one element in a singleton. Exercise 2 of [TakeutiZaring] p. 15. (Contributed by NM, 21-Jun-1993.) |
β’ (π₯ β {π΄} β π₯ = π΄) | ||
Theorem | elsni 4642 | There is at most one element in a singleton. (Contributed by NM, 5-Jun-1994.) |
β’ (π΄ β {π΅} β π΄ = π΅) | ||
Theorem | rabsneq 4643* | Equality of class abstractions restricted to a singleton. (Contributed by AV, 17-May-2025.) |
β’ (π β π β {π₯ β {π} β£ π} = {π₯ β π β£ (π₯ = π β§ π)}) | ||
Theorem | absn 4644* | Condition for a class abstraction to be a singleton. Formerly part of proof of dfiota2 6496. (Contributed by Andrew Salmon, 30-Jun-2011.) (Revised by AV, 24-Aug-2022.) |
β’ ({π₯ β£ π} = {π} β βπ₯(π β π₯ = π)) | ||
Theorem | dfpr2 4645* | Alternate definition of a pair. Definition 5.1 of [TakeutiZaring] p. 15. (Contributed by NM, 24-Apr-1994.) |
β’ {π΄, π΅} = {π₯ β£ (π₯ = π΄ β¨ π₯ = π΅)} | ||
Theorem | dfsn2ALT 4646 | 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 4647 | 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 4648 | 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 4649 | 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 4650 | 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 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.) (Proof shortened by JJ, 23-Jul-2021.) |
β’ π΅ β V & β’ πΆ β V β β’ (π΄ β {π΅, πΆ} β (π΄ = π΅ β¨ π΄ = πΆ)) | ||
Theorem | nelpr2 4652 | 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 4653 | 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 4654 | 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 4655 | 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 4656 | 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 4657 | Membership in a set with two elements removed. Similar to eldifsn 4787 and eldiftp 4687. (Contributed by Mario Carneiro, 18-Jul-2017.) |
β’ (π΄ β (π΅ β {πΆ, π·}) β (π΄ β π΅ β§ π΄ β πΆ β§ π΄ β π·)) | ||
Theorem | rexdifpr 4658 | 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 4659 | 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 4660 | A class is a set iff it is a member of its singleton. (Contributed by NM, 5-Apr-2004.) |
β’ (π΄ β V β π΄ β {π΄}) | ||
Theorem | snid 4661 | 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 4662 | A setvar variable is a member of its singleton. (Contributed by David A. Wheeler, 8-Dec-2018.) |
β’ π₯ β {π₯} | ||
Theorem | elsn2g 4663 | 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 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, 12-Jun-1994.) |
β’ π΅ β V β β’ (π΄ β {π΅} β π΄ = π΅) | ||
Theorem | nelsn 4665 | 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 4666* | 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 4667* | 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 4668* | Conditions for a restricted class abstraction to be a singleton, in deduction form. (Contributed by Thierry Arnoux, 2-Dec-2021.) |
β’ (π₯ = π΅ β (π β π)) & β’ (π β π΅ β π΄) & β’ (π β π) & β’ (((π β§ π₯ β π΄) β§ π) β π₯ = π΅) β β’ (π β {π₯ β π΄ β£ π} = {π΅}) | ||
Theorem | ralsnsg 4669* | Substitution expressed in terms of quantification over a singleton. (Contributed by NM, 14-Dec-2005.) (Revised by Mario Carneiro, 23-Apr-2015.) |
β’ (π΄ β π β (βπ₯ β {π΄}π β [π΄ / π₯]π)) | ||
Theorem | rexsns 4670* | Restricted existential quantification over a singleton. (Contributed by Mario Carneiro, 23-Apr-2015.) (Revised by NM, 22-Aug-2018.) |
β’ (βπ₯ β {π΄}π β [π΄ / π₯]π) | ||
Theorem | rexsngf 4671* | Restricted existential quantification over a singleton. (Contributed by NM, 29-Jan-2012.) (Revised by Glauco Siliprandi, 17-Aug-2020.) |
β’ β²π₯π & β’ (π₯ = π΄ β (π β π)) β β’ (π΄ β π β (βπ₯ β {π΄}π β π)) | ||
Theorem | ralsngf 4672* | Restricted universal quantification over a singleton. (Contributed by NM, 14-Dec-2005.) (Revised by AV, 3-Apr-2023.) |
β’ β²π₯π & β’ (π₯ = π΄ β (π β π)) β β’ (π΄ β π β (βπ₯ β {π΄}π β π)) | ||
Theorem | reusngf 4673* | Restricted existential uniqueness over a singleton. (Contributed by AV, 3-Apr-2023.) |
β’ β²π₯π & β’ (π₯ = π΄ β (π β π)) β β’ (π΄ β π β (β!π₯ β {π΄}π β π)) | ||
Theorem | ralsng 4674* | 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 2129, ax-12 2166. (Revised by Gino Giotto, 30-Sep-2024.) |
β’ (π₯ = π΄ β (π β π)) β β’ (π΄ β π β (βπ₯ β {π΄}π β π)) | ||
Theorem | rexsng 4675* | Restricted existential quantification over a singleton. (Contributed by NM, 29-Jan-2012.) Avoid ax-10 2129, ax-12 2166. (Revised by Gino Giotto, 30-Sep-2024.) |
β’ (π₯ = π΄ β (π β π)) β β’ (π΄ β π β (βπ₯ β {π΄}π β π)) | ||
Theorem | reusng 4676* | Restricted existential uniqueness over a singleton. (Contributed by AV, 3-Apr-2023.) |
β’ (π₯ = π΄ β (π β π)) β β’ (π΄ β π β (β!π₯ β {π΄}π β π)) | ||
Theorem | 2ralsng 4677* | Substitution expressed in terms of two quantifications over singletons. (Contributed by AV, 22-Dec-2019.) |
β’ (π₯ = π΄ β (π β π)) & β’ (π¦ = π΅ β (π β π)) β β’ ((π΄ β π β§ π΅ β π) β (βπ₯ β {π΄}βπ¦ β {π΅}π β π)) | ||
Theorem | ralsngOLD 4678* | Obsolete version of ralsng 4674 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 4679* | Obsolete version of rexsng 4675 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 4680* | Restricted existential uniqueness over a singleton is equivalent to a restricted existential quantification over a singleton. (Contributed by AV, 3-Apr-2023.) |
β’ (π΄ β π β (βπ₯ β {π΄}π β β!π₯ β {π΄}π)) | ||
Theorem | exsnrex 4681 | 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 4682* | Convert a universal quantification restricted to a singleton to a substitution. (Contributed by NM, 27-Apr-2009.) |
β’ π΄ β V & β’ (π₯ = π΄ β (π β π)) β β’ (βπ₯ β {π΄}π β π) | ||
Theorem | rexsn 4683* | Convert an existential quantification restricted to a singleton to a substitution. (Contributed by Jeff Madsen, 5-Jan-2011.) |
β’ π΄ β V & β’ (π₯ = π΄ β (π β π)) β β’ (βπ₯ β {π΄}π β π) | ||
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 4787 and eldifpr 4657. (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 | dftp2 4690* | 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 4691 | Bound-variable hypothesis builder for unordered pairs. (Contributed by NM, 14-Nov-1995.) |
β’ β²π₯π΄ & β’ β²π₯π΅ β β’ β²π₯{π΄, π΅} | ||
Theorem | ifpr 4692 | Membership of a conditional operator in an unordered pair. (Contributed by NM, 17-Jun-2007.) |
β’ ((π΄ β πΆ β§ π΅ β π·) β if(π, π΄, π΅) β {π΄, π΅}) | ||
Theorem | ralprgf 4693* | 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 4694* | 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 4695* | 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 2129, ax-12 2166. (Revised by Gino Giotto, 30-Sep-2024.) |
β’ (π₯ = π΄ β (π β π)) & β’ (π₯ = π΅ β (π β π)) β β’ ((π΄ β π β§ π΅ β π) β (βπ₯ β {π΄, π΅}π β (π β§ π))) | ||
Theorem | ralprgOLD 4696* | Obsolete version of ralprg 4695 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 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 2129, ax-12 2166. (Revised by Gino Giotto, 30-Sep-2024.) |
β’ (π₯ = π΄ β (π β π)) & β’ (π₯ = π΅ β (π β π)) β β’ ((π΄ β π β§ π΅ β π) β (βπ₯ β {π΄, π΅}π β (π β¨ π))) | ||
Theorem | rexprgOLD 4698* | Obsolete version of rexprg 4697 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 4699* | 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 4700* | Convert a restricted existential quantification over a triple to a disjunction. (Contributed by Mario Carneiro, 23-Apr-2015.) |
β’ (π₯ = π΄ β (π β π)) & β’ (π₯ = π΅ β (π β π)) & β’ (π₯ = πΆ β (π β π)) β β’ ((π΄ β π β§ π΅ β π β§ πΆ β π) β (βπ₯ β {π΄, π΅, πΆ}π β (π β¨ π β¨ π))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |