![]() |
Metamath
Proof Explorer Theorem List (p. 47 of 482) | < 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-30702) |
![]() (30703-32225) |
![]() (32226-48151) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | elpwg 4601 | Membership in a power class. Theorem 86 of [Suppes] p. 47. See also elpw2g 5340. (Contributed by NM, 6-Aug-2000.) (Proof shortened by BJ, 31-Dec-2023.) |
β’ (π΄ β π β (π΄ β π« π΅ β π΄ β π΅)) | ||
Theorem | elpw 4602 | 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 4603 | Setvar variable membership in a power class. (Contributed by David A. Wheeler, 8-Dec-2018.) |
β’ (π₯ β π« π΄ β π₯ β π΄) | ||
Theorem | elpwd 4604 | Membership in a power class. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ (π β π΄ β π) & β’ (π β π΄ β π΅) β β’ (π β π΄ β π« π΅) | ||
Theorem | elpwi 4605 | Subset relation implied by membership in a power class. (Contributed by NM, 17-Feb-2007.) |
β’ (π΄ β π« π΅ β π΄ β π΅) | ||
Theorem | elpwb 4606 | Characterization of the elements of a power class. (Contributed by BJ, 29-Apr-2021.) |
β’ (π΄ β π« π΅ β (π΄ β V β§ π΄ β π΅)) | ||
Theorem | elpwid 4607 | An element of a power class is a subclass. Deduction form of elpwi 4605. (Contributed by David Moews, 1-May-2017.) |
β’ (π β π΄ β π« π΅) β β’ (π β π΄ β π΅) | ||
Theorem | elelpwi 4608 | If π΄ belongs to a part of πΆ, then π΄ belongs to πΆ. (Contributed by FL, 3-Aug-2009.) |
β’ ((π΄ β π΅ β§ π΅ β π« πΆ) β π΄ β πΆ) | ||
Theorem | sspw 4609 | The powerclass preserves inclusion. See sspwb 5445 for the biconditional version. (Contributed by NM, 13-Oct-1996.) Extract forward implication of sspwb 5445 since it requires fewer axioms. (Revised by BJ, 13-Apr-2024.) |
β’ (π΄ β π΅ β π« π΄ β π« π΅) | ||
Theorem | sspwi 4610 | The powerclass preserves inclusion (inference form). (Contributed by BJ, 13-Apr-2024.) |
β’ π΄ β π΅ β β’ π« π΄ β π« π΅ | ||
Theorem | sspwd 4611 | The powerclass preserves inclusion (deduction form). (Contributed by BJ, 13-Apr-2024.) |
β’ (π β π΄ β π΅) β β’ (π β π« π΄ β π« π΅) | ||
Theorem | pweq 4612 | Equality theorem for power class. (Contributed by NM, 21-Jun-1993.) (Proof shortened by BJ, 13-Apr-2024.) |
β’ (π΄ = π΅ β π« π΄ = π« π΅) | ||
Theorem | pweqALT 4613 | Alternate proof of pweq 4612 directly from the definition. (Contributed by NM, 21-Jun-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (π΄ = π΅ β π« π΄ = π« π΅) | ||
Theorem | pweqi 4614 | Equality inference for power class. (Contributed by NM, 27-Nov-2013.) |
β’ π΄ = π΅ β β’ π« π΄ = π« π΅ | ||
Theorem | pweqd 4615 | Equality deduction for power class. (Contributed by NM, 27-Nov-2013.) |
β’ (π β π΄ = π΅) β β’ (π β π« π΄ = π« π΅) | ||
Theorem | pwunss 4616 | 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 5293, ax-nul 5300, ax-pr 5423 and shorten proof. (Revised by BJ, 13-Apr-2024.) |
β’ (π« π΄ βͺ π« π΅) β π« (π΄ βͺ π΅) | ||
Theorem | nfpw 4617 | Bound-variable hypothesis builder for power class. (Contributed by NM, 28-Oct-2003.) (Revised by Mario Carneiro, 13-Oct-2016.) |
β’ β²π₯π΄ β β’ β²π₯π« π΄ | ||
Theorem | pwidg 4618 | A set is an element of its power set. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
β’ (π΄ β π β π΄ β π« π΄) | ||
Theorem | pwidb 4619 | 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 4620 | A set is a member of its power class. Theorem 87 of [Suppes] p. 47. (Contributed by NM, 5-Aug-1993.) |
β’ π΄ β V β β’ π΄ β π« π΄ | ||
Theorem | pwss 4621* | Subclass relationship for power class. (Contributed by NM, 21-Jun-2009.) |
β’ (π« π΄ β π΅ β βπ₯(π₯ β π΄ β π₯ β π΅)) | ||
Theorem | pwundif 4622 | 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 5293, ax-nul 5300, ax-pr 5423 and shorten proof. (Revised by BJ, 14-Apr-2024.) |
β’ π« (π΄ βͺ π΅) = ((π« (π΄ βͺ π΅) β π« π΄) βͺ π« π΄) | ||
Theorem | snjust 4623* | Soundness justification theorem for df-sn 4625. (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
β’ {π₯ β£ π₯ = π΄} = {π¦ β£ π¦ = π΄} | ||
Syntax | csn 4624 | Extend class notation to include singleton. |
class {π΄} | ||
Definition | df-sn 4625* | 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 4637. (Contributed by NM, 21-Jun-1993.) |
β’ {π΄} = {π₯ β£ π₯ = π΄} | ||
Syntax | cpr 4626 | Extend class notation to include unordered pair. |
class {π΄, π΅} | ||
Definition | df-pr 4627 |
Define unordered pair of classes. Definition 7.1 of [Quine] p. 48. For
example, π΄ β {1, -1} β (π΄β2) = 1 (ex-pr 30214). They are
unordered, so {π΄, π΅} = {π΅, π΄} as proven by prcom 4732. For a more
traditional definition, but requiring a dummy variable, see dfpr2 4643.
{π΄,
π΄} is also an
unordered pair, but also a singleton because of
{π΄} =
{π΄, π΄} (see dfsn2 4637). 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 4631. 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 4628 | Extend class notation to include unordered triple (sometimes called "unordered triplet"). |
class {π΄, π΅, πΆ} | ||
Definition | df-tp 4629 |
Define unordered triple of classes. Definition of [Enderton] p. 19.
Note: ordered triples are a completely different object defined below in df-ot 4633. As with all tuples, when the term "triple" is used without qualifier, it means "ordered triple". (Contributed by NM, 9-Apr-1994.) |
β’ {π΄, π΅, πΆ} = ({π΄, π΅} βͺ {πΆ}) | ||
Syntax | cop 4630 | Extend class notation to include ordered pair. |
class β¨π΄, π΅β© | ||
Definition | df-op 4631* |
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 4893, opprc2 4894, and
0nelop 5492). For Kuratowski's actual definition when
the arguments are
sets, see dfop 4868. For the justifying theorem (for sets) see
opth 5472.
See dfopif 4866 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 4631 when the arguments are proper classes. Ordinarily this difference is not important, since neither definition is meaningful in that case. Our df-op 4631 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 5510. This was simplified by Kazimierz Kuratowski in 1921 to our present definition. An even simpler definition β¨π΄, π΅β©3 = {π΄, {π΄, π΅}} is justified by opthreg 9627, 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 5736. 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 5352). 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 5514 and opthhausdorff 5513. If we restrict our sets to nonnegative integers, an ordered pair definition that involves only elementary arithmetic is provided by nn0opthi 14247. An ordered pair of real numbers can also be represented by a complex number as shown by cru 12220. 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 4866. (Contributed by NM, 28-May-1995.) (Revised by Mario Carneiro, 26-Apr-2015.) (Avoid depending on this detail.) |
β’ β¨π΄, π΅β© = {π₯ β£ (π΄ β V β§ π΅ β V β§ π₯ β {{π΄}, {π΄, π΅}})} | ||
Syntax | cotp 4632 | Extend class notation to include ordered triple. |
class β¨π΄, π΅, πΆβ© | ||
Definition | df-ot 4633 | Define ordered triple of classes. Definition of ordered triple in [Stoll] p. 25. (Contributed by NM, 3-Apr-2015.) |
β’ β¨π΄, π΅, πΆβ© = β¨β¨π΄, π΅β©, πΆβ© | ||
Theorem | sneq 4634 | Equality theorem for singletons. Part of Exercise 4 of [TakeutiZaring] p. 15. (Contributed by NM, 21-Jun-1993.) |
β’ (π΄ = π΅ β {π΄} = {π΅}) | ||
Theorem | sneqi 4635 | Equality inference for singletons. (Contributed by NM, 22-Jan-2004.) |
β’ π΄ = π΅ β β’ {π΄} = {π΅} | ||
Theorem | sneqd 4636 | Equality deduction for singletons. (Contributed by NM, 22-Jan-2004.) |
β’ (π β π΄ = π΅) β β’ (π β {π΄} = {π΅}) | ||
Theorem | dfsn2 4637 | Alternate definition of singleton. Definition 5.1 of [TakeutiZaring] p. 15. (Contributed by NM, 24-Apr-1994.) |
β’ {π΄} = {π΄, π΄} | ||
Theorem | elsng 4638 | 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 4639 | There is exactly one element in a singleton. Exercise 2 of [TakeutiZaring] p. 15. (Contributed by NM, 13-Sep-1995.) |
β’ π΄ β V β β’ (π΄ β {π΅} β π΄ = π΅) | ||
Theorem | velsn 4640 | There is only one element in a singleton. Exercise 2 of [TakeutiZaring] p. 15. (Contributed by NM, 21-Jun-1993.) |
β’ (π₯ β {π΄} β π₯ = π΄) | ||
Theorem | elsni 4641 | There is at most one element in a singleton. (Contributed by NM, 5-Jun-1994.) |
β’ (π΄ β {π΅} β π΄ = π΅) | ||
Theorem | absn 4642* | Condition for a class abstraction to be a singleton. Formerly part of proof of dfiota2 6495. (Contributed by Andrew Salmon, 30-Jun-2011.) (Revised by AV, 24-Aug-2022.) |
β’ ({π₯ β£ π} = {π} β βπ₯(π β π₯ = π)) | ||
Theorem | dfpr2 4643* | Alternate definition of a pair. Definition 5.1 of [TakeutiZaring] p. 15. (Contributed by NM, 24-Apr-1994.) |
β’ {π΄, π΅} = {π₯ β£ (π₯ = π΄ β¨ π₯ = π΅)} | ||
Theorem | dfsn2ALT 4644 | 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 4645 | 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 4646 | 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 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. (Contributed by NM, 13-Sep-1995.) |
β’ π΄ β V β β’ (π΄ β {π΅, πΆ} β (π΄ = π΅ β¨ π΄ = πΆ)) | ||
Theorem | elpr2g 4648 | 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 4649 | 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 4650 | Obsolete version of elpr2 4649 as of 25-May-2024. (Contributed by NM, 14-Oct-2005.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ π΅ β V & β’ πΆ β V β β’ (π΄ β {π΅, πΆ} β (π΄ = π΅ β¨ π΄ = πΆ)) | ||
Theorem | nelpr2 4651 | 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 4652 | 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 4653 | 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 4654 | 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 4655 | 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 4656 | Membership in a set with two elements removed. Similar to eldifsn 4786 and eldiftp 4686. (Contributed by Mario Carneiro, 18-Jul-2017.) |
β’ (π΄ β (π΅ β {πΆ, π·}) β (π΄ β π΅ β§ π΄ β πΆ β§ π΄ β π·)) | ||
Theorem | rexdifpr 4657 | Restricted existential quantification over a set with two elements removed. (Contributed by Alexander van der Vekens, 7-Feb-2018.) |
β’ (βπ₯ β (π΄ β {π΅, πΆ})π β βπ₯ β π΄ (π₯ β π΅ β§ π₯ β πΆ β§ π)) | ||
Theorem | snidg 4658 | 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 4659 | A class is a set iff it is a member of its singleton. (Contributed by NM, 5-Apr-2004.) |
β’ (π΄ β V β π΄ β {π΄}) | ||
Theorem | snid 4660 | 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 4661 | A setvar variable is a member of its singleton. (Contributed by David A. Wheeler, 8-Dec-2018.) |
β’ π₯ β {π₯} | ||
Theorem | elsn2g 4662 | 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 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, 12-Jun-1994.) |
β’ π΅ β V β β’ (π΄ β {π΅} β π΄ = π΅) | ||
Theorem | nelsn 4664 | 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 4665* | 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 4666* | 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 4667* | Conditions for a restricted class abstraction to be a singleton, in deduction form. (Contributed by Thierry Arnoux, 2-Dec-2021.) |
β’ (π₯ = π΅ β (π β π)) & β’ (π β π΅ β π΄) & β’ (π β π) & β’ (((π β§ π₯ β π΄) β§ π) β π₯ = π΅) β β’ (π β {π₯ β π΄ β£ π} = {π΅}) | ||
Theorem | ralsnsg 4668* | Substitution expressed in terms of quantification over a singleton. (Contributed by NM, 14-Dec-2005.) (Revised by Mario Carneiro, 23-Apr-2015.) |
β’ (π΄ β π β (βπ₯ β {π΄}π β [π΄ / π₯]π)) | ||
Theorem | rexsns 4669* | Restricted existential quantification over a singleton. (Contributed by Mario Carneiro, 23-Apr-2015.) (Revised by NM, 22-Aug-2018.) |
β’ (βπ₯ β {π΄}π β [π΄ / π₯]π) | ||
Theorem | rexsngf 4670* | Restricted existential quantification over a singleton. (Contributed by NM, 29-Jan-2012.) (Revised by Glauco Siliprandi, 17-Aug-2020.) |
β’ β²π₯π & β’ (π₯ = π΄ β (π β π)) β β’ (π΄ β π β (βπ₯ β {π΄}π β π)) | ||
Theorem | ralsngf 4671* | Restricted universal quantification over a singleton. (Contributed by NM, 14-Dec-2005.) (Revised by AV, 3-Apr-2023.) |
β’ β²π₯π & β’ (π₯ = π΄ β (π β π)) β β’ (π΄ β π β (βπ₯ β {π΄}π β π)) | ||
Theorem | reusngf 4672* | Restricted existential uniqueness over a singleton. (Contributed by AV, 3-Apr-2023.) |
β’ β²π₯π & β’ (π₯ = π΄ β (π β π)) β β’ (π΄ β π β (β!π₯ β {π΄}π β π)) | ||
Theorem | ralsng 4673* | 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 2130, ax-12 2164. (Revised by Gino Giotto, 30-Sep-2024.) |
β’ (π₯ = π΄ β (π β π)) β β’ (π΄ β π β (βπ₯ β {π΄}π β π)) | ||
Theorem | rexsng 4674* | Restricted existential quantification over a singleton. (Contributed by NM, 29-Jan-2012.) Avoid ax-10 2130, ax-12 2164. (Revised by Gino Giotto, 30-Sep-2024.) |
β’ (π₯ = π΄ β (π β π)) β β’ (π΄ β π β (βπ₯ β {π΄}π β π)) | ||
Theorem | reusng 4675* | Restricted existential uniqueness over a singleton. (Contributed by AV, 3-Apr-2023.) |
β’ (π₯ = π΄ β (π β π)) β β’ (π΄ β π β (β!π₯ β {π΄}π β π)) | ||
Theorem | 2ralsng 4676* | Substitution expressed in terms of two quantifications over singletons. (Contributed by AV, 22-Dec-2019.) |
β’ (π₯ = π΄ β (π β π)) & β’ (π¦ = π΅ β (π β π)) β β’ ((π΄ β π β§ π΅ β π) β (βπ₯ β {π΄}βπ¦ β {π΅}π β π)) | ||
Theorem | ralsngOLD 4677* | Obsolete version of ralsng 4673 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 4678* | Obsolete version of rexsng 4674 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 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 | elpwunsn 4683 | Membership in an extension of a power class. (Contributed by NM, 26-Mar-2007.) |
β’ (π΄ β (π« (π΅ βͺ {πΆ}) β π« π΅) β πΆ β π΄) | ||
Theorem | eqoreldif 4684 | 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 4685 | Members of an unordered triple of classes. (Contributed by FL, 2-Feb-2014.) (Proof shortened by Mario Carneiro, 11-Feb-2015.) |
β’ (π΄ β π β (π΄ β {π΅, πΆ, π·} β (π΄ = π΅ β¨ π΄ = πΆ β¨ π΄ = π·))) | ||
Theorem | eldiftp 4686 | Membership in a set with three elements removed. Similar to eldifsn 4786 and eldifpr 4656. (Contributed by David A. Wheeler, 22-Jul-2017.) |
β’ (π΄ β (π΅ β {πΆ, π·, πΈ}) β (π΄ β π΅ β§ (π΄ β πΆ β§ π΄ β π· β§ π΄ β πΈ))) | ||
Theorem | eltpi 4687 | A member of an unordered triple of classes is one of them. (Contributed by Mario Carneiro, 11-Feb-2015.) |
β’ (π΄ β {π΅, πΆ, π·} β (π΄ = π΅ β¨ π΄ = πΆ β¨ π΄ = π·)) | ||
Theorem | eltp 4688 | 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 4689* | 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 4690 | Bound-variable hypothesis builder for unordered pairs. (Contributed by NM, 14-Nov-1995.) |
β’ β²π₯π΄ & β’ β²π₯π΅ β β’ β²π₯{π΄, π΅} | ||
Theorem | ifpr 4691 | Membership of a conditional operator in an unordered pair. (Contributed by NM, 17-Jun-2007.) |
β’ ((π΄ β πΆ β§ π΅ β π·) β if(π, π΄, π΅) β {π΄, π΅}) | ||
Theorem | ralprgf 4692* | 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 4693* | 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 4694* | 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 2130, ax-12 2164. (Revised by Gino Giotto, 30-Sep-2024.) |
β’ (π₯ = π΄ β (π β π)) & β’ (π₯ = π΅ β (π β π)) β β’ ((π΄ β π β§ π΅ β π) β (βπ₯ β {π΄, π΅}π β (π β§ π))) | ||
Theorem | ralprgOLD 4695* | Obsolete version of ralprg 4694 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 4696* | 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 2130, ax-12 2164. (Revised by Gino Giotto, 30-Sep-2024.) |
β’ (π₯ = π΄ β (π β π)) & β’ (π₯ = π΅ β (π β π)) β β’ ((π΄ β π β§ π΅ β π) β (βπ₯ β {π΄, π΅}π β (π β¨ π))) | ||
Theorem | rexprgOLD 4697* | Obsolete version of rexprg 4696 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 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 > |